scholarly journals A Rational Deconstruction of Landin's J Operator

2006 ◽  
Vol 13 (17) ◽  
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.<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.

scholarly journals A Rational Deconstruction of Landin's J Operator

2006 ◽  
Vol 13 (4) ◽  
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.

scholarly journals Delimited control and computational effects

2014 ◽  
Vol 24 (1) ◽  
pp. 1-55 ◽  
Author(s):  
PAUL DOWNEN ◽  
ZENA M. ARIOLA
Keyword(s):  
Operational Semantics ◽  
Expressive Power ◽  
Reduction Theory ◽  
Level Control ◽  
Abstract Machine ◽  
Fine Grained ◽  
Control Operators

AbstractWe give a framework for delimited control with multiple prompts, in the style of Parigot's λμ-calculus, through a series of incremental extensions by starting with the pure λ-calculus. Each language inherits the semantics and reduction theory of its parent, giving a systematic way to describe each level of control. For each language of interest, we fully characterize its semantics in terms of a reduction semantics, operational semantics, continuation-passing style transform, and abstract machine. Furthermore, the control operations are expressed in terms of fine-grained primitives that can be used to build well-known, higher-level control operators. In order to illustrate the expressive power provided by various languages, we show how other computational effects can be encoded in terms of these control operators.

scholarly journals Classical logic, continuation semantics and abstract machines

1998 ◽  
Vol 8 (6) ◽  
pp. 543-572 ◽  
Author(s):  
Th. STREICHER ◽  
B. REUS
Keyword(s):  
Classical Logic ◽  
Denotational Semantics ◽  
Functional Languages ◽  
Abstract Machine ◽  
Control Operator ◽  
Abstract Machines ◽  
Elegant Method ◽  
Transition Rules ◽  
Operational Issues

One of the goals of this paper is to demonstrate that denotational semantics is useful for operational issues like implementation of functional languages by abstract machines. This is exemplified in a tutorial way by studying the case of extensional untyped call-by-name λ-calculus with Felleisen's control operator [Cscr ]. We derive the transition rules for an abstract machine from a continuation semantics which appears as a generalization of the ¬¬-translation known from logic. The resulting abstract machine appears as an extension of Krivine's machine implementing head reduction. Though the result, namely Krivine's machine, is well known our method of deriving it from continuation semantics is new and applicable to other languages (as e.g. call-by-value variants). Further new results are that Scott's D∞-models are all instances of continuation models. Moreover, we extend our continuation semantics to Parigot's λμ-calculus from which we derive an extension of Krivine's machine for λμ-calculus. The relation between continuation semantics and the abstract machines is made precise by proving computational adequacy results employing an elegant method introduced by Pitts.

scholarly journals An Operational Foundation for Delimited Continuations

2003 ◽  
Vol 10 (41) ◽  
Author(s):  
Malgorzata Biernacka ◽  
Dariusz Biernacki ◽  
Olivier Danvy
Keyword(s):  
Abstract Machine ◽  
Syntactic Theory ◽  
The Family ◽  
Delimited Continuations ◽  
Control Operators

We derive an abstract machine that corresponds to a definitional interpreter for the control operators shift and reset. Based on this abstract machine, we construct a syntactic theory of delimited continuations.<br /> <br />Both the derivation and the construction scale to the family of control operators shift_n and reset_n. The definitional interpreter for shift_n and reset_n has n + 1 layers of continuations, the corresponding abstract machine has n + 1 layers of control stacks, and the corresponding syntactic theory has n + 1 layers of evaluation contexts.<br /><br />See also BRICS-RS-05-24.

scholarly journals From Interpreter to Compiler and Virtual Machine: A Functional Derivation

2003 ◽  
Vol 10 (14) ◽  
Author(s):  
Mads Sig Ager ◽  
Dariusz Biernacki ◽  
Olivier Danvy ◽  
Jan Midtgaard
Keyword(s):  
Virtual Machine ◽  
Virtual Machines ◽  
Evaluation Function ◽  
Abstract Machine ◽  
Strong Normalization ◽  
Secd Machine ◽  
Evaluation Functions ◽  
Evaluation Order ◽  
Normalization Function

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.

scholarly journals A Lambda-Revelation of the SECD Machine

2002 ◽  
Vol 9 (53) ◽  
Author(s):  
Olivier Danvy
Keyword(s):  
Data Structure ◽  
Lambda Calculus ◽  
The Body ◽  
Abstract Machine ◽  
First Order ◽  
Secd Machine ◽  
Evaluation Functions ◽  
Transition Functions ◽  
Abstract Machines ◽  
Intermediate Results

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.

scholarly journals From Interpreter to Logic Engine by Defunctionalization

2003 ◽  
Vol 10 (25) ◽  
Author(s):  
Dariusz Biernacki ◽  
Olivier Danvy
Keyword(s):  
Logic Programming ◽  
Programming Language ◽  
Operational Semantics ◽  
Lambda Calculus ◽  
Transition System ◽  
Abstract Machine ◽  
Logic Programming Language ◽  
Delimited Continuations ◽  
Simple Logic ◽  
Control Operators

Starting from a continuation-based interpreter for a simple logic programming language, propositional Prolog with cut, we derive the corresponding logic engine in the form of an abstract machine. The derivation originates in previous work (our article at PPDP 2003) where it was applied to the lambda-calculus. The key transformation here is Reynolds's defunctionalization that transforms a tail-recursive, continuation-passing interpreter into a transition system, i.e., an abstract machine. Similar denotational and operational semantics were studied by de Bruin and de Vink in previous work (their article at TAPSOFT 1989), and we compare their study with our derivation. Additionally, we present a direct-style interpreter of propositional Prolog expressed with control operators for delimited continuations.<br /><br />Superseded by BRICS-RS-04-5.

Continuation-based compilation of functional languages for parallel machines

1992 ◽  
Vol 2 (4) ◽  
pp. 393-414
Author(s):  
J.-F. Giorgi ◽  
D. Le Métayer
Keyword(s):  
Parallel Machines ◽  
Parallel Implementation ◽  
Functional Expression ◽  
Functional Languages ◽  
Program Transformations ◽  
Task Management ◽  
Machine Code ◽  
Abstract Machine ◽  
Functional Term

We tackle the problems of correctness and efficiency of paralled implementations of functional languages. We present a compilation technique described in terms of program transformations in the functional framework. The original functional expression is transformed into a functional term, which can be seen as traditional machine code. The main feature of the parallel implementation is the use of continuations. We introduce a parallel abstract machine describing lazy task creation in terms of exportation of continuations. The advantages of the approach are twofold: (1)correetness proofs are made simpler and (2) the implementation is efficient because the use of continuations reduces the task management overhead.

scholarly journals A Syntactic Correspondence between Context-Sensitive Calculi and Abstract Machines

2005 ◽  
Vol 12 (22) ◽  
Author(s):  
Malgorzata Biernacka ◽  
Olivier Danvy
Keyword(s):  
Open Problem ◽  
Lazy Evaluation ◽  
Systematic Construction ◽  
Context Sensitive ◽  
Evaluation Functions ◽  
Abstract Machines ◽  
Explicit Substitutions ◽  
Delimited Continuations ◽  
Tail Recursion

We present a systematic construction of environment-based abstract machines from context-sensitive calculi of explicit substitutions, and we illustrate it with a series of calculi and machines: Krivine's machine with call/cc, the lambda-mu-calculus, delimited continuations, i/o, stack inspection, proper tail-recursion, and lazy evaluation. Most of the machines already exist but have been obtained independently and are only indirectly related to the corresponding calculi. All of the calculi are new and they make it possible to directly reason about the execution of the corresponding machines. In connection with the functional correspondence between evaluation functions and abstract machines initiated by Reynolds, the present syntactic correspondence makes it possible to construct reduction-free normalization functions out of reduction-based ones, which was an open problem in the area of normalization by evaluation.

scholarly journals A Syntactic Correspondence between Context-Sensitive Calculi and Abstract Machines

2005 ◽  
Vol 12 (38) ◽  
Author(s):  
Malgorzata Biernacka ◽  
Olivier Danvy
Keyword(s):  
Open Problem ◽  
Lazy Evaluation ◽  
Normal Order ◽  
Systematic Construction ◽  
Context Sensitive ◽  
Evaluation Functions ◽  
Abstract Machines ◽  
Explicit Substitutions ◽  
Delimited Continuations ◽  
Tail Recursion

We present a systematic construction of environment-based abstract machines from context-sensitive calculi of explicit substitutions, and we illustrate it with ten calculi and machines for applicative order with an abort operation, normal order with generalized reduction and call/cc, the lambda-mu-calculus, delimited continuations, stack inspection, proper tail-recursion, and lazy evaluation. Most of the machines already exist but have been obtained independently and are only indirectly related to the corresponding calculi. All of the calculi are new and they make it possible to directly reason about the execution of the corresponding machines.<br /> <br />In connection with the functional correspondence between evaluation functions and abstract machines initiated by Reynolds, the present syntactic correspondence makes it possible to construct reduction-free normalization functions out of reduction-based ones, which was an open problem in the area of normalization by evaluation.

Sign in / Sign up

Export Citation Format

Share Document