lambda!-calculus, Intersection Types, and Involutions
Document Open Access Logo

lambda!-calculus, Intersection Types, and Involutions

Authors Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, Marina Lenisa, Ivan Scagnetto

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2019.15.pdf
  • Filesize: 0.51 MB
  • 16 pages

Document Identifiers

Author Details

Alberto Ciaffaglione
  • Department of Mathematics, Computer Science and Physics, University of Udine, Italy
Pietro Di Gianantonio
  • Department of Mathematics, Computer Science and Physics, University of Udine, Italy
Furio Honsell
  • Department of Mathematics, Computer Science and Physics, University of Udine, Italy
Marina Lenisa
  • Department of Mathematics, Computer Science and Physics, University of Udine, Italy
Ivan Scagnetto
  • Department of Mathematics, Computer Science and Physics, University of Udine, Italy

Funding

Work supported by the Italian departmental research project "LambdaBridge" (D.R.N. 427/2018 of 03/08/2018, University of Udine).

Cite As Get BibTex

Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, Marina Lenisa, and Ivan Scagnetto. lambda!-calculus, Intersection Types, and Involutions. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 15:1-15:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.FSCD.2019.15

Abstract

Abramsky’s affine combinatory algebras are models of affine combinatory logic, which refines standard combinatory logic in the direction of Linear Logic. Abramsky introduced various universal models of computation based on affine combinatory algebras, consisting of partial involutions over a suitable formal language {of moves}, in order to discuss reversible computation in a Geometry of Interaction setting. We investigate partial involutions from the point of view of the model theory of lambda!-calculus. The latter is a refinement of the standard lambda-calculus, corresponding to affine combinatory logic. We introduce intersection type systems for the lambda!-calculus, by extending standard intersection types with a !_u-operator. These induce affine combinatory algebras, and, via suitable quotients, models of the lambda!-calculus. In particular, we introduce an intersection type system for assigning principal types to lambda!-terms, and we state a correspondence between the partial involution interpreting a combinator and the principal type of the corresponding lambda!-term. This analogy allows for explaining as unification between principal types the somewhat awkward linear application of involutions arising from Geometry of Interaction.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program semantics
  • Theory of computation → Linear logic
Keywords
  • Affine Combinatory Algebra
  • Affine Lambda-calculus
  • Intersection Types
  • Geometry of Interaction

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Samson Abramsky. A structural approach to reversible computation. Theoretical Computer Science, 347(3):441-464, 2005. URL: http://dx.doi.org/10.1016/j.tcs.2005.07.002.
  2. Samson Abramsky, Esfandiar Haghverdi, and Philip Scott. Geometry of Interaction and linear combinatory algebras. Mathematical Structures in Computer Science, 12(5):625–665, 2002. URL: http://dx.doi.org/10.1017/S0960129502003730.
  3. Samson Abramsky and Radha Jagadeesan. Games and full completeness for multiplicative linear logic. Journal of Symbolic Logic, 59(2):543–574, 1994. URL: http://dx.doi.org/10.2307/2275407.
  4. Samson Abramsky and Marina Lenisa. Linear realizability and full completeness for typed lambda-calculi. Annals of Pure and Applied Logic, 134(2):122-168, 2005. URL: http://dx.doi.org/10.1016/j.apal.2004.08.003.
  5. Joe Armstrong. Making reliable distributed systems in the presence of software errors. PhD thesis, KTH, Microelectronics and Information Technology, IMIT, 2003. NR 20140805. Google Scholar
  6. Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. Journal of Symbolic Logic, 48(4):931–940, 1983. URL: http://dx.doi.org/10.2307/2273659.
  7. HP Barendregt. The Lambda Calculus. Its Syntax and Semantics. North-Holland, Amsterdam, 1984. (revised edition). Google Scholar
  8. Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, Marina Lenisa, and Ivan Scagnetto. Reversible Computation and Principal Types in λ!-calculus. The Bulletin of Symbolic Logic, 2018. Google Scholar
  9. Alberto Ciaffaglione, Furio Honsell, Marina Lenisa, and Ivan Scagnetto. The involutions-as-principal types/application-as-unification Analogy. In Gilles Barthe, Geoff Sutcliffe, and Margus Veanes, editors, LPAR, volume 57 of EPiC Series in Computing, pages 254-270. EasyChair, 2018. URL: http://dblp.uni-trier.de/db/conf/lpar/lpar2018.html#CiaffaglioneHLS18.
  10. Ugo Dal Lago and Barbara Petit. The geometry of types. In The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'13, Proceedings, pages 167-178. ACM, 2013. Google Scholar
  11. Alessandra Di Pierro, Chris Hankin, and Herbert Wiklicky. Reversible combinatory logic. Mathematical Structures in Computer Science, 16(4):621–637, 2006. URL: http://dx.doi.org/10.1017/S0960129506005391.
  12. Erlang official website. Last access: 19 2018. URL: http://www.erlang.org.
  13. Pietro Di Gianantonio, Furio Honsell, and Marina Lenisa. A type assignment system for game semantics. Theoretical Computer Science, 398(1):150-169, 2008. Calculi, Types and Applications: Essays in honour of M. Coppo, M. Dezani-Ciancaglini and S. Ronchi Della Rocca. URL: http://dx.doi.org/10.1016/j.tcs.2008.01.023.
  14. Pietro Di Gianantonio and Marina Lenisa. Innocent Game Semantics via Intersection Type Assignment Systems. In Simona Ronchi Della Rocca, editor, Computer Science Logic 2013 (CSL 2013), volume 23 of Leibniz International Proceedings in Informatics (LIPIcs), pages 231-247, Dagstuhl, Germany, 2013. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2013.231.
  15. Jean-Yves Girard. Geometry of interaction 2: Deadlock-free algorithms. In Per Martin-Löf and Grigori Mints, editors, COLOG-88, pages 76-93, Berlin, Heidelberg, 1990. Springer Berlin Heidelberg. Google Scholar
  16. Jean-Yves Girard. Geometry of interaction III: accommodating the additives. London Mathematical Society Lecture Note Series, pages 329-389, 1995. Google Scholar
  17. Esfandiar Haghverdi. A categorical approach to linear logic, geometry of proofs and full completeness. University of Ottawa (Canada), 2000. Google Scholar
  18. Alex Simpson. Reduction in a Linear Lambda-Calculus with Applications to Operational Semantics. In Jürgen Giesl, editor, Term Rewriting and Applications, pages 219-234, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. Google Scholar
  19. Web Appendix with Erlang code. URL: http://www.dimi.uniud.it/scagnett/pubs/automata-erlang.pdf.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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