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.
Trees from functions as processes / Sangiorgi, Davide; Xu, Xian. - In: LOGICAL METHODS IN COMPUTER SCIENCE. - ISSN 1860-5974. - ELETTRONICO. - 14:3(2018), pp. 11.1-11.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 | 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.
