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. The conditions are presented in the π-calculus but can be adapted to other concurrency formalisms.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Arun-Kumar, S., Hennessy, M.: An efficiency preorder for processes. Acta Informatica 29, 737–760 (1992)
Barendregt, H.P.: The Lambda Calculus: Syntax, semantics. North-Holland (1984)
Berger, M., Honda, K., Yoshida, N.: Sequentiality and the π-calculus. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol. 2044, pp. 29–45. Springer, Heidelberg (2001)
Berger, M., Honda, K., Yoshida, N.: Genericity and the pi-calculus. Acta Informatica 42(2-3), 83–141 (2005)
Demangeon, R., Honda, K.: Full abstraction in a subtyped pi-calculus with linear types. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 280–296. Springer, Heidelberg (2011)
Dezani-Ciancaglini, M., Giovannetti, E.: From Bohm’s theorem to observational equivalences: an informal account. ENTCS 50(2), 83–116 (2001)
Hirschkoff, D., Madiot, J.M., Sangiorgi, D.: Duality and i/o-types in the π-calculus. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 302–316. Springer, Heidelberg (2012)
Milner, R.: Functions as processes. Mathematical Structures in Computer Science 2(2), 119–141 (1992)
Milner, R.: Communicating and Mobile Systems: The π-Calculus. CUP (1999)
Plotkin, G.D.: T ω as a universal domain. Journal of Computer and System Sciences 17, 209–236 (1978)
Sangiorgi, D.: Lazy functions and mobile processes. In: Proof, Language and Interaction: Essays in Honour of Robin Milner, pp. 691–720. MIT Press (2000)
Sangiorgi, D., Walker, D.: The π-calculus: a Theory of Mobile Processes. CUP (2001)
Scott, D.: Data types as lattices. SIAM Journal on Computing 5(3), 522–587 (1976)
Yoshida, N., Honda, K., Berger, M.: Linearity and bisimulation. Journal of Logic and Algebraic Programming 72(2), 207–238 (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sangiorgi, D., Xu, X. (2014). Trees from Functions as Processes. In: Baldan, P., Gorla, D. (eds) CONCUR 2014 – Concurrency Theory. CONCUR 2014. Lecture Notes in Computer Science, vol 8704. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-44584-6_7
Download citation
DOI: https://doi.org/10.1007/978-3-662-44584-6_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-44583-9
Online ISBN: 978-3-662-44584-6
eBook Packages: Computer ScienceComputer Science (R0)