Groups and Inverse Semigroups in Lambda Calculus

TL;DR

This work develops an inverse-semigroup framework for the invertibility of $λ$-terms across λ-theories, identifying finite hereditary permutations ($FHP$) and their infinite counterparts ($HP$) as canonical invertibles in relevant theories. By encoding these objects with permutation trees (PT) and analysing their algebraic structure, the authors show that $FHP$-modulo any theory $T$ forms an inverse semigroup, and $HP$-modulo $T$ does so whenever $T$ includes Böhm-tree theory; the natural order corresponds to finite or infinite $η$-expansion depending on the object. The main contributions include a broad recasting of prior results and a complete characterization: $FHP$ are exactly the invertible $λ$-terms in all theories between $λη$ and $H^+$, while $HP$ invertibility aligns with Böhm-tree theory, resolving conjectures about invertibles in intermediate theories. The work links invertibility in λ-calculus to inverse-momain theory, establishing $F$-inverse and residually finite structures and offering a unified algebraic perspective with potential implications for semantic models and observational theories such as Morris’ $H^*$.

Abstract

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.

Theorems & Definitions (24)

• Definition 1
• Lemma 2
• Definition 3
• Proposition 4
• Theorem 5
• Definition 6
• Definition 7
• Definition 8
• Definition 9
• Proposition 10