Full Abstraction in the Lazy Lambda Calculus

AbstractA theory of lazy λ-calculus is developed as a basis for lazy functional programming languages. This is motivated by a mismatch between the "standard" (i.e., sensible) theory of the classical λ-calculus and the practice of lazy functional programming. Part I sets up the fundamentals of the lazy λ-calculus starting from the pure lazy language λl. We develop the rudiments of weakly sensible λ-theory and characterize λl as the maximal such theory. The axiomatic framework of our theory is based on the notion of applicative transition systems which gives rise to lazy λ-models. The subclass of lazy λ-models which are operationally extensional are called lambda transition systems (lts′s). The canonical model of the lazy λ-calculus is the initial solution to the domain equation D ≅ [D → D]⊥. We set up the domain logic corresponding to the same type expression. In part II, we recast the full abstraction problem in the lazy λ-calculus. The pure lazy language λl is not equationally fully abstract w.r.t. D. In fact, λl, λlω, (a labelled version of λl), and λlc (λl augmented with a convergence testing constant) are all not equationally fully abstract w.r.t. D. We illustrate two approaches to full abstraction: •The expansive approach consists in enriching the language by augmenting it with appropriate constants, thereby enabling all finite semantic information to be represented syntactically as program phrases using the machinery of domain logic developed in Part I. We show that λ, which is λ augmented with a parallel convergence testing constant, is conditionally fully abstract .•The restrictive approach regards the language as prescribed and tailors the model to fit by "cutting down" (i.e., "quotienting out" by a bisimulation logical relation) the existing "over-generous" canonical model to an appropriate substructure. We establish a general method to construct inequationally fully abstract lazy λ-models which are retracts of for a class of sufficiently expressive lts′s in which the -projection maps are internally definable. The restrictive approach solves the abstraction problem for λlc and λlω but not λl. The full abstraction problem for λl is reduced to a conjecture of the conservativity of λlω over λl. Finally, we study lazy languages with ground data and show that it is wrong to conflate parallel or with parallel convergence testing