Groups and Inverse Semigroups in Lambda Calculus

Antonino Salibra; Antonio Bucciarelli; Arturo De Faveri; Giulio Manzonetto

arxiv: 2602.05654 · v4 · submitted 2026-02-05 · 💻 cs.LO

Groups and Inverse Semigroups in Lambda Calculus

Antonio Bucciarelli , Arturo De Faveri , Giulio Manzonetto , Antonino Salibra This is my paper

Pith reviewed 2026-05-16 07:02 UTC · model grok-4.3

classification 💻 cs.LO

keywords lambda calculuslambda theoriesinvertible lambda-termsinverse semigroupsfinite hereditary permutationseta-expansionBohm treesMorris theory

0 comments

The pith

Finite hereditary permutations are the invertible lambda-terms in every lambda-theory between lambda-eta and H+.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes that a specific class of lambda-terms known as finite hereditary permutations coincide exactly with the invertible elements under any lambda-theory lying in the interval from the basic extensional theory lambda-eta to Morris' observational theory H+. It models these terms using the algebraic structure of inverse semigroups, showing that the quotient of finite hereditary permutations by any such theory T always forms an inverse semigroup whose natural partial order matches eta-expansion. This algebraic correspondence is then used to lift known invertibility results from the endpoints of the interval to all intermediate theories. The approach also treats the infinite hereditary permutations, which form inverse semigroups precisely when the theory contains the theory of Bohm trees.

Core claim

The central claim is that the finite hereditary permutations modulo T are exactly the invertible lambda-terms for every lambda-theory T with lambda-eta contained in T contained in H+. This is obtained by proving that FHP/T is always an inverse semigroup, that its natural order coincides with eta-expansion, and that these facts together allow the set of invertible elements to be identified with the FHPs throughout the interval of theories.

What carries the argument

finite hereditary permutations (FHP) modulo a lambda-theory T, which form an inverse semigroup whose natural order corresponds to eta-expansion

If this is right

FHP/T forms an inverse semigroup for every lambda-theory T.
The natural order on FHP/T is precisely eta-expansion.
HP/T forms an inverse semigroup whenever T contains the theory of Bohm trees.
The set of invertible lambda-terms coincides with the FHPs in every theory from lambda-eta to H+.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same semigroup structure might classify invertible terms in variants of the lambda-calculus that lie outside the stated interval.
The correspondence between natural order and eta-expansion could be tested directly in concrete models such as the Bohm-tree model.

Load-bearing premise

The natural partial order of the inverse semigroup FHP/T coincides exactly with eta-expansion in the lambda-theory.

What would settle it

A lambda-term that is invertible in some theory strictly between lambda-eta and H+ yet is not equal modulo that theory to any finite hereditary permutation.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper shows FHPs are exactly the invertible terms in every theory from lambda-eta to H+ by framing them as inverse semigroups whose order matches eta-expansion.

read the letter

The main takeaway is that finite hereditary permutations are the invertible lambda terms across the whole interval of theories from lambda-eta to H+. The authors reach this by showing that FHP modulo any T forms an inverse semigroup and that the semigroup's natural order lines up with eta-expansion, which lets them lift the known invertibility at the endpoints to everything in between. They also handle the infinite HP case when T contains the Bohm tree theory. This unifies earlier results on the boundary theories under one algebraic setup rather than treating them as separate cases. The correspondence between the order and eta-expansion is the key step that makes the lifting work, and it fits cleanly with how inverse semigroups are usually ordered. The approach is straightforward once the semigroup structure is in place, and it avoids introducing new parameters or circular definitions. The soft spot is that the abstract states the theorems without giving the actual proof steps, so it is not possible to verify here whether the lifting argument covers all cases or if the infinite HP side has any hidden restrictions. The assumption that the order matches eta-expansion carries a lot of weight, and any gap there would affect the main claim. Nothing else looks shaky on the surface. This is aimed at people who already work with lambda theories and algebraic models of computation. A reader comfortable with inverse semigroups and the standard theories will see the value in the unification. It is worth sending to peer review because the result is specific, the framework is standard, and the claims are checkable once the proofs are written out.

Referee Report

2 major / 2 minor

Summary. The paper studies invertibility of λ-terms modulo λ-theories, centering on finite hereditary permutations (FHPs) as the invertible elements of λη and hereditary permutations (HPs) as those of H*. It shows that FHP/T forms an inverse semigroup for any λ-theory T, that HP/T is an inverse semigroup whenever T contains the theory of Böhm trees, and that the natural order on these semigroups corresponds to (finite or infinite) η-expansion. From these correspondences the authors conclude that FHPs are precisely the invertible λ-terms in every theory T satisfying λη ⊆ T ⊆ H+ (Morris’ observational theory).

Significance. If the central claims hold, the work supplies a uniform inverse-semigroup account of invertibility across the interval of λ-theories from λη to H+, recasting earlier results on groups of invertible terms and supplying a new algebraic tool for studying observational equivalences. The explicit link between the semigroup order and η-expansion is a concrete technical advance that may be reusable in other studies of term equivalence.

major comments (2)

[§5] The lifting argument that uses the natural-order/η-expansion correspondence to extend invertibility from the boundary theories λη and H* to the entire interval [λη, H+] is load-bearing for the main theorem; the manuscript must supply an explicit statement of the relevant lemma (including the precise definition of the order on FHP/T) and its proof.
[§4.2] The claim that HP/T is an inverse semigroup precisely when T contains the Böhm-tree theory is used to handle the upper end of the interval; the manuscript should isolate the minimal axioms of the Böhm-tree theory that are actually invoked in the inverse-semigroup verification.

minor comments (2)

[Introduction] Notation for the theories H* and H+ is introduced only in the abstract; a short paragraph in the introduction recalling Morris’ definition of H+ via β-normal-form observables would improve readability.
[§3] The manuscript refers to “the natural order” on an inverse semigroup without reminding the reader of its standard definition (a ≤ b iff a = e b for some idempotent e); adding this one-line reminder before the correspondence theorem would help readers outside semigroup theory.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and constructive suggestions. The comments highlight opportunities to strengthen the clarity of our central arguments, and we will incorporate the requested additions in the revised manuscript.

read point-by-point responses

Referee: [§5] The lifting argument that uses the natural-order/η-expansion correspondence to extend invertibility from the boundary theories λη and H* to the entire interval [λη, H+] is load-bearing for the main theorem; the manuscript must supply an explicit statement of the relevant lemma (including the precise definition of the order on FHP/T) and its proof.

Authors: We agree that the lifting argument is central and that its presentation can be improved. In the revised version we will insert a new, self-contained lemma (placed at the beginning of §5) that states the precise definition of the natural order on FHP/T, records the correspondence between this order and η-expansion, and supplies a complete proof of the correspondence. The lemma will then be invoked explicitly in the lifting step that extends invertibility from the boundary theories to the full interval [λη, H+]. revision: yes
Referee: [§4.2] The claim that HP/T is an inverse semigroup precisely when T contains the Böhm-tree theory is used to handle the upper end of the interval; the manuscript should isolate the minimal axioms of the Böhm-tree theory that are actually invoked in the inverse-semigroup verification.

Authors: We accept the suggestion. Section 4.2 will be revised to isolate and list the minimal set of axioms from the Böhm-tree theory that are actually used in the verification that HP/T forms an inverse semigroup. This will make transparent exactly which properties of the Böhm-tree theory are required for the upper bound of the interval. revision: yes

Circularity Check

0 steps flagged

No circularity; derivation self-contained via external algebraic structure

full rationale

The paper defines FHP/T and HP/T as inverse semigroups for theories T in the interval [λη, H+], proves the natural order coincides with η-expansion (or infinite η-expansion), and lifts invertibility from the boundary theories. These steps are stated as theorems resting on the standard definition of inverse semigroups and the known properties of λ-theories (Böhm trees, observational equivalence via β-normal forms). No equation reduces a claimed prediction to a fitted input by construction, no self-citation is load-bearing for the central result, and no ansatz or uniqueness theorem is smuggled in from prior author work. The derivation therefore remains independent of its own outputs.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on standard domain assumptions about lambda theories and the algebraic properties of inverse semigroups; no free parameters or new entities are introduced.

axioms (2)

domain assumption Lambda theories between lambda eta and H+ preserve the invertibility of FHP terms under the semigroup order.
Invoked to extend the invertibility result from the base theory to the full interval.
domain assumption The theory of Bohm trees is contained in any T for which HP/T forms an inverse semigroup.
Used to guarantee the inverse-semigroup structure for hereditary permutations.

pith-pipeline@v0.9.0 · 5566 in / 1211 out tokens · 32358 ms · 2026-05-16T07:02:17.489067+00:00 · methodology

Groups and Inverse Semigroups in Lambda Calculus

Core claim

What carries the argument

If this is right

Where Pith is reading between the lines

Load-bearing premise

What would settle it

discussion (0)