The Lazy Lambda Calculus in a Concurrency Scenario

AbstractThe use of λ-calculus in richer settings, possibly involving parallelism, is examined in terms of the effect on the equivalence between λ-terms. We concentrate on Abramsky′s lazy λ-calculus and we follow two directions. Firstly, the λ-calculus is studied within a process calculus by examining the equivalence [formula] induced by Milner′s encoding into the π-calculus. We start from a characterization of [formula] presented in (Sangiorgi D., 1992) Ph.D. thesis. We derive a few simpler operational characterisations, from which we prove full abstraction w.r.t. Levy-Longo Trees. Secondly, we examine Abramsky′s applicative bisimulation when the λ-calculus is augmented with (well-formed) operators, that is symbols equipped with reduction rules describing their behaviour. In this way, the maximal discrimination between pure λ-terms (i.e., the finest behavioural equivalence) is obtained when all operators are used. We prove that the presence of certain non-deterministic operators is sufficient and necessary to induce it and that it coincides with the discrimination given by [formula]. We conclude that the introduction of non-determinism into the λ-calculus is exactly what makes applicative bisimulation appropriate for reasoning about the functional terms when concurrent features are also present in the language, or when they are embedded into a concurrent language