Document Open Access Logo

Non-Wellfounded Proof Theory For (Kleene+Action)(Algebras+Lattices)

Authors Anupam Das, Damien Pous

PDF
Thumbnail PDF

File

LIPIcs.CSL.2018.19.pdf
  • Filesize: 495 kB
  • 18 pages

Document Identifiers

Author Details

Anupam Das
  • University of Copenhagen, Copenhagen, Denmark
Damien Pous
  • Univ Lyon, CNRS, ENS de Lyon, UCB Lyon 1, LIP, Lyon, 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 MiLC, grant agreement No. 753431). This work 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

Anupam Das and Damien Pous. Non-Wellfounded Proof Theory For (Kleene+Action)(Algebras+Lattices). In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 19:1-19:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.CSL.2018.19

Abstract

We prove cut-elimination for a sequent-style proof system which is sound and complete for the equational theory of Kleene algebra, and where proofs are (potentially) non-wellfounded infinite trees. We extend these results to systems with meets and residuals, capturing `star-continuous' action lattices in a similar way. We recover the equational theory of all action lattices by restricting to regular proofs (with cut) - those proofs that are unfoldings of finite graphs.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
  • Theory of computation → Regular languages
Keywords
  • Kleene algebra
  • proof theory
  • sequent system
  • non-wellfounded proofs

Metrics

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

Related Versions

References

  1. C. J. Anderson, N. Foster, A. Guha, J.-B. Jeannin, D. Kozen, C. Schlesinger, and D. Walker. NetKAT: semantic foundations for networks. In Proc. POPL, pages 113-126. ACM, 2014. URL: http://dx.doi.org/10.1145/2535838.2535862.
  2. J.-M. Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3):297-347, 1992. Google Scholar
  3. A. Angus and D. Kozen. Kleene algebra with tests and program schematology. Technical Report TR2001-1844, CS Dpt., Cornell University, July 2001. URL: http://hdl.handle.net/1813/5831.
  4. Maurice Boffa. Une condition impliquant toutes les identités rationnelles. Informatique Théorique et Applications, 29(6):515-518, 1995. URL: http://www.numdam.org/article/ITA_1995__29_6_515_0.pdf.
  5. Thomas Braibant and Damien Pous. An efficient Coq tactic for deciding Kleene algebras. In Proc. 1st ITP, volume 6172 of Lecture Notes in Computer Science, pages 163-178. Springer Verlag, 2010. URL: http://dx.doi.org/10.1007/978-3-642-14052-5_13.
  6. Samuel R. Buss. An introduction to proof theory. Handbook of proof theory, 137:1-78, 1998. Google Scholar
  7. Wojciech Buszkowski. On action logic: Equational theories of action algebras. J. Log. Comput., 17(1):199-217, 2007. URL: http://dx.doi.org/10.1093/logcom/exl036.
  8. Pierre Clairambault. Least and greatest fixpoints in game semantics. In Proc. FoSSaCS, pages 16-31, 2009. URL: http://dx.doi.org/10.1007/978-3-642-00596-1_3.
  9. J. H. Conway. Regular algebra and finite machines. Chapman and Hall, 1971. Google Scholar
  10. Anupam Das and Damien Pous. A cut-free cyclic proof system for Kleene algebra. In Proc. TABLEAUX, volume 10501 of Lecture Notes in Computer Science, pages 261-277. Springer Verlag, 2017. URL: http://dx.doi.org/10.1007/978-3-319-66902-1_16.
  11. Anupam Das and Damien Pous. Non-Wellfounded Proof Theory For (Kleene+Action)(Algebras+Lattices). Full version of this extended abstract, 2018. URL: https://hal.archives-ouvertes.fr/hal-01703942.
  12. H. Doornbos, R. Backhouse, and J. van der Woude. A calculational approach to mathematical induction. Theoretical Computer Science, 179(1-2):103-135, 1997. URL: http://dx.doi.org/10.1016/S0304-3975(96)00154-5.
  13. 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, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2016.42.
  14. Jérôme Fortier and Luigi Santocanale. Cuts for circular proofs: semantics and cut-elimination. In Proc. CSL, volume 23 of LIPIcs, pages 248-262, 2013. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2013.248.
  15. Alain Frisch and Luca Cardelli. Greedy regular expression matching. In Proc. ICALP, volume 3142 of Lecture Notes in Computer Science, pages 618-629. Springer Verlag, 2004. URL: http://dx.doi.org/10.1007/978-3-540-27836-8_53.
  16. N. Galatos, P. Jipsen, T. Kowalski, and H. Ono. Residuated Lattices: An Algebraic Glimpse at Substructural Logics. Elsevier, 2007. Google Scholar
  17. J.-Y. Girard. Linear logic. Theoretical Computer Science, 50:1-102, 1987. Google Scholar
  18. Fritz Henglein and Lasse Nielsen. Regular expression containment: coinductive axiomatization and computational interpretation. In Proc. POPL 2011, pages 385-398. ACM, 2011. URL: http://dx.doi.org/10.1145/1926385.1926429.
  19. C. A. R. Hoare, Bernhard Möller, Georg Struth, and Ian Wehrman. Concurrent Kleene Algebra. In Proc. CONCUR, volume 5710 of Lecture Notes in Computer Science, pages 399-414. Springer Verlag, 2009. URL: http://dx.doi.org/10.1007/978-3-642-04081-8_27.
  20. P. Jipsen. From semirings to residuated Kleene lattices. Studia Logica, 76(2):291-303, 2004. URL: http://dx.doi.org/10.1023/B:STUD.0000032089.54776.63.
  21. S. C. Kleene. Representation of events in nerve nets and finite automata. In Automata Studies, pages 3-41. Princeton University Press, 1956. URL: http://www.rand.org/pubs/research_memoranda/2008/RM704.pdf.
  22. D. Kozen. On Hoare logic and Kleene algebra with tests. ACM Trans. Comput. Log., 1(1):60-76, 2000. URL: http://dx.doi.org/10.1145/343369.343378.
  23. D. Kozen and M.-C. Patron. Certification of compiler optimizations using Kleene algebra with tests. In Proc. CL2000, volume 1861 of Lecture Notes in Artificial Intelligence, pages 568-582. Springer Verlag, 2000. URL: http://dx.doi.org/10.1007/3-540-44957-4_38.
  24. Dexter Kozen. A completeness theorem for Kleene algebras and the algebra of regular events. In Proc. LICS, pages 214-225. IEEE, 1991. URL: http://dx.doi.org/10.1109/LICS.1991.151646.
  25. Dexter Kozen. On action algebras. In J. van Eijck and A. Visser, editors, Logic and Information Flow, pages 78-88. MIT Press, 1994. Google Scholar
  26. A. Krauss and T. Nipkow. Proof pearl: Regular expression equivalence and relation algebra. Journal of Algebraic Reasoning, 49(1):95-106, 2012. URL: http://dx.doi.org/10.1007/s10817-011-9223-4.
  27. D. Krob. Complete systems of B-rational identities. Theoretical Computer Science, 89(2):207-343, 1991. URL: http://dx.doi.org/10.1016/0304-3975(91)90395-I.
  28. Joachim Lambek. The mathematics of sentence structure. The American Mathematical Monthly, 65:154-170, 1958. Google Scholar
  29. Ewa Palka. An infinitary sequent system for the equational theory of *-continuous action lattices. Fundamenta Informaticae, pages 295-309, 2007. URL: http://iospress.metapress.com/content/r5p53611826876j0/.
  30. Damien Pous. Kleene Algebra with Tests and Coq tools for while programs. In Proc. ITP, volume 7998 of Lecture Notes in Computer Science, pages 180-196. Springer Verlag, 2013. URL: http://dx.doi.org/10.1007/978-3-642-39634-2_15.
  31. V. Pratt. Action logic and pure induction. In Proc. JELIA, volume 478 of Lecture Notes in Computer Science, pages 97-120. Springer Verlag, 1990. URL: http://dx.doi.org/10.1007/BFb0018436.
  32. Volodimir Nikiforovych Redko. On defining relations for the algebra of regular events. Ukrainskii Matematicheskii Zhurnal, 16:120-126, 1964. Google Scholar
  33. Kurt Schütte. Proof Theory. Grundlehren der mathematischen Wissenschaften 225. Springer Berlin Heidelberg, 1977. Translation of Beweistheorie, 1968. Google Scholar
  34. Christian Wurm. Kleene algebras, regular languages and substructural logics. In Proc. GandALF, EPTCS, pages 46-59, 2014. URL: http://dx.doi.org/10.4204/EPTCS.161.7.
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