A Rational Deconstruction of Landin's J Operator

Landin's J operator was the first control operator for functional languages. It was specified with an extension of the SECD machine, which was the first abstract machine for functional languages. We present a family of compositional evaluation functions corresponding to this extension of the SECD machine, using a series of elementary transformations (transformation into continuation-passing style (CPS) and defunctionalization, chiefly) and their left inverses (transformation into direct style and refunctionalization). To this end, we modernize the SECD machine into a bisimilar one that operates in lock step with the original one but that (1) does not use a data stack and (2) uses the caller-save rather than the callee-save convention for environments. We then characterize the J operator in terms of CPS and in terms of delimited-control operators in the CPS hierarchy. As a byproduct, we also present a reduction semantics for applicative expressions with the J operator, based on Curien's original calculus of explicit substitutions. This reduction semantics mechanically corresponds to the modernized version of the SECD machine and to the best of our knowledge, it provides the first syntactic theory of applicative expressions with the J operator.<br /> <br />The present work is concluded by a motivated wish to see Landin's name added to the list of co-discoverers of continuations. Methodologically, however, it mainly illustrates the value of Reynolds's defunctionalization and of refunctionalization as well as the expressive power of the CPS hierarchy (a) to account for the first control operator and the first abstract machine for functional languages and (b) to connect them to their successors.

A Rational Deconstruction of Landin's J Operator

Landin's J operator was the first control operator for functional languages, and was specified with an extension of the SECD machine. Through a series of meaning-preserving transformations (transformation into continuation-passing style (CPS) and defunctionalization) and their left inverses (transformation into direct style and refunctionalization), we present a compositional evaluation function corresponding to this extension of the SECD machine. We then characterize the J operator in terms of CPS and in terms of delimited-control operators in the CPS hierarchy. Finally, we present a motivated wish to see Landin's name added to the list of co-discoverers of continuations.

A Rational Deconstruction of Landin's SECD Machine

Landin's SECD machine was the first abstract machine for the lambda-calculus viewed as a programming language. Both theoretically as a model of computation and practically as an idealized implementation, it has set the tone for the subsequent development of abstract machines for functional programming languages. However, and even though variants of the SECD machine have been presented, derived, and invented, the precise rationale for its architecture and modus operandi has remained elusive. In this article, we deconstruct the SECD machine into a lambda-interpreter, i.e., an evaluation function, and we reconstruct lambda-interpreters into a variety of SECD-like machines. The deconstruction and reconstructions are transformational: they are based on equational reasoning and on a combination of simple program transformations--mainly closure conversion, transformation into continuation-passing style, and defunctionalization.<br /> <br />The evaluation function underlying the SECD machine provides a precise rationale for its architecture: it is an environment-based eval-apply evaluator with a callee-save strategy for the environment, a data stack of intermediate results, and a control delimiter. Each of the components of the SECD machine (stack, environment, control, and dump) is therefore rationalized and so are its transitions.<br /> <br />The deconstruction and reconstruction method also applies to other abstract machines and other evaluation functions. It makes it possible to systematically extract the denotational content of an abstract machine in the form of a compositional evaluation function, and the (small-step) operational content of an evaluation function in the form of an abstract machine.

A Functional Correspondence between Evaluators and Abstract Machines

We bridge the gap between functional evaluators and abstract machines for the lambda-calculus, using closure conversion, transformation into continuation-passing style, and defunctionalization of continuations.<br /> <br />We illustrate this bridge by deriving Krivine's abstract machine from an ordinary call-by-name evaluator and by deriving an ordinary call-by-value evaluator from Felleisen et al.'s CEK machine. The first derivation is strikingly simpler than what can be found in the literature. The second one is new. Together, they show that Krivine's abstract machine and the CEK machine correspond to the call-by-name and call-by-value facets of an ordinary evaluator for the lambda-calculus.<br /> <br /> We then reveal the denotational content of Hannan and Miller's CLS machine and of Landin's SECD machine. We formally compare the corresponding evaluators and we illustrate some relative degrees of freedom in the design spaces of evaluators and of abstract machines for the lambda-calculus with computational effects.<br /> <br />For the purpose of this work, we distinguish between virtual machines, which have an instruction set, and abstract machines, which do not. The Categorical Abstract Machine, for example, has an instruction set, but Krivine's machine, the CEK machine, the CLS machine, and the SECD machine do not; they directly operate on lambda-terms instead. We present the abstract machine that corresponds to the Categorical Abstract Machine.

From Interpreter to Compiler and Virtual Machine: A Functional Derivation

We show how to derive a compiler and a virtual machine from a compositional interpreter. We first illustrate the derivation with two evaluation functions and two normalization functions. We obtain Krivine's machine, Felleisen et al.'s CEK machine, and a generalization of these machines performing strong normalization, which is new. We observe that several existing compilers and virtual machines--e.g., the Categorical Abstract Machine (CAM), Schmidt's VEC machine, and Leroy's Zinc abstract machine--are already in derived form and we present the corresponding interpreter for the CAM and the VEC machine. We also consider Hannan and Miller's CLS machine and Landin's SECD machine.<br /> <br />We derived Krivine's machine via a call-by-name CPS transformation and the CEK machine via a call-by-value CPS transformation. These two derivations hold both for an evaluation function and for a normalization function. They provide a non-trivial illustration of Reynolds's warning about the evaluation order of a meta-language.

A Lambda-Revelation of the SECD Machine

We present a simple inter-derivation between lambda-interpreters, i.e., evaluation functions for lambda-terms, and abstract reduction machines for the lambda-calculus, i.e., transition functions. The two key derivation steps are the CPS transformation and Reynolds's defunctionalization. By transforming the interpreter into continuation-passing style (CPS), its flow of control is made manifest as a continuation. By defunctionalizing this continuation, the flow of control is materialized as a first-order data structure.<br /> <br />The derivation applies not merely to connect independently known lambda-interpreters and abstract machines, it also applies to construct the abstract machine corresponding to a lambda-interpreter and to construct the lambda-interpreter corresponding to an abstract machine. In this article, we treat in detail the canonical example of Landin's SECD machine and we reveal its denotational content: the meaning of an expression is a partial endo-function from a stack of intermediate results and an environment to a new stack of intermediate results and an environment. The corresponding lambda-interpreter is unconventional because (1) it uses a control delimiter to evaluate the body of each lambda-abstraction and (2) it assumes the environment to be managed in a callee-save fashion instead of in the usual caller-save fashion.