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.

翻译：本文研究λ项在λ理论下的可逆性。其中，有限遗传置换（FHP）类λ项及其无限推广（HP）扮演着基础角色。具体而言，FHPs是最小外延λ理论λη中的可逆元，HPs是最大合理λ理论H*中的可逆元。我们的方法基于逆半群——一种推广了群与半格的代数结构。我们证明：对于任意λ理论T，FHP模T总构成逆半群；而当T包含Böhm树理论时，HP模T也构成逆半群。逆半群天然配备一个偏序。我们证明该自然序在FHP/T中对应于η展开，在HP/T中对应于无限η展开。基于这些对应关系，我们得到本工作的两个主要贡献：首先，将开篇引述的结果置于更广泛的框架中重新阐述；其次，证明FHPs是所有介于λη与H+之间的λ理论中的可逆λ项。其中H+是Morris的观测λ理论，其通过β正规形式定义可观测性。