University
of Bath

MATH0069: Programming Language Implementation Techniques

Department of Mathematical Sciences

A Normal Form


An obvious awkwardness about the CEK rules given earlier is the way in which we have to define multiple rules for any term that needs to know the values of sub-terms in order to proceed, as is the case with function application, conditions and let binding. The rules can be simplified by translating terms into A normal form (ANF) and then using a ANF version of the CEK machine. In summary, the purpose of rewriting the program into ANF is that any sub-term is guaranteed to be one of an integer constant, a string constant, a variable or a rec term, each of which is trivially evaluable - a task we delegate to the gamma function. The consequence is that every source term can then be evaluated in a single step, since there are no complex sub-terms on which we have to call the interpreter recursively. Simplification of the rules is not the only issue in question however: the first rule set also led to the creation of very many activiation records in order to handle the "recursive call" of the interpreter so that we could recognize when we had finished evaluating a sub-term. Yet, in effect they are only administrative, in the sense that they are carrying out the simplification of the sub-terms at run-time, when that reorganization can in fact be done statically (at compile-time, if you wish). Thus it is that the ANF rule set only creates activation records when it is essential, in order to implement a function call (in non-tail position). Thus a new rule set for ANF/TLL is:

<integer-constant, E, AR(x,C',E',K')> --> <C', E'[x:=integer-constant], K'> <string-constant, E, AR(x,C',E',K')> --> <C', E'[x:=string-constant], K'> <variable, E, AR(x,C',E',K')> --> <C', E'[x:=gamma(variable,E)], K'> <(rec variable1 variable2 term), E, AR(x,C',E',K')> --> <C', E'[x:=y], K', x> whererec y = CL(variable2, E[variable1:=y], term) <(term1 term2), E, K> --> <term, E'[variable:=operand], K> where gamma(term1,E) = CL(variable, E', term) and gamma(term2,E) = operand <(if term1 term2 term3), E, K> --> <term2, E, K> if gamma(term1,E) is not false --> <term3, E, K> otherwise <(let variable term1 term2), E, K> --> <term2, E[variable:=initial-value], K, nil> where gamma(term1,E) = initial-value <(let variable (if term1.1 term1.2 term1.3) term2), E, K> --> <term1.2, E, AR(variable,term2,E,K)> if gamma(term1.1,E) is not false --> <term1.3, E, AR(variable,term2,E,K)> otherwise <(let variable (term1.1 term1.2) term2), E, K> --> <term, E'[variable:=operand], AR(variable,term2,E,K)> where gamma(term1.1,E) = CL(variable, E', term) and gamma(term1.2,E) = operand

Leaving us with the question of how to translate terms into ANF. We can specify what we want to achieve by means of a recursive procedure:

ANF integer-constant = integer-constant ANF string-constant = string-constant ANF variable = variable ANF (rec variable1 variable2 term) = (rec variable1 variable2 ANF(term)) ANF (term1 term2) = case (class-of term1,class-of term2) => (variable,value) (term1 term2) => (variable,variable) (term1 term2) => (variable,term) ANF (let id2 term2 (term1 id2)) where id2 = fresh-identifier() => (term,variable) ANF (let id1 term1 (id1 term2)) where id1 = fresh-identifier() => (term,term) ANF (let id1 term1 (let id2 term2 (id1 id2))) where id1 = fresh-identifier() and id2 = fresh-identifier() => (_,_) error! ...

Note: this is not a particularly efficient way of doing the job, since the way in which recursion is used leads to each constructed term being analysed over again. On the other hand it is relatively clear what is happening. A much more efficient (linear cost) implementation uses a form of continuation passing to remember "what to do next". This comes from a paper about ANF (Flanagan et al, 1993) and is written in Scheme:

(define (normalize-term M) (normalize M (lambda (x) x))) (define (normalize M k) (match M [`(lambda ,params ,body) (k `(lambda ,params ,(normalize-term body)))] [`(let (,x ,M1) ,M2) (normalize M1 (lambda (N1) `(let ,x ,N1 ,(normalize M2 k))))] [`(if ,M1 ,M2 ,M3) (normalize-name M1 (lambda (t) (k `(if ,t ,(normalize-term M2) ,(normalize-term M3)))))] [`(,fn . ,M*) (if (primop? fn) (normalize-name* M* (lambda (t*) (k `(,fn . ,t*)))) (normalize-name fn (lambda (t) (normalize-name* M* (lambda (t*) (k `(,t . ,t*)))))))] [V (k V)])) (define (normalize-name M k) (normalize M (lambda (N) (if (value? N) (k N) (let ((t (newvar))) `(let ,t ,N ,(k t))))))) (define (normalize-name* M* k) (if (null? M*) (k '()) (normalize-name (car M*) (lambda (t) (normalize-name* (cdr M*) (lambda (t*) (k `(,t . ,t*))))))))

And a simple example of what it can do...given the input:

(+ (+ 2 2) (let (x 1) (f x))) results in: (let (t1 (+ 2 2)) (let (x 1) (let (t2 (f x)) (+ t1 t2))))

A familiar and slightly bigger example illustrates the earlier reference to tail-calling. First the traditional recursive factorial:

(let g (fix f (lambda n (if (zero? n) 1 (* n (f (- n 1)))))) (g 10))

which translates to:

(let g (fix f (lambda n (let k122 (zero? n) (test k122 1 (let k123 (- n 1) (let k124 (f k123) (* n k124))))))) (g 10)))

in which we observe that the recursive call is in the initializer of a let expression, the rule for which we see constructs an activiation record to enable the return to evaluate the body. It should be obvious that this definition will construct a number of activation records equal to the magnitude of the argument to g/f. Now look at the traditional accumulating parameter recursive factorial:

(let g (fix f (lambda (n a) (if (zero? n) a (f (- n 1) (* n a))))) (g 10 1))

which translates to:

(let g (fix f (lambda (n a) (let k165 (zero? n) (if k165 1 (let k166 (- n 1) (let k167 (* n a) (f k166 k167))))))) (g 10))

Here we observe that the recursive call is in the body of the let and the rule for evaluating a call does not construct an activation record, but instead passes on the current activation record. The net effect of this is that this definition does not construct any activiation records at all, despite being a recursive function. The reason is that the ANF translation formalizes the notion that the last function call in a function can be replaced by a goto. In consequence, recursive definitions having this property run in bounded space, just as if they were loops.


Julian Padget, jap@maths.bath.ac.uk