Functional runtime systems within the lambda-sigma calculus

1998 ◽  
Vol 8 (2) ◽  
pp. 131-176 ◽  
Author(s):  
THÉRÈSE HARDIN ◽  
LUC MARANGET ◽  
BRUNO PAGANO
Keyword(s):  
Runtime Systems ◽  
Formal Proofs ◽  
Input Language ◽  
Adequate Theory ◽  
Abstract Machines ◽  
Explicit Substitutions ◽  
Krivine Machine

We define a weak λ-calculus, λσw, as a subsystem of the full λ-calculus with explicit substitutions λσ[uArr ]. We claim that λσw could be the archetypal output language of functional compilers, just as the λ-calculus is their universal input language. Furthermore, λσ[uArr ] could be the adequate theory to establish the correctness of functional compilers. Here we illustrate these claims by proving the correctness of four simplified compilers and runtime systems modelled as abstract machines. The four machines we prove are the Krivine machine, the SECD, the FAM and the CAM. Thus, we give the first formal proofs of Cardelli's FAM and of its compiler.

scholarly journals A Concrete Framework for Environment Machines

2006 ◽  
Vol 13 (3) ◽  
Author(s):  
Malgorzata Biernacka ◽  
Olivier Danvy
Keyword(s):  
Lambda Calculus ◽  
Intermediate Step ◽  
Abstract Machine ◽  
Abstract Machines ◽  
Reduction Strategies ◽  
Explicit Substitutions ◽  
One Step ◽  
The Common ◽  
Krivine Machine ◽  
Common Understanding

We materialize the common understanding that calculi with explicit substitutions provide an intermediate step between an abstract specification of substitution in the lambda-calculus and its concrete implementations. To this end, we go back to Curien's original calculus of closures (an early calculus with explicit substitutions), we extend it minimally so that it can also express one-step reduction strategies, and we methodically derive a series of environment machines from the specification of two one-step reduction strategies for the lambda-calculus: normal order and applicative order. The derivation extends Danvy and Nielsen's refocusing-based construction of abstract machines with two new steps: one for coalescing two successive transitions into one, and the other for unfolding a closure into a term and an environment in the resulting abstract machine. The resulting environment machines include both the Krivine machine and the original version of Krivine's machine, Felleisen et al.'s CEK machine, and Leroy's Zinc abstract machine.

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.

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 Syntactic Correspondence between Context-Sensitive Calculi and Abstract Machines

2006 ◽  
Vol 13 (18) ◽  
Author(s):  
Malgorzata Biernacka ◽  
Olivier Danvy
Keyword(s):  
Lazy Evaluation ◽  
Normal Order ◽  
Systematic Construction ◽  
Context Sensitive ◽  
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, i/o, stack inspection, proper tail-recursion, and lazy evaluation. Most of the machines already exist but they 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.

scholarly journals A Concrete Framework for Environment Machines

2005 ◽  
Vol 12 (15) ◽  
Author(s):  
Malgorzata Biernacka ◽  
Olivier Danvy
Keyword(s):  
Lambda Calculus ◽  
Intermediate Step ◽  
Common Belief ◽  
Normal Order ◽  
Abstract Machine ◽  
Abstract Machines ◽  
Reduction Strategies ◽  
Explicit Substitutions ◽  
One Step ◽  
The Common

We materialize the common belief that calculi with explicit substitutions provide an intermediate step between an abstract specification of substitution in the lambda-calculus and its concrete implementations. To this end, we go back to Curien's original calculus of closures (an early calculus with explicit substitutions), we extend it minimally so that it can express one-step reduction strategies, and we methodically derive a series of environment machines from the specification of two one-step reduction strategies for the lambda-calculus: normal order and applicative order. The derivation extends Danvy and Nielsen's refocusing-based construction of abstract machines with two new steps: one for coalescing two successive transitions into one, and one for unfolding a closure into a term and an environment in the resulting abstract machine. The resulting environment machines include both the idealized and the original versions of Krivine's machine, Felleisen et al.'s CEK machine, and Leroy's Zinc 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.

Designing energy efficient communication runtime systems: a view from PGAS models

2011 ◽  
Vol 63 (3) ◽  
pp. 691-709 ◽  
Author(s):  
Abhinav Vishnu ◽  
Shuaiwen Song ◽  
Andres Marquez ◽  
Kevin Barker ◽  
Darren Kerbyson ◽  
...  
Keyword(s):  
Energy Efficient ◽  
Runtime Systems ◽  
Energy Efficient Communication ◽  
Efficient Communication

scholarly journals Extremal Values of the Sackin Tree Balance Index

2021 ◽  
Author(s):  
Mareike Fischer
Keyword(s):  
Phylogenetic Trees ◽  
Theoretical Computer Science ◽  
Search Trees ◽  
Formal Proofs ◽  
Birth Process ◽  
Ordered Trees ◽  
Research Areas ◽  
New Findings ◽  
Mathematical Phylogenetics ◽  
Extremal Values

AbstractTree balance plays an important role in different research areas like theoretical computer science and mathematical phylogenetics. For example, it has long been known that under the Yule model, a pure birth process, imbalanced trees are more likely than balanced ones. Also, concerning ordered search trees, more balanced ones allow for more efficient data structuring than imbalanced ones. Therefore, different methods to measure the balance of trees were introduced. The Sackin index is one of the most frequently used measures for this purpose. In many contexts, statements about the minimal and maximal values of this index have been discussed, but formal proofs have only been provided for some of them, and only in the context of ordered binary (search) trees, not for general rooted trees. Moreover, while the number of trees with maximal Sackin index as well as the number of trees with minimal Sackin index when the number of leaves is a power of 2 are relatively easy to understand, the number of trees with minimal Sackin index for all other numbers of leaves has been completely unknown. In this manuscript, we extend the findings on trees with minimal and maximal Sackin indices from the literature on ordered trees and subsequently use our results to provide formulas to explicitly calculate the numbers of such trees. We also extend previous studies by analyzing the case when the underlying trees need not be binary. Finally, we use our results to contribute both to the phylogenetic as well as the computer scientific literature using the new findings on Sackin minimal and maximal trees to derive formulas to calculate the number of both minimal and maximal phylogenetic trees as well as minimal and maximal ordered trees both in the binary and non-binary settings. All our results have been implemented in the Mathematica package SackinMinimizer, which has been made publicly available.

Sign in / Sign up

Export Citation Format

Share Document