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.
Type de document :
RR-2515, INRIA. 1995
Liste complète des métadonnées
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 14:39:04
Dernière modification le : jeudi 11 janvier 2018 - 16:29:50
Document(s) archivé(s) le : dimanche 4 avril 2010 - 21:28:20



  • HAL Id : inria-00074163, version 1



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



Consultations de la notice


Téléchargements de fichiers