Lazy functions and mobile processes

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.