Document Open Access Logo

Cyclic Proofs and Jumping Automata

Authors Denis Kuperberg , Laureline Pinault, Damien Pous

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2019.45.pdf
  • Filesize: 0.57 MB
  • 14 pages

Document Identifiers

Author Details

Denis Kuperberg
  • Univ Lyon, CNRS, ENS de Lyon, UCBL, LIP UMR 5668, F-69342, LYON Cedex 07, France
Laureline Pinault
  • Univ Lyon, CNRS, ENS de Lyon, UCBL, LIP UMR 5668, F-69342, LYON Cedex 07, France
Damien Pous
  • Univ Lyon, CNRS, ENS de Lyon, UCBL, LIP UMR 5668, F-69342, LYON Cedex 07, France

Funding

This work has been funded by the European Research Council (ERC) under the European Union’s Horizon 2020 programme (CoVeCe, grant agreement No 678157), and was supported by the LABEX MILYON (ANR-10-LABX-0070) of Université de Lyon, within the program "Investissements d'Avenir" (ANR-11-IDEX-0007) operated by the French National Research Agency (ANR).

Cite As Get BibTex

Denis Kuperberg, Laureline Pinault, and Damien Pous. Cyclic Proofs and Jumping Automata. In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, pp. 45:1-45:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.FSTTCS.2019.45

Abstract

We consider a fragment of a cyclic sequent proof system for Kleene algebra, and we see it as a computational device for recognising languages of words. The starting proof system is linear and we show that it captures precisely the regular languages. When adding the standard contraction rule, the expressivity raises significantly; we characterise the corresponding class of languages using a new notion of multi-head finite automata, where heads can jump.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
Keywords
  • Cyclic proofs
  • regular languages
  • multi-head automata
  • transducers

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Bahareh Afshari and Graham E. Leigh. Cut-free completeness for modal mu-calculus. In LiCS, pages 1-12, 2017. URL: https://doi.org/10.1109/LICS.2017.8005088.
  2. Stefano Berardi and Makoto Tatsuta. Classical System of Martin-Löf’s Inductive Definitions Is Not Equivalent to Cyclic Proof System. In FoSSaCS, pages 301-317, 2017. URL: https://doi.org/10.1007/978-3-662-54458-7_18.
  3. Stefano Berardi and Makoto Tatsuta. Equivalence of inductive definitions and cyclic proofs under arithmetic. In LiCS, pages 1-12, 2017. URL: https://doi.org/10.1109/LICS.2017.8005114.
  4. James Brotherston and Alex Simpson. Sequent calculi for induction and infinite descent. Journal of Logic and Computation, 21(6):1177-1216, 2011. URL: https://doi.org/10.1093/logcom/exq052.
  5. Anupam Das, Amina Doumane, and Damien Pous. Left-handed completeness for Kleene algebra, via cyclic proofs. In LPAR, volume 57 of EPiC Series in Computing, pages 271-289. Easychair, 2018. URL: https://doi.org/10.29007/hzq3.
  6. Anupam Das and Damien Pous. A cut-free cyclic proof system for Kleene algebra. In TABLEAUX, volume 10501 of Lecture Notes in Computer Science, pages 261-277. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66902-1_16.
  7. Anupam Das and Damien Pous. Non-wellfounded proof theory for (Kleene+action)(algebras+lattices). In CSL, volume 119 of LIPIcs, pages 18:1-18:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.CSL.2018.19.
  8. Christian Dax, Martin Hofmann, and Martin Lange. A Proof System for the Linear Time μ-Calculus. In FSTTCS, volume 4337 of Lecture Notes in Computer Science, pages 273-284. Springer, 2006. URL: https://doi.org/10.1007/11944836_26.
  9. Amina Doumane. Constructive completeness for the linear-time μ-calculus. In LiCS, pages 1-12, 2017. URL: https://doi.org/10.1109/LICS.2017.8005075.
  10. Amina Doumane, David Baelde, and Alexis Saurin. Infinitary proof theory: the multiplicative additive case. In CSL, volume 62 of LIPIcs, pages 42:1-42:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, September 2016. URL: https://doi.org/10.4230/LIPIcs.CSL.2016.42.
  11. Jérôme Fortier and Luigi Santocanale. Cuts for circular proofs: semantics and cut-elimination. In CSL, volume 23 of LIPIcs, pages 248-262, 2013. URL: https://doi.org/10.4230/LIPIcs.CSL.2013.248.
  12. Alain Frisch and Luca Cardelli. Greedy Regular Expression Matching. In ICALP, volume 3142 of Lecture Notes in Computer Science, pages 618-629. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-27836-8_53.
  13. Fritz Henglein and Lasse Nielsen. Regular expression containment: coinductive axiomatization and computational interpretation. In POPL, 2011, pages 385-398. ACM, 2011. URL: https://doi.org/10.1145/1926385.1926429.
  14. Markus Holzer, Martin Kutrib, and Andreas Malcher. Multi-Head Finite Automata: Characterizations, Concepts and Open Problems. In International Workshop on The Complexity of Simple Programs (CSP), pages 93-107, 2008. URL: https://doi.org/10.4204/EPTCS.1.9.
  15. Denis Kuperberg, Laureline Pinault, and Damien Pous. Cyclic Proofs and Jumping Automata, 2019. Version with appendix. URL: https://hal.archives-ouvertes.fr/hal-02301651.
  16. Alexander Meduna and Petr Zemek. Jumping Finite Automata. Int. J. Found. Comput. Sci., 23(7):1555-1578, 2012. URL: https://doi.org/10.1142/S0129054112500244.
  17. Marcel Paul Schützenberger. Sur une Variante des Fonctions Sequentielles. Theor. Comput. Sci., 4(1):47-57, 1977. Google Scholar
  18. Alex Simpson. Cyclic Arithmetic Is Equivalent to Peano Arithmetic. In FoSSaCS, pages 283-300, 2017. URL: https://doi.org/10.1007/978-3-662-54458-7_17.
  19. Andrew C Yao and Ronald L. Rivest. k+1 Heads Are Better than k. Journal of the ACM, 25(2):337-340, 1978. URL: https://doi.org/10.1145/322063.322076.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact