Jones N.D.Partial evaluation and automatic program generation.1999

BTA by solving constraints 181

1.(inequality constraint rules)

(a)C [ f ! 0 f , ! ' f g

) C [ f ! 0 f , = , 0 = ' g if is a type variable

(b)C [ f ! 0 f , S b g

) C [ f ! 0 f , S b , = Dg if is a type variable

(c) C [ f ! 0 f , b ' g

)C [ f ! 0 f , = ' g

(d)C [ f S b , b 0 g

)C [ f S b , S b 0, > 0 g if , 0 are type variables

(e)C [ f S b 0, b 0 g

)C [ f S b , S b 0, > 0 g if , 0 are type variables

(f)C [ f S b , S b g ) C [ f S b g

(g)C [ f ! 0 f D g ) C [ f = D, 0 = D g

(h)C [ f S b D g ) C

(i)C [ f S b S g ) C

(j)C [ f D b g ) C [ f D = g

(k)C [ f b D g ) C [ f S b g if is a type variable

2.(equational constraint rules)

(a)C [ f = g ) C

3.(dependency constraint rules)

(a)C [ f > D g ) C

(b)C [ f S > g ) C

(c)C [ f D > g ) C [ f = D g

4.(occurs check rule)

(a)C ) C [ f = D g if C is cyclic and is on a cycle in G(C).

Figure 8.5: Transformation rules for constraint systems.

182 Partial Evaluation for the Lambda Calculus

Proof

1.De ne a megastep as follows: apply any applicable rule and then apply the equational constraint transformation rules exhaustively. It is easy to see that every megastep terminates and that after it terminates all equational constraints have been eliminated. Let c be the number of constraints; n the number of variables occurring in them; and v the number of inequality constraints with a variable on the left-hand side. It is easy to check that every megastep decreases the sum c + n + 2v by at least one. Consequently every sequence of megasteps terminates.

2.By de nition of normal form.

3.None of the rules introduce b-inequalities with a variable on the left-hand side.

2

From a constraint system C in normal form we can nd a solution that characterizes a minimal completion of the original expression e. Consider two completions te1 and te2. If an operator is static in te1 and dynamic in te2, then there will be at least one subexpression of type D in te2, where the corresponding subexpression in te1 has a type t 6= D.

Now let C be a normal form constraint system. The normalization process can have forced subexpressions to have type D, but these subexpressions must be dynamic in all completions (cf. Proposition 8.4). To ensure that no other subexpressions get type D, we interpret all inequalities in C as equations. Since C is a normal form constraint system, by Proposition 8.5, part 2, these equations have a most general uni er U [163]. Let BS be the substitution that maps every type variable occurring in U(C) to S. Since neither U nor BS substitutes D for any type variable, all the dependency constraints in C are trivially satis ed.

Note that there may be other ways of choosing a minimal completion, since some substitutions of D for a type variable correspond to moving a lift-expression (see Section 8.4). Avoiding type D whenever possible is a simple way to choose one minimal completion.

8.7.5Binding-time analysis algorithm

Given an expression e and a binding-time assumption , do the following:

1. Generate the constraint system C = C (e) (Section 8.7.3).

V

2. Compute normal form constraint system Cnf such that C )+ Cnf (Section 8.7.4).

184 Partial Evaluation for the Lambda Calculus

E[[T [[te]] s]] d = E[[ (te)]]

There may be two reasons why one side is de ned while the other is not.

1.If a call-by-value strategy is used then the right side may be unde ned while the left side is de ned. This is because unfolding can discard non-terminating expressions (Section 5.5.2). Suppose we have

( x.2) bomb

where bomb is a non-terminating expression made residual thus trivially terminating at partial evaluation time. Partial evaluation will discard the bomb, but evaluation of (( x.2) bomb) will loop under call-by-value. What has been said elsewhere in the chapter does not rely on any speci c evaluation strategy, but the correctness result does rely on our lambda calculus being non-strict. For a strict language, a weaker result holds: if both sides are de ned, they are equal.

2.As often mentioned it is hard to guarantee termination for a non-trivial partial evaluator as Lambdamix, and it is easy to construct an example where T loops on te where normal evaluation of (te) would terminate. When

proving E[[T [[te]] s]] d = E[[ (te)]] we shall assume that T is well-de ned on all subexpressions of te. To get a smoother proof we shall make an even stronger assumption, namely that the binding-time analysis ensures that T is total. (Given any one concrete program to partially evaluate the two assumptions are identical.) If we lift this restriction our correctness result will be weakened to: if both sides are de ned, they are equal. To get such a non-trivial binding-time analysis ensuring termination of Lambdamix, the techniques from Chapter 14 must be generalized to a higher-order language and this has not yet been done.

The rest of the section is devoted to the formalization and proof of the correctness result outlined above. Readers who are not interested may go straight to the next section without loss of continuity.

8.8.2The correctness theorem

The relation R to be de ned below (De nition 8.7) is central to the correctness proof. Intuitively, the relation R expresses that the function T handles a given twolevel expression te correctly. For an expression of type S, let the initial environmentbe split into a specialization-time part s and a run-time part d. Relation R implies that the result of partial evaluation must be the right answer:

T [[te]] s = E[[ (te)]]

Correctness of Lambdamix 185

expressing that if te has type S then normal evaluation of the unannotated expression yields the same result as partial evaluation of the annotated expression. For an expression of type D, relation R implies that the result of partial evaluation must be an expression, the residual program, which when evaluated yields the right answer:

E[[T [[te]] s]] d = E[[ (te)]]

For expressions of a function type, R expresses that the result of applying the function to a proper argument yields a proper answer.

De nition 8.7 The relation R holds for (te, s, d, , t) 2 2Exp 2Env Env

Env Type i

1.` te : t if suits s,

2.One of the following holds

(a)te has type S and T [[te]] s = E[[ (te)]]

(b)te has type D and E[[T [te]] s]] d = E[[ (te)]]

(c)te has type t = t1 ! t2 and for all te1: R(te1, s, d, , t1) implies R(te te1, s, d, , t2)

2

Note that the recursive de nition of R has nite depth since in the de nition of R(te, s, d , , t), the recursive applications of R, concern tuples (te0, 0s, 0d , 0, t0) where t0 has fewer type constructors than t.

Since an expression may have free variables, the environments involved s, d,must in some sense be well-behaved. It turns out that the condition on the environments can also be formulated in terms of R.

De nition 8.8 Given a set of identi ers, VarSet, and three environments, , s, d and a type environment that suits s, we say that s, d, agree on VarSet i

Suppose s, d, agree on VarSet. Then for all variables of type S: s(x) =(x), and for variables y of type D: d( s(y)) = (y). For a higher-order example: Suppose s maps identi er f to a function of type S ! S. By expanding the de nitions of `agreement' and R we nd that 8 te1: T [[te1]] s = E[[te1]] implies T [[f te1]] s = E[[f te1]] .

Theorem 8.1 (Main Correctness Theorem) Assuming that binding-time analysis ensures that T is de ned on all arguments to which it is applied, the following holds:

For all s, d, , , simultaneous ful lment of the following three conditions

186Partial Evaluation for the Lambda Calculus

1.suits s,

2.s, d, agree on FreeVars(te),

3.` te : t for some type t,

implies that R(te, s, d, , t) also holds.

Proof The proof proceeds by induction on the structure of te. The proofs for the most interesting cases are found below. The remaining cases are proven elsewhere [105]. 2

Corollary 8.1 Assume te, s, d, , given such that suits s, and s, d, agree on FreeVars(te).

1. If ` te : S then T [[te]] s = E[[ (te)]]

2. If ` te : D then E[[T [[te]] s]] d = E[[ (te)]]

2

We now introduce a name, H, for the property expressed by Theorem 8.1. H is also used as induction hypothesis in the proof. H expresses that if environments agree on the free variables of a well-annotated two-level expression then the relation R will hold for the expression, the environments, and the type.

De nition 8.9 Given a two-level expression te, H(te) holds if 8 s, d, , the following three conditions

The proofs of the di erent cases all proceed in the same way. Assume te, s,d, , are given such that the three conditions of De nition 8.9 are ful lled. The inductive assumption gives that H(te0) for the subexpressions of te. Except in the case of abstraction the free variables of te are exactly those of the largest proper subexpressions of te. Thus s, d, agree on the free variables of these expressions too (in the case of abstraction we have to construct some new environments 0s, 0d,0). By well-annotatedness of te the subexpressions are also well-annotated and the inference rules of Figure 8.4 give us types for the subexpressions. This gives us some facts of the form R(sub-texp, s, d, , t0) which then leads (with more or less trouble) to the goal: R(te, s, d, , t).

Case: x.te

Proof Assume s, d, , are given satisfying the conditions in De nition 8.9. It thus holds that ` x.te : t00 where t00 must have the form t0 ! t. Assume furthermore that te0 is given such that R(te0, s, d, , t0). By alpha conversion of x.te we can assume without loss of generality that x does not occur in any expressions other than the subexpressions of x.te.

Correctness of Lambdamix 187

De ne 0s = s [x 7! T[[te0]] s] and0 = [x 7! [[E (te0)]] ] and

0 = [x 7!t0]

and observe that 8 id 2 FreeVars(te): R(id, 0s, d, 0, 0(id)) since 8 id 2 FreeVars( x.te): R(id, s, d, , (id)) and R(x, 0s, d, 0, t0) where R(x, 0s, d,0, t0) follows from the assumption that R(te0, s, d, , t0). We now have that 0s,

d, 0 agree on FreeVars(te), that 0 suits 0s (clear), and that 0 ` te : t. Hence R(te, 0s, d, 0, t) by the induction hypothesis.

We are now close to the desired conclusion: last step is Lemma 8.1.

Lemma 8.1 Assume, with the above de nitions and assumptions, that R(te, 0s,d, 0, t) holds. Then R(( x.te) te0, s , d , , t) also holds.

Proof The type t must either have form t1 ! ... ! tn ! S or t1 ! ... ! tn ! D. We assume that t = t1 ! ... ! tn ! S. (The opposite assumption leads to a very similar development.) Now R(te, 0s, d, 0, t) may be written:

8 te1, . . . , ten: (8 i 2 [1..n]: ` tei : ti and R(tei, 0s, d, 0, ti )) implies

E[[ (te te1 ... ten)]] 0

=T [[te te1 ... ten]] 0s

where the equation may be rewritten to

(E[[ (te)]] 0) (E[[ (te1)]] 0) . . . (E[[ (ten)]] 0)

=(T [[te]] 0s) (T [[te1 ]] 0s) . . . (T [[ten]] 0s)

Since x is not free in tei we may again rewrite to get (E[[ (te)]] 0) (E[[ (te1)]] ) . . . (E[[ (ten)]] )

=(T [[te]] 0s) (T [[te1 ]] s) . . . (T [[ten]] s)

Now use the de nitions of 0s and 0 and the application rules for T and E to get

(E[[ (( x.te) te0)]] ) (E[[ (te1)]] ) . . . (E[[ (ten)]] ) = (T [[( x.te) te0]] s ) (T [[te1]] s) . . . (T [[ten ]] s)

More uses of the application rules yield

E[[ (( x.te) te0 te1 ... ten)]] s

=T [[( x.te) te0 te1 ... ten ]]

Now step back and see that the property which we want to establish, R(( x.te) te0, s, d, , t), may be written:

188 Partial Evaluation for the Lambda Calculus

Case: x.te

Proof Let s, d, , be given, and assume they satisfy the conditions in De - nition 8.9. Then it holds that ` x.te : D, and by the inference rules it holds also that [x 7!D] ` te : D.

We shall assume that we have at hand an in nite list of variable names which have not previously been used, and when we write xnew we refer to an arbitrary

Since [x 7!D] clearly suits s[x 7!xnew] and [x 7!D] ` te : D we may conclude from Lemma 8.2 and the induction hypothesis that 8 w 2 Val: R(te,s[x 7!xnew], d[xnew 7!w], [x 7!w], D). To nish the proof for this case we must show that

E[[T [[ x.te]] s]] d = E[[ ( x.te)]]

We rewrite the left-hand side of the equation:

E[[T [[ x.te]] s]] d

=E[[ xnew.(T [[te]] s[x 7!xnew ])]] d

=v.E[[T [[te]] s[x 7!xnew]]] d[xnew 7!v]

and the right-hand side:

E[[ ( x.te)]]

=E[[ x. (te)]]

=v.E[[ (te)]] [x 7!v]

It now remains to show that

v.E[[T [[te]] s[x 7!xnew]]] d[xnew 7!v] = v.E[[ (te)]] [x 7!v]

Correctness of Lambdamix 189

When the two functions are applied to the same (arbitrary) w 2 Val the equality to be shown is

E[[T [[te]] s[x 7!xnew]]] d[xnew 7!w] = E[[ (te)]] [x 7!w]

which follows directly from 8 w 2 Val: R(te, s[x 7!xnew], d[xnew 7!w], [x 7!w],

Case: fix te

Proof The proof is by xpoint induction. The basic idea is to use the structural induction hypothesis H(te) to show the induction step in the xpoint induction.

Assume s, d, , are given satisfying the conditions in De nition 8.9. It thus holds that ` fix te : t and ` te : t ! t. Since FreeVars(fix te) = FreeVars(te) it follows from the induction hypothesis that R(te, s, d, , t ! t).

By the inference rules of Figure 8.4 t is of form t1 ! . . . ! tn ! S, n > 0 or t1 ! . . . ! tn ! D, n > 0. For now we shall assume that t = t1 ! . . . ! tn ! S.

We will take tet? to be an (arbitrary) closed two-level expression of type t such that

T [[tet?]] s = x1.. . . xn.? = E[[ (tet?)]]

Thus R(tet?, s, d, , t1 ! . . . ! tn ! S) holds. By induction on m, repeatedly using R(te, s, d, , t ! t) we see that R(te (te (. . . tet?)), s, d, , t) where there are m applications of of te holds for any m.

Since t is of form t1 ! . . . ! tn ! S, R(fix te, s, d, , t) may also be written: 8 te1, . . . , ten: (8i 2 [1::n]: ` tei : ti and R(tei, s, d, , ti)) implies

T [(fix te) te1 . . . ten]] s

=E[[ ((fix te) te1 . . . ten)]]

This equation is shown by

T [(fix te) te1 . . . ten]] s

=(T [[fix te]] s) (T [[te1]] s) . . . (T [[ten]] s)

=t(T [[te]] s)((T [[te]] s). . . (T [[tet?]] s)) (T [[te1]] s) . . . (T [[ten]] s)

Distribute applications over t, and use T 's rule for application

=t(T [[(te (te (. . . tet?))) te1 . . . ten]] s)

=t(E[[ (te (te (. . . tet?))) te1 . . . ten]] )

=t (E[[ (te)]] ) ((E[[ (te)]] ) . . . (E[[ (tet?)]] ) )

(E[[ (te1)]] ) . . . (E[[ (ten)]] )

=(E[[ (fix te)]] ) (E[[ (te1 )]] ) . . . (E[[ (ten )]] )

=E[[ ((fix te) te1 . . . ten)]]

190 Partial Evaluation for the Lambda Calculus

If t is of form t1 ! . . . ! tn ! D, the proof proceeds in a very similar manner

8.9Exercises

Some of the exercises involve nding a minimal completion. The formal algorithm to do this is targeted for an e cient implementation and is not suited to be executed by hand (for other than very small examples). So if not otherwise stated just use good sense for nding minimal completions.

Exercise 8.1 Find a minimal completion for the lambda expression listed below given the binding-time assumptions = [m0 7!S, n0 7!D]. Specialize the program with respect to m0 = 42.

( m. n.+ m n) m0 n0

2

Exercise 8.2 Find a minimal completion for the lambda expression listed below given the binding-time assumptions = [x0 7!S, xs0 7!S, vs0 7!D]. Specialize the program with respect to x0 = c and xs0 = (a b c d).

(fix lookup. x. xs. vs. if (null? xs)

then 'error

else if (equal? x (car xs)) then (car vs)

else (lookup x (cdr xs) (cdr vs))) x0 xs0 vs0

2

Exercise 8.3 In previous chapters, a self-interpreter sint has been de ned by

[[sint]]L p d = [[p]]L d

De ne sint, basing it on E for instance, such that this equation holds for the

Exercise 8.4

1.Write a self-interpreter sint for the lambda calculus by transforming the function E into a lambda expression fix E. e. .if . . . e' ' with free variables e' and '.

2.Find a minimal completion for sint given binding-time assumptions = [env' 7!S, ' 7!D].

3.Find a minimal completion for sint given binding-time assumptions = [env' 7!S, ' 7!(S ! D)].