Alexis Saurin

Rémy Cerda, Giulio Manzonetto, Alexis Saurin

Although the $λ$I-calculus is a natural fragment of the $λ$-calculus, obtained by forbidding the erasure of arguments, its equational theories did not receive much attention. The reason is that all proper denotational models studied in the literature equate all non-normalizable $λ$I-terms, whence the associated theory is not very informative. The goal of this paper is to introduce a previously unknown theory of the $λ$I-calculus, induced by a notion of evaluation trees that we call "Ohana trees". The Ohana tree of a $λ$I-term is an annotated version of its Böhm tree, remembering all free variables that are hidden within its meaningless subtrees, or pushed into infinity along its infinite branches. We develop the associated theories of program approximation: the first approach -- more classic -- is based on finite trees and continuity, the second adapts Ehrhard and Regnier's Taylor expansion. We then prove a Commutation Theorem stating that the normal form of the Taylor expansion of a $λ$I-term coincides with the Taylor expansion of its Ohana tree. As a corollary, we obtain that the equality induced by Ohana trees is compatible with abstraction and application. Subsequently, we introduce a denotational model designed to capture the equality induced by Ohana trees. Although presented as a non-idempotent type system, our model is based on a suitably modified version of the relational semantics of the $λ$-calculus, which is known to yield proper models of the $λ$I-calculus when restricted to non-empty finite multisets. To track variables occurring in subterms that are hidden or pushed to infinity in the evaluation trees, we generalize the system in two ways: first, we reintroduce annotated versions of the empty multiset indexed by sets of variables; second, (...)

Rémy Cerda, Alexis Saurin

We introduce a generic presentation of 'syntactic objects built by mixed induction and coinduction' encompassing all standard kinds of infinitary terms, as well as derivation trees in non-wellfounded proof systems. We then define a notion of coinductive rewriting of such objects, which is equivalent to the original presentation of infinitary rewriting relying on metric convergence and ordinal-indexed sequences of rewriting steps. This provides a unified coinductive presentation of e.g. first-order infinitary rewriting, infinitary λ-calculi, and cut-elimination in non-wellfounded proofs. We then formulate and study the coinductive counterpart of compression, i.e. the property of an infinitary rewriting system such that all rewriting sequences of any ordinal length can be 'compressed' to equivalent sequences of length at most ω(which ensures that they can be finitely approximated). We characterise compression in our generic setting for coinductive rewriting, 'factorising' the part of the proof that can be performed at this level of generality. Our proof is fully coinductive, avoiding any detour via rewriting sequences. Finally we focus on the non-wellfounded proof system \muMALL\infty for multiplicative-additive linear logic with fixed points, and we put our results to work in order to prove that compression holds for cut-elimination in this setting, which is a key lemma of several extension of cut-elimination to similar systems.