LIPIcs.CSL.2016.42.pdf
- Filesize: 0.53 MB
- 17 pages
Document
Infinitary Proof Theory: the Multiplicative Additive Case
Authors
-
Part of:
Volume:
25th EACSL Annual Conference on Computer Science Logic (CSL 2016)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Computer Science Logic (CSL) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2016-08-29
Cite As Get BibTex
David Baelde, Amina Doumane, and Alexis Saurin. Infinitary Proof Theory: the Multiplicative Additive Case. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 42:1-42:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.CSL.2016.42
Abstract
Infinitary and regular proofs are commonly used in fixed point logics. Being natural intermediate devices between semantics and traditional finitary proof systems, they are commonly found in completeness arguments, automated deduction, verification, etc. However, their proof theory is surprisingly underdeveloped. In particular, very little is known about the computational behavior of such proofs through cut elimination. Taking such aspects into account has unlocked rich developments at the intersection of proof theory and programming language theory. One would hope that extending this to infinitary calculi would lead, e.g., to a better understanding of recursion and corecursion in programming languages. Structural proof theory is notably based on two fundamental properties of a proof system: cut elimination and focalization. The first one is only known to hold for restricted (purely additive) infinitary calculi, thanks to the work of Santocanale and Fortier; the second one has never been studied in infinitary systems. In this paper, we consider the infinitary proof system muMALLi for multiplicative and additive linear logic extended with least and greatest fixed points, and prove these two key results. We thus establish muMALLi as a satisfying computational proof system in itself, rather than just an intermediate device in the study of finitary proof systems.
Subject Classification
Keywords
- Infinitary proofs
- linear logic
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Andreas Abel and Brigitte Pientka. Wellfounded recursion with copatterns: a unified approach to termination and productivity. In Greg Morrisett and Tarmo Uustalu, editors, ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA - September 25-27, 2013, pages 185-196. ACM, 2013. URL: http://dx.doi.org/10.1145/2500365.2500591.
- Andreas Abel, Brigitte Pientka, David Thibodeau, and Anton Setzer. Copatterns: programming infinite structures by observations. In Roberto Giacobazzi and Radhia Cousot, editors, The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'13, Rome, Italy - January 23-25, 2013, pages 27-38. ACM, 2013. URL: http://dx.doi.org/10.1145/2429069.2429075.
-
Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3):297-347, 1992.
-
David Baelde. Least and greatest fixed points in linear logic. ACM Transactions on Computational Logic (TOCL), 13(1):2, 2012.
- David Baelde, Amina Doumane, and Alexis Saurin. Least and greatest fixed points in ludics. In Stephan Kreutzer, editor, 24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7-10, 2015, Berlin, Germany, volume 41 of LIPIcs, pages 549-566. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2015.549.
- David Baelde, Amina Doumane, and Alexis Saurin. Infinitary proof theory : the multiplicative additive case. HAL, hal-01339037, June 2016. URL: https://hal.archives-ouvertes.fr/hal-01339037.
- Michele Basaldella, Alexis Saurin, and Kazushige Terui. On the meaning of focalization. In Alain Lecomte and Samuel Tronçon, editors, Ludics, Dialogue and Interaction - PRELUDE Project - 2006-2009. Revised Selected Papers, volume 6505 of Lecture Notes in Computer Science, pages 78-87. Springer, 2011. URL: http://dx.doi.org/10.1007/978-3-642-19211-1_5.
- James Brotherston and Nikos Gorogiannis. Cyclic abduction of inductively defined safety and termination preconditions. In Markus Müller-Olm and Helmut Seidl, editors, Static Analysis - 21st International Symposium, SAS 2014, Munich, Germany, September 11-13, 2014. Proceedings, volume 8723 of Lecture Notes in Computer Science, pages 68-84. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-319-10936-7_5.
-
James Brotherston and Alex Simpson. Sequent calculi for induction and infinite descent. Journal of Logic and Computation, 21(6):1177-1216, December 2011.
- Pierre-Louis Curien and Guillaume Munch-Maccagnoni. The duality of computation under focus. In Cristian S. Calude and Vladimiro Sassone, editors, Theoretical Computer Science - 6th IFIP TC 1/WG 2.2 International Conference, TCS 2010, Held as Part of WCC 2010, Brisbane, Australia, September 20-23, 2010. Proceedings, volume 323 of IFIP Advances in Information and Communication Technology, pages 165-181. Springer, 2010. URL: http://dx.doi.org/10.1007/978-3-642-15240-5_13.
- Christian Dax, Martin Hofmann, and Martin Lange. A proof system for the linear time μ-calculus. In FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, India, December 13-15, 2006, Proceedings, pages 273-284, 2006. URL: http://dx.doi.org/10.1007/11944836_26.
- Amina Doumane, David Baelde, Lucca Hirschi, and Alexis Saurin. Towards Completeness via Proof Search in the Linear Time mu-Calculus. Accepted for publication at LICS, January 2016. URL: https://hal.archives-ouvertes.fr/hal-01275289.
- Jérôme Fortier and Luigi Santocanale. Cuts for circular proofs: semantics and cut-elimination. In Simona Ronchi Della Rocca, editor, Computer Science Logic 2013 (CSL 2013), CSL 2013, September 2-5, 2013, Torino, Italy, volume 23 of LIPIcs, pages 248-262. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2013. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2013.248.
- David Janin and Igor Walukiewicz. Automata for the modal mu-calculus and related results. In Jirí Wiedermann and Petr Hájek, editors, Mathematical Foundations of Computer Science 1995, 20th International Symposium, MFCS'95, Prague, Czech Republic, August 28 - September 1, 1995, Proceedings, volume 969 of Lecture Notes in Computer Science, pages 552-562. Springer, 1995. URL: http://dx.doi.org/10.1007/3-540-60246-1_160.
- Roope Kaivola. Axiomatising linear time mu-calculus. In CONCUR'95: Concurrency Theory, 6th International Conference, Philadelphia, PA, USA, August 21-24, 1995, Proceedings, pages 423-437, 1995. URL: http://dx.doi.org/10.1007/3-540-60218-6_32.
- Dexter Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, 27:333-354, 1983. URL: http://dx.doi.org/10.1016/0304-3975(82)90125-6.
- Olivier Laurent. Polarized games. Annals of Pure and Applied Logic, 130(1-3):79-123, 2004. URL: http://dx.doi.org/10.1016/j.apal.2004.04.006.
-
Olivier Laurent. A proof of the focalization property of linear logic. Unpublished note, May 2004.
- Paul-André Melliès and Nicolas Tabareau. Resource modalities in tensor logic. Annals of Pure and Applied Logic, 161(5):632-653, 2010. URL: http://dx.doi.org/10.1016/j.apal.2009.07.018.
- Dale Miller and Alexis Saurin. From proofs to focused proofs: A modular proof of focalization in linear logic. In Jacques Duparc and Thomas A. Henzinger, editors, Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007, Proceedings, volume 4646 of Lecture Notes in Computer Science, pages 405-419. Springer, 2007. URL: http://dx.doi.org/10.1007/978-3-540-74915-8_31.
- Luigi Santocanale. μ-bicomplete categories and parity games. ITA, 36(2):195-227, 2002. URL: http://dx.doi.org/10.1051/ita:2002010.
- Luigi Santocanale. A calculus of circular proofs and its categorical semantics. In Mogens Nielsen and Uffe Engberg, editors, Foundations of Software Science and Computation Structures, volume 2303 of Lecture Notes in Computer Science, pages 357-371. Springer, 2002. URL: http://dx.doi.org/10.1007/3-540-45931-6_25.
- Luigi Santocanale. Free μ-lattices. Journal of Pure and Applied Algebra, 168(2-3):227-264, March 2002. URL: https://hal.archives-ouvertes.fr/hal-01261049, URL: http://dx.doi.org/10.1016/S0022-4049(01)00098-6.
- Robert S. Streett and E. Allen Emerson. An automata theoretic decision procedure for the propositional mu-calculus. Information and Computation, 81(3):249-264, 1989. URL: http://dx.doi.org/10.1016/0890-5401(89)90031-X.
- Kazushige Terui. Computational ludics. Theoretical Computer Science, 412(20):2048-2071, 2011. URL: http://dx.doi.org/10.1016/j.tcs.2010.12.026.
- Igor Walukiewicz. On completeness of the mu-calculus. In Proceedings of the Eighth Annual Symposium on Logic in Computer Science (LICS'93), Montreal, Canada, June 19-23, 1993, pages 136-146. IEEE Computer Society, 1993. URL: http://dx.doi.org/10.1109/LICS.1993.287593.
- Igor Walukiewicz. Completeness of Kozen’s axiomatisation of the propositional mu-calculus. In Proceedings, 10th Annual IEEE Symposium on Logic in Computer Science, San Diego, California, USA, June 26-29, 1995, pages 14-24. IEEE Computer Society, 1995. URL: http://dx.doi.org/10.1109/LICS.1995.523240.
- Igor Walukiewicz. Completeness of Kozen’s axiomatisation of the propositional mu-calculus. Information and Computation, 157(1-2):142-182, 2000. URL: http://dx.doi.org/10.1006/inco.1999.2836.
-
Noam Zeilberger. The logical basis of evaluation order and pattern matching. PhD thesis, The logical basis of evaluation order and pattern matching, 2009.