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}
}

Document

DOI: 10.4230/LIPIcs.CSL.2012.152

On the equational consistency of order-theoretic models of the lambda-calculus

Authors: Alberto Carraro and Antonino Salibra

Published in: LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)

Abstract

Answering a question by Honsell and Plotkin, we show that there are two equations between lambda terms, the so-called subtractive equations, consistent with lambda calculus but not satisfied in any partially ordered model with bottom element. We also relate the subtractive equations to the open problem of the order-incompleteness of lambda calculus.

Cite as

Alberto Carraro and Antonino Salibra. On the equational consistency of order-theoretic models of the lambda-calculus. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 152-166, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{carraro_et_al:LIPIcs.CSL.2012.152,
  author =	{Carraro, Alberto and Salibra, Antonino},
  title =	{{On the equational consistency of order-theoretic models of the lambda-calculus}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{152--166},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{C\'{e}gielski, Patrick and Durand, Arnaud},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.152},
  URN =		{urn:nbn:de:0030-drops-36703},
  doi =		{10.4230/LIPIcs.CSL.2012.152},
  annote =	{Keywords: Lambda calculus, order-incompleteness, partially ordered models}
}

Search Results

Documents authored by Salibra, Antonino

Groups and Inverse Semigroups in Lambda Calculus

Abstract

Cite as

On the equational consistency of order-theoretic models of the lambda-calculus

Abstract

Cite as

Thanks for your feedback!

Could not send message