A self-interpreter of lambda calculus having a normal form

A subtyping relation ≤ between types is often accompanied by a typing rule, called subsumption: if a term a has type T and T≤U, then a has type U. In presence of subsumption, a well-typed term does not codify its proof of well typing. Since a semantic interpretation is most naturally defined by induction on the structure of typing proofs, a problem of coherence arises: different typing proofs of the same term must have related meanings. We propose a proof-theoretical, rewriting approach to this problem. We focus on F≤, a second-order lambda calculus with bounded quantification, which is rich enough to make the problem interesting. We define a normalizing rewriting system on proofs, which transforms different proofs of the same typing judgement into a unique normal proof, with the further property that all the normal proofs assigning different types to a given term in a given environment differ only by a final application of the subsumption rule. This rewriting system is not defined on the proofs themselves but on the terms of an auxiliary type system, in which the terms carry complete information about their typing proof. This technique gives us three different results:— Any semantic interpretation is coherent if and only if our rewriting rules are satisfied as equations.— We obtain a proof of the existence of a minimum type for each term in a given environment.— From an analysis of the shape of normal form proofs, we obtain a deterministic typechecking algorithm, which is sound and complete by construction.

Download Full-text

A New One-Pass Transformation into Monadic Normal Form

BRICS Report Series ◽

10.7146/brics.v9i52.21767 ◽

2002 ◽

Vol 9 (52) ◽

Author(s):

Olivier Danvy

Keyword(s):

Normal Form ◽

Symbolic Computation ◽

Normal Forms ◽

Lambda Calculus ◽

Higher Order

We present a translation from the call-by-value lambda-calculus to monadic normal forms that includes short-cut boolean evaluation. The translation is higher-order, operates in one pass, duplicates no code, generates no chains of thunks, and is properly tail recursive. It makes a crucial use of symbolic computation at translation time.

Download Full-text

A Complete, Co-Inductive Syntactic Theory of Sequential Control and State

BRICS Report Series ◽

10.7146/brics.v14i4.21927 ◽

2007 ◽

Vol 14 (4) ◽

Cited By ~ 2

Author(s):

Kristian Støvring ◽

Søren B. Lassen

Keyword(s):

Normal Form ◽

Lambda Calculus ◽

Higher Order ◽

Syntactic Theory ◽

Sequential Control ◽

Contextual Equivalence

We present a new co-inductive syntactic theory, eager normal form bisimilarity, for the untyped call-by-value lambda calculus extended with continuations and mutable references. We demonstrate that the associated bisimulation proof principle is easy to use and that it is a powerful tool for proving equivalences between recursive imperative higher-order programs. The theory is modular in the sense that eager normal form bisimilarity for each of the calculi extended with continuations and/or mutable references is a fully abstract extension of eager normal form bisimilarity for its sub-calculi. For each calculus, we prove that eager normal form bisimilarity is a congruence and is sound with respect to contextual equivalence. Furthermore, for the calculus with both continuations and mutable references, we show that eager normal form bisimilarity is complete: it coincides with contextual equivalence.

Download Full-text

On one-pass CPS transformations

Journal of Functional Programming ◽

10.1017/s0956796807006387 ◽

2007 ◽

Vol 17 (6) ◽

pp. 793-812 ◽

Cited By ~ 6

Author(s):

OLIVIER DANVY ◽

KEVIN MILLIKIN ◽

LASSE R. NIELSEN

Keyword(s):

Fixed Point ◽

Normal Form ◽

Lambda Calculus ◽

Higher Order ◽

The Other ◽

Left Inverse ◽

Post Processing ◽

Transformation Time ◽

Special Case ◽

Implementation Technique

AbstractWe bridge two distinct approaches to one-pass CPS transformations, i.e, CPS transformations that reduce administrative redexes at transformation time instead of in a post-processing phase. One approach is compositional and higher-order, and is independently due to Appel, Danvy and Filinski, and Wand, building on Plotkin's seminal work. The other is non-compositional and based on a reduction semantics for the lambda-calculus, and is due to Sabry and Felleisen. To relate the two approaches, we use three tools: Reynolds's defunctionalization and its left inverse, refunctionalization; a special case of fold–unfold fusion due to Ohori and Sasano, fixed-point promotion; and an implementation technique for reduction semantics due to Danvy and Nielsen, refocusing. This work is directly applicable to transforming programs into monadic normal form.

Download Full-text

Clocked lambda calculus

Mathematical Structures in Computer Science ◽

10.1017/s0960129515000389 ◽

2015 ◽

Vol 27 (5) ◽

pp. 782-806

Author(s):

JÖRG ENDRULLIS ◽

DIMITRI HENDRIKS ◽

JAN WILLEM KLOP ◽

ANDREW POLONSKY

Keyword(s):

Fixed Point ◽

Normal Form ◽

Normal Forms ◽

Lambda Calculus ◽

Discrimination Power ◽

Discriminating Power

One of the best-known methods for discriminating λ-terms with respect to β-convertibility is due to Corrado Böhm. The idea is to compute the infinitary normal form of a λ-term M, the Böhm Tree (BT) of M. If λ-terms M, N have distinct BTs, then M ≠βN, that is, M and N are not β-convertible. But what if their BTs coincide? For example, all fixed point combinators (FPCs) have the same BT, namely λx.x(x(x(. . .))).We introduce a clocked λ-calculus, an extension of the classical λ-calculus with a unary symbol τ used to witness the β-steps needed in the normalization to the BT. This extension is infinitary strongly normalizing, infinitary confluent and the unique infinitary normal forms constitute enriched BTs, which we call clocked BTs. These are suitable for discriminating a rich class of λ-terms having the same BTs, including the well-known sequence of Böhm's FPCs.We further increase the discrimination power in two directions. First, by a refinement of the calculus: the atomic clocked λ-calculus, where we employ symbols τp that also witness the (relative) positions p of the β-steps. Second, by employing a localized version of the (atomic) clocked BTs that has even more discriminating power.

Download Full-text

On One-Pass CPS Transformations

BRICS Report Series ◽

10.7146/brics.v14i6.21929 ◽

2007 ◽

Vol 14 (6) ◽

Author(s):

Olivier Danvy ◽

Kevin Millikin ◽

Lasse R. Nielsen

Keyword(s):

Fixed Point ◽

Normal Form ◽

Lambda Calculus ◽

Higher Order ◽

The Other ◽

Left Inverse ◽

Post Processing ◽

Transformation Time ◽

Special Case ◽

Implementation Technique

We bridge two distinct approaches to one-pass CPS transformations, i.e., CPS transformations that reduce administrative redexes at transformation time instead of in a post-processing phase. One approach is compositional and higher-order, and is independently due to Appel, Danvy and Filinski, and Wand, building on Plotkin's seminal work. The other is non-compositional and based on a reduction semantics for the lambda-calculus, and is due to Sabry and Felleisen. To relate the two approaches, we use three tools: Reynolds's defunctionalization and its left inverse, refunctionalization; a special case of fold-unfold fusion due to Ohori and Sasano, fixed-point promotion; and an implementation technique for reduction semantics due to Danvy and Nielsen, refocusing. This work is directly applicable to transforming programs into monadic normal form.

Download Full-text

Theoretical Pearls: Self-interpretation in lambda calculus

Journal of Functional Programming ◽

10.1017/s0956796800020062 ◽

1991 ◽

Vol 1 (2) ◽

pp. 229-233 ◽

Cited By ~ 16

Author(s):

Henk Barendregt

Keyword(s):

Normal Form ◽

Programming Languages ◽

Lambda Calculus ◽

Direct Consequence ◽

Functional Program ◽

Computer Scientists ◽

Strange Loop ◽

Reduction Machine ◽

Image Position ◽

Computable Functions

Programming languages which are capable of interpreting themselves have been fascinating computer scientists. Indeed, if this is possible then a ‘strange loop’ (in the sense of Hofstadter, 1979) is involved. Nevertheless, the phenomenon is a direct consequence of the existence of universal languages. Indeed, if all computable functions can be captured by a language, then so can the particular job of interpreting the code of a program of that language. Self-interpretation will be shown here to be possible in lambda calculus.The set of λ-terms, notation Λ, is defined by the following abstract syntaxwhereis the set {v, v′, v″, v′″,…} of variables. Arbitrary variables are usually denoted by x, y,z,… and λ-terms by M,N,L,…. A redex is a λ-term of the formthat is, the result of substituting N for (the free occurrences of) x in M. Stylistically, it can be said that λ-terms represent functional programs including their input. A reduction machine executes such terms by trying to reduce them to normal form; that is, redexes are continuously replaced by their contracta until hopefully no more redexes are present. If such a normal form can be reached, then this is the output of the functional program; otherwise, the program diverges.

Download Full-text

Theoretical Pearls:Representing ‘undefined’ in lambda calculus

Journal of Functional Programming ◽

10.1017/s0956796800000447 ◽

1992 ◽

Vol 2 (3) ◽

pp. 367-374 ◽

Cited By ~ 13

Author(s):

Henk Barendregt

Keyword(s):

Normal Form ◽

Recursive Function ◽

Lambda Calculus ◽

Recursion Theory ◽

Partial Recursive Function ◽

Normalization Theorem ◽

Image Position

AbstractLet ψ be a partial recursive function (of one argument) with λ-defining termF∈Λ°. This meansThere are several proposals for whatF⌜n⌝ should be in case ψ(n) is undefined: (1) a term without a normal form (Church); (2) an unsolvable term (Barendregt); (3) an easy term (Visser); (4) a term of order 0 (Statman).These four possibilities will be covered by one ‘master’ result of Statman which is based on the ‘Anti Diagonal Normalization Theorem’ of Visser (1980). That ingenious theorem about precomplete numerations of Ershov is a powerful tool with applications in recursion theory, metamathematics of arithmetic and lambda calculus.

Download Full-text

Pragmatic Aspects of Type-Directed Partial Evaluation

BRICS Report Series ◽

10.7146/brics.v3i15.19977 ◽

1996 ◽

Vol 3 (15) ◽

Author(s):

Olivier Danvy

Keyword(s):

Side Effects ◽

Normal Form ◽

Partial Evaluation ◽

Lambda Calculus ◽

Residual Program ◽

Typed Lambda Calculus ◽

Free Variables ◽

Simple Corollary ◽

Pragmatic Aspects ◽

Imperative Language

Type-directed partial evaluation stems from the residualization of static values in dynamic contexts, given their type and the type of their free variables. Its algorithm coincides with the algorithm for coercing a subtype value into a supertype value, which itself coincides with Berger and Schwichtenberg's normalization algorithm for the simply typed lambda-calculus. Type-directed partial evaluation thus can be used to specialize a compiled, closed program, given its type. Since Similix, let-insertion is a cornerstone of partial evaluators for call-by-value procedural languages with computational effects (such as divergence). It prevents the duplication of residual computations, and more generally maintains the order of dynamic side effects in the residual program. This article describes the extension of type-directed partial evaluation to insert residual let expressions. This extension requires the user to annotate arrow types with effect information. It is achieved by delimiting and abstracting control, comparably to continuation-based specialization in direct style. It enables type-directed partial evaluation of programs with effects (e.g., a definitional lambda-interpreter for an imperative language) that are in direct style. The residual programs are in A-normal form. A simple corollary yields CPS (continuation-passing style) terms instead. We illustrate both transformations with two interpreters for Paulson's Tiny language, a classical example in partial evaluation.

Download Full-text

Solving Equations in the lambda-Calculus using Syntactic Encapsulation

BRICS Report Series ◽

10.7146/brics.v2i49.19950 ◽

1995 ◽

Vol 2 (49) ◽

Author(s):

Mayer Goldberg

Keyword(s):

Normal Form ◽

Lambda Calculus ◽

Systems Of Equations ◽

Left Hand ◽

Right Hand ◽

Solving Equations ◽

The Right ◽

The Given ◽

Programming Calculi

Syntactic encapsulation is a relation between an expression and one of its sub-expressions, that constraints how the given sub-expression can be used throughout the reduction of the expression. In this paper, we present a class of systems of equations, in which the right-hand side of each equation is syntactically encapsulated in the left-hand side. This class is general enough to allow equations to contain self-application, and to allow unknowns to appear on both sides of the equation. Yet such a system is simple enough to be solvable, and for a solution (though of course not its normal form) to be obtainable in constant time. Keywords: lambda-calculus, programming calculi.

Download Full-text