Lambda-calculi for (strict) parallel functions (Q1314269): Difference between revisions

The main purpose of the paper is to solve the full abstraction problem between (versions of) lazy pure \(\lambda\)-calculus and two canonical domains of parallel (= continuous) functions. The lazy \(\lambda\)-calculus evaluates \(\lambda\)-terms to abstractions, by means of the call-by-name (i.e. left or head) strategy; it was shown by Abramsky and Ong that the initial solution of the domain equation \(D\simeq[D\to D]_ \perp\), which expresses that \(D\) is isomorphic to the lifted space of its continuous functions, is fully abstract for this calculus if some parallel convergence testing combinator is added to the language [\textit{S. Abramsky} and \textit{C.-H. L. Ong}, Inf. Comput. 105, No. 2, 159-267 (1993; Zbl 0779.03003)]. The point of view here is to add computational methods (call-by-value and parallel computation), rather than ad hoc combinators and rules. It is shown that Abramsky and Ong's domain is also fully abstract with respect to these new evaluation mechanisms, and that it is still true for the initial solution of \(D\simeq [D\to_{ \perp} D]_ \perp\), where \([D\to_{ \perp} D]\) refers to strict continuous functions, when call- by-name is disallowed. The proofs follow Abramsky and Ong's pattern, namely: dualize each domain into a type assignment system, define a realizability interpretation, and show that realizability, typeability, and standard interpretability are all equivalent; the full abstraction follows from both the fact that the models are nearly extensional and that all their finite elements are definable (using the join operator, which models parallelism). The paper is self-contained and section 1 is a very good introduction to the general problem of full abstraction in pure \(\lambda\)-calculus and to the links with Abramsky and Ong's paper. Very much related is a paper of \textit{L. Egidi}, \textit{F. Honsell} and \textit{S. Ronchi della Rocca} [Ann. Soc. Math. Pol., Ser. IV, Fundam. Inf. 16, No. 2, 149-169 (1992; Zbl 0762.68042)], where the second of the domains above is studied with respect to the Plotkin call-by-value calculus (where variables are allowed as values) and the SECD reduction strategy.