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 On the Equivalence between Small-Step and Big-Step Abstract Machines: A Simple Application of Lightweight Fusion

2007 ◽  
Vol 14 (16) ◽  
Author(s):  
Olivier Danvy ◽  
Kevin Millikin
Keyword(s):  
Fixed Point ◽  
Simple Proof ◽  
Recursive Function ◽  
State Transition ◽  
Transition Function ◽  
Simple Application ◽  
Small Step ◽  
Final State ◽  
Abstract Machines ◽  
State Transition Function

We show how Ohori and Sasano's recent lightweight fusion by fixed-point promotion provides a simple way to prove the equivalence of the two standard styles of specification of abstract machines: (1) in small-step form, as a state-transition function together with a `driver loop,' i.e., a function implementing the iteration of this transition function; and (2) in big-step form, as a tail-recursive function that directly maps a given configuration to a final state, if any. The equivalence hinges on our observation that for abstract machines, fusing a small-step specification yields a big-step specification. We illustrate this observation here with a recognizer for Dyck words, the CEK machine, and Krivine's machine with call/cc.<br /> <br />The need for such a simple proof is motivated by our current work on small-step abstract machines as obtained by refocusing a function implementing a reduction semantics (a syntactic correspondence), and big-step abstract machines as obtained by CPS-transforming and then defunctionalizing a function implementing a big-step semantics (a functional correspondence).

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 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 Investigation of Abadi and Cardelli's Untyped Calculus of Objects

2008 ◽  
Vol 15 (6) ◽  
Author(s):  
Jacob Johannsen
Keyword(s):  
Program Transformations ◽  
Small Step ◽  
Abstract Machine ◽  
Abstract Machines ◽  
Explicit Substitutions ◽  
The Relationship ◽  
Two Machines

We study the relationship between the natural (big-step) semantics and the reduction (small-step) semantics of Abadi and Cardelli's untyped calculus of objects. By applying Danvy et al.'s functional correspondence to the natural semantics, we derive an abstract machine for this calculus, and by applying Danvy et al.'s syntactic correspondence to the reduction semantics, we also derive an abstract machines for this calculus. These two abstract machines are identical. The fact that the machines are identical, and the fact that they have been derived using meaning-preserving program transformations, entail that the derivation constitutes a proof of equivalence between natural semantics and the reduction semantics. The derivational nature of our proof contrasts with Abadi and Cardelli's soundness proof, which was carried out by pen and paper. We also note that the abstract machine is new.<br /> <br />To move closer to actual language implementations, we reformulate the calculus to use explicit substitutions. The reformulated calculus is new. By applying the functional and syntactic correspondences to natural and reduction semantics of this new calculus, we again obtain two abstract machines. These two machines are also identical, and as such, they establish the equivalence of the natural semantics and the reduction semantics of the new calculus.<br /> <br />Finally, we prove that the two abstract machines are strongly bisimilar. Therefore, the two calculi are computationally equivalent.

scholarly journals A Rational Deconstruction of Landin's SECD Machine

2003 ◽  
Vol 10 (33) ◽  
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.<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.

scholarly journals Inter-Deriving Semantic Artifacts for Object-Oriented Programming

2008 ◽  
Vol 15 (5) ◽  
Author(s):  
Olivier Danvy ◽  
Jacob Johannsen
Keyword(s):  
Operational Semantics ◽  
Object Oriented ◽  
Object Oriented Programming ◽  
Small Step ◽  
Abstract Machine ◽  
Abstract Machines ◽  
Explicit Substitutions

We present a new abstract machine for Abadi and Cardelli's untyped calculus of objects. What is special about this semantic artifact (i.e., man-made construct) is that is mechanically corresponds to both the reduction semantics (i.e., small-step operational semantics) and the natural semantics (i.e., big-step operational semantics) specified in Abadi and Cardelli's monograph. This abstract machine therefore embodies the soundness of Abadi and Cardelli's reduction semantics and natural semantics relative to each other. <br /> <br />To move closer to actual implementations, which use environments rather than actual substitutions, we then represent object methods as closures and in the same inter-derivational spirit, we present three new semantic artifacts: a reduction semantics for a version of Abadi and Cardelli's untyped calculus of objects with explicit substitutions, an environment-based abstract machine, and a natural semantics (i.e., an interpreter) with environments. These three new semantic artifacts mechanically correspond to each other, and furthermore, they are coherent with the previous ones since as we show, the two abstract machines are bisimilar. Overall, though, the significance of these artifacts lies in them not having been designed from scratch and then proved correct: instead, they were mechanically inter-derived.

An Auto-Focus Algorithm of Fast Search Based on Combining Rough and Fine Adjustment

2012 ◽  
Vol 468-471 ◽  
pp. 534-537
Author(s):  
Zhao Hua Lin ◽  
Xin Liu ◽  
Yu Liang Zhang ◽  
Shu Mei Zhang
Keyword(s):  
Focal Plane ◽  
Narrow Range ◽  
Evaluation Function ◽  
Small Step ◽  
Uniform Sampling ◽  
Fast Search ◽  
Optical Measure ◽  
Fine Adjustment ◽  
Auto Focusing ◽  
Image Definition

A coarse and fine combined fast search and auto-focusing algorithm was suggested in this paper. This method can automatically search and find the focal plane by evaluating the image definition. The Krisch operator based edge energy function was used as the big-step coarse focusing, and then the wavelet transform based image definition evaluation function, which is sensitivity to the variation in image definition, was used to realize the small-step fine focusing in a narrow range. The un-uniform sampling function of the focusing area selection used in this method greatly reduces the workload and the required time for the data processing. The experimental results indicate that this algorithm can satisfy the requirement of the optical measure equipment for the image focusing.

scholarly journals Small-step and big-step semantics for call-by-need

2009 ◽  
Vol 19 (6) ◽  
pp. 699-722 ◽  
Author(s):  
KEIKO NAKATA ◽  
MASAHITO HASEGAWA
Keyword(s):  
Denotational Semantics ◽  
Small Step

AbstractWe present natural semantics for acyclic as well as cyclic call-by-need lambda calculi, which are proved equivalent to the reduction semantics given by Ariola and Felleisen (J. Funct. Program., vol. 7, no. 3, 1997). The natural semantics are big-step and use global heaps, where evaluation is suspended and memorized. The reduction semantics are small-step, and evaluation is suspended and memorized locally in let-bindings. Thus two styles of formalization describe the call-by-need strategy from different angles. The natural semantics for the acyclic calculus is revised from the previous presentation by Maraist et al. (J. Funct. Program., vol. 8, no. 3, 1998), and its adequacy is ascribed to its correspondence with the reduction semantics, which has been proved equivalent to call-by-name by Ariola and Felleisen. The natural semantics for the cyclic calculus is inspired by that of Launchbury (1993) and Sestoft (1997), and we state its adequacy using a denotational semantics in the style of Launchbury; adequacy of the reduction semantics for the cyclic calculus is in turn ascribed to its correspondence with the natural semantics.

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.

Sign in / Sign up

Export Citation Format

Share Document