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

164 Partial Evaluation for the Lambda Calculus

mal form lambda expressions. These are not di cult to interpret and even to specialize, although they are rather hard for humans to decipher. The ideas were later extended to give a self-applicable partial evaluator for the same language, using essentially the two level type system to be seen in this chapter. The partial evaluator was implemented, self-application gave the usual speedups, and it has since been proven correct by Wand using the technique of `logical relations' [191,279].

8.1The lambda calculus and self-interpretation

The classical lambda calculus (extended with constants, conditionals, and a x- point operator) is used here for simplicity and to allow a more complete treatment than would be possible for a larger and more practical language.

A lambda calculus program is an expression, e, together with an initial environment, , which is a function from identi ers to values. The program takes its input through its free variables. The expression syntax given below di ers from that of Section 3.2 in that we have introduced an explicit xed-point operator.

Examples of relevant base functions include =, *, cons, etc. The xed-point operator fix computes the least xed point of its argument and is used to de ne recursive functions. For example, a program computing xn can be de ned by

(fix p. n'. x'. if (= n' 0) then 1

else (* x' (p (- n' 1) x'))) n x

Note that fix f.e is equivalent to the Scheme constructs (rec f e) and (letrec ((f e)) f). Why introduce an explicit xed-point operator instead of using the Y-combinator written as a lambda expression (Section 3.2.6) to express recursion? This is because an explicit fix allows a simpler binding-time analysis.

As a rst step towards partial evaluation we show a self-interpreter for the lambda calculus in Figure 8.1. Below we explain the notation used in Figure 8.1 and the remainder the chapter.

Figure 8.1: Lambda calculus self-interpreter.

Notation

Const is a ` at' domain of constants large enough to include concrete syntax representations of lambda expressions (as input to and output from mix) and booleans for use in conditionals. As in earlier chapters (and in our implementation) a suitable choice is the set of Lisp S-expressions. Further, we assume there are enough base functions to test equality, and to compose and decompose abstract syntax.

The separated sum of domains Const and Funval is written Val = Const + Funval. Given an element b 2 Const, v = b"Const 2 Val is tagged as originating from Const. In SML or Miranda this would be written v = Const b. We have introduced the " notation for symmetry with v#Const. This strips o the tag yielding an element in Const if v is tagged as originating from Const. If v has any other tag, then v#Const produces an error.

We assume that all operations are strict in the error value but omit details. The domain Funval = Val ! Val contains partial functions from Val to Val. Function V computes the value (in Const) of a constant expression (in Exp). Function O links names to base functions. The notation [var 7!value] is, as in Section 2.1, a shorthand for x.if (x=var) then value else ( x) and is used to update environments. Expression v1 ! v2, v3 has the value v2 if v1 equals true and value v3 if v1 equals false, else the error value.

Since we use lambda calculus both as an object level programming language and as a meta-language, we distinguish notationally between the two for clarity. Object level lambda expressions are written in typewriter style: e e, var.e, fix e etc., and the meta-language is in italics: e e, var.e, x e etc.

166 Partial Evaluation for the Lambda Calculus

The self-interpreter

The structure of the self-interpreter is not much di erent from that of the lambda calculus interpreter written in ML and presented in Section 3.3.1. First-order structures have been replaced by functions in two places:

The environment is implemented by a function from variables to values. Looking up the value of a variable var thus amounts to applying the environment . This replaces the parallel lists of names and values seen in the interpreters from earlier chapters.

The value of an abstraction var.e is a function which, when applied to an

argument value, evaluates e in an extended environment binding var to the value. The value of an application e1 e2 is found by applying the value of e1, which must be a function, to the value of e2. This mechanism replaces the use of explicit closures.

It should be clear that, despite the extensive use of syntactic sugar, Figure 8.1 does de ne a self-interpreter, as the function E can easily be transformed into a lambda expression: fix E. e. .if . . . .

8.2Partial evaluation using a two-level lambda calculus

As in the previous chapters we divide the task of partial evaluation into two phases:rst we apply binding-time analysis, which yields a suitably annotated program, then reduce the static parts, blindly obeying the annotations. An annotated program is a two-level lambda expression. The two-level lambda calculus has two di erent versions of each of the following constructions: application, abstraction, conditionals, xed points, and base function applications. One version is dynamic, the other is static. The static operators are those of the standard lambda calculus: if, fix, , etc. and the dynamic operators are underlined: if, fix, , @. (@ denotes a dynamic application.) The abstract syntax of two-level expressions is given in Figure 8.2.

Intuitively, all static operators , @, . . . are treated by the partial evaluator as they were treated by the self-interpreter. The result of evaluating a dynamic operator ( , @, . . . ) is to produce a piece of code for execution at run-time | a constant which is the concrete syntax representation of a residual one-level lambda expression, perhaps with free variables.

The lift operator also builds code | a constant expression with the same value as lift's argument. The operator lift is applied to static subexpressions of a dynamic expression.

A two-level program is a two-level expression te together with an initial environment s which maps the free variables of te to constants, functions, or code pieces. We shall assume that free dynamic variables are mapped to distinct, new variable

Partial evaluation using a two-level lambda calculus 167

Figure 8.2: Two-level lambda calculus syntax.

names. The T -rules (Figure 8.3) then ensure that these new variables become the free variables of the residual program.

Variables bound by , will also (eventually) generate fresh variable names in the residual program, whereas variables bound by can be bound at specialization time to all kinds of values: constants, functions, or code pieces.

The T -rule for a dynamic application is

T [[te1 @ te2]] = build-@(T [[te1]] #Code, T [[te2]] #Code)"Code

The recursive calls T [[te1]] and T [[te2 ]] produce the code for residual operator and operand expressions, and the function build-@ `glues' them together to form an application to appear in the residual program (concretely, an expression of the form (te1' te2')). All the build-functions are strict.

The projections (#Code) check that both operator and operand reduce to code pieces, to avoid applying specialization time operations (e.g. boolean tests) to residual program pieces. Finally, the newly composed expression is tagged ("Code) as being a piece of code.

The T -rule for variables is

T [[var]] = (var)

The environment is expected to hold the values of all variables regardless of whether they are prede ned constants, functions, or code pieces. The environment is updated in the usual way in the rule for static , and in the rule for , the formal parameter is bound to an as yet unused variable name, which we assume available whenever needed:

T [[ var.te]] = let nvar = newname(var)

in build- (nvar, T [[te]] [var 7!nvar]#Code)"Code

168 Partial Evaluation for the Lambda Calculus

Two-level value domains

Figure 8.3: Two-level lambda calculus interpreter.

Each occurrence of var in te will then be looked up in [var 7!nvar], causing var to be replaced by the fresh variable nvar. Since var.te might be duplicated, and thus become the `father' of many -abstractions in the residual program, this renaming is necessary to avoid name confusion in residual programs. Any free dynamic variables must be bound to their new names in the initial static environments. The generation of new variable names relies on a side e ect on a global state (a name counter). In principle this could be avoided by adding an extra parameter to T , but for the sake of notational simplicity we have used a less formal solution.

The valuation functions for two-level lambda calculus programs are given in Figure 8.3. The rules contain explicit tagging and untagging with " and #; Section 8.3 will discuss su cient criteria for avoiding the need to perform them.

Congruence and consistency of annotations 169

Example 8.1 Consider again the power program:

(fix p. n'. x'. if (= n' 0) then 1

else (* x' (p (- n' 1) x'))) n x

and suppose that n is known and x is not. A suitably annotated power program, power-ann, would be:

(fix p. n'. x'. if (= n' 0) then (lift 1)

else (* x' (p (- n' 1) x'))) n x

Partial evaluation of power (that is, two-level evaluation of power-ann) in environment s = [n 7!2"Const, x 7!xnew"Code] yields:

T [[power-ann]] s

= T [[(fix p. n'. x'.if ...) n x]] s

=* xnew (* xnew 1)

In the power example it is quite clear that for all d2, = [n 7!2, x 7!d2], s = [n 7!2, x 7!xnew], and d = [xnew 7!d2] (omitting injections for brevity) it holds that

E[[power]] = E[[T [[power-ann]] s]] d

This is the mix equation (see Section 4.2.2) for the lambda calculus. Section 8.8

8.3Congruence and consistency of annotations

The semantic rules of Figure 8.3 check explicitly that the values of subexpressions are in the appropriate summands of the value domain, in the same way that a type-checking interpreter for a dynamically typed language would. Type-checking on the y is clearly necessary to prevent partial evaluation from committing type errors itself on a poorly annotated program.

Doing type checks on the y is not very satisfactory for practical reasons. Mix is supposed to be a general and automatic program generation tool, and one wishes for obvious reasons for it to be impossible for an automatically generated compiler to go down with an error message.

Note that it is in principle possible | but unacceptably ine cient in practice | to avoid partial evaluation-time errors by annotating as dynamic all operators