DROPS

Document

DOI: 10.4230/LIPIcs.FSCD.2026.9

Groups and Inverse Semigroups in Lambda Calculus

Authors: Antonio Bucciarelli, Arturo De Faveri, Giulio Manzonetto, and Antonino Salibra

Published in: LIPIcs, Volume 378, 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)

Abstract

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 FHP/T, and to infinite η-expansion in 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.

Cite as

Antonio Bucciarelli, Arturo De Faveri, Giulio Manzonetto, and Antonino Salibra. Groups and Inverse Semigroups in Lambda Calculus. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 9:1-9:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{bucciarelli_et_al:LIPIcs.FSCD.2026.9,
  author =	{Bucciarelli, Antonio and De Faveri, Arturo and Manzonetto, Giulio and Salibra, Antonino},
  title =	{{Groups and Inverse Semigroups in Lambda Calculus}},
  booktitle =	{11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
  pages =	{9:1--9:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-433-8},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{378},
  editor =	{Pfenning, Frank},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.9},
  URN =		{urn:nbn:de:0030-drops-263596},
  doi =		{10.4230/LIPIcs.FSCD.2026.9},
  annote =	{Keywords: Lambda Calculus, Invertibility, Groups, Inverse Semigroups}
}

Search Results

Documents authored by De Faveri, Arturo

Groups and Inverse Semigroups in Lambda Calculus

Abstract

Cite as

Thanks for your feedback!

Could not send message