On the dynamics of cut-elimination for circular and non-wellfounded proofs
In this talk, I will consider the structural proof theory of fixed-point logics and their cut-elimination theorems, focusing on their computational content.
More specifically, I will consider logics with least and greatest fixed-points, expressing inductive and coinductive properties, and proof systems for those logics admitting “circular” and non-wellfounded proofs [1, 2, 4, 5]. Those derivations are finitely branching but admit infinitely deep branches, possibly subject to some regularity conditions. Circular derivations are closely related with proofs by infinite descent [3] and shall be equipped with a global condition preventing vicious circles in proofs.
In order to unveil the computational content of those logical systems, I will concentrate on linear logic extended with least and greatest fixed points (µLL), that is, on the µ-calculus considered in a linear setting, where the structural rules of contraction and weakening are prohibited (or carefully controlled at least). In particular, following the spirit of structural proof-theory and of the Curry-Howard correspondence, we will be interested not only in the structure of provability but also in the structure of proofs themselves, corresponding to programs (while formulas correspond to data and codata types).
I will first introduce the non-wellfounded proof systems for µLL and for its exponential-free fragment, µMALL (that is, multiplicative and additive linear logic with least and greatest fixed points). After establishing cut-elimination for µMALL [2], I will show how to generalize the cut-elimination result to µLL (as well as to the intuitionistic and classical non-wellfounded sequent calculi). After that, I will discuss limitations of the validity condition considered above, from a computational perspective, and introduce a more flexible validity condition, called bouncing-validity [1], and establish a cut-elimination theorem for this richer system which, while proving the same theorems, admits more valid proofs that is, through the bridge of the Curry-Howard correspondence, more programs.
References
- [1]
- David Baelde, Amina Doumane, Denis Kuperberg, and Alexis Saurin, Bouncing Threads for Circular and Non-wellfounded Proofs – Towards Compositionality with Circular Proofs, To appear in 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2022 (Haifa, Israel), 2022. long version of the present paper, available at https://hal.archives-ouvertes.fr/hal-03682126.
- [2]
- 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 (Marseille, France), (LIPIcs), Vol. 62. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 42:1-42:17. http://www.dagstuhl.de/dagpub/978-3-95977-022-4
- [3]
- James Brotherston and Alex Simpson, Sequent Calculi for Induction and Infinite Descent, Journal of Logic and Computation, vol. 21 (2011), no. 6, pp. 1177–1216.
- [4]
- Jérôme Fortier and Luigi Santocanale, Cuts for Circular Proofs: Semantics and Cut-elimination, Computer Science Logic 2013 (CSL 2013), CSL 2013 (Torino, Italy), (Simona Ronchi Della Rocca, editor), (LIPIcs), , Vol. 23. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2013, 248-262.
- [5]
- Luigi Santocanale, A Calculus of Circular Proofs and Its Categorical Semantics, Foundations of Software Science and Computation Structures, (Mogens Nielsen and Uffe Engberg, editors), vol. 2303, Lecture Notes in Computer Science, Springer, 2002, pp. 357–371
This document was translated from LATEX by HEVEA.