Lévy-Longo Trees and Böhm Trees are the best known tree structures on the λ-calculus. We give general conditions under which an encoding of the λ-calculus into the π-calculus is sound and complete with respect to such trees. We apply these conditions to various encodings of the call-by-name λ-calculus, showing how the two kinds of tree can be obtained by varying the behavioural equivalence adopted in the π-calculus and/or the encoding.
Sangiorgi, D., Xu, X. (2018). Trees from functions as processes. LOGICAL METHODS IN COMPUTER SCIENCE, 14(3), 1-41 [10.23638/LMCS-14(3:11)2018].
Trees from functions as processes
Sangiorgi, Davide;
2018
Abstract
Lévy-Longo Trees and Böhm Trees are the best known tree structures on the λ-calculus. We give general conditions under which an encoding of the λ-calculus into the π-calculus is sound and complete with respect to such trees. We apply these conditions to various encodings of the call-by-name λ-calculus, showing how the two kinds of tree can be obtained by varying the behavioural equivalence adopted in the π-calculus and/or the encoding.File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
1804.05797.pdf
accesso aperto
Tipo:
Versione (PDF) editoriale
Licenza:
Licenza per Accesso Aperto. Creative Commons Attribuzione (CCBY)
Dimensione
579.94 kB
Formato
Adobe PDF
|
579.94 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
