On the representation of McCarthy's in the -calculus |
| |
Authors: | Arnaud Carayol Daniel Hirschkoff Davide Sangiorgi |
| |
Affiliation: | aIRISA, Campus de Beaulieu, 35042 Rennes, France;bLIP, ENS Lyon, 46 allée d’Italie, 69364 Lyon Cedex 7, France;cDipartimento di Scienze dell’Informazione, Universita di Bologna, Via di Mura Anteo Zamboni 7, 40127 Bologna, Italy |
| |
Abstract: | We study the encoding of , the call-by-name λ-calculus enriched with McCarthy's amb operator, into the π-calculus. Semantically, amb is a challenging operator, for the fairness constraints that it expresses. We prove that, under a certain interpretation of divergence in the λ-calculus (weak divergence), a faithful encoding is impossible. However, with a different interpretation of divergence (strong divergence), the encoding is possible, and for this case we derive results and coinductive proof methods to reason about that are similar to those for the encoding of pure λ-calculi. We then use these methods to derive the most important laws concerning amb. We take bisimilarity as behavioural equivalence on the π-calculus, which sheds some light on the relationship between fairness and bisimilarity. |
| |
Keywords: | Fairness Lambda-calculus π -calculus Behavioural equivalence |
本文献已被 ScienceDirect 等数据库收录! |
|