Trees from Functions as Processes
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. The conditions are presented in the π-calculus but can be adapted to other concurrency formalisms.
KeywordsVariable Context Process Context Behavioural Equivalence Expansion Relation Initial Abstraction
Unable to display preview. Download preview PDF.
- 2.Barendregt, H.P.: The Lambda Calculus: Syntax, semantics. North-Holland (1984)Google Scholar
- 6.Dezani-Ciancaglini, M., Giovannetti, E.: From Bohm’s theorem to observational equivalences: an informal account. ENTCS 50(2), 83–116 (2001)Google Scholar
- 9.Milner, R.: Communicating and Mobile Systems: The π-Calculus. CUP (1999)Google Scholar
- 11.Sangiorgi, D.: Lazy functions and mobile processes. In: Proof, Language and Interaction: Essays in Honour of Robin Milner, pp. 691–720. MIT Press (2000)Google Scholar
- 12.Sangiorgi, D., Walker, D.: The π-calculus: a Theory of Mobile Processes. CUP (2001)Google Scholar