Journal of Functional Programming (1993), vol. 11, pp. 1–000

Specifying the Correctness of Binding-Time Analysis

Mitchell Wand†

College of Computer Science, Northeastern University, 360 Huntington Avenue, 161CN, Boston, MA 02115, USA (wand@ccs.northeastern.edu)

Abstract

Mogensen has exhibited a very compact partial evaluator for the pure lambda calculus, using binding-time analysis followed by specialization. We give a correctness criterion for this partial evaluator and prove its correctness relative to this specification. We show that the conventional properties of partial evaluators, such as the Futamura projections, are consequences of this specification. By considering both a flow analysis and the transformation it justifies together, this proof suggests a framework for incorporating flow analyses into verified compilers.

1 Introduction

Compilers for modern programming languages such as Scheme, ML, or Haskell typically perform a variety of optimizations in order to produce good code. Typically, an optimization consists of an analysis to collect information about a portion of the program, followed by a transformation based on the results of the analysis. While program analyses of various sorts have been studied intensively for many years, it has proven remarkably difficult to specify the correctness of an analysis in a way that actually justifies the resulting transformation.

Here we study one such analysis: binding-time analysis. Binding-time analysis annotates a program to indicate which portions of the program can be executed at compile-time and which cannot be executed until run-time. Because it is temporal rather than value-based, binding-time analysis does not seem to fit comfortably into the framework of abstract interpretation. Therefore it poses a challenge to theories of analysis and transformation.

Binding-time analysis is intended to support program specialization or staging (Jorring & Scherlis, 1986). Here we show the correctness of a binding-time analysis by showing that it justifies a specializer.

Our framework is based on the off-line partial evaluator of Mogensen (1992b), a very compact self-applicable partial evaluator for the pure λ-calculus. Mogensen’s partial evaluator formulates binding-time analysis as a solution of a set of constraints on the annotation of a program (that is, as an annotated type-inference

† Work supported by the National Science Foundation under grant numbers CCR-9002253 and CCR-9014603. A preliminary version of this paper appeared in the Proceedings of the 20th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (January, 1993).

tree for a certain type system). The constraints are based on those in (Gomard, 1990). The annotated tree is fed to a program-specializer P, which produces the residual (run-time) term.

Our main theorem is that if the specializer is given any annotation of the input program that satisfies the binding-time constraints, its output is a suitably specialized version of the input program.

In order to do this, we must formalize the notion of a “suitably specialized version of the input program.” Our version of this notion is similar to, but simpler than, the specification given by Gomard (1992). We then show that the typical properties of partial evaluators, such as the Futamura projections, follow from the specification.

This paper is organized as follows: in Section 2 we review the relevant fundamentals of partial evaluation and consider how an arbitrary programming language can be modelled inside the λ-calculus. In Section 3 we show how the λ-calculus itself can be modelled. In Section 4 we present Mogensen’s partial evaluator. In Section 5 we state and prove our main theorem relating binding-time analysis and partial evaluation, and in Section 6 we show how the expected specialization behavior of partial evaluators follows from the main theorem. In Section 7 we consider self-application of the partial evaluator, and show how the Futamura projections can be derived from the main theorem. In Section 8 we present a brief account of the operational semantics of the language of annotated terms. Section 9 compares our work to other approaches to binding-time analysis, and Section 10 gives some conclusions.

2 Partial Evaluation and Representation

We begin by recapitulating the usual terminology of partial evaluation.

Definition 1 A programming language L is specified by a set Π of L-programs, a set Δ of L-data, and for every n ≥ 0, an (n + 2)-ary relation

L_{n}(π, d_{1}, … d_{n}) ≡ d

such that each L_{n} is a partial function. The relation L_{n}(π, d_{1}, … d_{n}) ≡ d represents the assertion that program π, given inputs d_{1}, …, d_{n}, produces output d.

We will almost always omit the subscript on L. We shall ambiguously regard this as an (n + 2)-place relation or as a partial function from programs and inputs to outputs. In the latter interpretation, ≡ is the equality on elements of the set Δ. The functional interpretation is used, for example, in the definition of a partial evaluator:

Definition 2 An L-program P is a partial evaluator iff for all L-programs π and L-data d_{1} and d_{2},

L_{1}(L_{1}(P, π, d_{1}), d_{2}) = L_{2}(π, d_{1}, d_{2})

The partial evaluators we will consider are off-line. In an off-line partial evaluator, the program π is first transformed in some way independent of the static input d_{1}:

Definition 3 An off-line partial evaluator is a pair (Φ, P), where Φ is a map Π → Δ and P is an L-program such that for all L-programs π and L-data d_{1} and d_{2},

L_{2}(L_{2}(P, Φ(π), d_{1}), d_{2}) = L_{3}(π, d_{1}, d_{2})

In general, we will not be concerned with the algorithmic aspects of the transformation Φ, so we will not bother to consider the implementation of Φ as an L-program.

For these definitions to make sense, π (or Φ(π) in the off-line case) must also be an element of the set Δ of L-data. To prove the correctness of partial evaluators and similar program transformers, we must consider this representation explicitly. Our tool for studying this representation will be the pure λ-calculus.

The basic techniques for representing various quantities in the λ-calculus are well-known. For example, when considering computations on the integers, one first defines a set of numerals, that is, a mapping associating each integer n with a closed normal form λ-term ⌈n⌉. Then we say a function f on the integers is representable iff there exists a λ-term F such that for all n, F ⌈n⌉ =_{β} ⌈f(n)⌉.

To carry out a similar analysis for an arbitrary programming language L, we give a coding ⟨−⟩ from programs and data in the language into normal form λ-terms, and a λ-term S which is the semantics or interpreter for the language. We can then define the input-output behavior of the language by

L_{n}(π, d_{1}, … d_{n}) ≡ d ⟺ S⟨π⟩⟨d_{1}⟩ … ⟨d_{n}⟩ = ⟨d⟩

where the equality on the right is equality in some λ-theory (for us, this will be =_{β}). Note that unlike the usual formulations of denotational semantics, in which the translation from a program to its meaning is specified informally, the semantics S is internalized as a term in the λ-calculus. This step is crucial for dealing with self-application.

From now on we will assume that our programming languages have been specified in this way. As an example of this style of specification, we can define the notion of a translation of an L-program into the λ-calculus:

Definition 4 A translation of an L-program π is a λ-term T such that for all S-data d, T ⟨d⟩ = S⟨π⟩⟨d⟩.

Thus T ⟨d⟩ =_{β} ⟨d′⟩ ⟺ S⟨π⟩⟨d⟩ = ⟨d′⟩ ⟺ L(π, d) ≡ d′.

3 Representing λ-Terms in Pure λ-calculus

We are interested in performing binding-time analysis and partial evaluation on λ-terms themselves. We therefore need to specify the λ-calculus as a programming language dealing with λ-terms as inputs and outputs. To do this, we must specify a representation of λ-terms and an interpreter manipulating those representations.

The representation needs to code each λ-term as a normal form λ-term. Mogensen (1992a) uses the following coding:

\begin{aligned}⌈x⌉ & ≡ λabc.ax \\ ⌈MN⌉ & ≡ λabc.b⌈M⌉⌈N⌉ \\ ⌈λx.M⌉ & ≡ λabc.c(λx.⌈M⌉) \end{aligned}

This coding uses two tricks: first, it uses the coding of the sum A+B as (∀C)((A → C) → (B → C) → C), so that each element of a “sum domain” is modelled as its own case-function. Thus a case expression

case m of
V ar(x) ⇒ … x …
App(M, N) ⇒ … M … N …
Abs(M) ⇒ … M …

would be represented as

m(λx. … x …)(λmn. … m … n …)(λm. … m …)

Second, it uses so-called “higher-order abstract syntax” (Pfenning & Elliott, 1988), in which the binding operators in the represented language are modelled by binding in the lambda-calculus. Any free occurrences of x in the body of λx.M will be bound by the x in λx.⌈M⌉.

We also need to specify an interpreter. This task will be filled by a self-interpreter E. A self-interpreter is a λ-term E such that E⌈M⌉ =_{β} M (Barendregt, 1991). E needs to have the properties that

\begin{matrix}E(V ar x) = & x \\ E(App MN) = & (EM)(EN) \\ E(Abs M) = & λv.E(Mv) \end{matrix}

Here we are using informal notation for abstract syntax of the λ-term input to E. It is easy to display a term that satisfies these properties:

E ≡ Y (λe.λm.m(λx.x)
(λmn.(em)(en))
(λm.λv.e(mv)))

where Y is the standard fixpoint operator.

Theorem 1 (E is a self-interpreter) For any λ-term M, E⌈M⌉ =_{β} M

Proof By structural induction on M (Mogensen, 1992a).

If we use E as our interpreter, then the programming language of Λ of λ-terms has an input-output relation specified by

Λ(M, N_{1}, … N_{n}) ≡ R
⟺ E⌈M⌉⌈N_{1}⌉ … ⌈N_{k}⌉ =_{β} ⌈R⌉
⟺ M⌈N_{1}⌉ … ⌈N_{k}⌉ =_{β} ⌈R⌉

Since here the set Δ of Λ-data is the set of normal-form λ-terms, our use of ≡ for equality on elements of Δ and its usual use for equality of λ-terms up to α-congruence coincide. Henceforth, we will use the symbol = to denote βconvertibility, and ≡, when necessary, to denote α-congruence of λ-terms.

4 The Partial Evaluator

We next present the partial evaluator for Λ given by (Mogensen, 1992b). This is an off-line partial evaluator, so it is divided into two phases: a binding-time analysis (the transformation Φ), and a specialization phase (a Λ-program P).

The binding-time analysis produces an annotated version of the input program by assigning each phrase of the program a type in a system due to Gomard (1990). The types are as follows:

t ::= d | v | t → t | μv.t

where in μv.t, t must be of the form (t_{1} → … → t_{n} → d), and all occurrences of v in t must be positive. The intention is that the type d denotes the type of “dynamic” quantities: i.e., representations of untyped λ-terms. The other types are built from d in the usual way, and correspond to the types one might find in an ordinary compiler. Recursive types are intended to denote their unfolding into an infinite tree. The presence of the recursive types allows loops to be formed in the static portion of the analyzed program, and the use of a single run-time type d allows unrestricted self-application in the dynamic portion.

Annotated terms are given by the following grammar:

W ::= v | W W | λv.W | W W | \underline{λ}v.W

The first three productions correspond to static (compile-time) calculations, and the last two correspond to dynamic (residual, run-time) operations, which correspond at compile-time to emitting code. Annotated terms have elsewhere been called 2-level λ-terms.

The annotated terms are produced by decorating a type-inference tree. Thus, instead of considering typing judgements of the form A ⊢ M : t, we consider judgements of the form A ⊢ M : t [W], meaning that under hypotheses A, term M can be assigned type t with annotated term W. When this judgement is true, we say that W is an annotation of M with type t. The type system can be written as follows:

A ⊢ x : A(x) [x]

\frac{A ⊢ M : s → t [W_{1}] A ⊢ N : s [W_{2}]}{A ⊢ MN : t [W_{1}W_{2}]}

\frac{A[x ↦ s] ⊢ M : t [W]}{A ⊢ (λx.M) : s → t [λx.W]}

\frac{A ⊢ M : d [W_{1}] A ⊢ N : d [W_{2}]}{A ⊢ MN : d [W_{1} W_{2}]}

\frac{A[x ↦ d] ⊢ M : d [W]}{A ⊢ (λx.M) : d [\underline{λ}x.W]}

A tree of judgements in which every node satisfies these constraints is a derivation. For purposes of checking these constraints, types are regarded as equal iff their unfoldings into infinite trees are equal; thus no separate rules for recursive types are necessary. We shall not consider algorithms for performing these annotations; instead we shall assume that we have such an algorithm Φ; see (Gomard, 1990; Henglein, 1991).

Mogensen uses a representation scheme for annotated terms similar to that for ordinary λ-terms:

\begin{matrix}⌊x⌋ ≡ & λabcde.ax \\ ⌊W W′⌋ ≡ & λabcde.b⌊W ⌋⌊W′⌋ \\ ⌊λx.W ⌋ ≡ & λabcde.c(λx.⌊W ⌋) \\ ⌊W W′⌋ ≡ & λabcde.d⌊W ⌋⌊W′⌋ \\ ⌊\underline{λ}x.W ⌋ ≡ & λabcde.e(λx.⌊W ⌋) \end{matrix}

To specialize a program, one must interpret the annotated term, evaluating all the static (compile-time) parts (just like E) and emitting code for all the dynamic (residual) parts. This can be expressed in terms of abstract syntax by:

\begin{matrix}P (P var x) = & x \\ P (Sapp W W′) = & (P W)(P W′) \\ P (Sabs W) = & λv.P (W v) \\ P (Dapp W W′) = & App(P W)(P W′) \\ P (Dabs W) = & Abs(λv.P (W (V ar v))) \end{matrix}

where P var, etc., represent the abstract syntax of annotated terms. This can be realized by a λ-term P operating on the ⌊−⌋ representation as follows:

P ≡ Y (λp.λm.m(λx.x)
(λww′.(pw)(pw′))
(λw.λv.p(wv))
(λww′.λabc.b(pw)(pw′))
(λw.λabc.c(λv.p(w(λabc.av)))))

We first show some simple properties of P. As usual, we will use the symbol = to denote β-convertibility, and ≡, when necessary, to distinguish α-congruence of λ-terms.

Lemma 1 ⌊W [y/x]⌋ ≡ ⌊W ⌋[y/x]

Proof Easy induction on W.

Lemma 2 P (⌊W ⌋[N/x]) = (P ⌊W ⌋)[N/x]

Proof By induction on the size of W. We will do two cases; the others are similar. For the base case, we have P (⌊x⌋[N/x]) = P (λabcde.aN) = N and (P ⌊x⌋)[N/x] = x[N/x] = N. For static abstractions over a variable y distinct from x, we have

P (⌊λy.M⌋[N/x])
= P ((λabcde.c(λy.⌊M⌋))[N/x])  definition of ⌊λy.M⌋
= P (λabcde.c(λy′.⌊M⌋[y′/y][N/x])) substitution (y′ fresh)
= λv.P ((λy′.⌊M⌋[y′/y][N/x])v)  definition of P
= λy′.P ((λy′.⌊M⌋[y′/y][N/x])y′)  α-conversion
= λy′.P (⌊M⌋[y′/y][N/x])  β-conversion
= λy′.P (⌊M[y′/y]⌋[N/x])  Lemma 1
= λy′.(P ⌊M[y′/y]⌋)[N/x]  induction hypothesis at M[y′/y]
(M[y′/y] is smaller than λy.M)
= λy′.(P (⌊M⌋[y′/y]))[N/x]  Lemma 1
= λy′.(P ⌊M⌋)[y′/y][N/x]  induction hypothesis
= (λy.P ⌊M⌋)[N/x]  substitution
= P (⌊λy.M⌋)[N/x]  definition of P

Corollary 1 (Substitution Lemma) If ρ is a substitution, then (P ⌊W ⌋)ρ = P (⌊W ⌋ρ).

Proof By repeated application of the preceding lemma for each x ∈ dom(ρ).

We will often write P ⌊W ⌋ρ to mean, interchangeably, either of the terms above. Note that it would be incorrect to bring the ρ inside the ⌊−⌋: in general P (⌊W ⌋ρ) ≠ P (⌊W ρ⌋). We will consider this further in Section 8. The resemblance of P ⌊W ⌋ρ to a conventional environment semantics is, of course, not coincidental, since by choosing equality to be interconvertibility, we are in effect working in the open term model, in which evaluation in an environment is the same as substitution. Our results hold a fortiori in any λ-model.

5 Correctness of the Partial Evaluator

Our goal is to show that the pair (Φ, P) is a correct off-line partial evaluator. The correctness proof must somehow involve the binding-time analysis as well: otherwise one could change the binding-time analysis arbitrarily without invalidating P, which is clearly impossible. Furthermore, the usual notion of partial evaluation only involves the programs that can be assigned relatively simple types like d or d → d, while the algorithm clearly involves arbitrary types. Furthermore, the algorithm P crucially involves non-closed terms. Hence we must find an induction hypothesis that covers arbitrary types and terms with free variables.

We do this by using the technique of logical relations. For every closed type t, we will define a binary relation R_{t}. We begin by setting up some standard machinery. If R and S are binary relations on λ-terms, define the relation R → S in the standard way by

\begin{matrix}(R → S)(M, M′) \\ ⟺ (∀N, N′)(R(N, N′) ⟹ S(MN, M′N′)) \end{matrix}

Next, let η range over partial maps from type variables to binary relations, and let ⟨⟩ denote the empty map. We can define R_{t,η} by:

\begin{matrix}R_{d,η}  = & \{(M, M′) | EM =_{β} M′\} \\ R_{v,η}  = & η(v) \\ R_{(s→t),η} = & R_{s,η} → S_{t,η} \\ R_{(μv.t),η} = & ⋂\{S | R_{t,η[S/v]} ⊆ S\} \end{matrix}

We shall always assume that η is defined on all the free variables of t; it is a routine matter to check that this assumption is an invariant of all our calculations. Had our language included other base types o, R_{o} would be the equality relation on the other base types.

Lemma 3 (Fixed-Point Lemma)

1. If R_{(μv.t),η} = S, then S = R_{t,η[S/v]}.

2. If t′ is a closed type, then R_{t,η[t′/v]} = R_{t[t′/v],η}

3. R_{(μv.t),η} = R_{t[(μv.t)/v],η}

Proof

(1) Since all the occurrences of v in t must be positive, the intersection in the last line must be a fixed point. (2) Routine calculation. (3) Follows from (1) and (2).

In the remainder we will consider only closed types, for which we define R_{t} = R_{t,⟨⟩}.

Lemma 4 (Admissibility) If M = M′ and N = N′, then R_{t}(M, N) ⟺ R_{t}(M′, N′).

Proof By induction on the length |t| of t, defined by |d| = 0, |s → t| = |t| + 1, and |μv.t| = |t| + 1. If the type is d, then

\begin{matrix}R_{d}(M, N) ⟺ & EM = N \\ ⟺ & EM′ = N′ \\ ⟺ & R_{d}(M′, N′) \end{matrix}

If the type is s → t, then |t| < |s → t|, so we have

\begin{matrix}R_{s→t}(M, N) ⟺ & [R_{s}(P, Q) ⟹ R_{t}(MP, NQ)] \\ ⟺ & [R_{s}(P, Q) ⟹ R_{t}(M′P, N′Q)] \\ ⟺ & R_{s→t}(M′, N′) \end{matrix}

The last case is that the type is μv.t. Now, since t is of the form t_{1} → … → t_{n} → d, t[μv.t/v] = t_{1}[μv.t/v] → … t_{n}[μv.t/v] → d. So |t[μv.t/v]| = |t| < |μv.t|. So

R_{μv.t}(M, N) ⟺ R_{t[μv.t/v]}(M, N)  Lemma 3
⟺ R_{t[μv.t/v]}(M′, N′)  Lemma 4
⟺ R_{μv.t}(M′, N′)  Lemma 3

The following definition makes the main theorem easier to state.

Definition 5 For substitutions ρ and ρ′ we say (ρ, ρ′) ⊧ A iff for all x ∈ dom(A),

R_{A(x)}(ρ(x), ρ′(x))

We say A ⊧ M : t [W] iff

(ρ, ρ′) ⊧ A ⟹ R_{t}(P ⌊W ⌋ρ, Mρ′)

Theorem 2 (Main Theorem) If A ⊢ M : t [W], then A ⊧ M : t [W].

The theorem says roughly that if M can be assigned type t with annotated term W, then P (⌊W ⌋) and M are related by relation R_{t}. More precisely, it says that if ρ and ρ′ are substitutions related by symbol table (type hypotheses) A, then the corresponding substitution instances of P (⌊W ⌋) and M are also related. This proposition is the generalization of the simple first-order case (E(P ⌊W ⌋) = M) to handle higher-order terms.

Proof The proof is by induction on the structure of the proof of A ⊢ M : t [W]. Thus the proof has five cases, one for each rule of inference for ⊢. For each case, we show that the rule preserves ⊧.

Case 1 (Variable). Assume x ∈ dom(A). Then A ⊢ x : A(x) [x]. We need to show A ⊧ x : A(x) [x]. So assume (ρ, ρ′) ⊧ A. We need to prove that

R_{A(x)}(P ⌊x⌋ρ, xρ′)

holds. We calculate:

R_{A(x)}(P ⌊x⌋ρ, xρ′) ⟺ R_{A(x)}(xρ, xρ′)  definition of P
⟺ R_{A(x)}(ρ(x), ρ′(x))

which holds because (ρ, ρ′) ⊧ A

Case 2 (Static Application). Assume A ⊧ M : s → t [W] and A ⊧ N : s [W′]. We must show A ⊧ MN : t [W W′]. So assume (ρ, ρ′) ⊧ A. We want to show

R_{t}(P ⌊W W′⌋ρ, (MN)ρ′)

By the induction hypotheses, we have R_{s→t}(P ⌊W ⌋ρ, Mρ′) and R_{s}(P ⌊W′⌋ρ, Nρ′). So we have

R_{t}((P ⌊W ⌋ρ)(P ⌊W′⌋ρ), (Mρ′)(Nρ′)) definition of R_{s→t}
R_{t}(((P ⌊W ⌋)(P ⌊W′⌋))ρ, (MN)ρ′)  substitution
R_{t}(P ⌊W W′⌋ρ, (MN)ρ′)  definition of P

Case 3 (Static Abstraction). Assume A[x ↦ s] ⊧ M : t [W]. We need to show that A ⊧ (λx.M) : s → t [λx.W]. So assume (ρ, ρ′) ⊧ A. We need to show

R_{s→t}(P ⌊λx.W ⌋ρ, (λx.M)ρ′)

By the definition of R_{s→t}, it suffices to assume R_{s}(W_{1}, M_{1}) and then show that

R_{t}((P ⌊λx.W ⌋ρ)W_{1}, ((λx.M)ρ′)M_{1})

Now,

\begin{matrix}(P ⌊λx.W ⌋ρ)W_{1} = & ((λx.P ⌊W ⌋)ρ)W_{1} \\ = & (P ⌊W ⌋)ρ[W_{1}/x] \end{matrix}

(we write ρ[N/x] for the substitution mapping x to N and any other variable y to ρ(y); thus ((λx.M)ρ)N =_{β} M(ρ[N/x]).) Furthermore, ((λx.M)ρ′)M_{1} = Mρ′[M_{1}/x], so by Lemma 4 it will suffice to show

R_{t}((P ⌊W ⌋)ρ[W_{1}/x], Mρ′[M_{1}/x])

But (ρ[W_{1}/x], ρ′[M_{1}/x]) ⊧ A[x ↦ s], so the desired conclusion follows from A[x ↦ s] ⊧ M : t [W].

Case 4 (Dynamic Application). Assume A ⊧ M : d [W] and A ⊧ N : d [W′]. We must show A ⊧ MN : d[W W′]. So assume (ρ, ρ′) ⊧ A. We want to show

R_{d}(P ⌊W W′⌋ρ, (MN)ρ′)

We calculate:

E(P ⌊W W′⌋ρ)
= E(P (λabcde.d(⌊W ⌋ρ)(⌊W′⌋ρ))) definition of ⌊−⌋
= E(λabc.b(P ⌊W ⌋ρ)(P ⌊W′⌋ρ))  definition of P
= (E(P ⌊W ⌋ρ))(E(P ⌊W′⌋ρ))  definition of E
= (Mρ′)(Nρ′)  induction hypotheses
= (MN)ρ′  substitution

Case 5 (Dynamic Abstraction). Assume A[x ↦ d] ⊧ M : d [W]. We need to show that A ⊧ λx.M : d [\underline{λ}x.W]. So assume (ρ, ρ′) ⊧ A. We need to show that

R_{d}(P ⌊\underline{λ}x.w⌋ρ, (λx.M)ρ′)

Now, R_{d}(λabc.ax, x) holds, so let ρ_{1} = ρ[λabc.ax/x] and ρ′_{1} = ρ′[x/x] ; then (ρ_{1}, ρ′_{1}) ⊧ A[x ↦ d]. Therefore, by the induction hypothesis, we know that

R_{d}(P ⌊W ⌋ρ_{1}, Mρ′)

that is,

E(P ⌊W ⌋ρ_{1}) = Mρ′_{1}  (1)

Now, to establish R_{d}(P ⌊\underline{λ}x.W ⌋ρ, (λx.M)ρ′), we calculate:

E(P ⌊\underline{λ}x.W ⌋ρ)
= E(P (⌊\underline{λ}x.W ⌋r))  Corollary 1
= E(P (λabcde.e(λx.⌊W ⌋))ρ)  definition of ⌊\underline{λ}x.W ⌋
= E(P (λabcde.e((λx.⌊W ⌋)ρ)))  definition of substitution
= E(λabc.c(λx.P (((λx.⌊W ⌋)ρ)(λabc.ax)))) definition of P
= E(λabc.c(λx.P (⌊W ⌋ρ[(λabc.ax)/x]))) β-reduction
= E(λabc.c(λx.P (⌊W ⌋ρ_{1})))  definition of ρ_{1}
= λx.E(P (⌊W ⌋ρ_{1}))  definition of E
= λx.Mρ′[x/x]  Equation 1
= (λx.M)ρ′

This completes the cases for the proof.

Most of the time we will be concerned with closed terms:

Corollary 2 If M is a closed term, and ∅ ⊢ M : t [W], then R_{t}(P ⌊W ⌋, M).

This specification for a partial evaluator looks rather different from the usual one, so it is useful to check to see that the usual properties of partial evaluators hold. Most often we will be interested in the following case:

Corollary 3 (Specialization Theorem) Let M, N, N′ be closed terms, and let W be an annotation of M with type t → d. If R_{t}(N, N′), then E(P ⌊W ⌋N) = MN′

Proof

R_{t→d}(P ⌊W ⌋, M)  Corollary 2
R_{t}(N, N′)  Assumption
R_{d}(P ⌊W ⌋N, MN′) Definition of R_{t→d}
E(P ⌊W ⌋N) = MN′ Definition of R_{d}

6 Relation to Traditional Partial Evaluation

According to definition 3, (Φ, P) is an off-line partial evaluator iff for all L-programs π and L-data d_{1} and d_{2},

L_{1}(L_{1}(P, Φ(π), d_{1}), d_{2}) = L_{2}(π, d_{1}, d_{2})

In the case of the λ-calculus, programs are closed terms and data are terms. Programs are represented using the coding ⌈−⌉, and the datum Φ(π) is an annotated term, represented using the coding ⌊−⌋. This leaves open the question of how the other data are represented.

The easiest way to do this is to represent the datum d_{1} as ⌈d_{1}⌉ at specialization time (that is, when it is static data), and as itself at run time (when it is dynamic data). Then at specialization time we have

L_{2}(P, Φ(π), d_{1}) = Q
⟺ P ⌊Φ(π)⌋⌈d_{1}⌉ = ⌈Q⌉
⟺ E(P ⌊Φ(π)⌋⌈d_{1}⌉) = Q

but at run time

L_{1}(L_{1}(P, Φ(π), d_{1}), d_{2}) = L_{2}(π, d_{1}, d_{2})
⟺ L_{1}(Q, d_{2}) = L_{2}(π, d_{1}, d_{2})
⟸ Qd_{2} = πd_{1}d_{2}
⟺ E(P ⌊Φ(π)⌋⌈d_{1}⌉)d_{2} = πd_{1}d_{2}

So it will clearly suffice to show that E(P ⌊Φ(π)⌋⌈d_{1}⌉) = πd_{1}. This is accomplished easily:

Corollary 4 (Partial Evaluation Theorem (mixed representation))

Let M be a closed term with an annotation W of type d → d. Then for any closed term N,

E(P ⌊W ⌋⌈N⌉) = MN

Hence P ⌊W ⌋⌈N⌉ is a closed term equivalent under E to MN: that is, it is a program for M specialized to N.

Proof E⌈N⌉ = N, so we have R_{d}(⌈N⌉, N). Therefore, by the Specialization Theorem we have

E(P ⌊W ⌋⌈N⌉) = MN

Here W plays the role of Φ(π). This result also shows the correctness of the partial evaluator using a double encoding, in which d_{1} is represented as ⌈d_{1}⌉ at run time and as ⌈⌈d_{1}⌉⌉ at specialization time (Launchbury, 1991).

It would be better to have a version of partial evaluation that used the same representation for both static and dynamic data. This can be obtained by looking at the types which the binding-time analysis assigns to the representations.

For any type β, let T_{β} denote the type

(μt).((β → β) → (t → t → β) → ((β → t) → β) → β)

This type, introduced in (Mogensen, 1992b), is the type of the representation of λ-terms interpreted as case functions with target β.

Lemma 5 If M is a closed λ-term, and β is any type, then R_{T_{β}}(⌈M⌉, ⌈M⌉).

Proof The proof is by induction on M. As usual we need to consider open terms as well. The induction hypothesis is: Let ρ, ρ′ be substitutions such that for all x ∈ dom(ρ) = dom(ρ′), R_{β}(ρ(x), ρ′(x)). Then R_{T_{β}}(⌈M⌉ρ, ⌈M⌉ρ′).

Now, by the structure of T_{β}, to show R_{T_{β}}(⌈M⌉ρ, ⌈M⌉ρ′) we must show that whenever R_{β→β}(N, N′), R_{T_{β}→T_{β}→β}(P, P′), and R_{(β→T_{β})→β}(Q, Q′), we have

R_{β}((⌈M⌉ρ)NP Q, (⌈M⌉ρ′)N′P′Q′)

We show this for each case in turn:

Case 1 (Variable). We calculate:

R_{β}((⌈M⌉ρ)NP Q, (⌈M⌉ρ′)N′P′Q′)
⟺ R_{β}(((λabc.ax)ρ)NP Q, ((λabc.ax)ρ′)N′P′Q′) definition of ⌈x⌉
⟺ R_{β}(N(ρ(x)), N′(ρ′(x)))  admissibility

But R_{β→b}(N, N′) and R_{β}(ρ(x), ρ′(x)), so R_{β}(N(ρ(x)), N′(ρ′(x))) is true.

Case 2 (Application). We calculate similarly:

R_{β}((⌈M_{1}M_{2}⌉ρ)NP Q, (⌈M_{1}M_{2}⌉ρ′)N′P′Q′)

⟺ R_{β}(((λabc.b⌈M_{1}⌉⌈M_{2}⌉)ρ)NP Q, ((λabc.b⌈M_{1}⌉⌈M_{2}⌉)ρ′)N′P′Q′)

definition of ⌈M_{1}M_{2}⌉

⟺ R_{β}((λabc.b(⌈M_{1}⌉ρ)(⌈M_{2}⌉ρ))NP Q, (λabc.b(⌈M_{1}⌉ρ′)(⌈M_{2}⌉ρ′))N′P′Q′)

substitution

⟺ R_{β}(P (⌈M_{1}⌉ρ)(⌈M_{2}⌉ρ), P (⌈M_{1}⌉ρ′)(⌈M_{2}⌉ρ′))

admissibility

But by the induction hypothesis R_{T_{β}}(⌈M_{1}⌉ρ, ⌈M_{1}⌉ρ′), R_{T_{β}}(⌈M_{2}⌉ρ, ⌈M_{2}⌉ρ′), and by the assumption R_{T_{β}→T_{β}→β}(P, P′), so the last line is true.

Case 3 (Abstraction). Last, we consider the case of λx.M. We claim that R_{β→T_{β}}((λx.⌈M⌉)ρ, (λx.⌈M⌉)ρ′). To establish the claim, assume that R_{β}(S, S′). We must then show that R_{T_{β}}(((λx.⌈M⌉)ρ)S, ((λx.⌈M⌉)ρ′)S′):

\begin{matrix}R_{T_{β}}((λx.⌈M⌉)ρS, (λx.⌈M⌉)ρ′S′) \\ ⟺ R_{T_{β}}(⌈M⌉(ρ[S/x]), ⌈M⌉(ρ′[S′/x])) \end{matrix}

but (ρ[S/x], ρ′[S′/x]) satisfies the conditions of the induction hypothesis, so the last line is true.

Now we can calculate R_{T_{β}}(⌈λx.M⌉ρ, ⌈λx.M⌉ρ′) as before:

R_{β}((⌈λx.M⌉ρ)NP Q, (⌈λx.M⌉ρ′)N′P′Q′)

⟺ R_{β}(((λabc.c(λx.⌈M⌉))ρ)NP Q, ((λabc.c(λx.⌈M⌉))ρ′)N′P′Q′)

definition of ⌈λx.M⌉

⟺ R_{β}((λabc.c((λx.⌈M⌉)ρ))NP Q, (λabc.c((λx.⌈M⌉)ρ′))N′P′Q′)

substitution

⟺ R_{β}(Q((λx.⌈M⌉)ρ), Q′((λx.⌈M⌉)ρ′))

admissibility

but R_{(β→T_{β})→β}(Q, Q′) and R_{β→T_{β}}((λx.⌈M⌉)ρ, (λx.⌈M⌉)ρ′), so the last line is true.

Using this type, we can show the correctness of the partial evaluator using the ⌈−⌉ coding at both specialization time and run time. Using this representation we have that at specialization time

L_{2}(P, Φ(π), d_{1}) = Q
⟺ P ⌊Φ(π)⌋⌈d_{1}⌉ = ⌈Q⌉
⟺ E(P ⌊Φ(π)⌋⌈d_{1}⌉) = Q

as before, but at run time

L_{2}(L_{2}(P, Φ(π), d_{1}), d_{2}) = L_{3}(π, d_{1}, d_{2})
⟺ L_{2}(Q, ⌈d_{2}⌉) = L_{3}(π, ⌈d_{1}⌉, ⌈d_{2}⌉)
⟺ Q⌈d_{2}⌉ = π⌈d_{1}⌉⌈d_{2}⌉
⟺ E(P ⌊Φ(π)⌋⌈d_{1}⌉)⌈d_{2}⌉ = π⌈d_{1}⌉⌈d_{2}⌉

so it suffices to show that E(P ⌊Φ(π)⌋⌈d_{1}⌉) = π⌈d_{1}⌉:

Corollary 5 (Partial Evaluation Theorem (uniform representation))

Let M be a closed term with an annotation W of type T_{d} → d. Then for any closed term N,

E(P ⌊W ⌋⌈N⌉) = M⌈N⌉

Hence P ⌊W ⌋⌈N⌉ is a closed term equivalent under E to M⌈N⌉: that is, it is a program for M specialized to N.

Proof By the main theorem, R_{T_{d}→d}(P ⌊W ⌋, M). By Lemma 5, R_{T_{d}}(⌈N⌉, ⌈N⌉) Therefore, R_{d}(P ⌊W ⌋⌈N⌉, M⌈N⌉), that is E(P ⌊W ⌋⌈N⌉) = MN.

This completes the connection with the “classical” definition of partial evaluation in Section 2.

7 Correctness of the Self-Applications

We next check to see that the properties of the Futamura projections follow from our specification.

7.1 First Projection

The first Futamura projection states that partially evaluating an interpreter with respect to a program gives a translation of the program into the language of the partial evaluator.

To get this projection, Mogensen exhibits the following annotation E^{a} of E with type T_{d} → d:

E^{a} ≡ Y λe.λm.m \begin{matrix}(λx.x) \\ (λmn.(e m) (e n)) \\ (λm.\underline{λ}v.e (m v)) \end{matrix}

where

Y ≡ λh.(λx.h (x x)) (λx.h (x x))

Hence for any closed term M, we have

R_{T_{d}→d}(P ⌊E^{a}⌋, E)  Main Theorem
R_{T_{d}}(⌈M⌉, ⌈M⌉)  Lemma 5
E(P ⌊E^{a}⌋⌈M⌉) = E⌈M⌉ = M Specialization Theorem

So for any N, we have E(P ⌊E^{a}⌋⌈M⌉)N = MN. Hence there is a closed term R such that P ⌊E^{a}⌋⌈M⌉ = ⌈R⌉ and for all N, L(R, N) ≡ L(M, N), as desired.

We can generalize this result to an arbitrary programming language L as defined in Section 2. Assume L is specified by a coding ⟨−⟩ and an interpreter S. If the coding ⟨−⟩ uses either ordinary or higher-order abstract syntax, then the same reasoning as Lemma 5 will hold, so that we get R_{t_{L}}(⟨M⟩, ⟨M⟩) for some type t_{L} that represents the grammar of the language.

If S is compositional, then we can always annotate S with type t_{L} → d. This effectively views S as translating from the programs of the source language into λ-terms (rather than into their meanings). We can do this by marking all of S as dynamic, except for those parts that recursively call S. For example, a fragment of the semantics might be

S⟨e_{1} + e_{2}⟩ = λρ.(+(S⟨e_{1}⟩ρ))(S⟨e_{2}⟩ρ)

where we have explicitly curried the +. We would annotate this as:

S⟨e_{1} + e_{2}⟩ = \underline{λ}ρ.(+ ((S⟨e_{1}⟩) ρ)) ((S⟨e_{2}⟩) ρ)

In the homelier language of backquotes and commas, the right-hand side would be something like

             `(lambda (r) ((+ (,(S e1) r)) (,(S e2) r)))

Now we can state the first projection:

Corollary 6 (First Projection) Let S^{a} be any annotation of S with type t_{L} → d. If P ⌊S^{a}⌋⟨π⟩ = ⌈T ⌉ then T is a translation of π.

Proof Calculating as before, we get

R_{t_{L}→d}(P ⌊S^{a}⌋, S)  Main Theorem
R_{t_{L}}(⟨π⟩, ⟨π⟩)  for any π in the language
E(P ⌊S^{a}⌋⟨π⟩) = S⟨π⟩ Specialization Theorem

So let P ⌊S^{a}⌋⟨π⟩ = ⌈T ⌉. Then

T ⟨d⟩ = E⌈T ⌉⟨d⟩ = E(P ⌊S^{a}⌋⟨π⟩)⟨d⟩ = S⟨π⟩⟨d⟩

as desired.

This projection is the basis for the compilers developed in (Wand, 1982; Clinger, 1984; Wand & Oliva, 1992), etc. In each case, we begin with a suitable semantics (typically a stack semantics) for the source language. The stack semantics (say S) is turned into a compiler by performing a binding-time analysis to separate compiletime and run-time operations, thus getting a compiler S^{a} written in the language of annotated terms. The language of annotated or 2-level terms is a natural language in which to write a compiler, and P acts as the interpreter for 2-level terms, much as E acts as the interpreter for pure λ-terms. We will explore these connections further in Section 8.

7.2 Second projection

The second projection states that partially evaluating the partial evaluator with respect to an interpreter gives a compiler.

Definition 6 If L is a programming language, then a compiler for L is a λ-term C such that for any L-program π, C⟨π⟩ = ⌈T ⌉, where T is a translation of π.

Recall that T is a translation of π iff for all L-data d, T ⟨d⟩ = S⟨π⟩⟨d⟩, where S is the interpreter for L. Therefore, to show C is a compiler, it suffices to show that E(C⟨π⟩) = S⟨π⟩.

We can proceed as before for the syntax ⌊−⌋ of annotations, getting a type

U_{β} = (μt).((β → β)
→ (t → t → β)
→ ((β → t) → β)
→ (t → t → β)
→ ((β → t) → β)
→ β)

for codings of annotated terms (Mogensen, 1992b), and a lemma

Lemma 6 If W is a closed annotated λ-term, and β is any type, then R_{U_{β}}(⌊W ⌋, ⌊W ⌋).

Proof As for Lemma 5.

Mogensen gives the following annotation P^{a} of P with type U_{d} → d:

P^{a} ≡ Y λp.λm.m \begin{matrix}(λx.x) \\ (λww′.(p w) (p w′)) \\ (λw.\underline{λ}v.p (m v)) \\ (λww′.\underline{λ}abc.b (p w) (p w′)) \\ (λw.\underline{λ}abc.c (\underline{λ}v.p (m (\underline{λ}abc.a v)))) \end{matrix}

where

Y ≡ λh.(λx.h (x x)) (λx.h (x x))

Corollary 7 (Second Projection) Let L be a language with interpreter S and annotation S^{a} of type t_{L} → d, and let P^{a} be any annotation of P with type U_{d} → d. If P ⌊P^{a}⌋⌊S^{a}⌋ = ⌈C⌉, then C is a compiler for L.

Proof We have:

R_{U_{d}→d}(P ⌊P^{a}⌋, P)  Main Theorem
R_{U_{d}}(⌊S^{a}⌋, ⌊S^{a}⌋)  Lemma 2
E(P ⌊P^{a}⌋⌊S^{a}⌋) = P ⌊S^{a}⌋ Specialization Theorem

Let P ⌊P^{a}⌋⌊S^{a}⌋ = ⌈C⌉. We can now check to see that C is a compiler:

E(C⟨π⟩)
= E(E⌈C⌉⟨π⟩)
= E(E(P ⌊P^{a}⌋⌊S^{a}⌋)⟨π⟩) definition of ⌈C⌉
= E(P ⌊S^{a}⌋⟨π⟩)  preceding calculation
= S⟨π⟩  first projection

7.3 Third Projection

Futamura’s third projection states that partially evaluating the partial evaluator with respect to itself produces a compiler generator.

Definition 7 A compiler generator is a term G such that for any language L with interpreter S and annotation S^{a} of type t_{L} → d, G⌊S^{a}⌋ = ⌈C⌉, where C is a compiler for L.

Corollary 8 (Third Projection) Let P ⌊P^{a}⌋⌊P^{a}⌋ = ⌈G⌉. Then G is a compiler-generator.

Proof Let P ⌊P^{a}⌋⌊P^{a}⌋ = ⌈G⌉. We first calculate, as before:

R_{U_{d}→d}(P ⌊P^{a}⌋, P)  Main Theorem
R_{U_{d}}(⌊P^{a}⌋, ⌊P^{a}⌋)  Lemma 2
E(P ⌊P^{a}⌋⌊P^{a}⌋) = P ⌊P^{a}⌋ Specialization Theorem

To check that G is a compiler-generator, let us define C by G⌊S^{a}⌋ = ⌈C⌉. We need to show that C is a compiler. Now

⌈C⌉ = G⌊S^{a}⌋ = E⌈G⌉⌊S^{a}⌋
= E(P ⌊P^{a}⌋⌊P^{a}⌋)⌊S^{a}⌋
= P ⌊P^{a}⌋⌊S^{a}⌋  by the preceding calculation

But the second projection showed that if we have ⌈C⌉ = P ⌊P^{a}⌋⌊S^{a}⌋, then C is a compiler. So G is a compiler generator.

Note that these projections were derived solely from the definition of R_{t} and the fact that P satisfied the Main Theorem. They did not depend on the text of P. So they would continue to work for any other partial evaluator that satisfied the Main Theorem. This supports the thesis that the Main Theorem is a proper specification of a partial evaluator.

8 Operational Semantics of the 2-level Lambda Calculus

Elsewhere in this issue, Palsberg (1993) presents a correctness result based on an operational semantics for annotated terms W. In our presentation, the term P serves as an interpreter for annotated terms, yielding a denotational (though not compositional) semantics. In order to compare his results with ours, we present a brief account of an operational semantics for annotated terms.

Recall that the grammar of annotated (or 2-level) terms is given by

W ::= v | W W | λv.W | W W | \underline{λ}v.W

We can define substitution on these terms in the obvious way, treating both λ and \underline{λ} as binders. Let |W | denote the λ-term obtained from a 2-level term W by erasing all the binding-time information.

We can define static reduction on 2-level terms as follows:

Definition 8 →_{s} is the smallest relation on 2-level terms such that:

1. (λx.W)W′ →_{s} W [W′/x]

2. If W →_{s} W′ then W V →_{s} W′V, V W →_{s} V W′ λv.W →_{s} λv.W′, W V →_{s} W′ V, V W →_{s} V W′, and \underline{λ}v.W →_{s} \underline{λ}v.W′.

→_{s}^{∗} is the reflexive, transitive closure of →_{s}.

So static reduction is ordinary β-reduction (on static redexes), closed under congruence of all term-builders. However, dynamic applications and abstractions are never reduced.

We first give a subject reduction theorem for 2-level terms under static reduction:

Theorem 3 (Subject Reduction Theorem) If A ⊢ |W | : t [W] and W →_{s}^{∗} W′, then A ⊢ |W′| : t [W′].

Proof Consider a typed λ-calculus with the same types as considered above, with two constants

\begin{matrix}Dapp : d → d → d \\ Dabs : (d → d) → d \end{matrix}

It is clear that this calculus has the subject reduction property, even in the presence of recursive types, since the usual proof of the subject reduction theorem uses only induction on the size of terms, and not induction on the structure of types. Let us write ⊢_{1} for the typing judgement in this calculus.

We give a translation \overline{(−)} from 2-level terms to terms of this calculus as follows:

\begin{matrix}\overline{v} ≡ & v \\ \overline{W W′} ≡ & \overline{W} \overline{W′} \\ \overline{λv.W} ≡ & λv.\overline{W} \\ \overline{W W′} ≡ & Dapp \overline{W} \overline{W′} \\ \overline{\underline{λ}v.W} ≡ & Dabs(λv.\overline{W}) \end{matrix}

Inspection of the typing rules in the two systems shows that A ⊢ |W | : t [W] ⟺ A ⊢_{1} \overline{W} : t. Furthermore W →_{s} W′ implies \overline{W} → \overline{W′}. So if A ⊢ |W | : t [W] and W →_{s} W′, we have A ⊢_{1} \overline{W} : t. Hence A ⊢_{1} \overline{W′} : t by the subject reduction theorem, and therefore A ⊢ |W′| : t [W′]. The result then follows by induction on the number of reduction steps in the →_{s}^{∗} reduction.

Now we can show that no static reduction of a well-typed term can go wrong.

Definition 9 A confused redex is a subterm of the form (\underline{λ}x.W)V or (λx.W) V.

Corollary 9 (Safety) If A ⊢ M : t [W] and W →_{s}^{∗} W′, then W′ contains no confused redex.

Proof It is easy to see that no confused redex can have a type, and hence no well-typed term can contain a confused redex.

We can also easily show that static reduction is sound with respect to P, that is, it preserves the meaning of 2-level terms. We begin with two lemmas:

Lemma 7 For any 2-level term W, P ⌊λx.W ⌋ = λx.P ⌊W ⌋ and P ⌊\underline{λ}x.W ⌋ = \underline{λ}x.P ⌊W ⌋.

Proof Similar to the corresponding proof for E in (Mogensen, 1992a). We do the case of static abstraction:

P ⌊λx.W ⌋
= P (λabcde.c(λx.⌊W ⌋)) definition of ⌊−⌋
= λv.P ((λx.⌊W ⌋)v)  definition of P
= λx.P ((λx.⌊W ⌋)x)  α-conversion
= λx.P ⌊W ⌋  β-reduction

Lemma 8 For any 2-level terms W and W′, P ⌊W [W′/x]⌋ = (P ⌊W ⌋)[P ⌊W′⌋/x]

Proof By induction on the size of W. We do two representative cases. For the base case, when W ≡ x, we have

(P ⌊x⌋)[P ⌊W′⌋/x]
= x[P ⌊W′⌋/x]  definition of P
= P ⌊W′⌋  substitution
= P ⌊x[W′/x]⌋  substitution

For static abstractions over a variable y distinct from x, we calculate as follows, assuming without loss of generality that a, b, c, d, e, and v are fresh:

P (⌊(λy.V)[W′/x]⌋)
= P (⌊λy′.V [y′/y][W′/x]⌋)  substitution
= P (λabcde.c(λy′.⌊V [y′/y][W′/x]⌋)) definition of ⌊−⌋
= λv.P ((λy′.⌊V [y′/y][W′/x]⌋)v)  definition of P
= λy′.P ((λy′.⌊V [y′/y][W′/x]⌋)y′)  α-conversion
= λy′.P ⌊V [y′/y][W′/x]⌋  β-reduction
= λy′.((P ⌊V [y′/y]⌋)[P ⌊W′⌋/x])  induction hypothesis at V [y′/y]
(V [y′/y] is smaller than λy.V)
= λy′.((P ⌊V ⌋)[P ⌊y′⌋/y][P ⌊W′⌋/x]) induction hypothesis at V
= λy′.((P ⌊V ⌋)[y′/y][P ⌊W′⌋/x])  definition of P
= (λy.P ⌊V ⌋)[P ⌊W′⌋/x]  substitution
= (P ⌊λy.V ⌋)[P ⌊W′⌋/x]  Lemma 7

Theorem 4 (Soundness of static reduction) If W →_{s} W′, then P ⌊W ⌋ = P ⌊W′⌋.

Proof By induction on the definition of →_{s}. For the base case, β-reduction, we have (λx.W)W′ →_{s} W [W′/x]. Then

P ⌊(λx.W)W′⌋
= (P ⌊λx.W ⌋)(P ⌊W′⌋) definition of P
= (λx.P ⌊W ⌋)(P ⌊W′⌋) Lemma 7
= (P ⌊W ⌋)[P ⌊W′⌋/x] β-reduction
= P (⌊W [W′/x]⌋)  Lemma 8

For the induction step, we need to show that if P ⌊W ⌋ = P ⌊W′⌋, then P ⌊W V ⌋ = P ⌊W′V ⌋, P ⌊λx.W ⌋ = P ⌊λx.W′⌋, etc. The application cases are trivial from the compositionality of P; the abstraction cases follow immediately from Lemma 7.

9 Comparison with Related Work

Mogensen (1992b) is the primary source for our development. He exhibits the various terms above. He also includes the binding-time annotations that allow the partial evaluator to be self-applied. He proves the correctness of the self-interpreter (Mogensen, 1992a), but does not give either a specification or proof of the partial evaluator.

Gomard (1992) discusses a larger self-applicable partial evaluator in a two-level λ-calculus with constants. He gives a correctness criterion similar in intent to ours. Our specification is simpler because it avoids the model-theoretic details and assumptions used in (Gomard, 1992).

Both Mogensen and Gomard, as do we, use a two-level type system like that of Nielson and Nielson (1988), except that the run-time code is untyped. Launchbury (1991) discusses the encoding issues for a strongly-typed self-applicable partial evaluator with a full multi-level type system. However, he remarks in Section 6 of (Launchbury, 1991) that the same encoding issues arise in the untyped case. This paper is in part an attempt to sort out these issues.

Launchbury (1989) gives a characterization of binding-time analysis in terms of congruence relations: a quantity may be deferred to run-time if its value does not alter the result of the compile-time computation. This idea was neatly extended to higher-order computations and partially-static structures by Hunt and Sands (1991) using partial equivalence relations. Unfortunately, this characterization does not seem to be strong enough to justify emitting code on the basis of the bindingtime analysis, which is our primary goal.

Consel (1990) presents an algorithm for binding time analysis for a higher-order untyped language with partially static structures, based on an abstract interpretation. However, no correctness criterion is stated. It would be interesting to see how our approach might handle partially static structures. More recently, Consel and Khoo (1992) have shown the correctness of on-line and off-line partial evaluators for a first-order language using an instrumented semantics; in this framework binding-time analysis appears as an abstract interpretation of the on-line partial evaluation. They then derive the off-line specializer (corresponding to our P) from the on-line partial evaluator by coarsening the tests to depend only on the data available from the binding-time analysis. Their approach also shows the correctness of the binding-time analysis and specialization together, but the technical details seem quite different from ours; their approach is heavily dependent on model-theoretic details that we have been able to avoid. It would be interesting to see if our results could be adapted to give a simpler account in the first-order case.

Palsberg (1993) gives an operational semantics of 2-level λ-terms equivalent to the account in Section 8. His main result is analogous to our Corollary 9, which states that no static reduction of a well-typed 2-level term can go wrong. He identifies a subclass of the static reductions, which he calls the top-down reductions, and a different notion of acceptability, which he calls well-annotatedness. He then shows that no top-down reduction of a well-annotated term can go wrong. In comparison with our Corollary 9, his result allows more 2-level terms to be considered, but restricts the class of permissible reductions.

10 Conclusions

This paper is part of an investigation into the nature of program analysis and optimization. The goal of program analysis is to annotate a program with certain propositions about the behavior of that program. One can then apply optimizations to the program that are justified by those propositions. Typically, an analysis is specified by a set of local consistency conditions (the “flow equations”). Our approach is to show that any solution of the consistency conditions justifies the resulting transformation.

We have carried through this program for binding-time analysis. Following (Gomard, 1990; Mogensen, 1992b), we formulated binding-time analysis as the solution of a set of local constraints (the typing rules). We then showed that any such solution was a valid input to a simple program specializer, that is, if the specializer is given any annotation of the input program that satisfies the local constraints, its output is a suitably specialized version of the input program.

In order to do this, we formalized the notion of a “suitably specialized version of the input program.” Our version of this notion is similar to, but simpler than, the specification given by Gomard (1992). We then showed that the typical properties of partial evaluators, such as the Futamura projections, follow from the specification.

By considering both an analysis and the transformation it justifies together, this proof suggests a framework for incorporating flow analyses into verified compilers. By separating this soundness result from the algorithm for solving the flow equations, we obtain much simpler proofs, avoiding the many model-theoretic details that complicate typical proofs involving abstract interpretation.

This work suggests that the proposition associated with a program analysis can simply be that “the optimization works.” This avoids a morass of model-theoretic details, at the expense of needing to know what it means for the proposed optimization to work for each possible result of the flow analysis. Thus the flow analysis and its enabled optimization should be proved correct together.

22 M. Wand

Acknowledgements

Thanks to Bob Muller, whose questions in our seminar got me started on this topic, and to Neil Jones, Torben Mogensen, Jens Palsberg, and Carsten Gomard for their extensive E-mail discussions and comments.

References

Barendregt, Henk. 1991. Self-interpretation in lambda calculus. Journal of functional

programming, 1(2), 229–234. Clinger, William. 1984 (Aug.). The scheme 311 compiler: An exercise in denotational

semantics. Pages 356–364 of: Proc. 1984 ACM Symposium on Lisp and Functional Programming.

Consel, Charles. 1990. Binding time analysis for higher order untyped functional languages. Pages 264–272 of: Proc. 1990 ACM Symposium on Lisp and Functional Programming.

Consel, Charles, & Khoo, Siau Cheng. 1992 (June). On-line & off-line partial evaluation: Semantic specifications and correctness proofs. Tech. rept. YALEU/DCS/RR-912. Yale University Department of Computer Science.

Gomard, Carsten K. 1990. Partial type inference for untyped functional programs. Pages

282–287 of: Proc. 1990 ACM Symposium on Lisp and Functional Programming. Gomard, Carsten K. 1992. A self-applicable partial evaluator for the lambda calculus:

Correctness and pragmatics. Acm transactions on programming languages and systems, 14(2), 147–172.

Henglein, Fritz. 1991. Efficient type inference for higher-order binding-time analysis. Pages 448–472 of: Hughes, J. (ed), Functional programming languages and computer architecture, 5th acm conference. Lecture Notes in Computer Science, vol. 523. Berlin, Heidelberg, New York: Springer-Verlag.

Hunt, Sebastian, & Sands, David. 1991. Binding time analysis: A new perspective. Pages 154–165 of: Proceedings of the symposium on partial evaluation and semantics-based program manipulation. SIGPLAN Notices 26(9), September, 1991.

Jorring, U., & Scherlis, William L. 1986. Compilers and staging transformations. Pages

86–96 of: Conf. Rec. 13th ACM Symposium on Principles of Programming Languages. Launchbury, John. 1989 (Nov.). Projection factorizations in partial evaluation. Ph.D.

thesis, University of Glasgow. Launchbury, John. 1991. A strongly-typed self-applicable partial evaluator. In: Hughes,

John (ed), Functional programming languages and computer architecture, vol. 523. Berlin, Heidelberg, and New York: Springer-Verlag.

Mogensen, Torben Æ. 1992a (June). Efficient self-interpretation in lambda calculus. to

appear. Mogensen, Torben Æ. 1992b. Self-applicable partial evaluation for pure lambda calculus.

Pages 116–121 of: Consel, Charles (ed), Acm sigplan workshop on partial evaluation and semantics-based program manipulation.

Nielson, Flemming, & Nielson, Hanne Riis. 1988. Two-level semantics and code generation.

Theoretical computer science, 56, 59–133. Palsberg, Jens. 1993. Correctness of binding time analysis. Journal of functional program-

ming, 11. Pfenning, Frank, & Elliott, Conal. 1988 (June). Higher-order abstract syntax. Pages

199–208 of: Proceedings sigplan ’88 conference on programming language design and implementation.

Wand, Mitchell. 1982. Deriving target code as a representation of continuation semantics.

Acm transactions on programming languages and systems, 4(3), 496–517. Wand, Mitchell, & Oliva, Dino P. 1992. Proving the correctness of storage representations.

Pages 151–160 of: Proc. 1992 ACM Symposium on Lisp and Functional Programming.