BRICS RS-96-34 Hatcliff & Danvy: A Computational Formalization for Partial Evaluation

BRICS

Basic Research in Computer Science

A Computational Formalization for Partial Evaluation

(Extended Version)

John Hatcliff Olivier Danvy

BRICS Report Series RS-96-34 ISSN 0909-0878 October 1996 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1996, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent publications in the BRICS Report Series. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK - 8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through World Wide Web and anonymous FTP:

http://www.brics.dk/
ftp://ftp.brics.dk/

This document in subdirectory RS/96/34/

A Computational Formalization for Partial Evaluation (extended version) ^{∗}

John Hatcliff  Olivier Danvy
BRICS^{†}
Oklahoma State University ^{‡}  University of Aarhus ^{§}

Abstract

We formalize a partial evaluator for Eugenio Moggi’s computational metalanguage. This formalization gives an evaluation-order independent view of binding-time analysis and program specialization, including a proper treatment of call unfolding, and enables us to express the essence of “control-based binding-time improvements” for let expressions. Specifically, we prove that the binding-time improvements given by “continuation-based specialization” can be expressed in the metalanguage via monadic laws.

∗A shorter version of this paper (essentially, a version without the proofs of Appendix B) will appear in a special issue of Mathematical Structures in Computer Science devoted to the 1995 Workshop on Logic, Domains, and Programming Languages (LDPL’95) at which this work was presented. The essential results of this work obtained during the fall of 1994 and refined throughout 1995 and 1996 while the first author was at the University of Copenhagen.

†

Basic Research in Computer Science, Centre of the Danish National Research Foundation.

‡

Department of Computer Science 219 Mathematical Sciences, Stillwater, OK 74078-1053, USA. E-mail: hatcliff@a.cs.okstate.edu

§

Department of Computer Science Ny Munkegade, Building 540, DK-8000 Aarhus C, Denmark. E-mail: danvy@brics.dk

1 Introduction

Partial evaluation is a program-transformation technique for specializing programs, based on propagating constant values and folding constant expressions [11, 42]. Over the last ten years, it has been organized as a two-phase process: binding-time analysis and program specialization. Binding-time analysis classifies which parts of the source program can be computed statically, i.e., at partial-evaluation time. Program specialization carries out these static computations and residualizes the other computational steps. This organization in two phases thus makes it clear that the more parts of a source program are static, the more this source program is specialized. Over the last five years, various pre-transformations have been investigated that “improve binding times” (making binding-time analysis classify more parts are static) and thus increase specialization.

Our goal is to formalize both the two-phase process of partial evaluation and binding-time improvements, using Moggi’s computational metalanguage.

Moggi’s computational metalanguage distinguishes values (terms with no remaining computation steps) and computations (terms with remaining computation steps). This makes it possible to express a variety of evaluation strategies (including call-by-name and call-by-value). In addition, programs can be parameterized with various notions of computations, expressed as computational monads. Monads are often claimed to make reasoning about programs easier — but very few applications actually exploit the monadic laws.

In this paper, we illustrate that the computational meta-language can be a useful framework for partial evaluation. It allows a clear distinction between static computation steps (to be performed at specialization time) and dynamic computation steps (to be residualized at specialization time and performed at run time). Moreover, it allows an evaluation-order independent view of binding-time analysis and program specialization.

To this end, we present a PCF-like version of the computational metalanguage, and give it a structural operational semantics. We specify bindingtime analysis as a non-standard type inference, and then a specializer using structural operational semantics. We prove the correctness of the bindingtime analysis and of the specializer.

The computational metalanguage enables us to formalize existing techniques in partial evaluation — namely the linguistic device of let insertion, and the partial-evaluation techniques of control-based binding-time improvement and continuation-based specialization, which we achieve by incorporating the monadic laws into our binding-time analysis and our specializer. We prove the equivalence between a continuation-based partial evaluator and our partial evaluator that applies the monadic laws. This formalizes binding-time improvements independently of any particular evaluation order.

We believe that the computational metalanguage also enables new insights and techniques, e.g., to process computational effects. Let us first review each of these points, before outlining the rest of the paper.

1.1 Call unfolding and computation duplication

A partial evaluator unfolds function calls. Call unfolding is thus necessary but in general it is unsound under call-by value. It is necessary to expose opportunities for constant propagation and folding. It is unsound under call-by-value because it may alter termination properties and duplicate computations. Since Similix [7], virtually all call-by-value partial evaluators insert a let expression for every dynamic (i.e., unknown) parameter, at each unfolding point. This insertion ensures sound call unfolding: termination properties are preserved and both code and computation duplications are avoided.

Moggi’s computational metalanguage specifies the order of computations through let expressions. By expressing source programs in this metalanguage, let expressions appear naturally. By residualizing these let expressions, sound call unfolding is achieved naturally.

For example, the call-by-value program

λz . (λ(x, y) . (x + 1) − (y + y)) @ (10, z × z)

can be specialized as follows. The inner β-redex can be reduced (noting application with the infix operator “@”), and the left-most addition can be computed. The residual program reads:

λz . 11 − ((z × z) + (z × z))

It is unsatisfactory because the computation of z×z has been duplicated. As mentioned above [7], call-by-value partial evaluators insert residual let expressions to name dynamic expressions that should not be duplicated. With such a strategy, the residual program reads:

λz . let a = z × z in 11 − (a + a)

This solution of inserting let expressions is effective, but ad hoc, in that there were no corresponding let expressions in the source program. In contrast, let expressions are an integral part of Moggi’s computational metalanguage. Using this metalanguage, the source program can be rewritten as follows.

λz . let a ⇐ z × z in (λ(x, y) . let v_{1} ⇐ x + 1 in \begin{matrix}let v_{2} ⇐ y + y \\ in & v_{1} − v_{2}) @ (10, a) \end{matrix}

Specializing this program amounts to β-reducing function applications (which is always sound because their argument is a value, not a computation), δ-reducing static operations, and unfolding let expressions that bind a unit computation.

Presently, the outer let expression is not unfolded because z is dynamic (its value is unknown) and the function application is β-reduced. This leads to:

λz . let a ⇐ z × z in let v_{1} ⇐ 10 + 1 in \begin{matrix}let v_{2} ⇐ a + a \\ in & v_{1} − v_{2} \end{matrix}

The static addition is performed, which leads to:

λz . let a ⇐ z × z in let v_{1} ⇐ unit 11 in \begin{matrix}let v_{2} ⇐ a + a \\ in & v_{1} − v_{2} \end{matrix}

The let expression declaring v_{1} is unfolded, and there is no other opportunity for static reduction. The result essentially coincides with the residual program above.

1.2 Control-based binding-time improvements

The structure of source programs influences the precision of binding-time analysis and thus the effectiveness of program specialization. A panoply of “binding-time improvements” aiming at restructuring source programs has been developed [42, Chapter 12] but they have not been formalized.

Essentially, a partial evaluator propagates static values into static contexts, where this propagation gives rise to a static computation. Bindingtime analysis thus refines the usual notions of data flow and control flow into a static and a dynamic data flow, and a static and a dynamic control flow. Data-flow and control-flow binding-time improvements respectively amount to improve the static data flow and the static control flow of a source program. The data-flow aspects have been recently clarified [17, 18], but the control-flow aspects still remain a research topic [6, 8, 10, 39, 45].

The program calculus for Moggi’s computational metalanguage includes monadic laws. Let us show how a partial evaluator applying monadic laws to restructure source programs captures the essence of control-based bindingtime improvements.

For example, the program

λf . ((λx . 2) @ (f @ 1)) + 3

can be specialized as follows. The inner β-redex can be reduced but because its argument is dynamic, a let expression must be inserted. The result reads:

λf . (let x = f @ 1 in 2) + 3

It would be unsound to unfold the let expression and discard f @ 1 from the residual program because f could have a computational effect (e.g., divergence). A partial evaluator needs to perform some contorsions to move the context of the let expression [·] + 3 in its body, yielding

λf . let x = f @ 1 in 5

Such restructurings are referred to as “control-based binding-time improvements” since they alter the control flow of the program so as to improve binding times. They are usually achieved by maintaining an explicit representation of control, using continuations. Specializers incorporating these techniques are known as “continuation-based specializers” [6, 42, 45]. Essentially they mimic one-pass CPS transformations [15].

We formalize this technique with the associativity of let expressions in Moggi’s computational metalanguage. Encoding the term above in the metalanguage yields:

λf . let v_{1} ⇐ let v_{2} ⇐ f @ 1 in (λx . unit 2) @ v_{2} in v_{1} + 3

Static reduction of the β-redex yields:

λf . let v_{1} ⇐ let v_{2} ⇐ f @ 1 ; in unit 2 in v_{1} + 3

Reassociating the let expression yields:

λf . let v_{2} ⇐ f @ 1 in let v_{1} ⇐ unit 2 in v_{1} + 3

Unfolding the inner let and statically reducing the addition yields:

λf . let v_{2} ⇐ f @ 1 ; in unit 5

The result essentially coincides with the residual program above.

1.3 Computational effects

Since Similix [7], partial evaluators classify computational effects (I/O, state, etc.) as dynamic computations. The specializer’s only duty is to maintain their order and to ensure that none disappears or is duplicated.

The computational metalanguage’s raison d’être is to provide a modular specification of computational effects. Using this medium, we originally planned to provide a sound treatment of side-effects that would be more effective than systematic residualization. We envisioned for example to split the store in regions: some side-effecting operations could then be classified as static and performed statically (e.g., a symbol table in an interpreter could be processed statically in a compiler) while others would be classified as dynamic and delayed until runtime (e.g., an error message associated with division by 0). This line of work is currently being pursued independently by Dussart and Thiemann [22].

1.4 This paper

The rest of this paper is organized as follows. Section 2 presents a PCF-like version of the computational metalanguage, Λ_{ml}. We give it a structural operational semantics. Section 3 presents an offline partial evaluator for Λ_{ml}. Section 4 addresses call unfolding. In Section 5, we return to the monadic laws and incorporate them into the specializer — adjusting the binding-time analysis accordingly. In Section 6, we prove the equivalence between a continuation-based partial evaluator and our partial evaluator that applies the monadic laws. After a review of related work in Section 7, Section 8 concludes.

Appendix A gives the details for translating call-by-name and call-by-value PCF into Λ_{ml}. Appendix B gives proof details.

e ∈ Terms[Λ_{ml}]
e ::= x | ⌜n⌝ | succ e | pred e | if0 e_{1} e_{2} e_{3} | λx . e | e_{0} @ e_{1} |
fix x. e | unit e | let x ⇐ e_{1} in e_{2}
τ ∈ Types[Λ_{ml}]
τ ::= nat | τ_{1} →τ̃_{2} | τ̃

Γ ∈ Assumptions[Λ_{ml}]
Γ ::= · | Γ, x:τ
Γ ⊢_{ml} ⌜n⌝ : nat  \frac{Γ ⊢_{ml} e : nat}{Γ ⊢_{ml} succ e : ñat}  \frac{Γ ⊢_{ml} e : nat}{Γ ⊢_{ml} pred e : ñat}

Γ ⊢_{ml} x : Γ(x) \frac{Γ ⊢_{ml} e_{1} : nat Γ ⊢_{ml} e_{2} : τ̃ Γ ⊢_{ml} e_{3} : τ̃}{Γ ⊢_{ml} if0 e_{1} e_{2} e_{3} : τ̃}

\frac{Γ, x:τ_{1} ⊢_{ml} e : τ̃_{2}}{Γ ⊢_{ml} λx . e : τ_{1} →τ̃_{2}}  \frac{Γ ⊢_{ml} e_{0} : τ_{1} →τ̃_{2} Γ ⊢_{ml} e_{1} : τ_{1}}{Γ ⊢_{ml} e_{0} @ e_{1} : τ̃_{2}}

\frac{Γ, x:τ̃ ⊢_{ml} e : τ̃}{Γ ⊢_{ml} fix x. e : τ̃}

monadic constructs:  \frac{Γ ⊢_{ml} e : τ}{Γ ⊢_{ml} unit e : τ̃}  \frac{Γ ⊢_{ml} e_{1} : τ̃_{1} Γ, x:τ_{1} ⊢_{ml} e_{2} : τ̃_{2}}{Γ ⊢_{ml} let x ⇐ e_{1} in e_{2} : τ̃_{2}}

Figure 1: The computational meta-language Λ_{ml}

2 The computational meta-language

2.1 Syntax Figure 1 presents the language Λ_{ml} based on Moggi’s computational metalanguage [48].^{1} The typing system of Λ_{ml} captures the distinction between values (terms with no remaining computation steps) and computations (terms with remaining computation steps). Types of the form nat and τ_{1} →τ_{2} are value types. Accordingly, the rules for numerals and abstractions belong to the introduction rules for value types. Types of the form τ̃ are computation types. All functions have computational co-domains. Thus, all applications have a computation type — capturing the fact that evaluating a function application always requires one or more computational steps.

1We have added fix, succ, pred, and if0 to Moggi’s published description [48].

The monadic constructs are used to make the computational process explicit.^{2} Intuitively, unit e is a trivial computation that simply yields the value of e. let x ⇐ e_{1} in e_{2} forces the evaluation of e_{1}. If that evaluation terminates, the resulting value is substituted for x in e_{2}, and evaluation continues with the modified version of e_{2}.

We identify terms up to renaming of bound variables (i.e., up to αequivalence) and use standard notation and conventions for substitution, free variables, contexts, etc. [2]. We write e_{1} ≡ e_{2} when e_{1} and e_{2} are α-equivalent.

We represent simultaneous substitutions e[x_{1} := e_{1} , ... , x_{n} := e_{n}] using a substitution function σ : Terms[Λ_{ml}]→Terms[Λ_{ml}] whose application is denoted eσ. A substitution σ is closed if, for all x ∈ dom σ, xσ is a closed term.

We write Γ ⊢_{ml} e_{1} , e_{2} : τ when both Γ ⊢_{ml} e_{1} : τ and Γ ⊢_{ml} e_{2} : τ. A closed substitution σ is compatible with an assumption Γ, if for all x ∈ dom Γ, · ⊢_{ml} xσ : Γ(x). Programs are closed terms with type ñat.

2.2 Operational semantics

Figure 2 presents single-step evaluation rules for Λ_{ml}.^{3} Axioms such as succ ⌜n⌝ ⟼_{i} unit ⌜n + 1⌝ define basic computation steps. The single inference rule describes contexts in which evaluation steps may occur.

The following lemma gives evaluation properties for closed terms at each type τ. The intuition is that each well-typed term (a) is a canonical term of

2The exact connection to the structure of a monad can be found in Moggi’s original work [48, page 61].

3Moggi originally gave a categorical interpretation for his computational meta-language [48]. Crole and Pitts extended Moggi’s work with a fix-point operator and an associated logic [13]. Later, Gordon developed an elegant operational theory for the meta-language with a fixpoint operator and inductive and coinductive types [31]. Λ_{ml} is basically a sublanguage of Gordon’s — except that we include directly type nat and associated operations whereas Gordon constructs them via inductive types. Here, we follow Gordon and our previous work [34, 36] and present a structural operational semantics for Λ_{ml}.

succ ⌜n⌝ ⟼_{i} unit ⌜n + 1⌝
(λx . e_{0}) @ e_{1} ⟼_{i} e_{0}[x := e_{1}]
fix x. e ⟼_{i} e[x := fix x. e]
let x ⇐ unit e_{1} in e_{2} ⟼_{i} e_{2}[x := e_{1}]

pred ⌜n + 1⌝ ⟼_{i} unit ⌜n⌝
pred ⌜0⌝ ⟼_{i} unit ⌜0⌝
if0 ⌜0⌝ e_{2} e_{3} ⟼_{i} e_{2}
if0 ⌜n + 1⌝ e_{2} e_{3} ⟼_{i} e_{3}

\frac{e ⟼_{i} e′}{E_{i}[e] ⟼_{i} E_{i}[e′]}  E_{i} ::= let x ⇐ [·] in e_{2}

Figure 2: Interpretation steps for Λ_{ml}

the corresponding type, or (b) can undergo an evaluation step that preserves typing. In particular, there are no “stuck” [56, p. 151] terms.^{4}

Lemma 1 (interpretation properties)

1. If · ⊢_{ml} e : nat then e ≡ ⌜n⌝ for some number n.

2. If · ⊢_{ml} e : τ_{1} →τ̃_{2} then e ≡ λx . e′ and x:τ_{1} ⊢_{ml} e′ : τ̃_{2}.

3. If · ⊢_{ml} e : τ̃ then exactly one of the following statements holds:

(a) e = unit e′ and · ⊢_{ml} e′ : τ.

(b) e ⟼_{i} e′ and · ⊢_{ml} e′ : τ̃.

Proof: by induction over the height of the derivation of · ⊢_{ml} e : τ relying on the property that if Γ, x:τ_{1} ⊢_{ml} e_{0} : τ_{0} and Γ ⊢_{ml} e_{1} : τ_{1} then Γ ⊢_{ml} e_{0}[x := e_{1}] : τ_{0}. See the proof of Lemma 2 (which generalizes the current lemma) given in Appendix B.

It is easy to check that e ⟼_{i} e′ and e ⟼_{i} e′′ implies e′ ≡ e′′. This justifies the definition of the following (partial) function in terms of the reflexive transitive closure of ⟼_{i}.

4For example, the untypable term ⌜3⌝ @ ⌜2⌝ is stuck: it cannot undergo an evaluation step and it is not a proper canonical term for any type.

Definition 1 (interpreter) For · ⊢_{ml} e : ñat,

int e = ⌜n⌝ iff e ⟼_{i}^{∗} unit ⌜n⌝

We write int e↓ when int e is defined and int e↑ when int e is undefined. As a consequence of Lemma 1, int e↑ implies that e heads an infinite sequence of computation steps.

Observing termination of terms in program contexts gives the following notion of operational approximation, which in turn, induces a notion of operational equivalence.^{5}

Definition 2 (operational approximation) For Γ ⊢_{ml} e_{1} , e_{2} : τ, and for all contexts C such that C [e_{1}] and C [e_{2}] are programs,

e_{1} ⪯ e_{2} iff int C [e_{1}]↓ implies int C [e_{2}]↓

Definition 3 (operational equivalence) For Γ ⊢_{ml} e_{1} , e_{2} : τ,

e_{1} ≈ e_{2} iff e_{1} ⪯ e_{2} and e_{2} ⪯ e_{1}

Note that if · ⊢_{ml} e_{1} , e_{2} : ñat and e_{1} ≈ e_{2}, then int e_{1} and int e_{2} are both undefined, or else both are defined and there exists a number n such that int e_{1} ≡ ⌜n⌝ ≡ int e_{2}.

2.3 Equational reasoning

Figure 3 presents notions of reduction for the computational meta-language Λ_{ml}. ⟶ also denotes construct-compatible one-step reduction, ⟶ ⟶ denotes the reflexive, transitive closure of ⟶, and =_{ml} denotes the smallest equivalence relation generated by ⟶ [2].

Theorem 1 (soundness of calculus) For Γ ⊢_{ml} e_{1} , e_{2} : τ,

e_{1} =_{ml} e_{2} ⇒ e_{1} ≈ e_{2}

Proof: The proof follows by a straightforward adaptation of Gordon’s operational theory [31, Chapters 3,4,5].

5It is sufficient to observe termination since one can always distinguish between numerals using conditional expressions.

succ ⌜n⌝ ⟶ unit ⌜n + 1⌝
(λx . e_{0}) @ e_{1} ⟶ e_{0}[x := e_{1}]
fix x. e ⟶ e[x := fix x. e]

pred ⌜n + 1⌝ ⟶ unit ⌜n⌝
pred ⌜0⌝ ⟶ unit ⌜0⌝
if0 ⌜0⌝ e_{2} e_{3} ⟶ e_{2}
if0 ⌜n + 1⌝ e_{2} e_{3} ⟶ e_{3}

Monadic reductions:

(let.β)  let x ⇐ unit e_{1} in e_{2} ⟶ e_{2}[x := e_{1}]
(let.η)  let x ⇐ e in unit x ⟶ e

(let.assoc) let x_{2} ⇐ \begin{matrix}let x_{1} ⇐ e_{1} \\ in & e_{2} \end{matrix}

in e_{3}

⟶ let x_{1} ⇐ e_{1} in \begin{matrix}let x_{2} ⇐ e_{2} \\ in & e_{3} \end{matrix} x_{1} ∉ FV(e_{3})

Figure 3: Notions of reduction ml for Λ_{ml}

2.4 Encoding evaluation strategies in Λ_{ml}

A variety of evaluation strategies for a PCF-like language Λ can be encoded in Λ_{ml} due to Λ_{ml}’s explicit distinction between values and computations. In previous work [34, 36], we proved the correctness of an encoding E_{n} of a call-by-name version of Λ into Λ_{ml}, and an encoding E_{v} of a call-by-value version of Λ into Λ_{ml}. These encodings can be found in Appendix A.2.^{6}

In summary, call-by-name Λ functions are encoded as functions from computations to computations; call-by-value Λ functions are encoded as functions from values to computations.^{7} Applications are translated as follows:

Call-by-name: E_{n}⟨[e_{0} @ e_{1}]⟩ = let x_{0} ⇐ E_{n}⟨[e_{0}]⟩ in x_{0} @ E_{n}⟨[e_{1}]⟩
Call-by-value: E_{v}⟨[e_{0} @ e_{1}]⟩ = let x_{0} ⇐ E_{v}⟨[e_{0}]⟩ in let x_{1} ⇐ E_{v}⟨[e_{1}]⟩ in x_{0} @ x_{1}

6These encodings are based on similar encodings given by e.g., Moggi [48] and Wadler [67].

7Alternative call-by-value encodings exist that are similar to the encoding of call-by-value procedures in the call-by-name programming language Algol 60 [36, Section 4].

Thus, evaluation of argument expressions in not forced in the call-by-name encoding, but is forced in the call-by-value encoding.

In general (i.e., in all encodings), a let is inserted around each computation step — making the computational structure of a program explicit. This property is crucial to the evaluation-order independent treatment of binding-time analysis and program specialization presented in the following section.

3 An offline partial evaluator for Λ_{ml}

A partial evaluator takes a source program p and a subset s of p’s input, and produces a residual program p_{s} which is specialized with respect to s. The correctness of the partial evaluator implies that running p_{s} on p’s remaining input d gives the same result as running p on the complete input s and d. The data s and d are often referred to as static and dynamic data (respectively) since s is fixed at specialization time whereas one may supply various data d during runs of p_{s}.

The specialized program p_{s} is obtained from p by evaluating constructs that depend only on s, while rebuilding constructs that may depend on dynamic data. “Offline” partial evaluation accomplishes this in two phases:

(1) a binding-time analysis phase, and (2) a specialization phase.

1. Binding-time analysis: Given assumptions about which program inputs are static and dynamic, binding-time analysis constructs an annotated program where each program construct is annotated with a specialization directive and a specialization type.

• Specialization directives: A construct is assigned a directive of eliminable if it depends only on static data and thus can be completely evaluated during the specialization phase. A construct is assigned a directive of residual if it may depend on dynamic data and thus must be reconstructed in the specialization phase.

• Specialization types: The specialization types (a.k.a. binding times) are the carriers of information during the analysis phase. They describe the “knownness” or the “unknownness” of expressions. This information is used to determine the specialization directives assigned to constructs. For example, if the argument of a destructor construct has a specialization type indicating that

w ∈ Terms[Λ_{ml}^{bt}]
w ::= x |

⌜n⌝ | succ w | pred w | if0 w_{1} w_{2} w_{3} | λx . w | w_{0} @ w_{1} | fix x. w | unit w | let x ⇐ w_{1} in w_{2} | \underline{n} | \underline{succ} w | \underline{pred} w | \underline{if0} w_{1} w_{2} w_{3} | \underline{λ}x . w | w_{0} \underline{@} w_{1} | \underline{fix} x. w | \underline{unit} w | \underline{let} x ⇐ w_{1} \underline{in} w_{2} | lift w

Figure 4: The binding-time annotated meta-language Λ_{ml}^{bt}

it is unknown, then that construct cannot be evaluated at specialization time and must be given a residual directive.

2. Specialization: During the specialization phase, the specializer simply follows the directives assigned during binding-time analysis: eliminable constructs are evaluated (and thus eliminated); residual constructs are reconstructed (and thus appear in the residual program).^{8}

3.1 Binding-time analysis

We first outline how binding-time information is expressed in a program annotated with specialization directives and types. Following this, we give a binding-time logic that determines which annotations are appropriate for a given source language term.

3.1.1 Specialization directives

A binding-time analysis for Λ_{ml} associates each Λ_{ml} term with a term in the annotated language Λ_{ml}^{bt} of Figure 4. Eliminable terms are non-underlined; residual terms are underlined. Identifiers are not annotated since the appropriate information can be determined from the environment. A coercion construct lift is added to Λ_{ml}^{bt} to residualize the result of evaluating an elim-

8Following other formal treatments of partial evaluation [42, 54, 68], we simplify the presentation by omitting folding and generalization strategies.

φ_{nat} ∈ STypes[nat]
φ_{nat} ::= s | d
φ_{τ_{1}→_{τ_{2}}} ∈ STypes[τ_{1} →τ̃_{2}]
φ_{τ_{1}→_{τ_{2}}} ::= φ_{τ_{1}} →φ_{τ_{2}} | d
φ_{τ} ∈ STypes[τ̃]
φ_{τ} ::= φ̃_{τ} | d

τ ∈ Types[Λ_{ml}^{bt}]
τ ::= nat | τ_{1} →τ̃_{2} | τ̃

Γ ∈ Assumptions[Λ_{ml}^{bt}]
Γ ::= · | Γ, x:τ[φ_{τ}]

Figure 5: Specialization types and binding-time assumptions for Λ_{ml}^{bt}

inable term. This allows static computation to occur in a residual context.^{9} A term w ∈ Λ_{ml}^{bt} is completely residual if it consists of only underlined constructs and identifiers. Residual-terms[Λ_{ml}^{bt}] denotes the set of completely residual terms. Intuitively, the specializer will output completely residual terms — all eliminable constructs will have been evaluated (this will be proved in Section 3.2).

3.1.2 Specialization types

Figure 5 presents a τ-indexed family of specialization types (STypes) for Λ_{ml}^{bt} (we omit type indices on specialization types when they can be inferred from the context). A specialization type φ is dynamic if φ = d; otherwise φ is static.

• s ∈ STypes[nat] will tag expressions of type nat that are guaranteed to evaluate to known data (i.e., numerals).

• d ∈ STypes[nat] will tag expressions of type nat whose evaluation may depend on unknown data and thus cannot be guaranteed to evaluate to numerals. However, because nat is a value type, one does know that the tagged expression will denote a value when dynamic data is supplied.

9We restrict lifting to base types for simplicity, as we wish to formalize control-flow binding-time improvements. Defining lift at higher types would enable data-flow bindingtime improvements, as investigated elsewhere [17, 18]. This definition is also interesting on its own [14].

• φ_{τ_{1}} → φ_{τ_{2}} ∈ STypes[τ_{1} →τ̃_{2}] will tag expressions of type τ_{1} → τ̃_{2} that are guaranteed to evaluate to known data (i.e., abstractions).

• d ∈ STypes[τ_{1} →τ̃_{2}] will tag expressions of type τ_{1} → τ̃_{2} whose evaluation may depend on unknown data and thus cannot be guaranteed to evaluate to an abstraction. However, because τ_{1} → τ̃_{2} is a value type, one does know that the tagged expression will denote a value when dynamic data is supplied.

• φ̃ ∈ STypes[τ̃] will tag expressions of type τ̃ that are guaranteed to either diverge or to evaluate to a trivial computation (i.e., unit e for some e ∈ Λ_{ml} of type τ).

• d ∈ STypes[τ̃] will tag expressions of type τ̃ whose evaluation may depend on unknown data and thus cannot be guaranteed to diverge or evaluate to a trivial computation.

Figure 5 also presents type assumptions for Λ_{ml}^{bt} variables. If Γ, x:τ[d] then x is a dynamic variable; if Γ, x:τ[φ] where φ is static then x is a static variable. Γ(x).type and Γ(x).spec-type project types and specialization types from an assumption for x ∈ dom Γ.

3.1.3 Binding-time analysis specification

Figures 6 and 7 present rules for deriving judgments of the form

Γ ⊢_{bt} e : τ[w : φ_{τ}].

Derivable judgements specify constraints that an actual binding-time analysis algorithm must satisfy. Intuitively, if Γ ⊢_{bt} e : τ[w : φ_{τ}], then given initial binding-time assumptions Γ that indicate which free variables are static or dynamic, a binding-time analysis algorithm maps e ∈ Terms[Λ_{ml}] of type τ ∈ Types[Λ_{ml}] to a directive annotated term w ∈ Terms[Λ_{ml}^{bt}] of specialization type φ_{τ} ∈ STypes[τ]. Specifying the analysis in this way allows one to reason about correctness of the analysis independently of the actual algorithm — proving correctness with respect to the constraints implies that any algorithm satisfying the constraints will be correct.

Γ ⊢_{bt} x : Γ(x).type[x : Γ(x).spec-type] Γ ⊢_{bt} ⌜n⌝ : nat[⌜n⌝ : s] Γ ⊢_{bt} ⌜n⌝ : nat[\underline{⌜n⌝} : d]

\frac{Γ ⊢_{bt} e : nat[w : s]}{Γ ⊢_{bt} succ e : ñat [succ w : s̃]}  \frac{Γ ⊢_{bt} e : nat[w : d]}{Γ ⊢_{bt} succ e : ñat [\underline{succ} w : d]}
\frac{Γ ⊢_{bt} e : nat[w : s]}{Γ ⊢_{bt} pred e : ñat [pred w : s̃]}  \frac{Γ ⊢_{bt} e : nat[w : d]}{Γ ⊢_{bt} pred e : ñat [\underline{pred} w : d]}

\frac{Γ ⊢_{bt} e_{1} : nat[w_{1} : s] Γ ⊢_{bt} e_{2} : τ̃[w_{2} : φ] Γ ⊢_{bt} e_{3} : τ̃[w_{3} : φ]}{Γ ⊢_{bt} if0 e_{1} e_{2} e_{3} : τ̃[if0 w_{1} w_{2} w_{3} : φ]}

\frac{Γ ⊢_{bt} e_{1} : nat[w_{1} : d] Γ ⊢_{bt} e_{2} : τ̃[w_{2} : d] Γ ⊢_{bt} e_{3} : τ̃[w_{3} : d]}{Γ ⊢_{bt} if0 e_{1} e_{2} e_{3} : τ̃[\underline{if0} w_{1} w_{2} w_{3} : d]}

\frac{Γ, x:τ_{1}[φ_{1}] ⊢_{bt} e : τ̃_{2}[w : φ_{2}]}{Γ ⊢_{bt} λx . e : τ_{1} →τ̃_{2}[λx . w : φ_{1} →φ_{2}]}

\frac{Γ, x:τ_{1}[d] ⊢_{bt} e : τ̃_{2}[w : d]}{Γ ⊢_{bt} λx . e : τ_{1} →τ̃_{2}[\underline{λ}x . w : d]}

\frac{Γ ⊢_{bt} e_{0} : τ_{1} →τ̃_{2}[w_{0} : φ_{1} →φ_{2}] Γ ⊢_{bt} e_{1} : τ_{1}[w_{1} : φ_{1}]}{Γ ⊢_{bt} e_{0} @ e_{1} : τ̃_{2}[w_{0} @ w_{1} : φ_{2}]}

\frac{Γ ⊢_{bt} e_{0} : τ_{1} →τ̃_{2}[w_{0} : d] Γ ⊢_{bt} e_{1} : τ_{1}[w_{1} : d]}{Γ ⊢_{bt} e_{0} @ e_{1} : τ̃_{2}[w_{0} \underline{@} w_{1} : d]}

Figure 6: Binding-time constraints (part 1)

\frac{Γ, x:τ̃[φ̃] ⊢_{bt} e : τ̃[w : φ̃]}{Γ ⊢_{bt} fix x. e : τ̃[fix x. w : φ̃]}  \frac{Γ, x:τ̃[d] ⊢_{bt} e : τ̃[w : d]}{Γ ⊢_{bt} fix x. e : τ̃[\underline{fix} x. w : d]}

\frac{Γ ⊢_{bt} e : τ[w : φ]}{Γ ⊢_{bt} unit e : τ̃[unit w : φ̃]}  \frac{Γ ⊢_{bt} e : τ[w : d]}{Γ ⊢_{bt} unit e : τ̃[\underline{unit} w : d]}

\frac{Γ ⊢_{bt} e_{1} : τ̃_{1}[w_{1} : φ̃_{1}] Γ, x:τ_{1}[φ_{1}] ⊢_{bt} e_{2} : τ̃_{2}[w_{2} : φ_{2}]}{Γ ⊢_{bt} let x ⇐ e_{1} in e_{2} : τ̃_{2}[let x ⇐ w_{1} in w_{2} : φ_{2}]}

\frac{Γ ⊢_{bt} e_{1} : τ̃_{1}[w_{1} : d] Γ, x:τ_{1}[d] ⊢_{bt} e_{2} : τ̃_{2}[w_{2} : d]}{Γ ⊢_{bt} let x ⇐ e_{1} in e_{2} : τ̃_{2}[\underline{let} x ⇐ w_{1} \underline{in} w_{2} : d]} (∗)

\frac{Γ ⊢_{bt} e : nat[w : s]}{Γ ⊢_{bt} e : nat[lift w : d]}

Figure 7: Binding-time constraints (part 2)

⌊·⌋ : Terms[Λ_{ml}^{bt}]→Terms[Λ_{ml}] is an erasing function that removes annotations and lift constructs. ⌊·⌋ : Assumptions[Λ_{ml}^{bt}]→Assumptions[Λ_{ml}] simply drops specialization types appearing in assumptions. ⌊σ⌋ represents the component-wise application of ⌊·⌋ : Terms[Λ_{ml}^{bt}]→Terms[Λ_{ml}].

Given an assumption Γ ∈ Assumptions[Λ_{ml}^{bt}], a closed Λ_{ml}^{bt} substitution σ is compatible with Γ if

for all x ∈ dom Γ, · ⊢_{ml} ⌊xσ⌋ : Γ(x).type[xσ : Γ(x).spec-type].

For expressions e ∈ Terms[Λ_{ml}], Γ_{bt} is a binding-time assumption for Γ ⊢_{ml} e : τ, if ⌊Γ_{bt}⌋ = Γ. Γ_{bt} = Γ_{s} ∪ Γ_{d} represents the splitting of a binding-time assumption Γ_{bt} into its (necessarily disjoint) static and dynamic variable assumptions.

Definition 4 (binding-time analysis) A binding-time analysis is a function

bta : Assumptions[Λ_{ml}^{bt}]→Terms[Λ_{ml}]→Terms[Λ_{ml}^{bt}]

such that when Γ_{bt} is a binding-time assumption for Γ ⊢_{ml} e : ñat,

Γ_{bt} ⊢_{bt} e : ñat[(bta Γ_{bt} e) : d].

The binding-time analysis rules specify a one-to-many relation between Λ_{ml} terms and Λ_{ml}^{bt} terms. Thus, there are many valid binding-time analysis functions — each varying in practical effectiveness. One usually desires an analysis that gives as many eliminable terms as possible. However, it may be useful to deliberately annotate some eliminable terms as residual to ensure that specialization terminates [42]. Our specification abstracts away from these orthogonal implementation issues.

Conversely, an induction over the derivation of Γ ⊢_{ml} e : τ[w : φ] shows that e ≡ ⌊w⌋. Thus, every well-annotated Λ_{ml}^{bt} term has exactly one Λ_{ml} term related to it — the Λ_{ml} term is the erasure of the Λ_{ml}^{bt} term.

3.2 Specialization

To specialize a binding-time analyzed program term w such that

Γ_{bt} = Γ_{s} ∪ Γ_{d} ⊢_{bt} e : ñat[w : d]

one supplies known data into the static variables via a substitution σ_{s} compatible with Γ_{s}. The resulting term wσ_{s} is then specialized using the rules of Figure 8 (which define the single-step specialization function ⟼_{s}).

• The interpretation rules allow interpreter steps to reduce eliminable (i.e., non-underlined) terms. This corresponds to the idea that partial evaluators are often described as having an interpreter component.

• The axiom lift coerces a static numeral to a dynamic numeral. This allows static values of type nat to occur in dynamic contexts.

• The compilation rules direct the activities of the specializer in dynamic contexts E_{s}. This corresponds to the fact that the non-interpretive component of the specializer simply constructs terms that appear in the residual program. In contexts E_{s}, r ranges over completely residual terms (i.e., terms containing only underlined constructs and free dynamic variables).

The following lemma gives specialization properties for the Λ_{ml}^{bt} terms satisfying judgements of the form Γ_{d} ⊢_{bt} e : τ[w : φ_{τ}]. The intuition is that Interpretation rules:

succ ⌜n⌝ ⟼_{i} unit ⌜n + 1⌝
(λx . w_{0}) @ w_{1} ⟼_{i} w_{0}[x := w_{1}]
fix x. w ⟼_{i} w[x := fix x. w]
let x ⇐ unit w_{1} in w_{2} ⟼_{i} w_{2}[x := w_{1}]

pred ⌜n + 1⌝ ⟼_{i} unit ⌜n⌝
pred ⌜0⌝ ⟼_{i} unit ⌜0⌝
if0 ⌜0⌝ w_{2} w_{3} ⟼_{i} w_{2}
if0 ⌜n + 1⌝ w_{2} w_{3} ⟼_{i} w_{3}

\frac{w ⟼_{i} w′}{E_{i}[w] ⟼_{i} E_{i}[w′]}  E_{i} ::= let x ⇐ [·] in w_{2}

\frac{w ⟼_{i} w′}{w ⟼_{s} w′}

Compilation rules:

lift ⌜n⌝ ⟼_{s} \underline{⌜n⌝} \frac{w ⟼_{s} w′}{E_{s}[w] ⟼_{s} E_{s}[w′]}

E_{s} ::= \underline{pred} [·] | \underline{succ} [·] | \underline{if0} [·] w_{2} w_{3} | \underline{if0} r_{1} [·] w_{3} | \underline{if0} r_{1} r_{2} [·] |

\underline{λ}x . [·] | [·] \underline{@} w_{1} | r_{0} \underline{@} [·] | \underline{fix} x. [·] |

\underline{unit} [·] | \underline{let} x ⇐ [·] \underline{in} w_{2} |

\underline{let} x ⇐ r_{1} \underline{in} [·] ...where r_{i} ∈ Residual-terms[Λ_{ml}^{bt}]

Figure 8: Specialization rules for Λ_{ml}^{bt}

each well-annotated term w (a) is a canonical annotated term of the appropriate type, or (b) is completely residual, or (c) can undergo a specialization step which preserves annotations. Moreover, each specialization step w ⟼_{s} w′ maintains Λ_{ml} convertibility on the corresponding erasures (i.e., ⌊w⌋ =_{ml} ⌊w′⌋).

Lemma 2 (specialization properties)

1. If Γ_{d} ⊢_{bt} e : nat[w : s] then w ≡ ⌜n⌝ ≡ e for some number n.

2. If Γ_{d} ⊢_{bt} e : τ_{1} →τ_{2}[w : φ_{1} →φ_{2}] then w ≡ λx . w′, e ≡ λx . ⌊w′⌋ and

Γ_{d}, x:τ_{1}[φ_{1}] ⊢_{bt} ⌊w′⌋ : τ_{2}[w′ : φ_{2}] for some w′ ∈ Terms[Λ_{ml}^{bt}].

3. If Γ_{d} ⊢_{bt} e : τ̃[w : φ̃] then exactly one of the following statements holds:

(a) w ≡ unit w′, e ≡ unit ⌊w′⌋ and Γ_{d} ⊢_{bt} ⌊w′⌋ : τ[w′ : φ] for some w′ ∈ Terms[Λ_{ml}^{bt}], or

(b) w ⟼_{i} w′ and Γ_{d} ⊢_{bt} ⌊w′⌋ : τ̃[w′ : φ̃] and e ≡ ⌊w⌋ ⟶ ⟶_{ml} ⌊w′⌋.

4. If Γ_{d} ⊢_{bt} e : nat[w : d] then exactly one of the following statements holds:

(a) w ∈ Residual-terms[Λ_{ml}^{bt}], or

(b) w ⟼_{s} w′, Γ_{d} ⊢_{bt} ⌊w′⌋ : τ[w′ : d], and e ≡ ⌊w⌋ ≡ ⌊w′⌋ ≡ ⌜n⌝ for some number n.

5. If Γ_{d} ⊢_{bt} e : τ_{1} →τ_{2}[w : d] then exactly one of the following statements holds:

(a) w ∈ Residual-terms[Λ_{ml}^{bt}], or

(b) w ⟼_{s} w′ and Γ_{d} ⊢_{bt} ⌊w′⌋ : τ[w′ : d] and e ≡ ⌊w⌋ ⟶ ⟶_{ml} ⌊w′⌋.

6. If Γ_{d} ⊢_{bt} e : τ̃[w : d] then exactly one of the following statements holds:

(a) w ∈ Residual-terms[Λ_{ml}^{bt}], or

(b) w ⟼_{s} w′ and Γ_{d} ⊢_{bt} ⌊w′⌋ : τ̃[w′ : d] and e ≡ ⌊w⌋ ⟶ ⟶_{ml} ⌊w′⌋.

Proof: by induction over the height of the derivation of Γ_{d} ⊢_{bt} e : τ[w : φ] relying on the property that if we have both Γ, x:τ_{1}[φ_{1}] ⊢_{bt} e_{0} : τ_{0}[w_{0} : φ_{0}] and Γ ⊢_{bt} e_{1} : τ_{1}[w_{1} : φ_{1}], then Γ ⊢_{bt} e_{0}[x := e_{1}] : τ_{0}[w_{0}[x := w_{1}] : φ_{0}]. See Appendix B for details.

It is easy to check that if w ⟼_{s} w′ and w ⟼_{s} w′′ then w′ ≡ w′′. Furthermore, by Lemma 2, well-annotated terms r ∈ Residual-terms[Λ_{ml}^{bt}] cannot undergo further specialization steps. This justifies the definition of the following (partial) function in terms of the reflexive, transitive closure of ⟼_{s}.

Definition 5 (specializer) For Γ_{d} ⊢_{bt} e : ñat[w : d],

spec w = r iff w ⟼_{s}^{∗} r

where r ∈ Residual-terms[Λ_{ml}^{bt}].

3.3 Correctness of binding-time analysis and specialization

A binding-time analysis is correct if it always produces sound directives. Directives are unsound if they direct the specializer to attempt the reduction of a non-redex. The last component of Lemma 2 implies that any bindingtime analysis satisfying our constraints is correct: when an annotated term (with only dynamic free variables) is specialized, the specializer always finds a redex to contract, or terminates because only residual components are left. In other words, the specializer never “sticks” on a non-redex.

Theorem 2 (correctness of binding-time analysis) For all Γ_{d} ⊢_{bt} e : ñat[w : d], exactly one of the following statements holds:

1. spec w = r where r ∈ Residual-terms[Λ_{ml}^{bt}], or

2. spec w↑ and w heads an infinite sequence of specialization steps.

Proof: follows from the definition of spec (Definition 5) and Lemma 2. See Appendix B for details.

This statement of binding-time correctness is analogous to statements of binding-time correctness for the λ-calculus [42, 54, 68].

A specializer is sound if its steps reflect a meaning-preserving transformation of the source program.

Theorem 3 (soundness of specialization) For all Γ_{d} ⊢_{bt} e : ñat[w : d],

spec w↓ implies e ≈ ⌊spec w⌋

Proof: Given the definition of spec (Definition 5) and Lemma 2, one has e =_{ml} ⌊spec w⌋ by induction over the number of specialization steps. The soundness of the Λ_{ml} calculus (Theorem 1) then gives the desired result.

3.4 Partial evaluation

An offline partial evaluator for Λ_{ml} is obtained by composing binding-time analysis with specialization. When supplied with a source expression e, a binding-time assumption Γ_{bt}, and a collection of “known” data σ_{s}, the partial evaluator specializes the program to the known data as directed by the binding-time analysis.

Definition 6 (partial evaluator) Let bta be a correct binding-time analysis, Γ_{bt} = Γ_{s} ∪ Γ_{d} be a binding-time assumption for Γ ⊢_{ml} e : ñat, and σ_{s} be a closed substitution compatible with Γ_{s}, then

pe e Γ_{bt} σ_{s} =^{def} ⌊spec (bta Γ_{bt} e)σ_{s}⌋

The correctness theorem for the partial evaluator is analogous to Kleene’s S_{n}^{m}-theorem: partial evaluation computes a program specialized to known input data (σ_{s}) such that running the specialized program on the remaining input data (σ_{d}) yields a result observationally equivalent to the result of running the source program on the complete input data.

Theorem 4 (correctness of partial evaluation) Let Γ_{bt} = Γ_{s} ∪ Γ_{d} be a binding-time assumption for Γ ⊢_{ml} e : ñat, let σ_{s} be a closed substitution compatible with Γ_{s}, and let σ_{d} be a closed substitution compatible with ⌊Γ_{d}⌋. If (pe e Γ_{bt} σ_{s})↓, then

e⌊σ_{s}⌋σ_{d} ≈ (pe e Γ_{bt} σ_{s})σ_{d}

Proof: follows from Theorem 3 and the definition of specialization (Definition 5) and partial evaluation (Definition 6). See Appendix B for details.

4 Call unfolding

At the core of a partial evaluator lies call unfolding. This basic transformation enables static information to be propagated across procedure boundaries. Call unfolding is implemented using the copy rule. Thus it is only sound in a call-by-name setting such as Launchbury’s [44]. In a call-by-value setting, call unfolding is unsound (i.e., it does not preserve observational equivalence).

For example, consider the following Λ-term (under call-by-value), occurring in a static context where e_{1} is dynamic.

pred ((λx . ⌜43⌝) @ e_{1})

Unfolding the inner call is unsound in general because e_{1} may diverge. Yet a partial evaluator such as Lambda-Mix would unfold it [29, 30].

Through a systematic insertion of let-expressions, partial evaluators such as Similix or Schism ensure sound call unfolding [7, 9]. They would unfold the term above into the following term

pred (let x = e_{1} in 43)

and would residualize the let expression to preserve the termination properties of the source term. Now a partial evaluator only needs to move the context pred [·] inside the let expression to enable a static reduction that yields the expected answer. This may require a binding-time improvement, as investigated in Section 5. The ⟼_{x} steps below represent how the above expression would be treated e.g., in Similix.

pred (let y = e_{1} in (λx . 43) @ y)
⟼_{x} pred (let y = e_{1} in 43)  ...unfold call
⟼_{x} let y = e_{1} in pred 43  ...binding-time improvement
⟼_{x} let y = e_{1} in 42  ...static computation

In Λ_{ml}, evaluation steps only occur in let contexts and thus their result is named. Encodings of Λ into Λ_{ml} (such as those in Appendix A.2) insert let constructs at all evaluation contexts (rather than in an ad hoc manner as above). Because of the more natural placement of let expressions, the binding-time improvement step in the evaluation above is avoided — specialization steps are simply reductions in the Λ_{ml} calculus.

For example, the call-by-value encoding of Appendix A.2 yields the following term (after performing some initial let.β reductions).

e ≡ let y_{1} ⇐ E_{v}⟨[e_{1}]⟩ in let y_{2} ⇐ (λx . unit ⌜43⌝) @ y_{1} in pred y_{2}

Assuming that e occurs in a static context and that E_{v}⟨[e_{1}]⟩ is dynamic, binding-time analysis would associate e with the following annotated term (where w_{1} is the annotation of E_{v}⟨[e_{1}]⟩).

w ≡ \underline{let} y_{1} ⇐ w_{1} \underline{in} let y_{2} ⇐ (λx . unit ⌜43⌝) @ y_{1} in pred y_{2}

Specialization reduces the inner let expression and yield the expected answer.

w
⟼_{s} \underline{let} y_{1} ⇐ E_{v}⟨[e]⟩ \underline{in} let y_{2} ⇐ unit ⌜43⌝ in pred y_{2}
⟼_{s} \underline{let} y_{1} ⇐ E_{v}⟨[e]⟩ \underline{in} pred 43
⟼_{s} let y_{1} ⇐ E_{v}⟨[e]⟩ in unit 42

Finally, another advantage of phrasing partial evaluation in terms of Λ_{ml} is that concepts of proper let-insertion and binding-time improvements (as discussed in the following section) can be presented independently of evaluation order. For example, our formalization of these concepts still remains valid if one considers e.g., a mixed evaluation strategy [16].

5 Control-based binding-time improvements

The partial evaluator defined in Section 3 is sensitive to the structure of source programs. Consider the two following Λ_{ml}-convertible expressions.

e_{1} ≡ let v_{1} ⇐ (let v_{2} ⇐ x_{2} in succ x_{1}) in e  ...where v_{2} ∉ FV(e)
e_{2} ≡ let v_{2} ⇐ x_{2} in let v_{1} ⇐ succ x_{1} in e

Assume Γ, x_{1} :nat, x_{2} :ñat ⊢_{ml} e_{1}, e_{2} : τ̃, and let Γ_{bt} = Γ′_{bt}, x_{1} :nat[s], x_{2} :ñat[d] be binding-time assumptions for e_{1} and e_{2} (i.e., x_{1} is a static variable, x_{2} is a dynamic variable).

Given the binding-time rules of Figures 6 and 7, e_{1} must map to the following expression w_{1} for some w (i.e., Γ ⊢_{bt} e_{1} : τ̃[w_{1} : d] is derivable).

w_{1} ≡ \underline{let} v_{1} ⇐ (\underline{let} v_{2} ⇐ x_{2} \underline{in} \underline{succ} lift x_{1}) \underline{in} w

On the other hand, e_{2} may map to the following expression w_{2} for some w′ (i.e., Γ ⊢_{bt} e_{2} : τ̃[w_{2} : d] is derivable).

w_{2} ≡ \underline{let} v_{2} ⇐ x_{2} \underline{in} let v_{1} ⇐ succ x_{1} in w′

In w_{1}, the let associated with v_{1} is forced to be residual. In w_{2}, it can be eliminable — which may enable further static computations, particularly within a loop.

This example captures in a nutshell the need for binding-time improvements: meaning-preserving transformations over source programs that enable more source expressions to be classified as static (and thus to be computed away statically, which yields more efficient specialized programs). In this example, e_{1} can be “binding-time improved” by transforming it to e_{2} using the let.assoc reduction of Λ_{ml} calculus (see Figure 3).

5.1 Flattening before binding-time analysis

The example above illustrates that the let.assoc reduction gives a useful binding-time improvement. This (along with the fact that let.assoc is confluent and strongly normalizing [34]) suggests a general strategy for improving binding times: before analyzing the binding times of a program, map this program to its let.assoc normal form.

The following example, however, illustrates that this strategy does not discover all binding-time improvements associated with the let.assoc reduction. During specialization, unfolding a call may expose flattening opportunities that are not apparent in the source program.

For example, assume that the following variant of e_{1} above is in let.assoc normal form.

e_{3} ≡ let v_{1} ⇐ ((λz . let v_{2} ⇐ x_{2} in succ x_{1}) @ ⌜0⌝) in e
...where v_{2} ∉ FV(e)

Using the same binding-time assumptions Γ_{bt} as above, e_{3} maps to w_{3} below for some w′′ (i.e., the let associated with v_{2} is forced to be residual).

w_{3} ≡ \underline{let} v_{1} ⇐ ((λz . \underline{let} v_{2} ⇐ x_{2} \underline{in} \underline{succ} lift x_{1}) @ ⌜0⌝) \underline{in} w′′

Specialization (after supply static data ⌜42⌝ for x_{1} includes the following step.

\underline{let} v_{1} ⇐ ((λz . \underline{let} v_{2} ⇐ x_{2} \underline{in} \underline{succ} lift ⌜42⌝) @ ⌜0⌝) \underline{in} w′′
⟼_{s} \underline{let} v_{1} ⇐ (\underline{let} v_{2} ⇐ x_{2} \underline{in} \underline{succ} lift ⌜42⌝) \underline{in} w′′

Note that this last term has the same problematic form as w_{1} above.

5.2 Flattening during specialization

The solution is to incorporate the flattening rule let.assoc of Figure 3 as a specialization step. One might be tempted to simply redefine specialization so that the specialization of w_{3} above proceeds as follows (i.e., a flattening step is taken whenever possible).

\underline{let} v_{1} ⇐ ((λz . \underline{let} v_{2} ⇐ x_{2} \underline{in} \underline{succ} lift ⌜42⌝) @ ⌜0⌝) \underline{in} w′′
⟼_{s} \underline{let} v_{1} ⇐ (\underline{let} v_{2} ⇐ x_{2} \underline{in} \underline{succ} lift ⌜42⌝) \underline{in} w′′
⟼_{f} \underline{let} v_{2} ⇐ x_{2} \underline{in} \underline{let} v_{1} ⇐ \underline{succ} lift ⌜42⌝ \underline{in} w′′

At this point, however, we are no better off than we were before since the specialization directives indicate that the let associated with v_{1} must be residualized.

\frac{Γ ⊢_{bt}^{+} e_{1} : τ̃_{1}[w_{1} : d] Γ, x:τ_{1}[d] ⊢_{bt}^{+} e_{2} : τ̃_{2}[w_{2} : φ]}{Γ ⊢_{bt}^{+} let x ⇐ e_{1} in e_{2} : τ̃_{2}[\underline{let} x ⇐ w_{1} \underline{in} w_{2} : φ]} (∗∗)

Figure 9: Modified binding-time constraints for Λ_{ml}^{bt}

Since it is the task of binding-time analysis to direct the specializer, the binding-time analysis also must reflect the possible use of the let.assoc rule. In the (∗) rule of Figure 7, the body of the \underline{let} is forced to have a specialization type (i.e., binding-time) of d since it cannot be consumed during specialization. However, after adding the flatten rule as a specialization step, a static expression in the body of a \underline{let} can be consumed. Allowing the body of the \underline{let} to have a static binding-time leads to the following annotation of e_{3} above.

w_{4} ≡ let v_{1} ⇐ ((λz . \underline{let} v_{2} ⇐ x_{2} \underline{in} succ x_{1}) @ ⌜0⌝) in w′′′

A specializer which incorporates the flattening rule now gives the desired behaviour.

let v_{1} ⇐ ((λz . \underline{let} v_{2} ⇐ x_{2} \underline{in} succ x_{1}) @ ⌜0⌝) in w′′′
⟼_{s} let v_{1} ⇐ (\underline{let} v_{2} ⇐ x_{2} \underline{in} succ ⌜42⌝) in w′′′
⟼_{f} \underline{let} v_{2} ⇐ x_{2} \underline{in} let v_{1} ⇐ succ ⌜42⌝ in w′′′
⟼_{s} \underline{let} v_{2} ⇐ x_{2} \underline{in} let v_{1} ⇐ unit ⌜43⌝ in w′′′
⟼_{s} \underline{let} v_{2} ⇐ x_{2} \underline{in} w′′′[v_{1} := ⌜43⌝]

We formalize the modified binding-time analysis and specializer in the following sections.

5.2.1 Binding-time analysis

Replacing the (∗) rule of Figure 7 with the (∗∗) rule in Figure 9 gives improved constraints Γ ⊢_{bt}^{+} e : τ[w : φ]. The following property verifies that the improved constraints are at least as “good” as the previous ones. The example above shows that in many cases the improved constraints are better, i.e., they give more opportunities for static computation.

Property 1 Γ ⊢_{bt} e : τ[w : φ] implies Γ ⊢_{bt}^{+} e : τ[w : φ] Proof: by induction over the derivation of Γ ⊢_{bt} e : τ[w : φ].

Binding-time analysis is defined as before (Definition 4). bta^{+} denotes the analysis functions based on the improved constraints.

5.2.2 Specialization

Figure 10 gives specialization steps which incorporate the flattening rules. The first flattening rule gives the previously discussed binding-time improvements. The second rule is added for stylistic reasons. It simplifies the presentation so that flattening does not occur in an interpreter context E_{i} but only in specialization contexts E_{s}. Essentially, the specializer will attempt to apply flattening rules first. Otherwise, specialization proceeds as before. Note that in applying the let.assoc reduction, a renaming may be necessary to avoid variable capture (in Figure 3, the condition is that x_{1} ∉ FV(e_{3})). We assume that necessary renamings take place when using the flattening rules of Figure 10 and we omit the corresponding formalization.

The following lemma gives specialization properties for the Λ_{ml}^{bt} terms satisfying judgements of the form Γ_{d} ⊢_{bt}^{+} e : τ[w : φ_{τ}]. It only differs from the previous specialization properties (Lemma 2) in that the third component (dealing with judgements of the form Γ_{d} ⊢_{bt} e : τ̃[w : φ̃]) now reflects the improved treatment of let constructs.^{10}

Lemma 3 (specialization properties)

1. If Γ_{d} ⊢_{bt}^{+} e : nat[w : s] then w ≡ ⌜n⌝ ≡ e for some number n.

2. If Γ_{d} ⊢_{bt}^{+} e : τ_{1} →τ_{2}[w : φ_{1} →φ_{2}] then w ≡ λx . w′, e ≡ λx . ⌊w′⌋ and Γ_{d}, x:τ_{1}[φ_{1}] ⊢_{bt}^{+} ⌊w′⌋ : τ_{2}[w′ : φ_{2}] for some w′ ∈ Terms[Λ_{ml}^{bt}].

3. If Γ_{d} ⊢_{bt}^{+} e : τ̃[w : φ̃] then exactly one of the following statements holds:

(a) w ≡ unit w′, e ≡ unit ⌊w′⌋ and Γ ⊢_{bt}^{+} ⌊w′⌋ : τ[w′ : φ] for some w′ ∈ Terms[Λ_{ml}^{bt}], or

(b) w ⟼_{i} w′ and w −̸→_{f} w′′ and Γ_{d} ⊢_{bt}^{+} ⌊w′⌋ : τ̃[w′ : φ̃] and e ≡ ⌊w⌋ ⟶ ⟶_{ml} ⌊w′⌋, or Flattening rules (where x_{1} ∉ FV(w_{3})):

10The current statement of Lemma 3 makes a few format changes and one minor technical correction to the Lemma in the shorter MSCS version of this paper: subcases 3(b)

and 3(c) have been switched, and the condition w −̸→_{f} w′′ has been added to subcase 3(b) to ensure that only one of the subcases of component 3 hold.

let x_{2} ⇐ (\underline{let} x_{1} ⇐ w_{1} \underline{in} w_{2}) in w_{3} ⟼_{f} \underline{let} x_{1} ⇐ w_{1} \underline{in} let x_{2} ⇐ w_{2} in w_{3}

let x_{2} ⇐ (let x_{1} ⇐ w_{1} in w_{2}) in w_{3} ⟼_{f} let x_{1} ⇐ w_{1} in let x_{2} ⇐ w_{2} in w_{3}

\frac{w ⟼_{f} w′}{w ⟼_{s^{+}} w′}

Interpretation rules:

succ ⌜n⌝ ⟼_{i} unit ⌜n + 1⌝
(λx . w_{0}) @ w_{1} ⟼_{i} w_{0}[x := w_{1}]
fix x. w ⟼_{i} w[x := fix x. w]
let x ⇐ unit w_{1} in w_{2} ⟼_{i} w_{2}[x := w_{1}]

pred ⌜n + 1⌝ ⟼_{i} unit ⌜n⌝
pred ⌜0⌝ ⟼_{i} unit ⌜0⌝
if0 ⌜0⌝ w_{2} w_{3} ⟼_{i} w_{2}
if0 ⌜n + 1⌝ w_{2} w_{3} ⟼_{i} w_{3}

\frac{w ⟼_{i} w′}{E_{i}[w] ⟼_{i} E_{i}[w′]}  E_{i} ::= let x ⇐ [·] in w_{2}

\frac{w ⟼_{i} w′}{w ⟼_{s^{+}} w′} where w −̸→_{f} w′′

Compilation rules:

lift ⌜n⌝ ⟼_{s^{+}} \underline{⌜n⌝} \frac{w ⟼_{s^{+}} w′}{E_{s}[w] ⟼_{s^{+}} E_{s}[w′]}

E_{s} ::= \underline{pred} [·] | \underline{succ} [·] | \underline{if0} [·] w_{2} w_{3} | \underline{if0} r_{1} [·] w_{3} | \underline{if0} r_{1} r_{2} [·] |

\underline{λ}x . [·] | [·] \underline{@} w_{1} | r_{0} \underline{@} [·] | \underline{fix} x. [·] |

\underline{unit} [·] | \underline{let} x ⇐ [·] \underline{in} w_{2} |

\underline{let} x ⇐ r_{1} \underline{in} [·] ...where r_{i} ∈ Residual-terms[Λ_{ml}^{bt}]

Figure 10: Modified specialization rules for Λ_{ml}^{bt} (c) w ≡ \underline{let} x ⇐ w_{1} \underline{in} w_{2}, e ≡ let x ⇐ ⌊w_{1}⌋ in ⌊w_{2}⌋, and

Γ_{d} ⊢_{bt}^{+} ⌊w_{1}⌋ : τ̃_{1}[w_{1} : d], Γ_{d}, x:τ_{1}[d] ⊢_{bt}^{+} ⌊w_{2}⌋ : τ̃_{2}[w_{2} : φ̃], for some w_{1}, w_{2} ∈ Terms[Λ_{ml}^{bt}], or

(d) w ⟼_{f} w′ and Γ_{d} ⊢_{bt}^{+} ⌊w′⌋ : τ̃[w′ : φ̃] and e ≡ ⌊w⌋ ⟶ ⟶_{ml} ⌊w′⌋.

4. If Γ_{d} ⊢_{bt}^{+} e : nat[w : d] then exactly one of the following statements holds:

(a) w ∈ Residual-terms[Λ_{ml}^{bt}], or

(b) w ⟼_{s^{+}} w′, Γ_{d} ⊢_{bt}^{+} ⌊w′⌋ : τ[w′ : d], and e ≡ ⌊w⌋ ≡ ⌊w′⌋ ≡ ⌜n⌝ for some number n.

5. If Γ_{d} ⊢_{bt}^{+} e : τ_{1} →τ_{2}[w : d] then exactly one of the following statements holds:

(a) w ∈ Residual-terms[Λ_{ml}^{bt}], or

(b) w ⟼_{s^{+}} w′ and Γ_{d} ⊢_{bt}^{+} ⌊w′⌋ : τ[w′ : d] and e ≡ ⌊w⌋ ⟶ ⟶_{ml} ⌊w′⌋.

6. If Γ_{d} ⊢_{bt}^{+} e : τ̃[w : d] then exactly one of the following statements holds:

(a) w ∈ Residual-terms[Λ_{ml}^{bt}], or

(b) w ⟼_{s^{+}} w′ and Γ_{d} ⊢_{bt}^{+} ⌊w′⌋ : τ̃[w′ : d] and e ≡ ⌊w⌋ ⟶ ⟶_{ml} ⌊w′⌋.

Proof: by induction over the height of the derivation of Γ_{d} ⊢_{bt}^{+} e : τ[w : φ] relying on the property that if both Γ, x:τ_{1}[φ_{1}] ⊢_{bt}^{+} e_{0} : τ_{0}[w_{0} : φ_{0}] and Γ ⊢_{bt}^{+} e_{1} : τ_{1}[w_{1} : φ_{1}] then Γ ⊢_{bt}^{+} e_{0}[x := e_{1}] : τ_{0}[w_{0}[x := w_{1}] : φ_{0}]. See Appendix B for details.

As before, if w ⟼_{s^{+}} w′ and w ⟼_{s^{+}} w′′ then w′ ≡ w′′. The definitions of specialization and partial evaluation as well as the proofs of correctness of binding-time analysis, specialization, and partial evaluation proceed exactly as before.

6 Equivalence with continuation-based specialization

Not only does the incorporation of the let.assoc lead to improved binding times, but the resulting improved specializer captures the essence of controlbased binding-time improvements as found in, e.g., the partial evaluator Similix [7]. To substantiate this claim, we recast Bondorf’s continuationbased specializer [6] in terms of Λ_{ml}, and prove that this specializer is equivalent to the spec^{+} of Section 5.2.2.

Interpretation rules:

⟨ unit w , nil ⟩ ⇓ unit w \frac{⟨ unit ⌜n + 1⌝ , E⃗_{i} ⟩ ⇓ a}{⟨ succ ⌜n⌝ , E⃗_{i} ⟩ ⇓ a}

\frac{⟨ unit ⌜n⌝ , E⃗_{i} ⟩ ⇓ a}{⟨ pred ⌜n + 1⌝ , E⃗_{i} ⟩ ⇓ a}  \frac{⟨ unit ⌜0⌝ , E⃗_{i} ⟩ ⇓ a}{⟨ pred ⌜0⌝ , E⃗_{i} ⟩ ⇓ a}
\frac{⟨ w_{2} , E⃗_{i} ⟩ ⇓ a}{⟨ if0 ⌜0⌝ w_{2} w_{3} , E⃗_{i} ⟩ ⇓ a}  \frac{⟨ w_{3} , E⃗_{i} ⟩ ⇓ a}{⟨ if0 ⌜n + 1⌝ w_{2} w_{3} , E⃗_{i} ⟩ ⇓ a}
\frac{⟨ w_{0}[x := w_{1}] , E⃗_{i} ⟩ ⇓ a}{⟨ (λx . w_{0}) @ w_{1} , E⃗_{i} ⟩ ⇓ a}  \frac{⟨ w[x := fix x. w] , E⃗_{i} ⟩ ⇓ a}{⟨ fix x. w , E⃗_{i} ⟩ ⇓ a}

\frac{⟨ w_{1} , \begin{matrix}let x ⇐ · \\ in & w_{2} \end{matrix} :: E⃗_{i} ⟩ ⇓ a}{⟨ \begin{matrix}let x ⇐ w_{1} \\ in & w_{2} \end{matrix} , E⃗_{i} ⟩ ⇓ a} (Push) x ∉ FV(E⃗_{i})

\frac{⟨ w_{2}[x := w_{1}] , E⃗_{i} ⟩ ⇓ a}{⟨ unit w_{1} , \begin{matrix}let x ⇐ · \\ in & w_{2} \end{matrix} :: E⃗_{i} ⟩ ⇓ a} (Pop)

Figure 11: Continuation-based specializer for Λ_{ml}^{bt} (part 1)

Compilation rules: ⟨ \underline{⌜n⌝} , nil ⟩ ⇓ \underline{⌜n⌝} ⟨ x , nil ⟩ ⇓ x ⟨ lift ⌜n⌝ , nil ⟩ ⇓ \underline{⌜n⌝}

\frac{⟨ w , nil ⟩ ⇓ r}{⟨ \underline{unit} w , nil ⟩ ⇓ \underline{unit} r}
\frac{⟨ w , nil ⟩ ⇓ r}{⟨ \underline{succ} w , nil ⟩ ⇓ \underline{succ} r}  \frac{⟨ w , nil ⟩ ⇓ r}{⟨ \underline{pred} w , nil ⟩ ⇓ \underline{pred} r}
\frac{⟨ w , nil ⟩ ⇓ r}{⟨ \underline{λ}x . w , nil ⟩ ⇓ \underline{λ}x . r}  \frac{⟨ w , nil ⟩ ⇓ r}{⟨ \underline{fix} x. w , nil ⟩ ⇓ \underline{fix} x. r}

\frac{⟨ w_{1} , nil ⟩ ⇓ r_{1} ⟨ w_{2} , nil ⟩ ⇓ r_{2}}{⟨ w_{1} \underline{@} w_{2} , nil ⟩ ⇓ r_{1} \underline{@} r_{2}}

\frac{⟨ w_{1} , nil ⟩ ⇓ r_{1}  ⟨ w_{2} , nil ⟩ ⇓ r_{2}  ⟨ w_{3} , nil ⟩ ⇓ r_{3}}{⟨ \underline{if0} w_{1} w_{2} w_{3} , nil ⟩ ⇓ \underline{if0} r_{1} r_{2} r_{3}}
\frac{⟨ w_{1} , nil ⟩ ⇓ r_{1}  ⟨ w_{2} , E⃗_{i} ⟩ ⇓ r_{2}}{⟨ \underline{let} x ⇐ w_{1} \underline{in} w_{2} , E⃗_{i} ⟩ ⇓ \underline{let} x ⇐ r_{1} \underline{in} r_{2}} (Assoc)  x ∉ FV(E⃗_{i})

Figure 12: Continuation-based specializer for Λ_{ml}^{bt} (part 2)

Figures 11 and 12 present the continuation-based specializer as a big-step operational semantics. Bondorf’s specializer is expressed denotationally, but there are standard techniques for going from a denotational specification to an operational one [53].^{11} The specializer manipulates configurations of the form ⟨ w , E⃗_{i} ⟩ where w ∈ Terms[Λ_{ml}^{bt}] and E⃗_{i} is a stack of interpretation contexts (i.e., E⃗_{i} is a continuation). The intuition is that E⃗_{i} accumulates static contexts (via the (Push) rule) and if possible moves them across dynamic let expressions to consume static values in the let body (via the (Assoc) rule). The (Pop) rule consumes a static value by reducing the top-most let in E⃗_{i}. In dynamic contexts (e.g., in the compilation rules), there is no need to accumulate contexts (i.e., the stack is delimited to be nil — which corresponds to the identity continuation).

The free variable restrictions in the (Push) and (Assoc) rules are analogous to the free variable restrictions on the flattening rules of Figure 10. The following is the fairly obvious extension of the notion of free variables to stacks of interpretation contexts.^{12}

FV(nil) = ∅
FV(\begin{matrix}let x ⇐ · \\ in & w_{2} \end{matrix} :: E⃗_{i}) = (FV(w_{2}) − \{x\}) ∪ FV(E⃗_{i})

Derivations in the continuation-based specializer give rise to context stacks that are well-formed in the following sense.

Definition 7 (well-formed context stack)

• nil is well-formed; and

• \begin{matrix}let x ⇐ · \\ in & w_{2} \end{matrix} :: E⃗_{i} is well-formed if E⃗_{i} is well-formed and x ∉ FV(E⃗_{i}).

11For stylistic reasons we have deviated slightly from Bondorf’s presentation, where all the rules for dynamic constructs are expressed in continuation-passing style, and dynamic contexts are thus accumulated as well. This accumulation, however, is not necessary since continuations are only used to move static contexts across dynamic let expressions. Based on this observation (made during our initial work, in the Fall of 1994), we have written our rules so that components of dynamic constructs (e.g., \underline{if0}) are specialized with respect to the identity continuation (i.e., nil).

12The material from the current paragraph down to the statement of Theorem 5 were omitted from the shorter version of this paper due to space constraints. Also, the free variable constraints on the (Push) (Figure 11) and (Assoc) (Figure 12) rules were not made explicit in the shorter version.

Intuitively, context stacks

E⃗_{i} ≡ \begin{matrix}let x_{1} ⇐ · \\ in & w_{1} \end{matrix} :: ⋯:: \begin{matrix}let x_{n} ⇐ · \\ in & w_{n} \end{matrix} :: nil

in the continuation-based specializer arise from contexts of the form

let x_{n} ⇐ (⋯ let x_{1} ⇐ · in w_{1} ⋯) in w_{n}.

in the term being specialized. As discussed in Section 5, for all i and for all j > i, α-conversion can give x_{i} ∉ FV(w_{j}).

The following property states that continuation-based specialization does indeed give rise to well-formed contexts. We write D ▷ ⟨ w , E⃗_{i} ⟩ ⇓ a when D is a derivation of ⟨ w , E⃗_{i} ⟩ ⇓ a).

Property 2 (well-formed context stacks are preserved) If D ▷ ⟨ w , E⃗_{i} ⟩ ⇓ a and E⃗_{i} is a well-formed context stack, then for all subderivations D′ ▷ ⟨ w′ , E⃗_{i}′ ⟩ ⇓ a′ of D, E⃗_{i}′ is a well-formed context stack.

Proof: by complete induction over the height of D. The only interesting case is the (Push) rule, and the side condition ensures that the property holds for the immediate subderivation.

The following theorem establishes the correspondence between the continuation-based specializer and spec^{+} of Section 5.2.2.

Theorem 5 For Γ_{d} ⊢_{bt}^{+} e : ñat[w : d],

⟨ w , nil ⟩ ⇓ r iff w ⟼_{s^{+}}^{∗} r

Proof: The proof is straightforward and follows the standard pattern for relating a big-step and small-step operational semantics [32, p. 111]. However, one must strengthen the statement to prove so as to handle arbitrary stacks of interpretation contexts in the inductive hypothesis. The full proof is in Appendix B.3.

Bondorf’s presentation [6] did not include a specification of binding-time analysis. However, our connection of continuation-based specialization and spec^{+} shows that the constraints given by Γ ⊢_{bt}^{+} e : τ[w : φ] judgements are the proper ones (appealing to the correctness of binding-time analysis for spec^{+}).

7 Related work

7.1 Computational meta-languages

Moggi introduced his computational metalanguage as a convenient format to specify denotational semantics modularly [48]. This metalanguage has been used for a variety of purposes including treating computational effects in functional languages [24, 31, 47, 63, 66], staging denotational-semantics definitions [12] and compiler translations [3, 36, 60], and explaining relationships between various constructive logics [4]. In an earlier work [34, 36], we have used this metalanguage to formalize the structure of continuationpassing styles.

Inspired by the present work, Nielsen has recently developed an evaluation-order independent presentation of partial evaluation and deforestation using Moggi’s metalanguage [49]. The distinction between values and computations given by the metalanguage type system (upon which we have relied heavily) lies at the foundation of his work as well. This continues a trend of unifying various program-specialization techniques [62]. Clearly Λ_{ml} stands as a promising testbed for this unification.

As noted above, the metalanguage and monads are commonly used to structure functional programs with computational effects. Both Nielsen [49] and Dussart and Thiemann [22] use monads to structure I/O and state in the partial evaluator itself.

Particular aspects of Moggi’s metalanguage highlighted in the present work also appear in other metalanguages. For example, Talcott uses letexpressions to specify computational steps [64]. Sabry and Felleisen demonstrate how a let-based intermediate language (called A-normal forms) can give benefits similar to CPS in dataflow analysis [58, 59].

Moggi also gave a computational λ-calculus λ_{c}. λ_{c} is essentially a call-by-value λ-calculus extended with equations that capture program equivalences holding under arbitrary monadic effects. It is straightforward to adapt our evaluation-order independent presentation based on Λ_{ml} to a call-by-value presentation based on λ_{c}. This alternative presentation expresses controlbased binding-time improvements via the monadic laws as formulated in λ_{c}. The reassociation of let expressions is again a prominent feature. In fact, the λ_{c} presentation has strong connections with the work of Flanagan et al.

[25] on the essence of compiling with continuations.

7.2 Partial evaluation

7.2.1 Styles of specification

The earliest work on partial evaluation as a two-phase process specified binding-time analysis as an abstract interpretation [43]. Since the work of Jones and Gomard [29, 30], binding-time analysis is more often specified using type systems (we have followed this approach in the present work). Palsberg [54] and Wand [68] further clarify the rôle of such specifications in their work on the correctness of binding-time analysis.

Specializers have mostly been specified as symbolic interpreters in functional style [42]. We note, however, a recent trend (including the present work) to use operational semantics for specifying specializers [1, 18, 33, 61, 62]. In fact, the first author has shown that by emphasizing the logical character of type-based and operational semantics specifications, the correctness of a partial evaluator can be mechanically verified [35].

Davies and Pfenning have developed a language for expressing staged computation based on the intuistionistic modal logic S4 [20, 19]. The type system of this language is strikingly similar to that of Moggi’s computational metalanguage. A modality analogous to the ˜· construction of Moggi is used to type code objects (in our terminology, objects whose specialization type is dynamic). Their language also includes a let construct which can act as an “eval function”. However, even though types and terms of both languages are quite similar, the similarity is superficial in the context of our application of the metalanguage. In our setting, staging information is not represented using the modality (as with Davies and Pfenning). Instead it is represented using specialization types which are external to the types of the meta-language itself. In our case, the modality is used to distinguish values from computations — a distinction not captured in Davies and Pfenning’s work. Benton, Bierman, and de Paiva [4] flesh out connections between Moggi’s computational metalanguage and the modal logic S4 in a more general context.

7.2.2 Call unfolding and let insertion

Most specializers ensuring sound call-unfolding under call-by-value adopt the technique of let insertion, as discussed in Section 4. One may, however, also enforce soundness by simply not unfolding calls where the argument expression is dynamic, at the price of reducing specialization. This must be expressed in the binding-time analysis by forbidding binding-times such as d → s (i.e., a static function mapping a dynamic argument into a static result). This restriction in fact also occurs in Nielson and Nielson’s twolevel λ-calculus [52]: the co-domain of a static function should be at least as dynamic as the domain of this function.

In contrast, consider a partial evaluator (e.g., Similix) that (1) ensures sound call-unfolding by let insertion, and (2) performs binding-time improvements by relocating static evaluation contexts inside dynamic let expressions. This partial evaluator does not constrain the domain and the codomain of static (call-by-value) functions. For example, in the term

((λx . 2) @ d) + 1

where d denotes a dynamic integer, the λ-abstraction is classified as a static function mapping a dynamic integer into a static integer (i.e., its binding time is d→s). As a corollary, the addition is classified as static. The residual program reads

let x ⇐ d in 3.

In both techniques above, the possible binding times (i.e., specialization types) are tied to the strategy used to enforce sound call unfolding. A pleasant feature of phrasing partial evaluation in terms of Λ_{ml} is that the characterization of sound call unfolding and possible binding times are orthogonal. The distinction between values and computations in the type system means that static functions with specialization types such as d → s can always be dealt with in a sound manner. It is the encoding into Λ_{ml} where one adopts a technique for a particular evaluation order.

7.2.3 Binding-time improvements

Consel and Danvy observed that a source transformation into continuationpassing style prevented a class of loss of static information across procedures, and they provided a syntactic characterization of this class [10]. Holst and Gomard observed that part of the same effect (intra-procedural and insensitive to call unfolding) could be obtained by “flattening” each source procedure [39]. Bondorf, Danvy, and Lawall observed that a further part of the same effect (accounting for call unfolding, but not crossing specialization points) could be obtained by specific control operations in the specializer itself [6, 45], rather than by CPS-transforming the program before partial evaluation. Our framework achieves this effect by extending the operational semantics of specialization with the let.assoc rule. This development matches contemporary work on determining the effect of the CPS transformation on flow analysis [51, 59]: enriching a direct-style calculus can yield analyses with an added precision that matches the extra precision obtained by the relocation of contexts performed by the CPS transformation.

Section 6 shows how the theory of monads captures the essence of controlbased binding-time improvements. This has practical benefits as well — it allows one to avoid using a functional representation of continuations in the specializer (one need only use the let.assoc rule). The disadvantage of representing continuations as functions shows up in a self-applicable partial evaluator, as self-application generates programs with many higher-order functions. Such programs are more difficult to reason about, e.g., when searching for binding-time improvements. This difficulty motivated Lawall and Danvy to stick to direct style [45], and Glück and Jørgensen to devise a multi-level cogen [27]. Thiemann has united both lines of work [65]. In the present case, and since continuation-passing style can be obtained from monadic style by simply selecting (a term representation of) the continuation monad, our method provides sound guidelines for treating continuations in an offline partial evaluator.

We also expect our technique to be particularly useful in online selfapplicable program specializers (e.g., supercompilers). In fact, preliminary work by the first author and Glück on online self-application uses a language called Sgraph [28] where let-bindings (in the style of Λ_{ml}) are a central feature [37].

Let us briefly attempt a taxonomy of continuation-based partial evaluators. The earliest one is reported in the literature by Bondorf [6]. Its goal is precisely to relocate static contexts across dynamic let expressions, as in the CPS transformation. The particular brand of continuation-passing style used for this relocation is expressible in direct style, using control operators (again as in the CPS transformation). In fact, this direct-style specializer turns out to be more efficient in practice [45]. A parallel development is taking place in the “cogen” approach to partial evaluation [8, 46, 65]. All these continuation-based specializers are specified as symbolic interpreters in functional style. An increasing number of specializers, however, are specified operationally. We have presented here such a specializer, which is continuation-based and delimits control to static contexts. This novel feature can be observed to be rippling back into the world of functional specializers, both with explicit continuations and with implicit continuations and the associated control operators [21].

As for data-flow binding-time improvements, they arise from insufficient binding-time coercions [17, 18]. In particular, the binding-time improvement arising from the presence of booleans and disjoint sums is known as “The Trick” [18, 42]. Because of the nature of disjoint sums, this coercion takes the form of a control-based binding-time improvement: The Trick amounts to duplicating static contexts across dynamic case expressions. Again, continuations can be used to move static contexts across dynamic conditional expressions, duplicating them in the conditional branches. This transformation, however, can also be naturally accomplished using the computational meta-language [36]. It gives rise to an analogue of Figure 9 for if0, and to a context duplication in Figure 12. It is interesting to note (this observation is due to Malmkjær) that if we consider a let expression as a “unary” case expression (i.e., a case expression with one conditional branch), then our let-rearranging rules coincide with the case-rearranging rules (also known as commuting conversions) that can be found both in partial evaluation [18], program extraction [55], and natural-deduction proof theory [26, 57].

7.2.4 Evaluation-order independence

We have formulated control-based binding-time improvements via monads using the computational meta-language because it allows an evaluationorder independent view of binding-time analysis and specialization. This appears particularly useful in settings where adopting mixed evaluation strategies (e.g., call-by-name and call-by-value) can be employed to enhance efficiency [16]. In addition, Nielsen and Sørensen have identified situations where transforming sections of call-by-value programs using the call-by-name CPS transformation can increase specialization [50]. The evaluationorder independent partial-evaluation strategy that we have given here seems well-suited for this endeavour since Λ_{ml} allows one to encode mixed evaluation strategies while remaining in direct style [34].

8 Conclusion

Partial evaluation offers a practical way of staging the execution of programs in order to adapt them to the context of their execution. We have identified Moggi’s computational metalanguage as a useful intermediate language for formalizing it. As a first step, we have formalized binding-time analysis and program specialization. Then we have shown how the intermediate language captures the essence of control-based binding-time improvements. Other work gives evidence that the metalanguage can provide an avenue for

e ∈ Terms[Λ]
e ::= x | f | ⌜n⌝ | succ e | pred e |

if0 e_{1} e_{2} e_{3} | λx:τ . e | e_{0} @ e_{1} | fix f:τ. e

x ∈ Identifiers[Λ]
f ∈ RecIdentifiers[Λ]
τ ∈ Types[Λ]
τ ::= nat | τ_{1} →τ_{2}
Γ ∈ Assumptions[Λ]
Γ ::= · | Γ, x:τ | Γ, f:τ

Figure 13: The language Λ

(a) incorporating other computational effects into partial evaluation such as I/O and state, and (b) unifying various program-specialization techniques.

Acknowledgements

Thanks are due to Karoline Malmkjær for comments on an earlier version of this paper, and to the anonymous referees for their perceptive reviews.

Most of this work was carried out while the first author was visiting the University of Copenhagen (DIKU), and we thank the DIKU TOPPS group for their interaction, encouragement, and financial support, e.g., to attend LDPL’95 in Darmstadt, Germany.

A The Language Λ

A.1 Syntax

Figure 13 presents the syntax of a PCF-like language Λ. We omit the usual typing rules as well as the call-by-name and call-by-value operational semantics for Λ.

The syntax of Λ includes two categories of identifiers: Identifiers are used in λ-bindings; RecIdentifiers are used in fix-bindings. This distinction is necessary under call-by-value evaluation of Λ, where Identifiers will only bind to canonical terms (i.e., values) whereas RecIdentifiers may bind to non-canonical terms (i.e., computations). This is reflected in the formal definition of values below.

Definition 8 (Values)

\begin{aligned}v & ∈ & Values_{n}[Λ] \\ v & ::= & ⌜n⌝ | λx . e \end{aligned}  \begin{aligned}v & ∈ & Values_{v}[Λ] \\ v & ::= & x | ⌜n⌝ | λx . e \end{aligned}

A.2 Encoding Λ evaluation in Λ_{ml}

Figures 14 and 15 give the call-by-name and call-by-value encodings of Λ in Λ_{ml}. In the call-by-name encoding, function arguments are passed unevaluated. This is reflected in the transformation on types, i.e., functions map computations to computations. In the call-by-value encoding, evaluation of function arguments is forced using the let construct. This is reflected in the transformation on types, i.e., functions map values to computations.^{13}

B Proofs

B.1 Properties of partial evaluation

The section gives the proofs for various partial evaluation properties and theorems occuring in Sections 3 and 4. We begin by considering various properties needed for the proof of Lemma 2 of Section 3.

Property 3 (substitution and binding-time constraints) If Γ, x:τ_{1}[φ_{1}] ⊢_{bt} e_{0} : τ_{0}[w_{0} : φ_{0}] and Γ ⊢_{bt} e_{1} : τ_{1}[w_{1} : φ_{1}] then

Γ ⊢_{bt} e_{0}[x := e_{1}] : τ_{0}[w_{0}[x := w_{1}] : φ_{0}].

Proof: The proof is a simple induction over the derivation of Γ, x:τ_{1}[φ_{1}] ⊢_{bt} e_{0} : τ_{0}[w_{0} : φ_{0}] and is omitted.

13One can also give a call-by-value encoding where functions map computations to computations. Instead of forcing evaluation of function arguments in the application structure (as in E_{v}), evaluation is forced immediately after an argument is received by a function [36].

E_{n}⟨[·]⟩ : Λ→Λ_{ml}
E_{n}⟨[v]⟩ = unit E_{n}⟨v⟩
E_{n}⟨[x]⟩ = x
E_{n}⟨[f]⟩ = f
E_{n}⟨[succ e]⟩ = let y ⇐ E_{n}⟨[e]⟩ in succ y
E_{n}⟨[pred e]⟩ = let y ⇐ E_{n}⟨[e]⟩ in pred y
E_{n}⟨[if0 e_{0} e_{1} e_{2}]⟩ = let y_{0} ⇐ E_{n}⟨[e_{0}]⟩ in if0 y_{0} E_{n}⟨[e_{1}]⟩ E_{n}⟨[e_{2}]⟩
E_{n}⟨[e_{0} @ e_{1}]⟩ = let y_{0} ⇐ E_{n}⟨[e_{0}]⟩ in y_{0} @ E_{n}⟨[e_{1}]⟩
E_{n}⟨[fix f. e]⟩ = fix f. E_{n}⟨[e]⟩
E_{n}⟨·⟩ : Values_{n}[Λ]→Λ_{ml}
E_{n}⟨⌜n⌝⟩ = ⌜n⌝
E_{n}⟨λx . e⟩ = λx . E_{n}⟨[e]⟩
E_{n}⟨nat⟩ = nat
E_{n}⟨τ_{1} →τ_{2}⟩ = E_{n}⟨[τ_{1}]⟩→E_{n}⟨[τ_{2}]⟩
E_{n}⟨[τ]⟩ = { \atop E_{n}⟨τ⟩}
E_{n}⟨[Γ, x:τ]⟩ = E_{n}⟨[Γ]⟩, x:E_{n}⟨[τ]⟩
E_{n}⟨[Γ, f:τ]⟩ = E_{n}⟨[Γ]⟩, f:E_{n}⟨[τ]⟩

Figure 14: Call-by-name encoding E_{n} into Λ_{ml}

E_{v}⟨[·]⟩ : Λ→Λ_{ml}
E_{v}⟨[v]⟩ = unit E_{v}⟨v⟩
E_{v}⟨[f]⟩ = f
E_{v}⟨[succ e]⟩ = let y ⇐ E_{v}⟨[e]⟩ in succ y
E_{v}⟨[pred e]⟩ = let y ⇐ E_{v}⟨[e]⟩ in pred y
E_{v}⟨[if0 e_{0} e_{1} e_{2}]⟩ = let y_{0} ⇐ E_{v}⟨[e_{0}]⟩ in if0 y_{0} E_{v}⟨[e_{1}]⟩ E_{v}⟨[e_{2}]⟩
E_{v}⟨[e_{0} @ e_{1}]⟩ = let y_{0} ⇐ E_{v}⟨[e_{0}]⟩ in let y_{1} ⇐ E_{v}⟨[e_{1}]⟩ in y_{0} @ y_{1}
E_{v}⟨[fix f. e]⟩ = fix f. E_{v}⟨[e]⟩
E_{v}⟨·⟩ : Values_{v}[Λ]→Λ_{ml}
E_{v}⟨⌜n⌝⟩ = ⌜n⌝
E_{v}⟨x⟩ = x
E_{v}⟨λx . e⟩ = λx . E_{v}⟨[e]⟩
E_{v}⟨nat⟩ = nat
E_{v}⟨τ_{1} →τ_{2}⟩ = E_{v}⟨τ_{1}⟩→E_{v}⟨[τ_{2}]⟩
E_{v}⟨[τ]⟩ = { \atop E_{v}⟨τ⟩}
E_{v}⟨[Γ, x:τ]⟩ = E_{v}⟨[Γ]⟩, x:E_{v}⟨τ⟩
E_{v}⟨[Γ, f:τ]⟩ = E_{v}⟨[Γ]⟩, f:E_{v}⟨[τ]⟩

Figure 15: Call-by-value encoding E_{v} into Λ_{ml} Property 4 (substitution and erasing) For all w_{0}, w_{1} ∈ Terms[Λ_{ml}^{bt}],

⌊w_{0}[x := w_{1}]⌋ ≡ ⌊w_{0}⌋[x := ⌊w_{1}⌋]

Proof: The proof is a simple induction over the structure of w_{0} and is omitted.

Proof of Lemma 2: The proof is by induction over the derivation of Γ_{d} ⊢_{bt} e : τ[w : φ]. We give illustrative cases. Note that for residual constructs, the desired properties follow directly from the IH. The case for \underline{succ} w below illustrates this.

Recall that given Γ ⊢_{bt} e : τ[w : φ], e ≡ ⌊w⌋ (see Section 3). We use this property often without giving explicit reference in the proof below.

case Γ_{d} ⊢_{bt} x : Γ(x).type[x : Γ(x).spec-type]:

We must have Γ(x).spec-type ≡ d since Γ_{d} contains only dynamic variables. It is possible that cases 4, 5, and 6 of Lemma 2 apply. But in each case, the conditions are satisfied since x ∈ Residual-terms[Λ_{ml}^{bt}] (because x is dynamic) by definition of Residual-terms[Λ_{ml}^{bt}], and x cannot undergo a specialization step.

case Γ_{d} ⊢_{bt} ⌜n⌝ : nat[⌜n⌝ : s]:

Immediate.

case Γ_{d} ⊢_{bt} ⌜n⌝ : nat[\underline{⌜n⌝} : d]:

Case 4 applies and since \underline{⌜n⌝} ∈ Residual-terms[Λ_{ml}^{bt}] and \underline{⌜n⌝} cannot undergo a specialization step, the conditions are satisfied.

case Γ_{d} ⊢_{bt} succ e : ñat [succ w : s̃] because Γ_{d} ⊢_{bt} e : nat[w : s]:

Case 3 applies. Since subcase 3(a) cannot hold, we show that subcase 3(b) holds. By IH, w ≡ ⌜n⌝ and thus succ ⌜w⌝ ⟼_{i} unit ⌜n + 1⌝. Since we have Γ_{d} ⊢_{bt} ⌊unit ⌜n + 1⌝⌋ : ñat [unit ⌜n + 1⌝ : s̃] and we also have succ ⌜n⌝ ≡ ⌊succ ⌜n⌝⌋ ⟶ ⟶_{ml} ⌊unit ⌜n + 1⌝⌋, the conditions of subcase 3(b) are satisfied.

case Γ_{d} ⊢_{bt} succ e : ñat [\underline{succ} w : d] because Γ_{d} ⊢_{bt} e : nat[w : d]:

Case 6 applies, and by IH either subcase 4(a) or subcase 4(b) holds for w. case 4(a): Then w ∈ Residual-terms[Λ_{ml}^{bt}] and w cannot undergo a specialization step. The conditions of 6(a) are satisfied since \underline{succ} w ∈ Residual-terms[Λ_{ml}^{bt}] and note \underline{succ} w cannot undergo a specialization step. case 4(b): Then w ⟼_{s} w′, Γ_{d} ⊢_{bt} ⌊w′⌋ : τ[w′ : d], and e ≡ ⌊w′⌋ ≡ ⌊w⌋ ≡ ⌜n⌝ for some number n. Since we have \underline{succ} w ⟼_{s} \underline{succ} w′, Γ_{d} ⊢_{bt} ⌊\underline{succ} w′⌋ : ñat [\underline{succ} w′ : d], and succ e ≡ ⌊\underline{succ} w⌋ ⟶ ⟶_{ml} ⌊\underline{succ} w′⌋, the conditions of 6(b) are satisfied.

case Γ_{d} ⊢_{bt} λx . e′ : τ_{1} →τ̃_{2}[λx . w′ : φ_{1} →φ_{2}] because Γ_{d}, x:τ_{1}[φ_{1}] ⊢_{bt} e′ : τ̃_{2}[w′ : φ_{2}]:

Case 2 applies and the conditions are satisfied since w ≡ λx . w′, e ≡ ⌊λx . w′⌋ ≡ λx . ⌊w′⌋ ≡ λx . e′ (by properties of ⌊·⌋ — see Section 3.1.3), and Γ_{d}, x:τ_{1}[φ_{1}] ⊢_{bt} ⌊w′⌋ : τ_{2}[w′ : φ_{2}] — where w and e are as defined in Lemma 2 case 2.

case Γ_{d} ⊢_{bt} e_{0} @ e_{1} : τ̃_{2}[w_{0} @ w_{1} : φ_{2}] because Γ_{d} ⊢_{bt} e_{0} : τ_{1} →τ̃_{2}[w_{0} : φ_{1} →φ_{2}] and Γ ⊢_{bt} e_{1} : τ_{1}[w_{1} : φ_{1}]:

It follows from the relationship between types and specialization types (see Figure 5) that either φ_{2} ≡ φ̃′_{2} (i.e., case 3 applies), or φ_{2} ≡ d (i.e., case 6 applies).

Case 3: Note subcase 3(a) cannot hold, so we show subcase 3(b) holds. By IH, w_{0} ≡ λx . w′_{0}, e_{0} ≡ ⌊λx . w′_{0}⌋ ≡ λx . ⌊w′_{0}⌋, and Γ_{d}, x:τ_{1}[φ_{1}] ⊢_{bt} ⌊w′_{0}⌋ : τ_{2}[w′_{0} : φ_{2}]. Now (λx . w′_{0}) @ w_{1} ⟼_{i} w′_{0}[x := w_{1}] and Γ_{d} ⊢_{bt} ⌊w′_{0}⌋[x := e_{1}] : τ_{2}[w′_{0}[x := w_{1}] : φ_{2}] by Property 3. Finally,

e_{0} @ e_{1} \begin{matrix}≡ ⌊(λx . w′_{0}) @ w_{1}⌋ \\ ≡ (λx . ⌊w′_{0}⌋) @ ⌊w_{1}⌋ \end{matrix}
⟶_{ml}
⌊w′_{0}⌋[x := ⌊w_{1}⌋] ≡ ⌊w′_{0}[x := w_{1}]⌋

where the last identity follows by Property 4. Thus, the conditions of subcase 3(b) are satisfied.

Case 6:

Note subcase 6(a) cannot hold since w_{0} @ w_{1} is not residual. To show subcase 6(b) holds, one follows exactly the steps used to show subcase 3(b) above.

case Γ_{d} ⊢_{bt} fix x. e : τ̃[fix x. w : φ̃] because Γ_{d}, x:τ̃[φ̃] ⊢_{bt} e : τ̃[w : φ̃]:

Case 3 applies, and since subcase 3(a) cannot hold, we only need to show that subcase 3(b) holds. We have fix x. w ⟼_{i} w[x := fix x. w] and Γ_{d} ⊢_{bt} e[x := fix x. e] : τ̃[w[x := fix w. w] : φ̃] by Property 3. Finally, fix x. e ≡ ⌊fix x. w⌋ ≡ fix x. ⌊w⌋ and fix x. ⌊w⌋ ⟶_{ml} ⌊w⌋[x := fix x. ⌊w⌋] ≡ ⌊w[x := fix x. w]⌋ where the last identity follows by Property 4. Thus, the conditions of subcase 3(b) are satisfied.

case Γ_{d} ⊢_{bt} let x ⇐ e_{1} in e_{2} : τ̃_{2}[let x ⇐ w_{1} in w_{2} : φ_{2}] because Γ_{d} ⊢_{bt} e_{1} : τ̃_{1}[w_{1} : φ̃_{1}] and Γ_{d}, x:τ_{1}[φ_{1}] ⊢_{bt} e_{2} : τ̃_{2}[w_{2} : φ_{2}]:

It follows from the relationship between types and specialization types (see Figure 5) that either φ_{2} ≡ φ̃′_{2} (i.e., case 3 applies), or φ_{2} ≡ d (i.e., case 6 applies).

Case 3:

Note subcase 3(a) cannot hold, so we show subcase 3(b) holds. By IH, case 3 applies for w_{1}. Case 3(a) for w_{1}: Then w_{1} ≡ unit w′_{1}, e_{1} ≡ unit ⌊w′_{1}⌋ and Γ_{d} ⊢_{bt} ⌊w′_{1}⌋ : τ_{1}[w′_{1} : φ_{1}]. Now let x ⇐ unit w′_{1} in w_{2} ⟼_{i} w_{2}[x := w′_{1}] and Γ_{d} ⊢_{bt} ⌊w_{2}⌋[x := ⌊w′_{1}⌋] : τ̃_{2}[w′_{0}[x := w_{1}] : φ_{2}] by Property 3. Finally,

let x ⇐ e_{1} in e_{2} ≡ ⌊let x ⇐ unit w′_{1} in w_{2}⌋
≡ let x ⇐ unit ⌊w′_{1}⌋ in ⌊w_{2}⌋
⟶ ⟶_{ml}
⌊w_{2}⌋[x := ⌊w′_{1}⌋] ≡ ⌊w_{2}[x := w′_{1}]⌋

where the last identity follows by Property 4. Thus, the conditions of subcase 3(b) are satisfied. Case 3(b) for w_{1}:

Then w_{1} ⟼_{i} w′_{1} and Γ_{d} ⊢_{bt} ⌊w′_{1}⌋ : τ̃_{1}[w′_{1} : φ̃_{1}] and e_{1} ≡ ⌊w_{1}⌋ ⟶_{ml} ⌊w′_{1}⌋. Therefore, let x ⇐ w_{1} in w_{2} ⟼_{i} let x ⇐ w′_{1} in w_{2} and Γ_{d} ⊢_{bt} let x ⇐ ⌊w′_{1}⌋ in e_{2} : τ̃_{2}[let x ⇐ w′_{1} in w_{2} : φ_{2}] and

let x ⇐ e_{1} in e_{2} ≡ ⌊let x ⇐ w_{1} in w_{2}⌋
≡ let x ⇐ ⌊w_{1}⌋ in ⌊w_{2}⌋
⟶ ⟶_{ml}
let x ⇐ ⌊w′_{1}⌋ in ⌊w_{2}⌋ ≡ ⌊let x ⇐ w′_{1} in w_{2}⌋.

Thus, the conditions of subcase 3(b) are satisfied. Case 6: Note subcase 6(a) cannot hold since let x ⇐ w_{1} in w_{2} is not residual. To show subcase 6(b) holds, one follows exactly the steps used to show subcase 3(b) above.

case Γ_{d} ⊢_{bt} e : nat[lift w : d] because Γ_{d} ⊢_{bt} e : nat[w : s]:

Case 4 applies, and note that subcase 4(a) cannot hold since lift w is not residual. So we show that subcase 4(b) holds. By IH, case 1 applies to w, and therefore w ≡ ⌜n⌝ ≡ e for some number n. Now lift ⌜n⌝ ⟼_{s} \underline{⌜n⌝} and Γ_{d} ⊢_{bt} ⌜n⌝ : nat[\underline{⌜n⌝} : d] and e ≡ ⌊lift ⌜n⌝⌋ ≡ ⌊\underline{⌜n⌝}⌋ ≡ ⌜n⌝.

We now give the proof of Theorem 2 which establishes the correctness of the binding-time analysis constraints.

Proof of Theorem 2: Clearly, either spec w↓ or spec w↑.

Case spec w↓:

By the definition of spec, there exists an r ∈ Residual-terms[Λ_{ml}^{bt}] such that spec w = r.

Case spec w↑: In this case we have two possibilities.

1. For all w′ such that w ⟼_{s}^{∗} w′, there exists a w′′ such that w′ ⟼_{s} w′′ (i.e., w heads an infinite series of specialization steps).

2. There exists an a ∉ Residual-terms[Λ_{ml}^{bt}] such that w ⟼_{s}^{∗} a and there does not exist an a′ such that a ⟼_{s} a′. However, this cannot be the case since by induction over the number of steps in w ⟼_{s}^{∗} a, Lemma 2 tells up that either a ∈ Residual-terms[Λ_{ml}^{bt}] or a ⟼_{s} a′ for some a′.

Given Lemma 2, the correctness of binding-time analysis (Theorem 2), and the soundness of specialization (Theorem 3), we can now establish the correctness of partial evaluation (Theorem 4).

Proof of Theorem 4:

Assume (pe e Γ_{bt} σ_{s})↓. The definition of partial evaluation (Definition 6) implies that spec (bta Γ_{bt} e)σ_{s}↓.

By definition of binding-time analysis (Definition 4), we have

Γ_{bt} = Γ_{s} ∪ Γ_{d} ⊢_{bt} e : ñat[(bta Γ_{bt} e) : d]

and by repeated application of Property 3 (substitution and binding-time constraints),

Γ_{d} ⊢_{bt} e⌊σ_{s}⌋ : ñat[(bta Γ_{bt} e)σ_{s} : d].

Now since spec (bta Γ_{bt} e)σ_{s}↓, by induction on the number of specialization steps (applying Lemma 2), we have

e⌊σ_{s}⌋ =_{ml} ⌊spec (bta Γ_{bt} e)σ_{s}⌋.

We can now reason as follows.

e⌊σ_{s}⌋ =_{ml} ⌊spec (bta Γ_{bt} e)σ_{s}⌋
⇒ e⌊σ_{s}⌋σ_{d} =_{ml} ⌊spec (bta Γ_{bt} e)σ_{s}⌋σ_{d}

...by substitutivity of ml

⇒ e⌊σ_{s}⌋σ_{d} =_{ml} pe e Γ_{bt} σ_{s}σ_{d}

...by definition of pe (Definition 6)

⇒ e⌊σ_{s}⌋σ_{d} ≈ pe e Γ_{bt} σ_{s}σ_{d}

...by soundness of ml (Theorem 1)

B.2 Control-based binding-time improvements

The section gives the proofs for various partial evaluation properties and theorems occuring in Sections 5. As before, we need a simple property showing how substitution interacts with the extended binding-time rules.

Property 5 (substitution and binding-time constraints) If Γ, x:τ_{1}[φ_{1}] ⊢_{bt}^{+} e_{0} : τ_{0}[w_{0} : φ_{0}] and Γ ⊢_{bt}^{+} e_{1} : τ_{1}[w_{1} : φ_{1}] then

Γ ⊢_{bt}^{+} e_{0}[x := e_{1}] : τ_{0}[w_{0}[x := w_{1}] : φ_{0}].

Proof: The proof is a simple induction over the derivation of Γ, x:τ_{1}[φ_{1}] ⊢_{bt}^{+} e_{0} : τ_{0}[w_{0} : φ_{0}] and is omitted.

Proof of Lemma 3: The proof is by induction over the derivation of Γ_{d} ⊢_{bt}^{+} e : τ[w : φ]. Note that only component 3 of Lemma 3 differs from the previously proven Lemma 2. Therefore we need only rework the cases to which component 3 applies and the cases that rely on component 3 in the inductive hypothesis.

Component 3 applies to cases where the resulting annotated terms include succ w, pred w, w_{0} @ w_{1} (subcase 3(b) applies), and unit w (subcase 3(a) applies). In these cases, the proof is exactly the same as for Lemma 2. Component 3 also applies to let x ⇐ w_{1} in w_{2}. This case must be reworked since it may now satisfy subcase 3(b) or subcase 3(d). In addition, the case \underline{let} x ⇐ w_{1} \underline{in} w_{2} can now fall under component 3 whereas in Lemma 2 it could not.

case Γ_{d} ⊢_{bt}^{+} let x ⇐ e_{1} in e_{2} : τ̃_{2}[let x ⇐ w_{1} in w_{2} : φ_{2}] because Γ_{d} ⊢_{bt}^{+} e_{1} : τ̃_{1}[w_{1} : φ̃_{1}] and Γ_{d}, x:τ_{1}[φ_{1}] ⊢_{bt}^{+} e_{2} : τ̃_{2}[w_{2} : φ_{2}]:

It follows from the relationship between types and specialization types (see Figure 5) that either φ_{2} ≡ φ̃′_{2} (i.e., case 3 applies), or φ_{2} ≡ d (i.e., case 6 applies).

Case 3:

Note neither subcase 3(a) nor 3(c) can hold, so we show subcase 3(b) holds or 3(d) holds. By IH, case 3 applies for w_{1}. Case 3(a) for w_{1}: (proceeding identically to the proof of Lemma 2).

Then w_{1} ≡ unit w′_{1}, e_{1} ≡ unit ⌊w′_{1}⌋ and Γ_{d} ⊢_{bt}^{+} ⌊w′_{1}⌋ : τ_{1}[w′_{1} : φ_{1}]. Now let x ⇐ unit w′_{1} in w_{2} ⟼_{i} w_{2}[x := w′_{1}] and Γ_{d} ⊢_{bt}^{+} ⌊w_{2}⌋[x := ⌊w′_{1}⌋] : τ̃_{2}[w′_{0}[x := w_{1}] : φ_{2}] by Property 5. Finally,

let x ⇐ e_{1} in e_{2} ≡ ⌊let x ⇐ unit w′_{1} in w_{2}⌋
≡ let x ⇐ unit ⌊w′_{1}⌋ in ⌊w_{2}⌋
⟶ ⟶_{ml}
⌊w_{2}⌋[x := ⌊w′_{1}⌋] ≡ ⌊w_{2}[x := w′_{1}]⌋

where the last identity follows by Property 4. Thus, the conditions of subcase 3(b) are satisfied. Case 3(b) for w_{1}: If w_{1} ≢ let y ⇐ w_{3} in w_{4} then the proof proceeds as in Lemma 2. That is, w_{1} ⟼_{i} w′_{1}, Γ_{d} ⊢_{bt}^{+} ⌊w′_{1}⌋ : τ̃_{1}[w′_{1} : φ̃_{1}] and e_{1} ≡ ⌊w_{1}⌋ ⟶_{ml} ⌊w′_{1}⌋. Therefore, let x ⇐ w_{1} in w_{2} ⟼_{i} let x ⇐ w′_{1} in w_{2} and Γ_{d} ⊢_{bt}^{+} let x ⇐ ⌊w′_{1}⌋ in e_{2} : τ̃_{2}[let x ⇐ w′_{1} in w_{2} : φ_{2}] and

let x ⇐ e_{1} in e_{2} ≡ ⌊let x ⇐ w_{1} in w_{2}⌋
≡ let x ⇐ ⌊w_{1}⌋ in ⌊w_{2}⌋
⟶ ⟶_{ml}
let x ⇐ ⌊w′_{1}⌋ in ⌊w_{2}⌋ ≡ ⌊let x ⇐ w′_{1} in w_{2}⌋.

Thus, the conditions of subcase 3(b) are satisfied. If w_{1} ≡ let y ⇐ w_{3} in w_{4}, then we show that the conditions of subcase 3(d) are satisfied. First of all, note that only subcase 3(d) can be satisfied since the resulting term must undergo a flattening step. We have

let x ⇐ (let y ⇐ w_{3} in w_{4}) in w_{2} ⟼_{f} let y ⇐ w_{3} in \begin{matrix}let x ⇐ w_{4} \\ in & w_{2} \end{matrix}

Now Γ_{d}, x:τ_{1}[φ_{1}] ⊢_{bt}^{+} e_{2} : τ̃_{2}[w_{2} : φ_{2}] and it follows that Γ_{d}, y:τ_{3}[φ_{3}], x:τ_{1}[φ_{1}] ⊢_{bt}^{+} e_{2} : τ̃_{2}[w_{2} : φ_{2}] since y ∉ FV(w_{2}). Now we also have Γ_{d}, y:τ_{3}[φ_{3}] ⊢_{bt}^{+} ⌊w_{4}⌋ : τ̃_{1}[w_{4} : φ̃_{1}]. From this we have

Γ_{d}, y:τ_{3}[φ_{3}] ⊢_{bt}^{+} let x ⇐ ⌊w_{4}⌋ in ⌊w_{2}⌋ : τ̃_{2}[let x ⇐ w_{4} in w_{2} : φ_{2}].

Furthermore,

Γ_{d} ⊢_{bt}^{+} let y ⇐ ⌊w_{3}⌋ in \begin{matrix}let x ⇐ ⌊w_{4}⌋ \\ in & ⌊w_{2}⌋ \end{matrix} : τ̃_{2}[let y ⇐ w_{3} in let x ⇐ w_{4} in w_{2} : φ_{2}].

Now

let x ⇐ (let y ⇐ e_{3} in e_{4}) in e_{2}
≡ ⌊let x ⇐ (let y ⇐ w_{3} in w_{4}) in w_{2}⌋
≡ let x ⇐ (let y ⇐ ⌊w_{3}⌋ in ⌊w_{4}⌋) in ⌊w_{2}⌋
⟶ ⟶_{ml} let y ⇐ ⌊w_{3}⌋ in let x ⇐ ⌊w_{4}⌋ in ⌊w_{2}⌋
≡ ⌊let y ⇐ w_{3} in let x ⇐ w_{4} in w_{2}⌋

Thus, the conditions of subcase 3(d) are satisfied.

Case 3(c) for w_{1} (i.e., w_{1} ≡ \underline{let} y ⇐ w_{3} \underline{in} w_{4}) and case 3(d) for w_{1} (i.e., w_{1} ≡ let y ⇐ w_{3} in w_{4}): In either of these cases, let x ⇐ w_{1} in w_{2} must undergo a flattening step and the proof proceeds as in the case above (i.e., the conditions of subcase 3(d) are satisfied).

Case 6:

Note subcase 6(a) cannot hold since let x ⇐ w_{1} in w_{2} is not residual. To show subcase 6(b) holds, one follows exactly the steps used to show subcase 3(b) or 3(d) for let x ⇐ w_{1} in w_{2} above.

case Γ_{d} ⊢_{bt}^{+} let x ⇐ e_{1} in e_{2} : τ̃_{2}[\underline{let} x ⇐ w_{1} \underline{in} w_{2} : φ_{2}] because Γ_{d} ⊢_{bt}^{+} e_{1} : τ̃_{1}[w_{1} : d] and Γ_{d}, x:τ_{1}[d] ⊢_{bt}^{+} e_{2} : τ̃_{2}[w_{2} : φ_{2}]:

It follows from the relationship between types and specialization types (see Figure 5) that either φ_{2} ≡ φ̃′_{2} (i.e., case 3 applies), or φ_{2} ≡ d (i.e., case 6 applies). If case 6 applies, the we are essentially treating the “unextended” form of the binding time rule for residual let’s — the proof proceeds as in Lemma 2. If case 3 applies, then it is immediately obvious that the conditions for subcase 3(c) (and only this subcase) are satisfied.

B.3 Equivalence with continuation-based specialization

This section proves Theorem 5, which establishes the equivalence of the specializer with flattening rules of Section 5 and the continuation-based specializer of Section 6. This requires showing that

1. specialization using the flattening specializer entails a corresponding continuation-based specialization, i.e.,

w ⟼_{s^{+}}^{∗} r implies ⟨ w , nil ⟩ ⇓ r

2. specialization using the continuation-based specializer entails a corresponding flattening specialization, i.e.,

⟨ w , nil ⟩ ⇓ r implies w ⟼_{s^{+}}^{∗} r.

In what follows, we refer to the above statements as part (1) and part (2) of Theorem 4. We treat part (1), and begin by establishing several preliminary properties.

The property below states that the specialization of an already flat interpretation context is equivalent the specialization of the corresponding non-flat interpretation context (which gets flattened by the specializer).

Property 6 (context stack splitting) For all x_{1}, x_{2}, w, w_{2}, w_{3} ∈ Terms[Λ_{ml}^{bt}] and context stacks E⃗_{i}_{1}, E⃗_{i}_{2} such that E⃗_{i}_{1} ++ (\begin{matrix}let x_{1} ⇐ · \\ in & \begin{matrix}let x_{2} ⇐ w_{2} \\ in & w_{3} \end{matrix} \end{matrix} :: E⃗_{i}_{2}) is a well-formed context stack, and x_{1} ∉

FV(w_{3}), x_{2} ∉ FV(E⃗_{i}_{2}), then

(a) ⟨ w , E⃗_{i}_{1} ++ (\begin{matrix}let x_{1} ⇐ · \\ in & \begin{matrix}let x_{2} ⇐ w_{2} \\ in & w_{3} \end{matrix} \end{matrix} :: E⃗_{i}_{2}) ⟩ ⇓ a

iff

⟨ w , E⃗_{i}_{1} ++ (\begin{matrix}let x_{1} ⇐ · \\ in & w_{2} \end{matrix} :: \begin{matrix}let x_{2} ⇐ · \\ in & w_{3} \end{matrix} :: E⃗_{i}_{2}) ⟩ ⇓ a

(b) E⃗_{i}_{1} ++ (\begin{matrix}let x_{1} ⇐ · \\ in & w_{2} \end{matrix} :: \begin{matrix}let x_{2} ⇐ · \\ in & w_{3} \end{matrix} :: E⃗_{i}_{2}) is a well-formed context stack.

Proof: Part (b) follows immediately from the preconditions and the definition of well-formed context stack. For part (a), we show only the “only if” direction which goes by induction over the structure of the derivation. The “if” direction is similar. We only consider the details of the cases for (Push) and (Pop) since these are the only rules that modify the context stack. The other cases are trivial or following immediately from the inductive hypothesis.

case (Push):

⟨ \begin{matrix}let x′_{1} ⇐ w′_{1} \\ in & w′_{2} \end{matrix} , E⃗_{i}_{1} ++ (\begin{matrix}let x_{1} ⇐ · \\ in & \begin{matrix}let x_{2} ⇐ w_{2} \\ in & w_{3} \end{matrix} \end{matrix} :: E⃗_{i}_{2}) ⟩ ⇓ a

because

⟨ w′_{1} , \begin{matrix}let x′_{1} ⇐ · \\ in & w′_{2} \end{matrix} :: E⃗_{i}_{1} ++ (\begin{matrix}let x_{1} ⇐ · \\ in & \begin{matrix}let x_{2} ⇐ w_{2} \\ in & w_{3} \end{matrix} \end{matrix} :: E⃗_{i}_{2}) ⟩ ⇓ a:

By the restriction on the (Push) rule,

x′_{1} ∉ FV(E⃗_{i}_{1} ++ (\begin{matrix}let x_{1} ⇐ · \\ in & \begin{matrix}let x_{2} ⇐ w_{2} \\ in & w_{3} \end{matrix} \end{matrix} :: E⃗_{i}_{2})),

so this context stack is well-formed.

By IH,

⟨ w′_{1} , \begin{matrix}let x′_{1} ⇐ · \\ in & w′_{2} \end{matrix} :: E⃗_{i}_{1} ++ (\begin{matrix}let x_{1} ⇐ · \\ in & w_{2} \end{matrix} :: \begin{matrix}let x_{2} ⇐ · \\ in & w_{3} \end{matrix} :: E⃗_{i}_{2}) ⟩ ⇓ a

and thus

⟨ \begin{matrix}let x′_{1} ⇐ w′_{1} \\ in & w′_{2} \end{matrix} , E⃗_{i}_{1} ++ (\begin{matrix}let x_{1} ⇐ · \\ in & w_{2} \end{matrix} :: \begin{matrix}let x_{2} ⇐ · \\ in & w_{3} \end{matrix} :: E⃗_{i}_{2}) ⟩ ⇓ a

case (Pop): if E⃗_{i}_{1} ≠ nil then the result follows from the IH. If E⃗_{i}_{1} = nil then we have

⟨ unit w_{1} , let x_{1} ⇐ · in \begin{matrix}let x_{2} ⇐ w_{2} \\ in & w_{3} \end{matrix} :: E⃗_{i}_{2} ⟩ ⇓ a

because ⟨ let x_{2} ⇐ w_{2}[x_{1} := w_{1}] in w_{3}[x_{1} := w_{1}] , E⃗_{i}_{2} ⟩ ⇓ a

...by (Pop)

because ⟨ w_{2}[x_{1} := w_{1}] , \begin{matrix}let x_{2} ⇐ · \\ in & w_{3}[x_{1} := w_{1}] \end{matrix} :: E⃗_{i}_{2} ⟩ ⇓ a

...by (Push)

Now since x_{1} ∉ FV(w_{3}), let x_{2} ⇐ · in w_{3}[x_{1} := w_{1}] ≡ let x_{2} ⇐ · in w_{3} and we have

⟨ w_{2}[x_{1} := w_{1}] , \begin{matrix}let x_{2} ⇐ · \\ in & w_{3} \end{matrix} :: E⃗_{i}_{2} ⟩ ⇓ a

...from above

implies ⟨ unit w_{1} , \begin{matrix}let x_{1} ⇐ · \\ in & w_{2} \end{matrix} :: \begin{matrix}let x_{2} ⇐ · \\ in & w_{3} \end{matrix} :: E⃗_{i}_{2} ⟩ ⇓ a

...by (Pop)

The following property states that residual terms are among the canonical terms of specialization.

Property 7 (residual terms are canonical) For all r ∈ Residual-terms[Λ_{ml}^{bt}],

⟨ r , nil ⟩ ⇓ r.

Proof: It is easy to see that the set Residual-terms[Λ_{ml}^{bt}] ⊂ Terms[Λ_{ml}^{bt}] is exactly generated by the following grammar

r ::= x | \underline{⌜n⌝} | \underline{succ} r | \underline{pred} r | \underline{if0} r_{1} r_{2} r_{3} | \underline{λ}x . r | r_{0} \underline{@} r_{1} |
\underline{fix} x. r | \underline{unit} r | \underline{let} x ⇐ r_{1} \underline{in} r_{2}

The proof follows by a simple induction over the structure of terms in this grammar.

The following property shows that each step in the flattening specializer is appropriately reflected in the continuation-based specializer.

Property 8 If w ⟼_{s^{+}} w′ and ⟨ w′ , nil ⟩ ⇓ a, then ⟨ w , nil ⟩ ⇓ a.

Proof: by induction over the structure of w, proceeding by cases according to the last rule used in w ⟼_{s^{+}} w′. We show only illustrative cases.

case succ ⌜n⌝ ⟼_{s^{+}} unit ⌜n + 1⌝:

by assumption we have ⟨ unit ⌜n + 1⌝ , nil ⟩ ⇓ a and thus we can conclude ⟨ succ ⌜n⌝ , nil ⟩ ⇓ a. case let x_{1} ⇐ succ ⌜n⌝ in w_{2} ⟼_{s^{+}} let x_{1} ⇐ unit ⌜n + 1⌝ in w_{2}: by assumption

⟨ let x_{1} ⇐ unit ⌜n + 1⌝ in w_{2} , nil ⟩ ⇓ a

thus ⟨ unit ⌜n + 1⌝ , \begin{matrix}let x_{1} ⇐ · \\ in & w_{2} \end{matrix} :: nil ⟩ ⇓ a ...by (Push)

Now we need to show

⟨ let x_{1} ⇐ succ ⌜n⌝ in w_{2} , nil ⟩ ⇓ a

which requires ⟨ succ ⌜n⌝ , \begin{matrix}let x_{1} ⇐ · \\ in & w_{2} \end{matrix} :: nil ⟩ ⇓ a

...by (Push)

which requires ⟨ unit ⌜n + 1⌝ , \begin{matrix}let x_{1} ⇐ · \\ in & w_{2} \end{matrix} :: nil ⟩ ⇓ a

and we have this from above.

case let x_{2} ⇐ (let x_{1} ⇐ w_{1} in w_{2}) in w_{3} ⟼_{s^{+}} let x_{1} ⇐ w_{1} in \begin{matrix}let x_{2} ⇐ w_{2} \\ in & w_{3} \end{matrix}

where x_{1} ∉ FV(w_{3}): by assumption

⟨ let x_{1} ⇐ w_{1} in let x_{2} ⇐ w_{2} in w_{3} , nil ⟩ ⇓ a

thus ⟨ w_{1} , let x_{1} ⇐ · in \begin{matrix}let x_{2} ⇐ w_{2} \\ in & w_{3} \end{matrix} :: nil ⟩ ⇓ a

...by (Push)

and ⟨ w_{1} , \begin{matrix}let x_{1} ⇐ · \\ in & w_{2} \end{matrix} :: \begin{matrix}let x_{2} ⇐ · \\ in & w_{3} \end{matrix} :: nil ⟩ ⇓ a

...by Property 6

Now we need to show

⟨ let x_{2} ⇐ (let x_{1} ⇐ w_{1} in w_{2}) in w_{3} , nil ⟩ ⇓ a

which requires ⟨ let x_{1} ⇐ w_{1} in w_{2} , \begin{matrix}let x_{2} ⇐ · \\ in & w_{3} \end{matrix} :: nil ⟩ ⇓ a

...by (Push)

which requires ⟨ w_{1} , \begin{matrix}let x_{1} ⇐ · \\ in & w_{2} \end{matrix} :: \begin{matrix}let x_{2} ⇐ · \\ in & w_{3} \end{matrix} :: nil ⟩ ⇓ a

...by (Push)

and we have this from above.

case let x_{2} ⇐ (\underline{let} x_{1} ⇐ w_{1} \underline{in} w_{2}) in w_{3} ⟼_{s^{+}} \underline{let} x_{1} ⇐ w_{1} \underline{in} \begin{matrix}let x_{2} ⇐ w_{2} \\ in & w_{3} \end{matrix}

where x_{1} ∉ FV(w_{3}): by assumption

⟨ \underline{let} x_{1} ⇐ w_{1} \underline{in} let x_{2} ⇐ w_{2} in w_{3} , nil ⟩ ⇓ a
thus ⟨ w_{1} , nil ⟩ ⇓ r_{1}
and ⟨ let x_{2} ⇐ w_{2} in w_{3} , nil ⟩ ⇓ r_{2}  ... by (Assoc)
and thus ⟨ w_{2} , \begin{matrix}let x_{2} ⇐ · \\ in & w_{3} \end{matrix} :: nil ⟩ ⇓ r_{2}  ... by (Push)
and note a ≡ \underline{let} x_{1} ⇐ r_{1} \underline{in} r_{2}

Now we need to show

⟨ let x_{2} ⇐ (\underline{let} x_{1} ⇐ w_{1} \underline{in} w_{2}) in w_{3} , nil ⟩ ⇓ a

which requires ⟨ \begin{matrix}\underline{let} x_{1} ⇐ w_{1} \\ \underline{in} & w_{2} \end{matrix} , \begin{matrix}let x_{2} ⇐ · \\ in & w_{3} \end{matrix} :: nil ⟩ ⇓ a

...by (Push)

which requires ⟨ w_{1} , nil ⟩ ⇓ r_{1}
and ⟨ w_{2} , \begin{matrix}let x_{2} ⇐ · \\ in & w_{3} \end{matrix} :: nil ⟩ ⇓ r_{2}

...by (Assoc)

and we have both of these from above. case \underline{if0} w_{1} w_{2} w_{3} ⟼_{s^{+}} \underline{if0} w′_{1} w_{2} w_{3} because w_{1} ⟼_{s^{+}} w′_{1}: by assumption

⟨ \underline{if0} w′_{1} w_{2} w_{3} , nil ⟩ ⇓ a

thus ⟨ w′_{1} , nil ⟩ ⇓ r_{1}
and ⟨ w_{2} , nil ⟩ ⇓ r_{2}
and ⟨ w_{3} , nil ⟩ ⇓ r_{3}
and note a ≡ \underline{if0} r_{1} r_{2} r_{3}

Now we need to show

⟨ \underline{if0} w_{1} w_{2} w_{3} , nil ⟩ ⇓ a

which requires ⟨ w_{1} , nil ⟩ ⇓ r_{1}  (1)
and ⟨ w_{2} , nil ⟩ ⇓ r_{2}  (2)
and ⟨ w_{3} , nil ⟩ ⇓ r_{3}  (3).

Now (1) follows from IH, and (2) and (3) follow from above. case lift ⌜n⌝ ⟼_{s^{+}} \underline{⌜n⌝}: by assumption we have ⟨ \underline{⌜n⌝} , nil ⟩ ⇓ a where a ≡ \underline{⌜n⌝} and we have ⟨ lift ⌜n⌝ , nil ⟩ ⇓ \underline{⌜n⌝} directly.

We can now prove part (1) (as enumerated above) of Theorem 5.

Lemma 4 w ⟼_{s^{+}}^{∗} r implies ⟨ w , nil ⟩ ⇓ r.

Proof: by induction over the number of steps n in w ⟼_{s^{+}}^{∗} r.

case n = 0:

we need to show ⟨ r , nil ⟩ ⇓ r and this follows since residual terms are canonical (Property 7).

case n = i + 1: that is, w ⟼_{s^{+}} w′ ⟼_{s^{+}}^{∗} r.

by IH, ⟨ w′ , nil ⟩ ⇓ r and so by Property 8, ⟨ w , nil ⟩ ⇓ r.

Now we turn to part (2) in the proof of Theorem 5. We need to show that, given ⟨ w , nil ⟩ ⇓ r, we have a corresponding sequence of specialization steps in the flattening specializer. As expected, the proof proceeds by induction over the derivation of ⟨ w , nil ⟩ ⇓ r. However, the inductive hypothesis must be strengthened to deal with configurations of the form ⟨ w , E⃗_{i} ⟩ ⇓ a. In this stronger case, we need to show that a term corresponding to w in the interpretation context associated with E⃗_{i} specializes to a.

The following definition shows how context stacks can be unstacked to yield a flattened interpretation context.

Definition 9 (unstacking)

unstack (nil) = [·]
unstack (\begin{matrix}let x_{1} ⇐ · \\ in & w_{2} \end{matrix} :: E⃗_{i})

=

let x_{1} ⇐ ·
in unstack (E⃗_{i})[w_{2}]

For example, unstacking the context stack

\begin{matrix}let x_{1} ⇐ · \\ in & w_{2} \end{matrix} :: \begin{matrix}let x_{2} ⇐ · \\ in & w_{3} \end{matrix} :: nil

yields the interpretation context

let x_{1} ⇐ ·
in \begin{matrix}let x_{2} ⇐ w_{2} \\ in & w_{3}. \end{matrix}

Note that nested let’s appearing in w_{2} are not necessarily flattened.

Observation 1 (contexts yielded by unstacking) For all E⃗_{i}, exactly one of the following holds:

1. unstack (E⃗_{i}) = [·], or

2. unstack (E⃗_{i}) = E′_{i} for some interpretation context E′_{i}.

The following lemma shows the flattening specialization steps induced by continuation-based specializer derivations.

Lemma 5 Let E⃗_{i} be a well-formed context stack.

⟨ w , E⃗_{i} ⟩ ⇓ a implies unstack (E⃗_{i})[w] ⟼_{s^{+}}^{∗} a

Proof: by induction over the derivation of ⟨ w , E⃗_{i} ⟩ ⇓ a. Some representative cases are given below. We will implicitly rely on Property 2 which states that all context stacks appearing as subderivations of ⟨ w , E⃗_{i} ⟩ ⇓ a are well-formed.

case ⟨ unit w , nil ⟩ ⇓ unit w:

unstack (nil)[unit w] = unit w and unit w ⟼_{s^{+}}^{∗} unit w by reflexivity of ⟼_{s^{+}}^{∗}.

case ⟨ succ ⌜n⌝ , E⃗_{i} ⟩ ⇓ a because ⟨ unit ⌜n + 1⌝ , E⃗_{i} ⟩ ⇓ a:

unstack (E⃗_{i})[succ ⌜n⌝]
⟼_{s^{+}} unstack (E⃗_{i})[unit ⌜n + 1⌝] ...relying on Observation 1
⟼_{s^{+}}^{∗} a  ...by IH

case ⟨ let x_{1} ⇐ w_{1} in w_{2} , E⃗_{i} ⟩ ⇓ a because ⟨ w_{1} , \begin{matrix}let x_{1} ⇐ · \\ in & w_{2} \end{matrix} :: E⃗_{i} ⟩ ⇓ a:

Note x_{1} ∉ FV(E⃗_{i}) by the side-condition and proceed by cases of E⃗_{i}. case E⃗_{i} ≡ nil:

unstack (E⃗_{i})[let x_{1} ⇐ w_{1} in w_{2}]
= let x_{1} ⇐ w_{1} in w_{2}  ...by def. of unstack
= unstack (\begin{matrix}let x_{1} ⇐ · \\ in & w_{2} \end{matrix} :: E⃗_{i})[w_{1}] ...by def. of unstack
⟼_{s^{+}}^{∗} a  ...by IH

case E⃗_{i} ≡ \begin{matrix}let x_{2} ⇐ · \\ in & w_{3} \end{matrix} :: E⃗_{i}′: Intuitively, we unfold the definition of unstack, apply the flattening rule, and then fold unstack.

unstack (E⃗_{i})[let x_{1} ⇐ w_{1} in w_{2}]
= let x_{2} ⇐ (let x_{1} ⇐ w_{1} in w_{2}) in unstack (E⃗_{i}′)[w_{3}]

...by definition of unstack

⟼_{s^{+}} let x_{1} ⇐ w_{1} in let x_{2} ⇐ w_{2} in unstack (E⃗_{i}′)[w_{3}]

...note x_{1} ∉ FV(E⃗_{i}′) ∪ FV(w_{3})

= let x_{1} ⇐ w_{1} in unstack (\begin{matrix}let x_{2} ⇐ · \\ in & w_{3} \end{matrix} :: E⃗_{i}′)[w_{2}]

...by definition of unstack

= unstack (\begin{matrix}let x_{1} ⇐ · \\ in & w_{2} \end{matrix} :: \begin{matrix}let x_{2} ⇐ · \\ in & w_{3} \end{matrix} :: E⃗_{i}′)[w_{1}]

...by definition of unstack

≡ unstack (\begin{matrix}let x_{1} ⇐ · \\ in & w_{2} \end{matrix} :: E⃗_{i})[w_{1}]
⟼_{s^{+}}^{∗} a

...by IH

case ⟨ unit w_{1} , \begin{matrix}let x ⇐ · \\ in & w_{2} \end{matrix} :: E⃗_{i} ⟩ ⇓ a because ⟨ w_{2}[x := w_{1}] , E⃗_{i} ⟩ ⇓ a:

unstack (\begin{matrix}let x ⇐ · \\ in & w_{2} \end{matrix} :: E⃗_{i})[unit w_{1}]
= let x_{1} ⇐ unit w_{1} in unstack (E⃗_{i})[w_{2}]

...definition of unstack

⟼_{s^{+}} unstack (E⃗_{i})[w_{2}][x_{1} := w_{1}]
≡ unstack (E⃗_{i})[w_{2}[x_{1} := w_{1}]]

...since \begin{matrix}let x ⇐ · \\ in & w_{2} \end{matrix} :: E⃗_{i}

..is a well-formed stack and thus x_{1} ∉ FV(E⃗_{i})

⟼_{s^{+}} a

...by IH

case ⟨ w_{1} \underline{@} w_{2} , nil ⟩ ⇓ r_{1} \underline{@} r_{2} because ⟨ w_{1} , nil ⟩ ⇓ r_{1} and ⟨ w_{2} , nil ⟩ ⇓ r_{2}:

unstack (nil)[w_{1} \underline{@} w_{2}]
= w_{1} \underline{@} w_{2}  ...definition of unstack
⟼_{s^{+}}^{∗} r_{1} \underline{@} w_{2}  ...by IH
⟼_{s^{+}}^{∗} r_{1} \underline{@} r_{2}  ...by IH

case ⟨ \underline{let} x ⇐ w_{1} \underline{in} w_{2} , E⃗_{i} ⟩ ⇓ \underline{let} x ⇐ r_{1} \underline{in} r_{2} because ⟨ w_{1} , nil ⟩ ⇓ r_{1} and ⟨ w_{2} , E⃗_{i} ⟩ ⇓ r_{2}

Note x_{1} ∉ FV(E⃗_{i}) and proceed by cases of E⃗_{i}. case E⃗_{i} ≡ nil:

unstack (E⃗_{i})[\underline{let} x_{1} ⇐ w_{1} \underline{in} w_{2}]
= \underline{let} x_{1} ⇐ w_{1} \underline{in} w_{2}  ...by definition of unstack
⟼_{s^{+}}^{∗} \underline{let} x_{1} ⇐ r_{1} \underline{in} w_{2}  ...by IH
⟼_{s^{+}}^{∗} \underline{let} x_{1} ⇐ r_{1} \underline{in} r_{2}  ...by IH

case E⃗_{i} ≡ \begin{matrix}let x_{2} ⇐ · \\ in & w_{3} \end{matrix} :: E⃗_{i}′:

Intuitively, we unfold the definition of unstack, apply the flattening rule, and then fold unstack.

unstack (E⃗_{i})[\underline{let} x_{1} ⇐ w_{1} \underline{in} w_{2}]
= let x_{2} ⇐ (\underline{let} x_{1} ⇐ w_{1} \underline{in} w_{2}) in unstack (E⃗_{i}′)[w_{3}]

...by definition of unstack

⟼_{s^{+}} \underline{let} x_{1} ⇐ w_{1} \underline{in} let x_{2} ⇐ w_{2} in unstack (E⃗_{i}′)[w_{3}]

...note x_{1} ∉ FV(E⃗_{i}′) ∪ FV(w_{3})

⟼_{s^{+}}^{∗} \underline{let} x_{1} ⇐ r_{1} \underline{in} let x_{2} ⇐ w_{2} in unstack (E⃗_{i}′)[w_{3}]

...by IH

= \underline{let} x_{1} ⇐ r_{1} \underline{in} unstack (\begin{matrix}let x_{2} ⇐ · \\ in & w_{3} \end{matrix} :: E⃗_{i}′)[w_{2}]

...by definition of unstack

⟼_{s^{+}}^{∗} \underline{let} x_{1} ⇐ r_{1} \underline{in} r_{2}

...by IH

As a corollary, we obtain the proof of part (2) of Theorem 5.

Corollary 1 ⟨ w , nil ⟩ ⇓ r implies w ⟼_{s^{+}}^{∗} r.

Proof: Since nil is a well-formed context stack, by Lemma 5 we have unstack (nil)[w] ⟼_{s^{+}}^{∗} r. Now since unstack (nil) = [·], we have w ⟼_{s^{+}}^{∗} r.

References

[1] Lars Ole Andersen. Program Analysis and Specialization for the C Programming Language. PhD thesis, DIKU, Computer Science Department, University of Copenhagen, Copenhagen, Denmark, May 1994. DIKU Rapport 94/19.

[2] Henk Barendregt. The Lambda Calculus — Its Syntax and Semantics. North-Holland, 1984.

[3] P. N. Benton. Strictness Analysis of Lazy Functional Programs. PhD thesis, Computer Laboratory, University of Cambridge, Cambridge, England, May 1995.

[4] P. N. Benton, G. M. Bierman, and V. C. V de Paiva. Computational types from a logical perspective I. Technical report 365, Computer Laboratory, University of Cambridge, Cambridge, England, May 1995.

[5] Hans-J. Boehm, editor. Proceedings of the Twenty-First Annual ACM Symposium on Principles of Programming Languages, Portland, Oregon, January 1994. ACM Press.

[6] Anders Bondorf. Improving binding times without explicit cpsconversion. In William Clinger, editor, Proceedings of the 1992 ACM Conference on Lisp and Functional Programming, LISP Pointers, Vol. V, No. 1, pages 1–10, San Francisco, California, June 1992. ACM Press.

[7] Anders Bondorf and Olivier Danvy. Automatic autoprojection of recursive equations with global variables and abstract data types. Science of Computer Programming, 16:151–195, 1991.

[8] Anders Bondorf and Dirk Dussart. Improving CPS-based partial evaluation: Writing cogen by hand. In Peter Sestoft and Harald Søndergaard, editors, Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, Technical Report 94/9, University of Melbourne, Australia, pages 1–10, Orlando, Florida, June 1994.

[9] Charles Consel. A tour of Schism: A partial evaluation system for higher-order applicative languages. In David A. Schmidt, editor, Proceedings of the Second ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pages 145–154, Copenhagen, Denmark, June 1993. ACM Press.

[10] Charles Consel and Olivier Danvy. For a better support of static data flow. In Hughes [40], pages 496–519.

[11] Charles Consel and Olivier Danvy. Tutorial notes on partial evaluation. In Susan L. Graham, editor, Proceedings of the Twentieth Annual ACM Symposium on Principles of Programming Languages, pages 493–501, Charleston, South Carolina, January 1993. ACM Press.

[12] Roy L. Crole and Andrew D. Gordon. Factoring an adequacy proof (preliminary report). In John T. O’Donnell and Kevin Hammond, editors, Functional Programming, Glasgow 1993, Workshops in Computing, pages 9–25, Ayr, Scotland, 1993. Springer-Verlag.

[13] Roy L. Crole and Andrew M. Pitts. New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic. Information and Computation, 98:171–210, 1992.

[14] Olivier Danvy. Type-directed partial evaluation. In Guy L. Steele Jr., editor, Proceedings of the Twenty-Third Annual ACM Symposium on Principles of Programming Languages, pages 242–257, St. Petersburg Beach, Florida, January 1996. ACM Press.

[15] Olivier Danvy and Andrzej Filinski. Representing control, a study of the CPS transformation. Mathematical Structures in Computer Science, 2(4):361–391, December 1992.

[16] Olivier Danvy and John Hatcliff. CPS transformation after strictness analysis. ACM Letters on Programming Languages and Systems, 1(3):195–212, 1993.

[17] Olivier Danvy, Karoline Malmkjær, and Jens Palsberg. The essence of eta-expansion in partial evaluation. LISP and Symbolic Computation, 8(3):209–227, 1995. An earlier version appeared in the proceedings of the 1994 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation.

[18] Olivier Danvy, Karoline Malmkjær, and Jens Palsberg. Eta-expansion does The Trick. ACM Transactions on Programming Languages and Systems, 1996. To appear.

[19] Rowan Davies. A temporal-logic approach to binding-time analysis. In Proceedings of the Eleventh Annual IEEE Symposium on Logic in Computer Science, pages 184–195, New Brunswick, New Jersey, July 1996. IEEE Computer Society Press.

[20] Rowan Davies and Frank Pfenning. A modal analysis of staged computation. In Guy L. Steele Jr., editor, Proceedings of the Twenty-Third Annual ACM Symposium on Principles of Programming Languages, pages 258–283, St. Petersburg Beach, Florida, January 1996. ACM Press.

[21] Dirk Dussart. PhD thesis, Katholieke Universiteit Leuven, Leuven, Belgium, 1997. Forthcoming.

[22] Dirk Dussart and Peter Thiemann. Imperative functional specialization. Berichte des Wilhelm-Schickard-Instituts WSI-96-28, Universität Tübingen, July 1996.

[23] R. Kent Dybvig, editor. Proceedings of the 1996 ACM SIGPLAN International Conference on Functional Programming, Philadelphia, Pennsylvania, May 1996. ACM Press.

[24] Andrzej Filinski. Representing monads. In Boehm [5], pages 446–457.

[25] Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. The essence of compiling with continuations. In David W. Wall, editor, Proceedings of the ACM SIGPLAN’93 Conference on Programming Languages Design and Implementation, SIGPLAN Notices, Vol. 28, No 6, pages 237–247, Albuquerque, New Mexico, June 1993. ACM Press.

[26] Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types, volume 7 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989.

[27] Robert Glück and Jesper Jørgensen. Efficient multi-level generating extensions for program specialization. In Hermenegildo and Swierstra [38], pages 259–278.

[28] Robert Glück and Andrei Klimov. Occam’s razor in metacomputation: the notion of a perfect process tree. In Patrick Cousot, Moreno Falaschi, Gilberto Filè, and Antoine Rauzy, editors, Proceedings of the Third International Workshop on Static Analysis WSA’93, number 724 in Lecture Notes in Computer Science, pages 112–123, Padova, Italy, September 1993.

[29] Carsten K. Gomard. A self-applicable partial evaluator for the lambdacalculus: Correctness and pragmatics. ACM Transactions on Programming Languages and Systems, 14(2):147–172, 1992.

[30] Carsten K. Gomard and Neil D. Jones. A partial evaluator for the untyped lambda-calculus. Journal of Functional Programming, 1(1):21– 69, 1991.

[31] Andrew D. Gordon. Functional Programming and Input/Output. PhD thesis, Computer Laboratory, University of Cambridge, Cambridge, England, February 1993. Technical Report No. 285.

[32] Carl A. Gunter. Semantics of Programming Languages: Structures and Techniques. MIT Press, 1992.

[33] John Hannan and Dale Miller. Deriving mixed evaluation from standard evaluation for a simple functional language. In J. L. A. van de Snepscheut, editor, Proceedings of a Conference on Mathematics of Program Construction, number 375 in Lecture Notes in Computer Science, pages 239–255, Groningen, The Netherlands, 1989.

[34] John Hatcliff. The Structure of Continuation-Passing Styles. PhD thesis, Department of Computing and Information Sciences, Kansas State University, Manhattan, Kansas, June 1994.

[35] John Hatcliff. Mechanically verifying the correctness of an offline partial evaluator. In Hermenegildo and Swierstra [38], pages 279–298.

[36] John Hatcliff and Olivier Danvy. A generic account of continuationpassing styles. In Boehm [5], pages 458–471.

[37] John Hatcliff and Robert Glück. An operational theory of selfapplicable on-line program specialization. In Olivier Danvy, Robert Glück, and Peter Thiemann, editors, Partial Evaluation, number 1110 in Lecture Notes in Computer Science, pages 161–182, Dagstuhl, Germany, February 1996.

[38] Manuel Hermenegildo and S. Doaitse Swierstra, editors. Seventh International Symposium on Programming Language Implementation and Logic Programming, number 982 in Lecture Notes in Computer Science, Utrecht, The Netherlands, September 1995.

[39] Carsten K. Holst and Carsten K. Gomard. Partial evaluation is fuller laziness. In Paul Hudak and Neil D. Jones, editors, Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, SIGPLAN Notices, Vol. 26, No 9, pages 223–233, New Haven, Connecticut, June 1991. ACM Press.

[40] John Hughes, editor. Proceedings of the Fifth ACM Conference on Functional Programming and Computer Architecture, number 523 in Lecture Notes in Computer Science, Cambridge, Massachusetts, August 1991. Springer-Verlag.

[41] Neil D. Jones, editor. Special issue on Partial Evaluation, Journal of Functional Programming, Vol. 3, Part 3. Cambridge University Press, July 1993.

[42] Neil D. Jones, Carsten K. Gomard, and Peter Sestoft. Partial Evaluation and Automatic Program Generation. Prentice Hall International Series in Computer Science. Prentice-Hall, 1993.

[43] Neil D. Jones, Peter Sestoft, and Harald Søndergaard. MIX: A selfapplicable partial evaluator for experiments in compiler generation. LISP and Symbolic Computation, 2(1):9–50, 1989.

[44] John Launchbury. A strongly-typed self-applicable partial evaluator. In Hughes [40], pages 145–164.

[45] Julia L. Lawall and Olivier Danvy. Continuation-based partial evaluation. In Carolyn L. Talcott, editor, Proceedings of the 1994 ACM Conference on Lisp and Functional Programming, LISP Pointers, Vol. VII, No. 3, Orlando, Florida, June 1994. ACM Press.

[46] Julia L. Lawall and Olivier Danvy. Continuation-based partial evaluation. Technical Report CS-95-178, Computer Science Department, Brandeis University, Waltham, Massachusetts, January 1995. An earlier version appeared in the proceedings of the 1994 ACM Conference on Lisp and Functional Programming.

[47] Sheng Liang, Paul Hudak, and Mark Jones. Monad transformers and modular interpreters. In Peter Lee, editor, Proceedings of the Twenty-Second Annual ACM Symposium on Principles of Programming Languages, pages 333–343, San Francisco, California, January 1995. ACM Press.

[48] Eugenio Moggi. Notions of computation and monads. Information and Computation, 93:55–92, 1991.

[49] Kristian Nielsen. Master’s thesis, DIKU, Computer Science Department, University of Copenhagen, Copenhagen, Denmark, 1997. Forthcoming.

[50] Kristian Nielsen and Morten Heine Sørensen. Call-by-name CPStranslation as a binding-time improvement. In Alan Mycroft, editor, Static Analysis, number 983 in Lecture Notes in Computer Science, pages 296–313, Glasgow, Scotland, September 1995. Springer-Verlag.

[51] Flemming Nielson. A denotational framework for data flow analysis. Acta Informatica, 18:265–287, 1982.

[52] Flemming Nielson and Hanne Riis Nielson. Two-Level Functional Languages, volume 34 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1992.

[53] Hanne Riis Nielson and Flemming Nielson. Semantics with Applications, a formal introduction. Wiley Professional Computing. John Wiley and Sons, 1992.

[54] Jens Palsberg. Correctness of binding-time analysis. In Jones [41], pages 347–363.

[55] Christine Paulin-Mohring and Benjamin Werner. Synthesis of ML programs in the system Coq. Journal of Symbolic Computation, 15:607– 640, 1993.

[56] Gordon D. Plotkin. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science, 1:125–159, 1975.

[57] Dag Prawitz. Natural Deduction. Almquist and Wiksell, Uppsala, 1965.

[58] Amr Sabry and Matthias Felleisen. Reasoning about programs in continuation-passing style. LISP and Symbolic Computation, 6(3/4): 289–360, December 1993.

[59] Amr Sabry and Matthias Felleisen. Is continuation-passing useful for data flow analysis? In Vivek Sarkar, editor, Proceedings of the ACM SIGPLAN’94 Conference on Programming Languages Design and Implementation, SIGPLAN Notices, Vol. 29, No 6, pages 1–12, Orlando, Florida, June 1994. ACM Press.

[60] Amr Sabry and Philip Wadler. Compiling with reflections. In Dybvig [23], pages 13–24.

[61] David Sands. Proving the correctness of recursion-based automatic program transformations. In Peter Mosses, Mogens Nielsen, and Michael Schwartzbach, editors, Proceedings of TAPSOFT ’95, number 915 in Lecture Notes in Computer Science, pages 681–695, Aarhus, Denmark, May 1995.

[62] Morten Heine Sørensen, Robert Glück, and Neil Jones. Towards unifying partial evaluation, deforestation, supercompilation, and GPC. In Donald Sannella, editor, Proceedings of the Fifth European Symposium on Programming, number 788 in Lecture Notes in Computer Science, pages 485–500, Edinburgh, Scotland, April 1994.

[63] Guy L. Steele Jr. Building interpreters by composing monads. In Boehm [5], pages 472–492.

[64] Carolyn Talcott. A theory for program and data type specification. Theoretical Computer Science, 104(1):129–159, 1992.

[65] Peter Thiemann. Cogen in six lines. In Dybvig [23], pages 180–189.

[66] Philip Wadler. The essence of functional programming (tutorial). In Andrew W. Appel, editor, Proceedings of the Nineteenth Annual ACM Symposium on Principles of Programming Languages, pages 1–14, Albuquerque, New Mexico, January 1992. ACM Press.

[67] Philip Wadler. Comprehending monads. Mathematical Structures in Computer Science, 2(4):461–493, December 1992.

[68] Mitchell Wand. Specifying the correctness of binding-time analysis. In Jones [41], pages 365–387.

Recent Publications in the BRICS Report Series

RS-96-34 John Hatcliff and Olivier Danvy. A Computational Formalization for Partial Evaluation (Extended Version). October 1996. 67 pp. To appear in Mathematical Structures in Computer Science.

RS-96-33 Jonathan F. Buss, Gudmund Skovbjerg Frandsen, and Jeffrey Outlaw Shallit. The Computational Complexity of Some Problems of Linear Algebra. September 1996. 39 pp. Revised version to appear in STACS ’97: 14th Annual Symposium on Theoretical Aspects of Computer Science Proceedings, LNCS, 1997.

RS-96-32 P. S. Thiagarajan. Regular Trace Event Structures. September 1996. 34 pp.

RS-96-31 Ian Stark. Names, Equations, Relations: Practical Ways to Reason about ‘new’. September 1996. ii+22 pp. To appear in Typed Lambda Calculi and Applications: 3rd International Conference, TLCA ’97 Proceedings, LNCS, 1997.

RS-96-30 Arne Andersson, Peter Bro Miltersen, and Mikkel Thorup. Fusion Trees can be Implemented with AC^{0} Instructions only. September 1996. 8 pp.

RS-96-29 Lars Arge. The I/O-Complexity of Ordered Binary-Decision Diagram Manipulation. August 1996. 35 pp. An extended abstract version appears in Staples, Eades, Kato, and Moffat, editors, Algorithms and Computation: 6th International Symposium, ISAAC ’95 Proceedings, LNCS 1004, 1995, pages 82�91.

RS-96-28 Lars Arge. The Buffer Tree: A New Technique for Optimal I/O Algorithms. August 1996. 34 pp. This report is a revised and extended version of the BRICS Report RS-94-16. An extended abstract appears in Akl, Dehne, Sack, and Santoro, editors, Algorithms and Data Structures: 4th Workshop, WADS ’95 Proceedings, LNCS 955, 1995, pages 334�345.

RS-96-27 Devdatt P. Dubhashi, Volker Priebe, and Desh Ranjan. Negative Dependence Through the FKG Inequality. July 1996. 15 pp.