Full abstraction in the lazy lambda calculus (Q1261291): Difference between revisions

Lazy call-by-name \(\lambda\)-calculus, which is called \(\lambda l\) in the paper, is the head-reduction strategy on pure closed \(\lambda\)-terms, with the proviso that all reductions terminate upon reaching abstractions. It is the basis of many functional languages and the present paper is devoted to its study, in particular to questions of full-abstraction (fully abstract models of a reduction strategy are denotational models where two \(\lambda\)-terms have the same interpretation iff they have the same operational behaviour). A theory of lazy \(\lambda\)-models is developed under a number of more or less equivalent facets, which correspond, roughly speaking, to the usual formalisms for \(\lambda\)-models enriched with a well behaved convergence predicate (where terms whose \(\lambda l\)-reduction terminates have to be interpreted). The canonical model of lazy \(\lambda\)-calculus is 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. \(D\) is presented and studied by means of the usual limit construction. Then the ``domain logic'' associated to \(D\) is introduced; this corresponds to the view of \(D\) as a ``filter model'', or as one of the particularly clear cases of the general ``Stone duality'' theory developed by the first author in previous work. Now \(D\) is also a model for \(\lambda l_ c\), \(\lambda l_ p\) and \(\lambda l_ \omega\), which are extensions of \(\lambda l\) obtained by adding respectively the constants: \(c\) (convergence testing), \(p\) (parallel convergence testing), or \(\pi_ n/n\in\omega\) (projections), with the usual reduction rules that make \(p\) work as an (untyped) ``parallel or'' and make the \(\pi_ n\) be the syntactic counterpart of the projections of \(D\) on its finite retracts (so that \(\lambda l_ \omega\) is a labelled version of \(\lambda l\)). The main results of the paper are that: 1) \(D\) is fully abstract for \(\lambda l_ p\) but not for \(\lambda l_ c\) and \(\lambda l_ \omega\), 2) one can construct retracts of \(D\) which are fully abstract wrt \(\lambda l_ c\) or \(\lambda l_ \omega\), 3) the full abstraction problem for \(\lambda l\) reduces to a conservativity result of \(\lambda l_ \omega\) over \(\lambda l\). The first set of results and proofs is in natural filiation to those in \textit{G. D. Plotkin's} ``LCF considered as a programming language'' [Theor. Comput. Sci. 5, 223-255 (1977; Zbl 0369.68006)], which, however, concern the typed language PCF, and of Wadsworth's work relating termination of the (complete) head reduction strategy on pure \(\lambda\)-terms and their denotation in Scott's model \(D_ \infty\), which is a minimal solution of \(D\simeq [D\to D]\). The paper is self-contained, proofs are complete and detailed, and one finds here some nice expository parts at a general level; but the length of the paper is mainly due to the fact that the authors enjoy presenting all abstract notions in a number of equivalent formalisms and variations, and use them in an interactive way; this does not help the reader to have a clear insight of what really happens at the essential (mathematical) level. However, if (s)he wishes to become familiar with all aspects of denotational semantics, (s)he will appreciate to have at hand this fully complete presentation (of the lazy versions). The semantic study of the lazy call-by-value \(\lambda\)-calculus, for which the canonical model is the initial solution of \(D\simeq [D\to_ \perp D]_ \perp\) (where only strict continuous functions are considered) is done by \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)], and also by G. Boudol and R. Pino- Perez in papers which are quoted there.