Giulio Manzonetto

Antonio Bucciarelli, Arturo De Faveri, Giulio Manzonetto et al.

We study invertibility of $λ$-terms modulo $λ$-theories. Here a fundamental role is played by a class of $λ$-terms called finite hereditary permutations (FHP) and by their infinite generalisations (HP). More precisely, FHPs are the invertible elements in the least extensional $λ$-theory $λη$ and HPs are those in the greatest sensible $λ$-theory $H^*$. Our approach is based on inverse semigroups, algebraic structures that generalise groups and semilattices. We show that FHP modulo a $λ$-theory $T$ is always an inverse semigroup and that HP modulo $T$ is an inverse semigroup whenever $T$ contains the theory of Böhm trees. An inverse semigroup comes equipped with a natural order. We prove that the natural order corresponds to $η$-expansion in $\mathrm{FHP} /T$, and to infinite $η$-expansion in $\mathrm{HP}/T$. Building on these correspondences we obtain the two main contributions of this work: firstly, we recast in a broader framework the results cited at the beginning; secondly, we prove that the FHPs are the invertible $λ$-terms in all the $λ$-theories lying between $λη$ and $H^+$. The latter is Morris' observational $λ$-theory, defined by using the $β$-normal forms as observables.

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, (...)

Adrienne Lancelot, Giulio Manzonetto, Guy McCusker et al.

The relational semantics of linear logic is a powerful framework for defining resource-aware models of the $λ$-calculus. However, its quantitative aspects are not reflected in the preorders and equational theories induced by these models. Indeed, they can be characterized in terms of (in)equalities between Böhm trees up to extensionality, which are qualitative in nature. We employ the recently introduced checkers calculus to provide a quantitative and contextual interpretation of the preorder associated to the relational semantics. This way, we show that the relational semantics refines the contextual preorder constraining the number of interactions between the related terms and the context.