ON STEPWISE EXPLICIT SUBSTITUTION

This paper starts by setting the ground for a lambda calculus notation that strongly mirrors the two fundamental operations of term construction, namely abstraction and application. In particular, we single out those parts of a term, called items in the paper, that are added during abstraction and application. This item notation proves to be a powerful device for the representation of basic substitution steps, giving rise to different versions of β-reduction including local and global β-reduction. In other words substitution, thanks to the new notation, can be easily formalised as an object language notion rather than remaining a meta language one. Such formalisation will have advantages with respect to various areas including functional application and the partial unfolding of definitions. Moreover our substitution is, we believe, the most general to date. This is shown by the fact that our framework can accommodate most of the known reduction strategies, which range from local to global. Finally, we show how the calculus of substitution of Abadi et al., can be embedded into our calculus. We show moreover that many of the rules of Abadi et al. are easily derivable in our calculus.

Download Full-text

Program Extraction from Proofs of Weak Head Normalization

BRICS Report Series ◽

10.7146/brics.v12i12.21878 ◽

2005 ◽

Vol 12 (12) ◽

Cited By ~ 1

Author(s):

Malgorzata Biernacka ◽

Olivier Danvy ◽

Kristian Støvring

Keyword(s):

Lambda Calculus ◽

Order Reduction ◽

Object Language ◽

Normal Order ◽

Minimal Logic ◽

Program Extraction ◽

First Order ◽

Typed Lambda Calculus

We formalize two proofs of weak head normalization for the simply typed lambda-calculus in first-order minimal logic: one for normal-order reduction, and one for applicative-order reduction in the object language. Subsequently we use Kreisel's modified realizability to extract evaluation algorithms from the proofs, following Berger; the proofs are based on Tait-style reducibility predicates, and hence the extracted algorithms are instances of (weak head) normalization by evaluation, as already identified by Coquand and Dybjer.

Download Full-text

Modeling, Sharing, and Recursion for Weak Reduction Strategies using Explicit Substitution

BRICS Report Series ◽

10.7146/brics.v3i56.18681 ◽

1996 ◽

Vol 3 (56) ◽

Cited By ~ 1

Author(s):

Zine-El-Abidine Benaissa ◽

Pierre Lescanne ◽

Kristoffer H. Rose

Keyword(s):

Programming Languages ◽

Data Structures ◽

Functional Programming ◽

Explicit Substitution ◽

Reduction Strategies ◽

Recursive Data Structures ◽

Recursive Data ◽

Parallel Evaluation ◽

Major Reduction ◽

Weak Reduction

We present the lambda sigma^a_w calculus, a formal synthesis of the concepts of sharing and explicit substitution for weak reduction. We show how lambda sigma^a_w can be used as a foundation of implementations of functional programming languages by modelling the essential ingredients of such implementations, namely weak reduction strategies, recursion, space leaks, recursive data structures, and parallel evaluation, in a uniform way. First, we give a precise account of the major reduction strategies used in functional programming and the consequences of choosing lambda-graph-reduction vs. environment-based evaluation. Second, we show how to add constructors and explicit recursion to give a precise account of recursive functions and data structures even with respect to space complexity. Third, we formalize the notion of space leaks in lambda sigma^a_w and use this to define a space leak free calculus; this suggests optimisations for call-by-need reduction that prevent space leaking and enables us to prove that the "trimming" performed by the STG machine does not leak space. In summary we give a formal account of several implementation techniques used by state of the art implementations of functional programming languages.Keywords. Implementation of functional programming, lambda calculus, weak reduction, explicit substitution, sharing, recursion, space leaks.

Download Full-text

A Concrete Framework for Environment Machines

BRICS Report Series ◽

10.7146/brics.v12i15.21881 ◽

2005 ◽

Vol 12 (15) ◽

Cited By ~ 1

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.

Download Full-text

A Concrete Framework for Environment Machines

BRICS Report Series ◽

10.7146/brics.v13i3.21909 ◽

2006 ◽

Vol 13 (3) ◽

Cited By ~ 1

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.

Download Full-text

Perpetuality in a named lambda calculus with explicit substitutions

Mathematical Structures in Computer Science ◽

10.1017/s0960129500003248 ◽

2001 ◽

Vol 11 (1) ◽

pp. 47-90 ◽

Cited By ~ 8

Author(s):

EDUARDO BONELLI

Keyword(s):

Lambda Calculus ◽

Strong Normalization ◽

Reduction Strategies ◽

Explicit Substitutions ◽

Type Substitution

We study perpetuality in the calculus of explicit substitutions λx. A reduction is called perpetual if it preserves the possibility of infinite reduction sequences. We then take a look at applications of this study: an inductive characterization of the λx-strongly normalizing terms, two perpetual reduction strategies for λx and finally a proof of strong normalization of a polymorphic lambda calculus with explicit substitutions Fes. To complete the study of Fes, the property of subject reduction is shown to hold by extending type assignments of the typing rules to allow non-pure types (types with possible occurrences of the type substitution operator).

Download Full-text

Modeling sharing and recursion for weak reduction strategies using explicit substitution

Lecture Notes in Computer Science - Programming Languages: Implementations, Logics, and Programs ◽

10.1007/3-540-61756-6_99 ◽

1996 ◽

pp. 393-407 ◽

Cited By ~ 8

Author(s):

Zine-El-Abidine Benaissa ◽

Pierre Lescanne ◽

Kristoffer H. Rose

Keyword(s):

Explicit Substitution ◽

Reduction Strategies ◽

Weak Reduction

Download Full-text

Reduction Strategies for Program Extraction

CLEI electronic journal ◽

10.19153/cleiej.6.1.2 ◽

2018 ◽

Vol 6 (1) ◽

Author(s):

Maribel Fernandez ◽

Ian Mackie ◽

Paula Severi ◽

Nora Szasz

Keyword(s):

Type System ◽

Lambda Calculus ◽

General Setting ◽

Type Systems ◽

Program Extraction ◽

Pure Type ◽

Typed Lambda Calculus ◽

Reduction Strategies ◽

Pure Type Systems ◽

Reduction Relation

We introduce Pure Type Systems with Pairs generalising earlier work on program extraction in Typed Lambda Calculus. We model the process of program extraction in these systems by means of a reduction relation called o-reduction, and give strategies for Bo-reduction which will be useful for an implementation of a proof assistant. More precisely, we give an algorithm to compute theo-normal form of a term in Pure Type System with Pairs, and show that this defines a prejection from Pure Type Systems with Pairs to standart Pure Type Systems. This result shows that o-reduction is an operational description of aprgram extraction that is independent of the particular Typed Lambda Calculus specified as a Pure Typoe System. For B-reduction, we define weak and strong reduction strategies using Interaction Nets, generalising well-know efficient strategies for the l-calculus to the general setting of Pure Type Systems.

Download Full-text