The lazy lambda calculus in a concurrency scenario

The use of lambda calculus in richer settings, pos-sibly involving parallelism, is examined in terms of its effect on the equivalence between lambda terms. We concentrate here on Abramsky ’s lazy lambda calculus and we follow two directions. First, the lambda calcu-lus is studied within a process calculus b y examining the equivalence E induced b y Milner’s encoding into the a-calculus. We give exact operational and denota-tional characterizations for G. Secondly, we examine Abramsky’s applicative bisi/nulation when the lambda calculus is augmented with (well-formed) operators, i.e. symbols equipped with reduction rules describing their behaviour. Then, maximal discrimination is ob-tained when all operators are considered; we show that this discrimination coincides with the one given b y Z+ and that the adoption of certain non-deterministic op-erators is sufficient and necessary to induce it.