Publication Data
A rational deconstruction of Landin's SECD machine with the J operator
Abstract: Landin's SECD machine was the first abstract machine for
applicative expressions, ie, functional programs. Landin's J operator was the first
control operator for functional languages, and was specified by an extension of the
SECD machine. We present a family of evaluation functions corresponding to this
extension of the SECD machine, using a series of elementary transformations
(transformation into continu-ation-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 lockstep 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 also identify that the dump component of the SECD machine is managed in a
callee-save way. The caller-save counterpart of the modernized SECD machine precisely
corresponds to Thielecke's double-barrelled continuations and to Felleisen's encoding
of J in terms of call/cc. We then variously 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 several reduction semantics for applicative expressions with the J
operator, based on Curien's original calculus of explicit substitutions. These
reduction semantics mechanically correspond to the modernized versions of the SECD
machine and to the best of our knowledge, they provide the first syntactic theories of
applicative expressions with the J operator. 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 (1) to account for the first control operator and the first abstract
machine for functional languages and (2) to connect them to their successors. Our work
also illustrates the value of Danvy and Nielsen's refocusing technique to connect
environment-based abstract machines and syntactic theories in the form of reduction
semantics for calculi of explicit substitutions.
