3 Search Results for "Salibra, Antonino"

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.FSCD.2025.12
Ohana Trees and Taylor Expansion for the λI-Calculus: No variable gets left behind or forgotten!

Authors: Rémy Cerda, Giulio Manzonetto, and Alexis Saurin

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
Although the λI-calculus is a natural fragment of the λ-calculus, obtained by forbidding the erasure, its equational theories did not receive much attention. The reason is that all proper denotational models studied in the literature equate all non-normalizable λI-terms, whence the associated theory is not very informative. The goal of this paper is to introduce a previously unknown theory of the λI-calculus, induced by a notion of evaluation trees that we call "Ohana trees". The Ohana tree of a λI-term is an annotated version of its Böhm tree, remembering all free variables that are hidden within its meaningless subtrees, or pushed into infinity along its infinite branches. We develop the associated theories of program approximation: the first approach - more classic - is based on finite trees and continuity, the second adapts Ehrhard and Regnier’s Taylor expansion. We then prove a Commutation Theorem stating that the normal form of the Taylor expansion of a λI-term coincides with the Taylor expansion of its Ohana tree. As a corollary, we obtain that the equality induced by Ohana trees is compatible with abstraction and application. We conclude by discussing the cases of Lévy-Longo and Berarducci trees, and generalizations to the full λ-calculus.
Cite as

Rémy Cerda, Giulio Manzonetto, and Alexis Saurin. Ohana Trees and Taylor Expansion for the λI-Calculus: No variable gets left behind or forgotten!. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 12:1-12:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{cerda_et_al:LIPIcs.FSCD.2025.12,
  author =	{Cerda, R\'{e}my and Manzonetto, Giulio and Saurin, Alexis},
  title =	{{Ohana Trees and Taylor Expansion for the \lambdaI-Calculus: No variable gets left behind or forgotten!}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{12:1--12:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.12},
  URN =		{urn:nbn:de:0030-drops-236277},
  doi =		{10.4230/LIPIcs.FSCD.2025.12},
  annote =	{Keywords: \lambda-calculus, program approximation, Taylor expansion, \lambdaI-calculus, persistent free variables, B\"{o}hm trees, Ohana trees}
}
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}
}
  • Refine by Type
  • 3 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 1 2025
  • 1 2012

  • Refine by Author
  • 2 Manzonetto, Giulio
  • 2 Salibra, Antonino
  • 1 Bucciarelli, Antonio
  • 1 Carraro, Alberto
  • 1 Cerda, Rémy
  • Show More...

  • Refine by Series/Journal
  • 3 LIPIcs

  • Refine by Classification
  • 2 Theory of computation → Lambda calculus
  • 1 Theory of computation → Denotational semantics
  • 1 Theory of computation → Rewrite systems

  • Refine by Keyword
  • 1 Böhm trees
  • 1 Groups
  • 1 Inverse Semigroups
  • 1 Invertibility
  • 1 Lambda Calculus
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact