Groups and Inverse Semigroups in Lambda Calculus

Abstract

We study invertibility of $\lambda$-terms modulo $\lambda$-theories. Here a fundamental role is played by a class of $\lambda$-terms called finite hereditary permutations (FHP) and by their infinite generalisations (HP). More precisely, FHPs are the invertible elements in the least extensional $\lambda$-theory $\lambda \eta$ and HPs are those in the greatest sensible $\lambda$-theory $H^*$. Our approach is based on inverse semigroups, algebraic structures that generalise groups and semilattices. We show that FHP modulo a $\lambda$-theory $T$ is always an inverse semigroup and that HP modulo $T$ is an inverse semigroup whenever $T$ contains the theory of B\"ohm trees. An inverse semigroup comes equipped with a natural order. We prove that the natural order corresponds to $\eta$-expansion in $\mathrm{FHP} /T$, and to infinite $\eta$-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 $\lambda$-terms in all the $\lambda$-theories lying between $\lambda \eta$ and $H^+$. The latter is Morris' observational $\lambda$-theory, defined by using the $\beta$-normal forms as observables.