scholarly journals Refocusing in Reduction Semantics

2004 ◽  
Vol 11 (26) ◽  
Author(s):  
Olivier Danvy ◽  
Lasse R. Nielsen
Keyword(s):  
Transitive Closure ◽  
Operational Semantics ◽  
Sufficient Conditions ◽  
Lambda Calculus ◽  
Transition Function ◽  
Evaluation Function ◽  
Abstract Machine ◽  
Worst Case ◽  
State Transition Function ◽  
Case Basis

The evaluation function of a reduction semantics (i.e., a small-step operational semantics with an explicit representation of the reduction context) is canonically defined as the transitive closure of (1) decomposing a term into a reduction context and a redex, (2) contracting this redex, and (3) plugging the contractum in the context. Directly implementing this evaluation function therefore yields an interpreter with a worst-case overhead, for each step, that is linear in the size of the input term. <br /> <br />We present sufficient conditions over the constituents of a reduction semantics to circumvent this overhead, by replacing the composition of (3) plugging and (1) decomposing by a single ``refocus'' function mapping a contractum and a context into a new context and a new redex, if any. We also show how to construct such a refocus function, we prove the correctness of this construction, and we analyze the complexity of the resulting refocus function. <br /> <br />The refocused evaluation function of a reduction semantics implements the transitive closure of the refocus function, i.e., a ``pre-abstract machine.'' Fusing the refocus function with the trampoline function computing the transitive closure gives a state-transition function, i.e., an abstract machine. This abstract machine clearly separates between the transitions implementing the congruence rules of the reduction semantics and the transitions implementing its reduction rules. The construction of a refocus function therefore shows how to mechanically obtain an abstract machine out of a reduction semantics, which was done previously on a case-by-case basis. <br /> <br />We illustrate refocusing by mechanically constructing Felleisen et al.'s CK machine from a call-by-value reduction semantics of the lambda-calculus, and by constructing a substitution-based version of Krivine's machine from a call-by-name reduction semantics of the lambda-calculus. We also mechanically construct three one-pass CPS transformers from three quadratic context-based CPS transformers for the lambda-calculus.

scholarly journals Syntactic Theories in Practice

2002 ◽  
Vol 9 (4) ◽  
Author(s):  
Olivier Danvy ◽  
Lasse R. Nielsen
Keyword(s):  
Programming Language ◽  
Time Complexity ◽  
Program Transformation ◽  
Transitive Closure ◽  
Sufficient Conditions ◽  
Evaluation Function ◽  
Worst Case ◽  
Syntactic Theory ◽  
Input Program ◽  
Syntactic Theories

The evaluation function of a syntactic theory is canonically defined as the transitive closure of (1) decomposing a program into an evaluation context and a redex, (2) contracting this redex, and (3) plugging the contractum in the context. Directly implementing this evaluation function therefore yields an interpreter with a worst-case overhead, for each step, that is linear in the size of the input program. We present sufficient conditions over a syntactic theory to circumvent this overhead, by replacing the composition of (3) plugging and (1) decomposing by a single ``refocusing'' function mapping a contractum and a context into a new context and a new redex, if there are any. We also show how to construct such a refocusing function, we prove its correctness, and we analyze its complexity.<br /> <br />We illustrate refocusing with two examples: a programming-language interpreter and a transformation into continuation-passing style. As a byproduct, the time complexity of this program transformation is mechanically changed from quadratic in the worst case to linear.

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.

scholarly journals An Operational Foundation for Delimited Continuations in the CPS Hierarchy

2004 ◽  
Vol 11 (29) ◽  
Author(s):  
Malgorzata Biernacka ◽  
Dariusz Biernacki ◽  
Olivier Danvy
Keyword(s):  
Operational Semantics ◽  
Lambda Calculus ◽  
Explicit Representation ◽  
Small Step ◽  
Abstract Machine ◽  
Delimited Continuations ◽  
New Applications ◽  
Control Operators

We present an abstract machine and a reduction semantics for the lambda-calculus extended with control operators that give access to delimited continuations in the CPS hierarchy. The abstract machine is derived from an evaluator in continuation-passing style (CPS); the reduction semantics (i.e., a small-step operational semantics with an explicit representation of evaluation contexts) is constructed from the abstract machine; and the control operators are the shift and reset family. At level n of the CPS hierarchy, programs can use the control operators shift_i and reset_i for 1 <= i <= n, the evaluator has n + 1 layers of continuations, the abstract machine has n + 1 layers of control stacks, and the reduction semantics has n + 1 layers of evaluation contexts.<br /> <br /> We also present new applications of delimited continuations in the CPS hierarchy: finding list prefixes and normalization by evaluation for a hierarchical language of units and products.

scholarly journals From Interpreter to Logic Engine by Defunctionalization

2004 ◽  
Vol 11 (5) ◽  
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 (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.

scholarly journals An Operational Foundation for Delimited Continuations in the CPS Hierarchy

2005 ◽  
Vol 12 (24) ◽  
Author(s):  
Malgorzata Biernacka ◽  
Dariusz Biernacki ◽  
Olivier Danvy
Keyword(s):  
Operational Semantics ◽  
Lambda Calculus ◽  
Explicit Representation ◽  
Small Step ◽  
Abstract Machine ◽  
Delimited Continuations ◽  
New Applications ◽  
Control Operators

We present an abstract machine and a reduction semantics for the lambda-calculus extended with control operators that give access to delimited continuations in the CPS hierarchy. The abstract machine is derived from an evaluator in continuation-passing style (CPS); the reduction semantics (i.e., a small-step operational semantics with an explicit representation of evaluation contexts) is constructed from the abstract machine; and the control operators are the shift and reset family. At level n of the CPS hierarchy, programs can use the control operators shift_i and reset_i for 1 <= i <= n, the evaluator has n + 1 layers of continuations, the abstract machine has n + 1 layers of control stacks, and the reduction semantics has n + 1 layers of evaluation contexts.<br /> <br /> We also present new applications of delimited continuations in the CPS hierarchy: finding list prefixes and normalization by evaluation for a hierarchical language of units and products.

The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus

2019 ◽  
Vol 29 ◽  
Author(s):  
ÁLVARO GARCÍA-PÉREZ ◽  
PABLO NOGUEIRA
Keyword(s):  
Operational Semantics ◽  
Lambda Calculus ◽  
Order Reduction ◽  
Normal Order ◽  
Abstract Machine ◽  
Reduction Strategy ◽  
Structural Operational Semantics ◽  
Standard Normal ◽  
De Bruijn ◽  
De Bruijn Indices

AbstractWe exploit the idea of proving properties of an abstract machine by using a corresponding semantic artefact better suited to their proof. The abstract machine is an improved version of Pierre Crégut’s full-reducing Krivine machine KN. The original version works with closed terms of the pure lambda calculus with de Bruijn indices. The improved version reduces in similar fashion but works on closures where terms may be open. The corresponding semantic artefact is a structural operational semantics of a calculus of closures whose reduction relation is purposely a reduction strategy. As shown in previous work, improved KN and the structural operational semantics ‘correspond’, i.e. both artefacts realise the same reduction strategy. In this paper, we prove in the calculus of closures that the reduction strategy simulates in lockstep (at every reduction step) the complete and standard normal-order strategy (i.e. leftmost reduction to normal form) of the pure lambda calculus. The simulation is witnessed by a substitution function from closures of the closure calculus to pure terms of the pure lambda calculus. Thus, KN also simulates normal-order in lockstep by the correspondence. This result is stronger than the known proof that KN is complete, for in the pure lambda calculus there are complete but non-standard strategies. The lockstep simulation proof consists of straightforward structural inductions, thanks to three properties of the closure calculus we call ‘index alignment’, ‘parameters-as-levels’ and ‘balanced derivations’. The first two come from KN. Thanks to these properties, a proof in a calculus of closures involving de Bruijn indices and de Bruijn levels is unproblematic. There is no lexical adjustment at binding lookup, on-the-fly alpha-conversion or recursive traversals of the term to deal with bound and free variables as in other calculi. This paper contributes to the framework for environment machines of Biernacka and Danvy a full-reducing open-terms closure calculus, its corresponding abstract machine, and a lockstep simulation proof via a substitution function.

scholarly journals Towards Compatible and Interderivable Semantic Specifications for the Scheme Programming Language, Part I: Denotational Semantics, Natural Semantics, and Abstract Machines

2008 ◽  
Vol 15 (7) ◽  
Author(s):  
Olivier Danvy
Keyword(s):  
Programming Language ◽  
Denotational Semantics ◽  
Transition Function ◽  
Evaluation Function ◽  
Small Step ◽  
Valuation Function ◽  
Abstract Machine ◽  
Abstract Machines

We derive two big-step abstract machines, a natural semantics, and the valuation function of a denotational semantics based on the small-step abstract machine for Core Scheme presented by Clinger at PLDI'98. Starting from a functional implementation of this small-step abstract machine, (1) we fuse its transition function with its driver loop, obtaining the functional implementation of a big-step abstract machine; (2) we adjust this big-step abstract machine so that it is in defunctionalized form, obtaining the functional implementation of a second big-step abstract machine; (3) we refunctionalize this adjusted abstract machine, obtaining the functional implementation of a natural semantics in continuation style; and (4) we closure-unconvert this natural semantics, obtaining a compositional continuation-passing evaluation function which we identify as the functional implementation of a denotational semantics in continuation style. We then compare this valuation function with that of Clinger's original denotational semantics of Scheme.

scholarly journals An Operational Foundation for Delimited Continuations in the CPS Hierarchy

2005 ◽  
Vol 12 (11) ◽  
Author(s):  
Malgorzata Biernacka ◽  
Dariusz Biernacki ◽  
Olivier Danvy
Keyword(s):  
Operational Semantics ◽  
Lambda Calculus ◽  
Explicit Representation ◽  
Small Step ◽  
Abstract Machine ◽  
Delimited Continuations ◽  
New Applications ◽  
Control Operators

We present an abstract machine and a reduction semantics for the lambda-calculus extended with control operators that give access to delimited continuations in the CPS hierarchy. The abstract machine is derived from an evaluator in continuation-passing style (CPS); the reduction semantics (i.e., a small-step operational semantics with an explicit representation of evaluation contexts) is constructed from the abstract machine; and the control operators are the shift and reset family. At level n of the CPS hierarchy, programs can use the control operators shift_i and reset_i for 1 <= i <= n , the evaluator has n + 1 layers of continuations, the abstract machine has n + 1 layers of control stacks, and the reduction semantics has n + 1 layers of evaluation contexts.<br /> <br /> We also present new applications of delimited continuations in the CPS hierarchy: finding list prefixes and normalization by evaluation for a hierarchical language of units and products.

scholarly journals Syntactic Theories in Practice

2001 ◽  
Vol 8 (31) ◽  
Author(s):  
Olivier Danvy ◽  
Lasse R. Nielsen
Keyword(s):  
Programming Language ◽  
Time Complexity ◽  
Transitive Closure ◽  
Sufficient Conditions ◽  
Time Factor ◽  
Evaluation Function ◽  
Syntactic Theory ◽  
Quadratic Factor ◽  
Syntactic Theories

The evaluation function of a syntactic theory is canonically defined as the transitive closure of (1) decomposing a program into an evaluation context and a redex, (2) contracting this redex, and (3) plugging the result in the context. Directly implementing this evaluation function therefore yields an interpreter with a quadratic time factor over its input. We present sufficient conditions over a syntactic theory to circumvent this quadratic factor, and illustrate the method with two programming-language interpreters and a transformation into continuation-passing style (CPS). In particular, we mechanically change the time complexity of this CPS transformation from quadratic to linear.

Robust H2 Output Feedback Controller Design for Damping Power System Oscillations

2017 ◽  
Vol 6 (10) ◽  
pp. 8
Author(s):  
Kho Hie Kwee ◽  
Hardiansyah .
Keyword(s):  
Power System ◽  
Output Feedback ◽  
Controller Design ◽  
Sufficient Conditions ◽  
Feedback Controller ◽  
Linear Matrix ◽  
Parameter Uncertainties ◽  
Worst Case ◽  
Output Feedback Controller ◽  
Power System Oscillations

This paper addresses the design problem of robust H2 output feedback controller design for damping power system oscillations. Sufficient conditions for the existence of output feedback controllers with norm-bounded parameter uncertainties are given in terms of linear matrix inequalities (LMIs). Furthermore, a convex optimization problem with LMI constraints is formulated to design the output feedback controller which minimizes an upper bound on the worst-case H2 norm for a range of admissible plant perturbations. The technique is illustrated with applications to the design of stabilizer for a single-machine infinite-bus (SMIB) power system. The LMI based control ensures adequate damping for widely varying system operating.

Sign in / Sign up

Export Citation Format

Share Document