Groups and Inverse Semigroups in Lambda Calculus
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2026
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866908990584127488 |
|---|---|
| author | Bucciarelli, Antonio De Faveri, Arturo Manzonetto, Giulio Salibra, Antonino |
| author_facet | Bucciarelli, Antonio De Faveri, Arturo Manzonetto, Giulio Salibra, Antonino |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2602_05654 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Groups and Inverse Semigroups in Lambda Calculus Bucciarelli, Antonio De Faveri, Arturo Manzonetto, Giulio Salibra, Antonino Logic in Computer Science 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. |
| title | Groups and Inverse Semigroups in Lambda Calculus |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2602.05654 |