On the representation of mccarthy’s amb in the pi-calculus

We study the encoding of λ[], the call by name λ-calculus enriched with McCarthy’s amb operator, into the pi-calculus. Semantically, amb is a challenging operator, for the fairness constraints that it expresses. We prove that, under a certain in-terpretation of divergence in the λ-calculus (weak divergence), a faithful encoding is impossible. However, with a different interpretation of divergence (strong diver-gence), 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 pi-calculus, which sheds some light on the relationship between fairness and bisimilarity. As a spin-off result, we show that there is no small-step operational semantics for λ[] that preserves the branching structure of terms and yields the correct predicates of convergence and (weak) divergence.