The rules of classical logic may be formulated in pairs corresponding to De Morgan duals: rules about "and" are dual to rules about "or". A line of work, including that of Filinski (1989), Griffin (1990), Parigot (1992), Danos, Joinet, and Schellinx (1995), Selinger (1998,2001), and Curien and Herbelin (2000), has led to the startling conclusion that call-by-value is the de Morgan dual of call-by-name.
This paper presents a dual calculus that corresponds to the classical sequent calculus of Gentzen (1935) in the same way that the lambda calculus of Church (1932,1940) corresponds to the intuitionistic natural deduction of Gentzen (1935). The paper includes crisp formulations of call-by-value and call-by-name that are obviously dual; no similar formulations appear in the literature. The paper gives a CPS translation and its inverse, and shows that the translation is both sound and complete, strengthening a result in Curien and Herbelin (2000).
We present a calculus that captures the operational semantics of call-by-need. The call-by-need lambda calculus is confluent, has a notion of standard reduction, and entails the same observational equivalence relation as the call-by-name calculus. The system can be formulated with or without explicit let bindings, admits useful notions of marking and developments, and has a straightforward operational interpretation.
One way to model a sound and complete translation from a source into a target calculus is with an adjoint or a Galois connection. In the special case of a reflection, one also has that the target calculus is isomorphic to a subset of the source. We show that three widely-studied translations form reflections. We use as our source language Moggi's computational lambda calculus lambda-c, which is an extension of Plotkin's call-by-value calculus lambda-v. We show that Plotkin's CPS translation, Moggi's monad translation, and Girard's translation to linear logic can all be regarded as reflections from this source language, and we put forward lambda-c as a model of call-by-value computation that improves on lambda-v. Our work strengthens Plotkin's and Moggi's original results, and improves on recent work based on equational correspondence, which uses equations rather than reductions.
Lazy, or call-by-need, languages schedule work dynamically by building closures, and shun side effects; strict, or call-by-value languages avoid the overhead of closures and may exploit side effects. Each style has complementary advantages and complimentary adherents.
The gap between the lazy and strict camps has two dimensions, which we shall name style and models. Recent developments suggest that along both dimensions the gap is shrinking. We list some commercial applications of each kind of language, and examine each dimension of difference in turn.
A number of compilers exploit the following strategy: translate a term to continuation-passing style (CPS) and optimise the resulting term. Recent work suggests that an alternative strategy is superior: optimise directly in an extended source calculus. We suggest that the appropriate relation between the source and target calculus may be captured by a special case of a Galois connection known as a reflection. Previous work has focussed on the weaker notion of an equational correspondence, which is based on equality rather than reduction. We show that Moggi's monad translation and that Plotkin's CPS translation can both be regarded as reflections, and thereby strengthen a number of results in the literature.
The mismatch between the operational semantics of the lambda calculus and the actual behavior of implementations is a major obstacle for compiler writers. They cannot explain the behavior of their evaluator in terms of source level syntax, and they cannot easily compare distinct implementations of different lazy strategies. In this paper we derive an equational characterization of call-by-need and prove it correct with respect to the original lambda calculus. The theory is a strictly smaller theory than the lambda calculus. Immediate applications of the theory concern the correctness proofs of a number of implementation strategies, e.g., the call-by-need continuation passing transformation and the realization of sharing via assignments.
Philip Wadler,
