A Rational Deconstruction of Landin's SECD Machine with the J Operator

Just as specializing a source interpreter can achieve compilation from a source language to a target language, we observe that specializing a target interpreter can achieve compilation from the target language to the source language. In both cases, the key issue is the choice of whether to perform an evaluation or to emit code that represents this evaluation. We substantiate this observation by specializing two source interpreters and two target interpreters. We first consider a source language of arithmetic expressions and a target language for a stack machine, and then the lambda-calculus and the SECD-machine language. In each case, we prove that the target-to-source compiler is a left inverse of the source-to-target compiler, i.e., it is a decompiler. In the context of partial evaluation, compilation by source-interpreter specialization is classically referred to as a Futamura projection. By symmetry, it seems logical to refer to decompilation by target-interpreter specialization as a Futamura embedding.

Download Full-text

A Rational Deconstruction of Landin’s SECD Machine

Implementation and Application of Functional Languages - Lecture Notes in Computer Science ◽

10.1007/11431664_4 ◽

2005 ◽

pp. 52-71 ◽

Cited By ~ 9

Author(s):

Olivier Danvy

Keyword(s):

Secd Machine

Download Full-text

Executing an SECD machine using logic programming

ACM SIGCSE Bulletin ◽

10.1145/199691.199793 ◽

1995 ◽

Vol 27 (1) ◽

pp. 228-232

Author(s):

Ken Slonneger

Keyword(s):

Logic Programming ◽

Secd Machine

Download Full-text

Operational, Denotational and Logical Descriptions: A Case Study1

Fundamenta Informaticae ◽

10.3233/fi-1992-16205 ◽

1992 ◽

Vol 16 (2) ◽

pp. 149-169

Author(s):

Lavinia Egidi ◽

Furio Honsell ◽

Simona Ronchi Della Rocca

Keyword(s):

Programming Languages ◽

Denotational Semantics ◽

Logical Description ◽

Secd Machine ◽

Type Assignment ◽

Completeness Result ◽

Natural Notion

The functional fragment of Landin’s ISWIM as implemented by the SECD machine is the paradigm of the procedural kernel of many programming languages. We investigate and compare operational, denotational and logical descriptions of the ISWIM-SECD system. Our goal is to illustrate how to derive from each of these descriptions logical tools for resoning about termination and equivalence of programs. First we show the correctness and incompleteness of the canonical denotational semantics. Then we give a fully abstract quotient semantics using a notion of applicative bisimulation. We discuss next a finitary logical description of the denotational semantics. This takes the form of a call-by-value intersection type assignment system. Finally we study this type assignment system for its own sake and give a completeness result for it with respect to a natural notion of interpretation.

Download Full-text

A Rational Deconstruction of Landin's J Operator

BRICS Report Series ◽

10.7146/brics.v13i17.21922 ◽

2006 ◽

Vol 13 (17) ◽

Cited By ~ 2

Author(s):

Olivier Danvy ◽

Kevin Millikin

Keyword(s):

Expressive Power ◽

Functional Languages ◽

Abstract Machine ◽

Control Operator ◽

Syntactic Theory ◽

Secd Machine ◽

Evaluation Functions ◽

Explicit Substitutions ◽

Control Operators

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. 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.

Download Full-text

A Rational Deconstruction of Landin's J Operator

BRICS Report Series ◽

10.7146/brics.v13i4.21910 ◽

2006 ◽

Vol 13 (4) ◽

Cited By ~ 1

Author(s):

Olivier Danvy ◽

Kevin Millikin

Keyword(s):

Functional Languages ◽

Evaluation Function ◽

Control Operator ◽

Secd Machine ◽

Control Operators

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.

Download Full-text

A Functional Correspondence between Evaluators and Abstract Machines

BRICS Report Series ◽

10.7146/brics.v10i13.21783 ◽

2003 ◽

Vol 10 (13) ◽

Cited By ~ 4

Author(s):

Mads Sig Ager ◽

Dariusz Biernacki ◽

Olivier Danvy ◽

Jan Midtgaard

Keyword(s):

Degrees Of Freedom ◽

Virtual Machines ◽

Lambda Calculus ◽

Instruction Set ◽

Abstract Machine ◽

Secd Machine ◽

Abstract Machines ◽

Closure Conversion

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. 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. 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. 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.

Download Full-text

A Rational Deconstruction of Landin's SECD Machine

BRICS Report Series ◽

10.7146/brics.v10i33.21801 ◽

2003 ◽

Vol 10 (33) ◽

Cited By ~ 7

Author(s):

Olivier Danvy

Keyword(s):

Programming Languages ◽

Subsequent Development ◽

Reconstruction Method ◽

Evaluation Function ◽

Program Transformations ◽

Abstract Machine ◽

Functional Programming Languages ◽

Secd Machine ◽

Abstract Machines ◽

Environment Control

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. 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. 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.

Download Full-text