Λ-Symsym: An Interactive Tool for Playing with Involutions and Types

Authors Furio Honsell, Marina Lenisa, Ivan Scagnetto



PDF
Thumbnail PDF

File

LIPIcs.TYPES.2020.7.pdf
  • Filesize: 0.87 MB
  • 18 pages

Document Identifiers

Author Details

Furio Honsell
  • University of Udine, Italy
Marina Lenisa
  • University of Udine, Italy
Ivan Scagnetto
  • University of Udine, Italy

Acknowledgements

The authors would like to thank the anonymous referees for their helpful comments.

Cite AsGet BibTex

Furio Honsell, Marina Lenisa, and Ivan Scagnetto. Λ-Symsym: An Interactive Tool for Playing with Involutions and Types. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.TYPES.2020.7

Abstract

We present the web portal Λ-symsym, available at http://158.110.146.197:31780/automata/, for experimenting with game semantics of λ^!-calculus, and its normalizing elementary sub-calculus, the λ^{EAL}-calculus. The λ^!-calculus is a generalization of the λ-calculus obtained by introducing a modal operator !, giving rise to a pattern β-reduction. Its sub-calculus corresponds to an applicatively closed class of terms normalizing in an elementary number of steps, in which all elementary functions can be encoded. The game model which we consider is the Geometry of Interaction model I introduced by Abramsky to study reversible computations, consisting of partial involutions over a very simple language of moves. Given a λ^!- or a λ^{EAL}-term, M, Λ-symsym provides: - an abstraction algorithm A^!, for compiling M into a term, A^!(M), of the linear combinatory logic CL^{!}, or the normalizing combinatory logic CL^{EAL}; - an interpretation algorithm [[ ]]^I yielding a specification of the partial involution [[A^!(M)]]^I in the model I; - an algorithm, I2T, for synthesizing from [[A^!(M)]]^I a type, I2T([[A^!(M)]]^I), in a multimodal, intersection type assignment discipline, ⊢_!. - an algorithm, T2I, for synthesizing a specification of a partial involution from a type in ⊢_!, which is an inverse to the former. We conjecture that ⊢_! M : I2T([[A^!(M)]]^I). Λ-symsym permits to investigate experimentally the fine structure of I, and hence the game semantics of the λ^!- and λ^{EAL}-calculi. For instance, we can easily verify that the model I is a λ^!-algebra in the case of strictly linear λ-terms, by checking all the necessary equations, and find counterexamples in the general case. We make this tool available for readers interested to play with games (-semantics). The paper builds on earlier work by the authors, the type system being an improvement.

Subject Classification

ACM Subject Classification
  • Theory of computation → Linear logic
Keywords
  • game semantics
  • lambda calculus
  • involutions
  • linear logic
  • implicit computational complexity

Metrics

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

References

  1. Samson Abramsky. Domain theory in logical form. Annals of Pure and Applied Logic, 51(1):1-77, 1991. URL: https://doi.org/10.1016/0168-0072(91)90065-T.
  2. Samson Abramsky. Retracing some paths in process algebra. In Ugo Montanari and Vladimiro Sassone, editors, CONCUR '96: Concurrency Theory, pages 1-17, Berlin, Heidelberg, 1996. Springer Berlin Heidelberg. Google Scholar
  3. Samson Abramsky. A structural approach to reversible computation. Theoretical Computer Science, 347(3):441-464, 2005. URL: https://doi.org/10.1016/j.tcs.2005.07.002.
  4. Samson Abramsky, Esfandiar Haghverdi, and Philip Scott. Geometry of interaction and linear combinatory algebras. Mathematical Structures in Computer Science, 12(5):625-665, 2002. Google Scholar
  5. 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: https://doi.org/10.1016/j.apal.2004.08.003.
  6. Patrick Baillot, Erika De Benedetti, and Simona Ronchi Della Rocca. Characterizing Polynomial and Exponential Complexity Classes in Elementary Lambda-Calculus. In Josep Diaz, Ivan Lanese, and Davide Sangiorgi, editors, Theoretical Computer Science, pages 151-163, Berlin, Heidelberg, 2014. Springer Berlin Heidelberg. Google Scholar
  7. Patrick Baillot and Kazushige Terui. A Feasible Algorithm for Typing in Elementary Affine Logic. In Paweł Urzyczyn, editor, Typed Lambda Calculi and Applications, pages 55-70, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. Google Scholar
  8. Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. A Filter Lambda Model and the Completeness of Type Assignment. The Journal of Symbolic Logic, 48(4):931-940, 1983. URL: http://www.jstor.org/stable/2273659.
  9. Henk Barendregt, Wil Dekkers, and Richard Statman. Lambda calculus with types. Cambridge University Press, 2013. Google Scholar
  10. A. Ciaffaglione, P. Di Gianantonio, F. Honsell, M. Lenisa, and I. Scagnetto. Reversible Computation and Principal Types in λ!-calculus. The Bulletin of Symbolic Logic, 25(2):931-940, 2019. Google Scholar
  11. Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, Marina Lenisa, and Ivan Scagnetto. Λ!-calculus, Intersection Types, and Involutions. In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), volume 131 of Leibniz International Proceedings in Informatics (LIPIcs), pages 15:1-15:16, Dagstuhl, Germany, 2019. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2019.15.
  12. Alberto Ciaffaglione, Furio Honsell, Marina Lenisa, and Ivan Scagnetto. The involutions-as-principal types/application-as-unification Analogy. In LPAR, volume 57, pages 254-270, 2018. Google Scholar
  13. Alberto Ciaffaglione, Furio Honsell, Marina Lenisa, and Ivan Scagnetto. Web Appendix with Erlang code. http://www.dimi.uniud.it/scagnett/pubs/automata-erlang.pdf, 2020. Accessed: 2020-01-19.
  14. M. Coppo, M. Dezani-Ciancaglini, F. Honsell, and G. Longo. Extended type structures and filter lambda models. In G. Lolli, G. Longo, and A. Marcja, editors, Logic Colloquium '82, volume 112 of Studies in Logic and the Foundations of Mathematics, pages 241-262. Elsevier, 1984. URL: https://doi.org/10.1016/S0049-237X(08)71819-6.
  15. Paolo Coppola, Ugo Dal Lago, and Simona Ronchi Della Rocca. Light Logics and the Call-by-Value Lambda Calculus. Logical Methods in Computer Science, Volume 4, Issue 4, 2008. URL: https://doi.org/10.2168/LMCS-4(4:5)2008.
  16. Paolo Coppola and Simone Martini. Optimizing Optimal Reduction: A Type Inference Algorithm for Elementary Affine Logic. ACM Trans. Comput. Logic, 7(2):219–260, 2006. URL: https://doi.org/10.1145/1131313.1131315.
  17. Erlang Ecosystem Foundation. Erlang official website. http://www.erlang.org, 2020. Accessed: 2020-01-19.
  18. I. Scagnetto F. Honsell, M. Lenisa. Types-as-game strategies for Hilbert style Computational Complexity. (submitted), 2020. Google Scholar
  19. Jean-Yves Girard. Geometry of interaction III: accommodating the additives. London Mathematical Society Lecture Note Series, pages 329-389, 1995. Google Scholar
  20. Jean-Yves Girard. Light linear logic. Information and Computation, 143(2):175-204, 1998. Google Scholar
  21. Furio Honsell and Marina Lenisa. Semantical analysis of perpetual strategies in λ-calculus. Theoretical Computer Science, 212(1):183-209, 1999. URL: https://doi.org/10.1016/S0304-3975(98)00140-6.
  22. Furio Honsell, Marina Lenisa, Luigi Liquori, and Ivan Scagnetto. Implementing Cantor’s Paradise. In Atsushi Igarashi, editor, Programming Languages and Systems, pages 229-250, Cham, 2016. Springer International Publishing. Google Scholar
  23. André Joyal, Ross Street, and Dominic Verity. Traced monoidal categories. In Mathematical Proceedings of the Cambridge Philosophical Society, volume 119(3), pages 447-468. [Cambridge, Eng.] Cambridge Philosophical Society., 1996. Google Scholar
  24. Robin Milner. Is Computing an Experimental Science? Journal of Information Technology, 2(2):58-66, 1987. URL: https://doi.org/10.1177/026839628700200202.
  25. Dag Prawitz. Natural deduction: A proof-theoretical study. Courier Dover Publications, 2006. Google Scholar
  26. Kazushige Terui. Light logic and polynomial time computation. PhD thesis, PhD thesis, Keio University, 2002. Google Scholar
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