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

Why is prospect theory's evaluation function S-shaped?

2009 ◽  
Author(s):  
Jessica M. Choplin ◽  
Amber N. Bloomfield
Keyword(s):  
Evaluation Function

Changes in indicators of intonation structure of speech in occupational activity of air traffic control operators

2019 ◽  
pp. 31-37
Author(s):  
K. I. Zasjad’ko ◽  
A. V. Bogomolov ◽  
S. K. Soldatov ◽  
A. P. Vonarshenko ◽  
A. F. Borejchuk ◽  
...  
Keyword(s):  
Functional State ◽  
Traffic Control ◽  
Air Traffic Control ◽  
Work Load ◽  
Work Capacity ◽  
Air Traffic ◽  
Experimental Series ◽  
Occupational Activity ◽  
Average Value ◽  
Control Operators

Introduction.The study is aimed to determine possible use of vocal signal analysis for diagnosis of functional states in air traffic control operators, with justifying selection of informative parameters of intonation structure of speech.Materials and methods.Experiments on semi-natural simulator complex with participation of 16 air traffic male dispatchers modelled occupational activity of air traffic dispatcher with moderate (6 aircrafts controlled) and intense (7–12 aircrafts controlled) work load. Duration of simulated working shiftwas 6 hours. Registration covered characteristics of main vocal tone of the examinees, with calculation of 8 jitter-factors that portrayed mirco-changes of main vocal tone curve and 2 tremor indices disclosing periodic waves of 4–16 Hz in main vocal tone curve. Functional state of the dispatchers was assessed via cardiac rhythm parameters. Reliability and work capacity of the dispatchers corresponded to correct radio traffi c, changes in threshold of reception and transfer of aircrafts in number of allowable dangerous approach of aircrafts, time to detection of input aircraft’s deviation from preset flight line.Results and discussion.According to analysis of the experiments results, some parameters of the main vocal tone carried significant changes both in first (simulated moderate work load) and second (simulated intense work load) experimental series.The data obtained prove lower level of psychic regulation of the dispatchers’ occupational activity during 3rd to 5thhours of “working shift” in the first experimental series and from 2nd to 4thhours of the second experimental series, due to decreased psychophysiologic resources and developing fatigue.Conclusion.Studies of changes in indicators of intonation structure of speech in occupational activity of air traffic dispatchers demonstrated that using such indicators provides adequate diagnosis of the functional state. The most informative indicators are average value, histogram asymmetry and excessive frequency of main vocal tone, duration of pauses between words of the dispatchers’ commands and fi ft h jitter-factor.

Evaluation functions for integral mapping

2017 ◽  
Vol 921 (3) ◽  
pp. 24-29 ◽  
Author(s):  
S.I. Lesnykh ◽  
A.K. Cherkashin
Keyword(s):  
Principal Component Analysis ◽  
Environmental Factors ◽  
Principal Components ◽  
Principal Component ◽  
Evaluation Function ◽  
Final Value ◽  
Evaluation Functions ◽  
Geographical Environment ◽  
Environmental Background ◽  
Integral Mapping

The proposed procedure of integral mapping is based on calculation of evaluation functions on the integral indicators (II) taking into account the feature of the local geographical environment, when geosystems in the same states in the different environs have various estimates. Calculation of II is realized with application of a Principal Component Analysis for processing of the forest database, allowing to consider in II the weight of each indicator (attribute). The final value of II is equal to a difference of the first (condition of geosystem) and the second (condition of environmental background) principal components. The evaluation functions are calculated on this value for various problems of integral mapping. The environmental factors of variability is excluded from final value of II, therefore there is an opportunity to find the invariant evaluation function and to determine coefficients of this function. Concepts and functions of the theory of reliability for making the evaluation maps of the hazard of functioning and stability of geosystems are used.

Sign in / Sign up

Export Citation Format

Share Document