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.TLCA.2015.123

Observability for Pair Pattern Calculi

Authors: Antonio Bucciarelli, Delia Kesner, and Simona Ronchi Della Rocca

Published in: LIPIcs, Volume 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)

Abstract

Inspired by the notion of solvability in the λ-calculus, we define a notion of observability for a calculus with pattern matching. We give an intersection type system for such a calculus which is based on non-idempotent types. The typing system is shown to characterize the set of terms having canonical form, which properly contains the set of observable terms, so that typability alone is not sufficient to characterize observability. However, the inhabitation problem associated with our typing system turns out to be decidable, a result which — together with typability — allows to obtain a full characterization of observability.

Cite as

Antonio Bucciarelli, Delia Kesner, and Simona Ronchi Della Rocca. Observability for Pair Pattern Calculi. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 123-137, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{bucciarelli_et_al:LIPIcs.TLCA.2015.123,
  author =	{Bucciarelli, Antonio and Kesner, Delia and Ronchi Della Rocca, Simona},
  title =	{{Observability for Pair Pattern Calculi}},
  booktitle =	{13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
  pages =	{123--137},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-87-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{38},
  editor =	{Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.123},
  URN =		{urn:nbn:de:0030-drops-51596},
  doi =		{10.4230/LIPIcs.TLCA.2015.123},
  annote =	{Keywords: solvability, pattern calculi, intersection types, inhabitation}
}

Document

DOI: 10.4230/LIPIcs.CSL.2011.97

Full Abstraction for Resource Calculus with Tests

Authors: Antonio Bucciarelli, Alberto Carraro, Thomas Ehrhard, and Giulio Manzonetto

Published in: LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011)

Abstract

We study the semantics of a resource sensitive extension of the lambda-calculus in a canonical reflexive object of a category of sets and relations, a relational version of the original Scott D infinity model of the pure lambda-calculus. This calculus is related to Boudol's resource calculus and is derived from Ehrhard and Regnier's differential extension of Linear Logic and of the lambda-calculus. We extend it with new constructions, to be understood as implementing a very simple exception mechanism, and with a ``must'' parallel composition. These new operations allow to associate a context of this calculus with any point of the model and to prove full abstraction for the finite sub-calculus where ordinary lambda-calculus application is not allowed. The result is then extended to the full calculus by means of a Taylor Expansion formula.

Cite as

Antonio Bucciarelli, Alberto Carraro, Thomas Ehrhard, and Giulio Manzonetto. Full Abstraction for Resource Calculus with Tests. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 97-111, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{bucciarelli_et_al:LIPIcs.CSL.2011.97,
  author =	{Bucciarelli, Antonio and Carraro, Alberto and Ehrhard, Thomas and Manzonetto, Giulio},
  title =	{{Full Abstraction for Resource Calculus with Tests}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{97--111},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-32-3},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{12},
  editor =	{Bezem, Marc},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.97},
  URN =		{urn:nbn:de:0030-drops-32250},
  doi =		{10.4230/LIPIcs.CSL.2011.97},
  annote =	{Keywords: resource lambda calculus, relational semantics, full abstraction, differential linear logic}
}

Search Results

Documents authored by Bucciarelli, Antonio

Groups and Inverse Semigroups in Lambda Calculus

Abstract

Cite as

Observability for Pair Pattern Calculi

Abstract

Cite as

Full Abstraction for Resource Calculus with Tests

Abstract

Cite as

Thanks for your feedback!

Could not send message