The lazy lambda calculus in a concurrency scenario (Q1327395): Difference between revisions

This interesting paper, which ends with several open problems, deals with the discrimination of pure \(\lambda\)-terms by means of operational considerations w.r.t. programming languages extending lazy \(\lambda\)- calculus and including possibly parallel or non-deterministic features. This is linked to the full abstraction problem, i.e. the complete adequation between the operational indiscernability of terms and the equality of their interpretations in a given mathematical model. Starting from lazy \(\lambda\)-calculus (left reduction which stops when reaching an abstraction) the full abstraction problem was solved, w.r.t. well-chosen ``canonical domains'', by \textit{S. Abramsky} and \textit{C.-H. L. Ong} [ibid. 105, No. 2, 159-267 (1993; Zbl 0779.03003)] adding a parallel convergence testing operator, and by \textit{G. Boudol} [ibid. 108, No. 1, 51-127 (1994; Zbl 0796.03021)] adding general computational methods, namely: call-by-value and parallel reduction mechanisms. The purpose of the author is to present solutions more close to common programming practice, and to make it clear whether the induced equivalences on pure terms are sensible to the addition of more operators. Two approaches are proposed, which both embed \(\lambda\)-calculus into richer settings, and, though apparently of a very different kind, turn out to be equivalent for discriminating pure terms. First, \(\lambda\)-calculus is studied within Milner's process \(\pi\)- calculus. Several simple characterizations of the congruence equ induced on pure terms by Milner's embedding are given, from which the full abstraction w.r.t. Levy-Longo trees is proved. Secondly, \(\lambda\)-calculus is augmented by any family of well-formed operators. It is shown that the discrimination between pure terms (in terms of Abramsky's applicative bisimulation) is maximal when all operators are used, coincides with equ, and is already induced by the mere presence of simple non-deterministic operators, for example the unary operator which, when applied to a term, outputs this term or the always divergent term \(\Omega\). This (kind of) non-determinism is actually necessary, in the precise sense that the same discriminating power cannot be recovered by adding only Church-Rosser operators, like the parallel convergence testing; in particular equ is more discriminating than the bisimulations considered by Abramsky and Boudol; in other words, their canonical models are not sound for equ.