Specifying the Correctness of Binding-Time Analysis

Mitchell Wand^{∗}

College of Computer Science Northeastern University

360 Huntington Avenue, 161CN Boston, MA 02115, USA

wand@flora.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 the incorporating flow analyses into verified compilers.

1 Introduction

Mogensen [11] has exhibited a very compact self-applicable partial evaluator for the pure lambda-calculus, using bindingtime analysis followed by specialization. He suggests that one virtue of such a “minimalist” approach is that it might allow mathematical analysis of the resulting structure. Here we do just that: we state a correctness criterion for such an off-line partial evaluator and show that Mogensen’s partial evaluator is correct with respect to this specification. The specification is similar to, but simpler and stronger than, the specification given by Gomard [5]. We then show that the typical properties of partial evaluators, such as the Futamura projections, follow from the specification.

Although there are some technical details in the proofs, the major contribution of this paper is the formulation of the specification. The traditional specification of partial evaluators is insufficiently specific to generate a correctness proof for partial evaluation of higher-order terms containing free variables. For example, Mogensen writes that his representation strategy “[has] the effect that the partial evaluator will only work on closed λ-terms.” Yet in the course of partially evaluating a closed term, his algorithm manipulates open terms as well. So the correctness criterion must be strong enough to specify the behavior of the algorithm on open terms. Our specification simplifies and clarifies the specification given by Gomard [5] for his self-applicable partial evaluator. Our criterion is strong enough to specify the behavior of the partial evaluator when it is applied to itself.

This paper is part of a larger investigation into the nature of flow analysis and optimization. The goal of flow 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. However, it has proven remarkably difficult to specify the semantics of these propositions in a way that justifies the resulting optimizations. Following Gomard [4], we formulate binding-time analysis as a solution of a set of constraints on the annotation of a program (that is, as an annotated type-inference tree for a certain type system). Our correctness result shows that any solution to this set of constraints justifies the resulting staging transformation [7]. Thus our result holds for any algorithm that solves such constraint systems.

This work suggests that the proposition associated with a flow 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.

This paper is organized as follows: In Section 2 we show how λ-terms can be coded as normal forms inside the λcalculus. In Sections 3 and 4 we present Mogensen’s selfevaluator and partial evaluator, respectively. In Section 5 we state and prove our main theorem relating binding-time analysis and partial evaluation, and show how the expected specialization behavior of the partial evaluator follows from the main theorem. In Section 6 we consider self-application of the partial evaluator, and show how the Futamura projections can be derived from the main theorem. Section 7 compares our work to other approaches to binding-time analysis, and Section 8 gives some conclusions.

2 Representing λ-Terms in Pure λ-calculus

When considering the expressive power of pure λ-calculus, one must show how the quantities to be manipulated are expressed in the λ-calculus. Thus, 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 ⌈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)⌉.

∗Work supported by the National Science Foundation under grant numbers CCR-9002253 and CCR-9014603.

To carry out this program for λ-terms themselves, Mogensen uses the following coding:

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

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 casefunction. 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” [13], in which the binding operators in the represented language are modelled by binding in the lambda-calculus. Any free occurrences of x in λx.M will be bound by the x in λx.⌈M⌉.

The usual terminology of partial evaluation discusses a language L and the assertion L(pgm, data) = output. For the λ-calculus, where the inputs and outputs are λ-terms themselves, we can interpret this assertion using the coding ⌈−⌉, as

Definition 1

L(M, N) ≡ R ⟺ M⌈N⌉ =_{β} ⌈R⌉

Similarly, we write

L(M, [N_{1}, …, N_{k}]) ≡ R ⟺ M⌈N_{1}⌉ … ⌈N_{k}⌉ =_{β} ⌈R⌉

Here we write M ≡ N to signify that M and N are identical up to conversion. When the inputs or outputs come from other sets, then we will use whatever codings are appropriate.

3 The Self-Interpreter

A self-interpreter is a λ-term E such that E⌈M⌉ =_{β} M [1]. 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 (λem.m (λx.x)
(λmn.(em)(en))
(λm.λv.e(mv)))

where Y is the standard fixpoint operator. It is also easy to show, by structural induction on M, that E⌈M⌉ = M for any λ-term M [10]. Thus L(M, N) ≡ R iff E⌈M⌉⌈N⌉ = R. Furthermore, L(E, [M, N]) ≡ R iff E⌈E⌉⌈M⌉⌈N⌉ = ⌈R⌉ iff E⌈M⌉⌈N⌉ = ⌈R⌉ iff L(M, N) ≡ R, so E is an interpreter under the usual definition (e.g. [5]).

4 The Partial Evaluator

The partial evaluator is divided into two phases: bindingtime analysis and specialization. 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 [4]. 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 λ-terms. The other types are built from d in the usual way, and correspond to the types one might find in an ordinary compiler.

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 (compiletime) calculations, and the last two correspond to dynamic (residual, run-time) operations, which correspond at compiletime to emitting code. 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[x ↦ t_{1}] ⊢ M : t_{2} [W]}{A ⊢ (λx.M) : t_{1} → t_{2} [λx.W]}

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

\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]}

We can use a representation scheme for annotated terms similar to that for ordinary λ-terms:

\begin{matrix}⌊x⌋ ≡ & λabcde.ax \\ ⌊MN⌋ ≡ & λabcde.b⌊M⌋⌊N⌋ \\ ⌊λx.M⌋ ≡ & λabcde.c(λx.⌊M⌋) \\ ⌊M N⌋ ≡ & λabcde.d⌊M⌋⌊N⌋ \\ ⌊\underline{λ}x.M⌋ ≡ & λabcde.e(λx.⌊M⌋) \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 (V ar x)  = & x \\ P (App W W′) = & (P W)(P W′) \\ P (Abs 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}

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(m(λabc.av)))))

5 The Correctness Criterion

All this is in [11]. Now we address something new: the question of the correctness of P. The correctness condition 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. Hence our correctness criterion must be defined at all types.

We do this by using the technique of logical relations. For every closed type t, we define a binary relation R_{t} on λ-terms as follows:

R_{d}(M, M′) ⟺ EM = M′
R_{s→t}(M, M′)
⟺ (∀N, N′)(R_{s}(N, N′) ⟹ R_{t}(MN, M′N′))

We extend this to recursive types (μv.t) by defining R_{(μv.t)} as the evident least fixpoint; this is defined since all the occurrences of v in t are positive. The details are shown in Appendix A.

For substitutions ρ and ρ′ we say (ρ, ρ′) ⊧ A iff for all x ∈ dom A, R_{A(x)}(ρ(x), ρ′(x)).

Now we can state the main theorem:

Theorem 1 (Main Theorem) if A ⊢ M : t [W], and (ρ, ρ′) ⊧ A, then R_{t}(P ⌊W ⌋ρ, Mρ′).

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 related. This proposition is the generalization of the simple first-order case (E(P ⌊W ⌋) = M) to handle higher-order terms.

The proof is by induction on the construction of the proof of A ⊢ M : t [W]. There are 5 cases, one for each proof rule. The proof is shown in Appendix A.

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

Corollary 1 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. The following corollary encapsulates most of our reasoning about partial evaluators:

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

Proof:

R_{t→d}(P ⌊M^{a}⌋, M)  Main Theorem
R_{t}(N, N′)  Assumption
R_{d}(P ⌊M^{a}⌋N, MN′) Definition of R_{t→d}
E(P ⌊M^{a}⌋N) = MN′ Definition of R_{d}

□

We can complete the connection the usual notion of partial evaluation by:

Corollary 3 (Partial Evaluation Theorem) Let M be a program with an annotation M^{a} of type d → d. Then for any program N,

E(P ⌊M^{a}⌋⌈N⌉) = MN

Hence P ⌊M^{a}⌋⌈N⌉ is a program equivalent under E to MN: that is, it is a program for M specialized to N.

Proof: We can always annotate a closed program N by making it entirely dynamic. Let N^{d} be the annotation that does this. Now E⌈N⌉ = N, so we have R_{d}(⌈N⌉, N). Therefore, by the Specialization Theorem we have

E(P ⌊M^{a}⌋⌈N⌉) = MN

□

In some sense, this corollary is the result that we were aiming for: it justifies the use of binding-time analysis together with the algorithm P to produce a specialized version of the input program.

6 Correctness of the Self-Applications

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

Before checking the Futamura projections, we need a bit of notation and a lemma. For any type β, let T_{β} denote the type

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

This is the type of the representation of λ-terms interpreted as case functions with target β.

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

Proof: 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_{T_{β}} (ρ(x), ρ′(x)). Then R_{T_{β}} (⌈M⌉ρ, ⌈M⌉ρ′) The proof is by induction on M. □

6.1 First Projection

The first Futamura projection states that partially interpreting an interpreter with respect to a program gives the same result as compiling 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 we have

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

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

In general, we can specify a programming language by giving a coding ⟨−⟩ from programs and data in the language into the λ-calculus, and a λ-term S which is the semantics or interpreter for the language. We can then define the inputoutput behavior of the language by

L_{S}(P, D) ≡ D′ ⟺ S⟨P ⟩⟨D⟩ = ⟨D′⟩

A translation of a program π is a λ-term T such that for all S-data D, L(T, D) ≡ L_{S}(π, D), that is, T ⟨D⟩ = S⟨π⟩⟨D⟩. Here we have extended the definition of L to include the coding ⟨−⟩, as contemplated in the original definition.

If the coding ⟨−⟩ uses either ordinary or higher-order abstract syntax, then the same reasoning as Lemma 1 will hold, so that we get R_{t}(⟨M⟩, ⟨M⟩) for some type t that represents the grammar of the language.

If S is compositional, then we can always annotate S with type t → 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 actually assemble the pieces into a λ-term. 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 4 (First Projection) If T ≡ L(P, [S, π]), then T is a translation of π.

Proof: Calculating as before, we get

R_{t→d}(P ⌊S^{a}⌋, S)  Main Theorem
R_{t}(⟨π⟩, ⟨π⟩)  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⟩

so L(T, D) ≡ S(π, D) as desired. □

6.2 Second projection

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

A compiler for S is a λ-term C such that for any Sprogram π and S-data D, L(C, π) ≡ T where T is a translation of π, that is, C⟨π⟩ = ⌈T ⌉, where T ⟨D⟩ = S⟨π⟩⟨D⟩. So 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, and a lemma

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

Proof: As for Lemma 1. □

Corollary 5 (Second Projection) If C ≡ L(P, [P^{a}, S^{a}]), then C is a compiler for S.

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

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

where

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

Hence 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

So, let C ≡ L(P, [P^{a}, S^{a}]), that is 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

□ 6.3 Third Projection

Futamura’s third projection states that L(P, [P, P]) produces a compiler generator, that is, a term G such that for any interpreter S, L(G, S) ≡ C where C is a compiler for S. That is, G⌊S^{a}⌋ = ⌈C⌉, where C is a compiler for S.

Corollary 6 (Third Projection) Let G ≡ L(P, [P^{a}, P^{a}]). Then G is a compiler-generator.

Proof: Let G ≡ L(P, [P^{a}, P^{a}]) ,that is, 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 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.

7 Comparison with Related Work

Mogensen [11] is the primary source for our development. He exhibits the various terms above. He also includes the binding-time annotations that allows the partial evaluator to be self-applied. He proves the correctness of the selfinterpreter [10], but does not give either a specification or proof of the partial evaluator.

Gomard [5] 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 [5].

Both Mogensen and Gomard, as do we, use a two-level type system like that of Nielson and Nielson [12], except that the run-time code is untyped. Launchbury [9] 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 [9] that the same encoding issues arise in the untyped case. This paper is in part an attempt to sort out these issues.

Launchbury [8] 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 [6] using partial equivalence relations. Unfortunately, this characterization does not seem to be strong enough to justify emitting code on the basis of the binding-time analysis, which is our primary goal.

Consel [2] 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 have shown the correctness of on-line and off-line partial evaluators for a first-order language using an instrumented semantics [3]; 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.

8 Conclusions

We have given a correctness criterion for a partial evaluator based on binding-time analysis. Our criterion is simpler than others proposed in the literature and is sufficiently powerful to specify the behavior of the partial evaluator in the case of self-application.

We consider this proof as being about binding-time analysis: the point of binding-time analysis is to justify the replacement of potentially expensive run-time computations by presumably cheaper compile-time computations whenever possible. Our correctness criterion is strong enough to justify this transformation. By considering both a flow analysis and the transformation it justifies together, this proof suggests a framework for the incorporating flow analyses into verified compilers.

Acknowledgements

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

Appendix A: Proof of the Main Theorem

We first state some lemmas. We will use the symbol = to denote β-convertibility, and ≡, when necessary, to distinguish congruence of λ-terms.

Lemma 3 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⌋[N/x][y′/y])  x ≢ y
= λy′.((P ⌊M⌋)[N/x])[y′/y]  induction hypothesis
= (λy.P ⌊M⌋)[N/x]  substitution
= P (⌊λy.M⌋)[N/x]  definition of P

□

Corollary 7 (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 ⌊−⌋: P (⌊W ⌋ρ) ≠ P (⌊W ρ⌋). 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.

We now define the relations R_{t} for each type t. If R and S are binary relations on λ-terms, we 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}

Let η range over maps from type variables to binary relations. Then 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 | S = R_{t,η[S/v]}\} \end{matrix}

Since all of the occurrences of v in t must be positive, the least fixed point in the last line must exist and must be a fixed point. In the remainder we will consider only closed types, for which we define R_{t} = R_{t,∅}. Had our language included other base types o, R_{o} would be the equality relation on the other base types.

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

\begin{matrix}R_{μv.t}(M, N) ⟺ & R_{t[μv.t/v]}(M, N) \\ ⟺ & R_{t[μv.t/v]}(M′, N′) \\ ⟺ & R_{μv.t}(M′, N′) \end{matrix}

□

For substitutions ρ and ρ′ we say (ρ, ρ′) ⊧ A iff for all x ∈ dom A, R_{A(x)}(ρ(x), ρ′(x)).

For the proof, it is easiest to reformulate the main theorem using using one more bit of notation. We say A ⊧ M : t [W] iff (ρ, ρ′) ⊧ A ⟹ R_{t}(P ⌊W ⌋ρ, Mρ′). Now the main theorem becomes:

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

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 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 x to ρ(x); thus ((λx.M)ρ) =_{β} M(ρ[N/x]).) Furthermore, ((λx.M)ρ′)M_{1} = Mρ′[M_{1}/x], so 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 3 (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}, ρ′) ⊧ A[x ↦ d]. Therefore, by the induction hypothesis, we know that R_{d}(P ⌊W ⌋ρ_{1}, Mρ′), that is,

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

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

E(P ⌊\underline{λ}x.W ⌋ρ)

= E(P (λabcde.e(λx.⌊W ⌋))ρ)  def’n of ⌊\underline{λ}x.W ⌋
= E(λabc.c(λx.P ((λx.⌊W ⌋)(λabc.ax)))ρ) definition of P
= E(λabc.c(λx.P (((λx.⌊W ⌋)ρ)(λabc.ax)))) Lemma 7

= E(λabc.c(λx.P (⌊W ⌋ρ[(λabc.ax)/x])))

= 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)ρ′

Case 4 (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 5 (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′⌋ρ))) = E(λabc.b(P ⌊W ⌋ρ)(P ⌊W′⌋ρ)) = (E(P ⌊W ⌋ρ))(E(P ⌊W′⌋ρ))

= (Mρ′)(Nρ′)  induction hypotheses

= (MN)ρ′

This completes the cases for the proof. □

References

[1] Henk Barendregt. Self-Interpretation in Lambda Calculus. Journal of Functional Programming, 1(2):229–234, April 1991.

[2] Charles Consel. Binding Time Analysis for Higher Order Untyped Functional Languages. In Proc. 1990 ACM Symposium on Lisp and Functional Programming, pages 264–272, 1990.

[3] Charles Consel and Siau Cheng Khoo. On-line & Off-line Partial Evaluation: Semantic Specifications and Correctness Proofs. Technical Report YALEU/DCS/RR-912, Yale University Department of Computer Science, June 1992.

[4] Carsten K. Gomard. Partial Type Inference for Untyped Functional Programs. In Proc. 1990 ACM Symposium on Lisp and Functional Programming, pages 282–287, 1990.

[5] Carsten K. Gomard. A Self-Applicable Partial Evaluator for the Lambda Calculus: Correctness and Pragmatics. ACM Transactions on Programming Languages and Systems, 14(2):147–172, 1992.

[6] Sebastian Hunt and David Sands. Binding Time Analysis: A New PERspective. In Proceedings of the Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pages 154–165, 1991. SIGPLAN Notices 26(9), September, 1991.

[7] U. Jorring and William L. Scherlis. Compilers and Staging Transformations. In Conf. Rec. 13th ACM Symposium on Principles of Programming Languages, pages 86–96, 1986.

[8] John Launchbury. Projection Factorizations in Partial Evaluation. PhD thesis, University of Glasgow, November 1989.

[9] John Launchbury. A Strongly-Typed Self-Applicable Partial Evaluator. In John Hughes, editor, Functional Programming Languages and Computer Architecture, volume 523, Berlin, Heidelberg, and New York, 1991. Springer-Verlag.

[10] Torben Æ. Mogensen. Efficient Self-Interpretation in Lambda Calculus. to appear, June 1992.

[11] Torben Æ. Mogensen. Self-applicable Partial Evaluation for Pure Lambda Calculus. In Charles Consel, editor, ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, pages 116–121, 1992.

[12] Flemming Nielson and Hanne Riis Nielson. Two-Level Semantics and Code Generation. Theoretical Computer Science, 56:59–133, 1988.

[13] Frank Pfenning and Conal Elliott. Higher-Order Abstract Syntax. In Proceedings SIGPLAN ’88 Conference on Programming Language Design and Implementation, pages 199–208, June 1988.