The lazy lambda calculus in a concurrency scenario

The use of lambda calculus in richer settings, possibly involving parallelism, is examined in terms of its effect on the equivalence between lambda terms, focusing on S. Abramsky´s (Ph.D thesis, Univ. of London, 1987) lazy lambda calculus. First, the lambda calculus is studied within a process calculus by examining the equivalence induced by R. Milner´s (1992) encoding into the π-calculus. Exact operational and denotational characterizations for this equivalence are given. Second, Abramsky´s applicative bisimulation is examined when the lambda calculus is augmented with (well-formed) operators, i.e. symbols equipped with reduction rules describing their behavior. Then, maximal discrimination is obtained when all operators are considered; it is shown that this discrimination coincides with the one given by the above equivalence and that the adoption of certain nondeterministic operators is sufficient and necessary to induce it