DISTRIBUTIVE EVALUATIONS OF λ-CALCULUS

Abstract

In this paper we address the problem of encoding evaluation strategies for the λ-calculus into prime event structures. In order for this to be possible the derivation spaces yielded by the evaluation mechanism must be prime algebraic cpo's. This requirement is not met by permutation equivalence (the standard concurrent semantics with which λ-calculus is equipped) since the derivation spaces it yields are upper semi-lattices. We solve this problem by taking the coarsest congruence contained in permutation equivalence such that permutations of disjoint reductions are equated and the downward closure of every derivation is a distributive lattice. This equivalence, called distributive permutation equivalence, is characterized directly by restricting permutations of redexes to those sets U which are distributive, i.e. for every u ∈ U, the development of every V ⊆ (U\{u}) does not duplicate or delete u. A simple consequence of our results is that the derivation spaces of the call-by-value λ-calculus are distributive lattices. Finally, we show that a sequential evaluation mechanism can not, in general, be effectively transformed into a maximally distributive one.