Groups and Inverse Semigroups in Lambda Calculus

TL;DR

This paper explores the invertibility of lambda calculus terms using inverse semigroup theory, revealing algebraic structures that characterize invertible elements across various lambda theories.

Contribution

It introduces a novel algebraic framework using inverse semigroups to analyze invertibility in lambda calculus, unifying and extending previous results.

Findings

FHPs form inverse semigroups modulo lambda theories.

HPs form inverse semigroups when theories include B"ohm trees.

FHPs are the invertible lambda-terms between lambda eta and Morris' observational theory.

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.