Skip to Main content Skip to Navigation

Lazy functions and mobile processes

Davide Sangiorgi 1
1 MEIJE - Concurrency, Synchronization and Real-time Programming
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : This paper continues the study of Milner's encoding of the lazy $\lambda$-calculus into the $\pi$-calculus \cite{Mil92}. The encoding is shown to give rise to a $\lambda$-model in which, in accordance with the theory of the lazy $\lambda$-calculus, conditional extensionality holds. However, the model is not fully abstract. To obtain full abstraction, the operational equivalence on $\lambda$-terms ({\em applicative bisimulation}) is refined. The new relation, called {\em open applicative bisimulation}, allows us to observe some internal structure of $\lambda$-terms, and coincides with the {\em Lévy-Longo Tree} equality. Milner's encoding is presented on a sublanguage of the $\pi$-calculus similar to those proposed by Boudol \cite{Bou92}, Honda and Tokoro \cite{HoTo91}. Some properties of bisimulation on this sublanguage are demonstrated and used to simplify a few proofs in the paper. For instance, {\em ground bisimulation}, a form of bisimulation where no name instantiation on input actions is required, is proved to be a congruence relation; as a corollary, various $\pi$-calculus bisimilarity equivalences (ground, late, early, open) are shown to coincide on this sublanguage.
Document type :
Complete list of metadata
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 2:39:04 PM
Last modification on : Saturday, January 27, 2018 - 1:31:01 AM
Long-term archiving on: : Sunday, April 4, 2010 - 9:28:20 PM


  • HAL Id : inria-00074163, version 1



Davide Sangiorgi. Lazy functions and mobile processes. RR-2515, INRIA. 1995. ⟨inria-00074163⟩



Record views


Files downloads