A partial evaluator for the untyped lambda-calculus

1991 ◽  
Vol 1 (1) ◽  
pp. 21-69 ◽  
Author(s):  
Carsten K. Gomard ◽  
Neil D. Jones
Keyword(s):  
Input Data ◽  
Partial Evaluation ◽  
Lambda Calculus ◽  
Higher Order ◽  
Residual Program ◽  
Source Program ◽  
Point Operator ◽  
Free Subset ◽  
Residual Code ◽  
Lambda Expression

AbstractThis article describes theoretical and practical aspects of an implemented self-applicable partial evaluator for the untyped lambda-calculus with constants and a fixed point operator. To the best of our knowledge, it is the first partial evaluator that is simultaneously higher-order, non-trivial, and self-applicable.Partial evaluation produces aresidual programfrom a source program and some of its input data. When given the remaining input data the residual program yields the same result that the source program would when given all its input data. Our partial evaluator produces a residual lambda-expression given a source lambda-expression and the values of some of its free variables. By self-application, the partial evaluator can be used to compile and to generate stand-alone compilers from a denotational or interpretive specification of a programming language.An essential component in our self-applicable partial evaluator is the use of explicitbinding time information.We use this to annotate the source program, marking asresidualthe parts for which residual code is to be generated and marking aseliminablethe parts that can be evaluated using only the data that is known during partial evaluation. We give a simple criterion,well-annotatedness,that can be used to check that the partial evaluator can handle the annotated higher-order programs without committing errors.Our partial evaluator is simple, is implemented in a side-effect free subset of Scheme, and has been used to compile and to generate compilers and a compiler generator. In this article we examine two machine-generated compilers and find that their structures are surprisingly natural.

scholarly journals RS-2 Tagging, Encoding, and Jones Optimality

2003 ◽  
Vol 10 (2) ◽  
Author(s):  
Olivier Danvy ◽  
Pablo E. Martínez López
Keyword(s):  
Partial Evaluation ◽  
Higher Order ◽  
The Self ◽  
Abstract Syntax ◽  
Original Source ◽  
Simple Representation ◽  
Residual Program ◽  
Source Program

A partial evaluator is said to be Jones-optimal if the result of specializing a self-interpreter with respect to a source program is textually identical to the source program, modulo renaming. Jones optimality has already been obtained if the self-interpreter is untyped. If the self-interpreter is typed, however, residual programs are cluttered with type tags. To obtain the original source program, these tags must be removed.<br /> <br />A number of sophisticated solutions have already been proposed. We observe, however, that with a simple representation shift, ordinary partial evaluation is already Jones-optimal, modulo an encoding. The representation shift amounts to reading the type tags as constructors for higher-order abstract syntax. We substantiate our observation by considering a typed self-interpreter whose input syntax is higher-order. Specializing this interpreter with respect to a source program yields a residual program that is textually identical to the source program, modulo renaming.

scholarly journals Higher-Order Rewriting and Partial Evaluation

1997 ◽  
Vol 4 (46) ◽  
Author(s):  
Olivier Danvy ◽  
Kristoffer H. Rose
Keyword(s):  
Partial Evaluation ◽  
Expressive Power ◽  
Higher Order ◽  
Program Transformations ◽  
Residual Program ◽  
Reduction System ◽  
Case Basis ◽  
Exotic Property

We demonstrate the usefulness of higher-order rewriting techniques for specializing programs, i.e., for partial evaluation. More precisely, we demonstrate how casting program specializers as combinatory reduction systems (CRSs) makes it possible to formalize the corresponding program transformations as meta-reductions, i.e., reductions in the internal "substitution calculus." For partial-evaluation problems, this means that instead of having to prove on a case-by-case basis that one's "two-level functions" operate properly, one can concisely formalize them as a combinatory reduction system and obtain as a corollary that static reduction does not go wrong and yields a well-formed residual program.<br />We have found that the CRS substitution calculus provides an adequate expressive power to formalize partial evaluation: it provides sufficient termination strength while avoiding the need for additional restrictions such as types that would complicate the description unnecessarily (for our purpose). We also review the benefits and penalties entailed by more expressive higher-order formalisms. In addition, partial evaluation provides a number of examples of higher-order rewriting where being higher order is a central (rather than an occasional or merely exotic) property. We illustrate this by demonstrating how standard but non-trivial partial-evaluation examples are<br />handled with higher-order rewriting.

scholarly journals Pragmatic Aspects of Type-Directed Partial Evaluation

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<br />a subtype value into a supertype value, which itself coincides with<br />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.<br />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<br />to insert residual let expressions. This extension requires the<br />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<br />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.

scholarly journals A Simple Take on Typed Abstract Syntax in Haskell-like Languages

2000 ◽  
Vol 7 (34) ◽  
Author(s):  
Olivier Danvy ◽  
Morten Rhiger
Keyword(s):  
Normal Forms ◽  
Partial Evaluation ◽  
Lambda Calculus ◽  
Higher Order ◽  
Abstract Syntax ◽  
Typed Lambda Calculus

<p>We present a simple way to program typed abstract syntax in a <br />language following a Hindley-Milner typing discipline, such as Haskell and ML, and we apply it to automate two proofs about normalization functions as embodied in type-directed partial evaluation for the simply typed lambda calculus: normalization functions (1) preserve types and (2) yield long beta-eta normal forms.</p><p>Keywords: Type-directed partial evaluation, normalization functions, simply-typed lambda-calculus, higher-order abstract syntax, Haskell.</p>

scholarly journals Efficient analyses for realistic off-line partial evaluation

1993 ◽  
Vol 3 (3) ◽  
pp. 315-346 ◽  
Author(s):  
Anders Bondorf ◽  
Jesper Jørgensen
Keyword(s):  
Linear Time ◽  
Partial Evaluation ◽  
Flow Analysis ◽  
Higher Order ◽  
Time Analysis ◽  
Specific Order ◽  
Binding Time ◽  
And Function ◽  
Constraint Sets ◽  
Binding Time Analysis

AbstractBased on Henglein's efficient binding-time analysis for the lambda calculus (with constants and ‘fix’) (Henglein, 1991), we develop three efficient analyses for use in the preprocessing phase of Similix, a self-applicable partial evaluator for a higher-order subset of Scheme. The analyses developed in this paper are almost-linear in the size of the analysed program. (1) A flow analysis determines possible value flow between lambda-abstractions and function applications and between constructor applications and selector/predicate applications. The flow analysis is not particularly biased towards partial evaluation; the analysis corresponds to the closure analysis of Bondorf (1991b). (2) A (monovariant) binding-time analysis distinguishes static from dynamic values; the analysis treats both higher-order functions and partially static data structures. (3) A new is-used analysis, not present in Bondorf (1991b), finds a non-minimal binding-time annotation which is ‘safe’ in a certain way: a first-order value may only become static if its result is ‘needed’ during specialization; this ‘poor man's generalization’ (Holst, 1988) increases termination of specialization. The three analyses are performed sequentially in the above mentioned order since each depends on results from the previous analyses. The input to all three analyses are constraint sets generated from the program being analysed. The constraints are solved efficiently by a normalizing union/find-based algorithm in almost-linear time. Whenever possible, the constraint sets are partitioned into subsets which are solved in a specific order; this simplifies constraint normalization. The framework elegantly allows expressing both forwards and backwards components of analyses. In particular, the new is-used analysis is of backwards nature. The three constraint normalization algorithms are proved correct (soundness, completeness, termination, existence of a best solution). The analyses have been implemented and integrated in the Similix system. The new analyses are indeed much more efficient than those of Bondorf (1991b); the almost-linear complexity of the new analyses is confirmed by the implementation.

Mechanizing proofs with logical relations – Kripke-style

2018 ◽  
Vol 28 (9) ◽  
pp. 1606-1638 ◽  
Author(s):  
ANDREW CAVE ◽  
BRIGITTE PIENTKA
Keyword(s):  
Case Studies ◽  
Operational Semantics ◽  
Lambda Calculus ◽  
Equational Theory ◽  
Higher Order ◽  
Abstract Syntax ◽  
Completeness Proof ◽  
Typed Lambda Calculus ◽  
Contextual Equivalence ◽  
The Right

Proofs with logical relations play a key role to establish rich properties such as normalization or contextual equivalence. They are also challenging to mechanize. In this paper, we describe two case studies using the proof environmentBeluga: First, we explain the mechanization of the weak normalization proof for the simply typed lambda-calculus; second, we outline how to mechanize the completeness proof of algorithmic equality for simply typed lambda-terms where we reason about logically equivalent terms. The development of these proofs inBelugarelies on three key ingredients: (1) we encode lambda-terms together with their typing rules, operational semantics, algorithmic and declarative equality using higher order abstract syntax (HOAS) thereby avoiding the need to manipulate and deal with binders, renaming and substitutions, (2) we take advantage ofBeluga's support for representing derivations that depend on assumptions and first-class contexts to directly state inductive properties such as logical relations and inductive proofs, (3) we exploitBeluga's rich equational theory for simultaneous substitutions; as a consequence, users do not need to establish and subsequently use substitution properties, and proofs are not cluttered with references to them. We believe these examples demonstrate thatBelugaprovides the right level of abstractions and primitives to mechanize challenging proofs using HOAS encodings. It also may serve as a valuable benchmark for other proof environments.

An untyped higher order logic with Y combinator

2007 ◽  
Vol 72 (4) ◽  
pp. 1385-1404
Author(s):  
James H. Andrews
Keyword(s):  
Model Theory ◽  
Lambda Calculus ◽  
Higher Order ◽  
Order Logic ◽  
Proof System ◽  
Cut Elimination ◽  
Higher Order Logic ◽  
Consistent Model

AbstractWe define a higher order logic which has only a notion of sort rather than a notion of type, and which permits all terms of the untyped lambda calculus and allows the use of the Y combinator in writing recursive predicates. The consistency of the logic is maintained by a distinction between use and mention, as in Gilmore's logics. We give a consistent model theory, a proof system which is sound with respect to the model theory, and a cut-elimination proof for the proof system. We also give examples showing what formulas can and cannot be used in the logic.

Sign in / Sign up

Export Citation Format

Share Document