License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2020.7
URN: urn:nbn:de:0030-drops-138867
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/13886/
Honsell, Furio ;
Lenisa, Marina ;
Scagnetto, Ivan
Λ-Symsym: An Interactive Tool for Playing with Involutions and Types
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.
BibTeX - Entry
@InProceedings{honsell_et_al:LIPIcs.TYPES.2020.7,
author = {Honsell, Furio and Lenisa, Marina and Scagnetto, Ivan},
title = {{\Lambda-Symsym: An Interactive Tool for Playing with Involutions and Types}},
booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)},
pages = {7:1--7:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-182-5},
ISSN = {1868-8969},
year = {2021},
volume = {188},
editor = {de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/13886},
URN = {urn:nbn:de:0030-drops-138867},
doi = {10.4230/LIPIcs.TYPES.2020.7},
annote = {Keywords: game semantics, lambda calculus, involutions, linear logic, implicit computational complexity}
}
|
Keywords: |
|
game semantics, lambda calculus, involutions, linear logic, implicit computational complexity |
|
Collection: |
|
26th International Conference on Types for Proofs and Programs (TYPES 2020) |
|
Issue Date: |
|
2021 |
|
Date of publication: |
|
07.06.2021 |
|
Supplementary Material: |
|
Software (Tool): http://158.110.146.197:31780/automata/ |
