Document Open Access Logo

Groups and Inverse Semigroups in Lambda Calculus

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

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2026.9.pdf
  • Filesize: 0.9 MB
  • 22 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Lambda calculus
Keywords
  • Lambda Calculus
  • Invertibility
  • Groups
  • Inverse Semigroups

Metrics

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 Get BibTex

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) https://doi.org/10.4230/LIPIcs.FSCD.2026.9

Author Details

Antonio Bucciarelli
  • Université Paris Cité, CNRS, IRIF, F-75013, Paris, France
Arturo De Faveri
  • Université Paris Cité, CNRS, IRIF, F-75013, Paris, France
Giulio Manzonetto
  • Université Paris Cité, CNRS, IRIF, F-75013, Paris, France
Antonino Salibra
  • Université Paris Cité, CNRS, IRIF, F-75013, Paris, France

References

  1. Samson Abramsky. Computational interpretations of linear logic. Theor. Comput. Sci., 111(1&2):3-57, 1993. URL: https://doi.org/10.1016/0304-3975(93)90181-R.
  2. Roberto Amadio and Pierre-Louis Curien. Domains and lambda-calculi, volume 46 of Cambridge Tracts in Theoretical Computer Science. CUP, 1998. Google Scholar
  3. Andrea Asperti and Giuseppe Longo. Categories, types and structures: an introduction to category theory for the working computer scientist. MIT Press, Cambridge, MA, 1991. Google Scholar
  4. Karl Auinger, Ganna Kudryavtseva, and Mária B. Szendrei. F-inverse monoids as algebraic structures in enriched signature. Indiana University Mathematics Journal, 70(5):2107-2131, 2021. Google Scholar
  5. Hendrik Pieter Barendregt, Wil Dekkers, and Richard Statman. Lambda Calculus with Types. Perspectives in logic. Cambridge University Press, 2013. URL: http://www.cambridge.org/de/academic/subjects/mathematics/logic-categories-and-sets/lambda-calculus-types.
  6. Henk Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, 1984. Google Scholar
  7. Henk Barendregt and Giulio Manzonetto. A Lambda Calculus Satellite, volume 94 of Studies in logic: Mathematical logic and foundations. College Publications, 2022. URL: https://www.collegepublications.co.uk/logic/mlf/?00035.
  8. Jan A. Bergstra and Jan Willem Klop. Invertible terms in the lambda calculus. Theor. Comput. Sci., 11:19-37, 1980. URL: https://doi.org/10.1016/0304-3975(80)90032-8.
  9. Lison Blondeau-Patissier, Pierre Clairambault, and Lionel Vaux Auclair. Strategies as resource terms, and their categorical semantics. Log. Methods Comput. Sci., 21(4), 2025. URL: https://doi.org/10.46298/LMCS-21(4:9)2025.
  10. Flavien Breuvart, Giulio Manzonetto, Andrew Polonsky, and Domenico Ruoppolo. New results on Morris’s observational theory: The benefits of separating the inseparable. In 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, volume 52 of Leibniz International Proceedings in Informatics (LIPIcs), pages 15:1-15:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.FSCD.2016.15.
  11. Corrado Böhm and Mariangiola Dezani-Ciancaglini. Combinatory logic as monoids. Fundamenta Informaticae, 12(4):525-540, 1989. Google Scholar
  12. Alonzo Church. The Calculi of Lambda Conversion. Princeton University Press, 1941. Google Scholar
  13. Pierre Clairambault. Causal Investigations in Interactive Semantics. HAL, 2024. URL: https://tel.archives-ouvertes.fr/tel-04523273.
  14. Mario Coppo, Mariangiola Dezani-Ciancaglini, and Maddalena Zacchi. Type theories, normal forms, and D_∞-lambda-models. Information and Computation, 72:85-116, 1987. Google Scholar
  15. Roberto Di Cosmo. A short survey of isomorphisms of types. Math. Struct. Comput. Sci., 15(5):825-838, 2005. URL: https://doi.org/10.1017/S0960129505004871.
  16. Lukasz Czajka. A new coinductive confluence proof for infinitary lambda calculus. Log. Methods Comput. Sci., 16(1), 2020. URL: https://doi.org/10.23638/LMCS-16(1:31)2020.
  17. Daniele D'Angeli, Emanuele Rodaro, and Jan Philipp Wächter. On the structure theory of partial automaton semigroups. Semigroup Forum, 101:51-76, 2020. Google Scholar
  18. Vincent Danos and Laurent Régnier. Local and asynchronous beta-reduction. In Proceedings of the 8th Annual IEEE Symposium on Logic in Computer Science (LICS 1993), pages 296-306, USA, 1993. IEEE Computer Society. Google Scholar
  19. Vincent Danos and Laurent Régnier. Reversible, irreversible and optimal lambda-machines. Theoretical Computer Science, 227(1-2):77-97, 1999. Google Scholar
  20. Mariangiola Dezani-Ciancaglini. Characterization of normal forms possessing inverse in the λ β η-calculus. Theoretical Computer Science, 2(3):323-337, 1976. Google Scholar
  21. Alejandro Díaz-Caro, Mauricio Guillermo, Alexandre Miquel, and Benoît Valiron. Realizability in the unitary sphere. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, pages 1-13. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785834.
  22. Thomas Ehrhard. On Köthe sequence spaces and linear logic. Math. Struct. Comput. Sci., 12(5):579-623, 2002. URL: https://doi.org/10.1017/S0960129502003729.
  23. Enno Folkerts. Invertibility in λη. In Thirteenth Annual IEEE Symposium on Logic in Computer Science, Indianapolis, Indiana, USA, June 21-24, 1998, pages 418-429. IEEE Computer Society, 1998. Google Scholar
  24. Jonathon Funk. Semigroups and toposes. Semigroup Forum, 75:480-519, 2007. Google Scholar
  25. Jonathon Funk and Benjamin Steinberg. The universal covering of an inverse semigroup. Applied Categorical Structures, 18:135-163, 2010. URL: https://doi.org/10.1007/s10485-008-9147-2.
  26. Pietro Di Gianantonio, Gianluca Franco, and Furio Honsell. Game semantics for untyped λ β η-calculus. In Jean-Yves Girard, editor, Typed Lambda Calculi and Applications, 4th International Conference, TLCA'99, L'Aquila, Italy, April 7-9, 1999, Proceedings, volume 1581 of Lecture Notes in Computer Science, pages 114-128. Springer, 1999. Google Scholar
  27. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1-101, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  28. Jean Goubault-Larrecq. Musings around the geometry of interaction, and coherence. Theoretical Computer Science, 412(20):1998-2014, 2011. URL: https://doi.org/10.1016/j.tcs.2010.12.023.
  29. Giulio Guerrieri and Federico Olimpieri. Categorifying non-idempotent intersection types. In Christel Baier and Jean Goubault-Larrecq, editors, 29th EACSL Annual Conference on Computer Science Logic, CSL 2021, Ljubljana, Slovenia (Virtual Conference), January 25-28, 2021, volume 183 of LIPIcs, pages 25:1-25:24. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CSL.2021.25.
  30. Karl H. Hofmann and Michael W. Mislove. All compact Hausdorff lambda models are degenerate. Fundamenta Informaticae, 22(1,2):23-52, 1995. URL: https://doi.org/10.3233/FI-1995-22122.
  31. John M. Howie. Fundamentals of Semigroup Theory, volume 12 of London Mathematical Society monographs. Oxford Science Publications, 1995. Google Scholar
  32. John Martin E. Hyland. A syntactic characterization of the equality in some models for the λ-calculus. Journal London Mathematical Society (2), 12(3):361-370, 1975. Google Scholar
  33. Benedetto Intrigila, Giulio Manzonetto, and Andrew Polonsky. Refutation of Sallé’s longstanding conjecture. In 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017, volume 84 of Leibniz International Proceedings in Informatics (LIPIcs), pages 20:1-20:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.FSCD.2017.20.
  34. Benedetto Intrigila, Giulio Manzonetto, and Andrew Polonsky. Degrees of extensionality in the theory of Böhm trees and Sallé’s conjecture. Logical Methods in Computer Science, 15(1), 2019. URL: https://doi.org/10.23638/LMCS-15(1:6)2019.
  35. Benedetto Intrigila and Monica Nesi. On structural properties of eta-expansions of identity. Information Processing Letters, 87(6):327-333, 2003. URL: https://doi.org/10.1016/S0020-0190(03)00344-2.
  36. Peter R. Jones, Stuart W. Margolis, John Meakin, and Joseph B. Stephen. Free products of inverse semigroups II. Glasgow Mathematical Journal, 33(3):373-387, 1991. Google Scholar
  37. Axel Kerinec, Giulio Manzonetto, and Federico Olimpieri. Why are proofs relevant in proof-relevant models? Proc. ACM Program. Lang., 7(POPL):218-248, 2023. URL: https://doi.org/10.1145/3571201.
  38. Dexter Kozen and Alexandra Silva. Practical coinduction. Mathematical Structures in Computer Science, 27(7):1132-1152, 2017. URL: https://doi.org/10.1017/S0960129515000493.
  39. Jean-Louis Krivine. On the structure of classical realizability models of ZF. In Hugo Herbelin, Pierre Letouzey, and Matthieu Sozeau, editors, 20th International Conference on Types for Proofs and Programs, TYPES 2014, Paris, France, May 12-15, 2014, volume 39 of LIPIcs, pages 146-161. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014. URL: https://doi.org/10.4230/LIPIcs.TYPES.2014.146.
  40. Joachim Lambek and Philip J. Scott. Introduction to higher order categorical logic, volume 007 of Cambridge studies in advanced mathematics. CUP, Cambridge, New York, Melbourne, 1986. Google Scholar
  41. Adrienne Lancelot, Beniamino Accattoli, and Maxime Vemclefs. Barendregt’s theory of the λ-calculus, refreshed and formalized. In Yannick Forster and Chantal Keller, editors, 16th International Conference on Interactive Theorem Proving, ITP 2025, Reykjavik, Iceland, September 28 - October 1, 2025, volume 352 of LIPIcs, pages 13:1-13:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.ITP.2025.13.
  42. Mark V. Lawson. Inverse Semigroups. World Scientific, 1998. Google Scholar
  43. Mark V. Lawson. Non-commutative Stone duality: inverse semigroups, topological groupoids and C*-algebras. International Journal of Algebra and Computation, 22(6):1-47, 2012. URL: https://doi.org/10.1142/S0218196712500580.
  44. Stefania Lusin and Antonino Salibra. The lattice of lambda theories. J. Log. Comput., 14(3):373-394, 2004. URL: https://doi.org/10.1093/logcom/14.3.373.
  45. Giulio Manzonetto and Antonino Salibra. Applying universal algebra to lambda calculus. Journal of Logic and Computation, 20(4):877-915, 2010. URL: https://doi.org/10.1093/logcom/exn085.
  46. James Hiram Morris. Lambda calculus models of programming languages. Phd thesis, Massachusetts Institute of Technology (MIT), 1968. Google Scholar
  47. Simona Ronchi Della Rocca and Luca Paolini. The Parametric Lambda Calculus: A Metamodel for Computation. Texts in Theoretical Computer Science. An EATCS Series. Springer Berlin, Heidelberg, 2004. Google Scholar
  48. Antonino Salibra. On the algebraic models of lambda calculus. Theoretical Computer Science, 249:197-240, 2000. URL: https://doi.org/10.1016/S0304-3975(00)00059-1.
  49. Rick Statman. Church’s semigroup is Sq-universal. In Proceedings of the 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021), volume 196 of Leibniz International Proceedings in Informatics (LIPIcs), pages 6:1-6:6. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.FSCD.2021.6.
  50. Steffen van Bakel, Franco Barbanera, Mariangiola Dezani-Ciancaglini, and Fer Jan de Vries. Intersection types for λ-trees. Theoretical Computer Science, 272:3-40, 2002. Google Scholar
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