SICP 7a
Metacircular Evaluation I

Table of Contents

1 Don a fez

Up until now, we have been thinking of programs as describing machines. Today we will describe a universal machine, eval, which can take a description of another machine as its input.

We're getting very close to the real spirit in the computer at this point. I have to show a certain amount of reverence and respect, so I'm going to wear a suit jacket for the only time that you'll ever see me wear a suit jacket here. And I think I'm also going to put on an appropriate hat for the occasion. Now, this is a lecture I have to warn you - let's see, normally, people under 40 and who don't have several children are advised to be careful. If they're really worried, they should leave. Because there's a certain amount of mysticism that will appear here that may be disturbing and cause trouble in your minds.

2 Evaluator for LISP

An evaluator takes an expression and environment as its input. An environment is a dictionary mapping symbol names to their values.

There are several special cases an evaluator needs to take care of.

Special case Example(s)
Numbers 3
Symbols x
Quotes 'foo, (quote foo)
Lambdas (lambda (x) (+ x y))
Conditionals (cond (p1 e1) (p2 e2) ...)

eval

(define eval
  (lambda (exp env)
    (cond ((number? exp) exp)
          ((symbol? exp) (lookup exp env))
          ((eq? (car exp) 'quote) (cadr exp))
          ((eq? (car exp) 'lambda)
           (list 'closure (cdr exp) env))
          ((eq? (car exp) 'cond)
           (evcond (cdr exp) env))
          (else (apply (eval (car exp) env)
                       (evlist (cdr exp) env))))))

Now define evcond, apply, evlist and lookup.

(define apply
  (lambda (proc args)
    (cond ((primitive? proc)
           (apply-primop proc args))
          ((eq? (car proc) 'closure)
           (eval (cadadr proc)
                 (bind (caadr proc)
                       args
                       (caddr proc))))
          (else error))))

Putting primitive? and apply-primop to one side for the time being, let's look at bind.

(define evlist
  (lambda (l env)
    (cond ((eq? l '()) '())
          (else
           (cons (eval (cadr l) env)
                 (evlist (cdr l) env))))))

evcond

(define evcond
  (lambda (clauses env)
    (cond ((eq? clauses '()) '())
          ((eq? (caar clauses) 'else)
           (eval (cadar clauses) env))
          ((false? (eval (caar clauses) env))
           (evcond (cdr clauses) env))
          (else
           (eval (cadar clauses) env)))))

bind

(define bind
  (lambda (vars vals env)
    (cons (pair-up vars vals)
          env)))

pair-up

(define pair-up
  (lambda (vars vals)
    (cond
     ((eq? vars '())
      (cond ((eq? vals '()) '())
            (else (error "too many arguments"))))
     ((eq? vals '()) (error "too few arguments"))
     (else
      (cons (cons (car vars)
                  (car vals))
            (pair-up (cdr vars)
                     (cdr vals)))))))

lookup

(define lookup
  (lambda (sym env)
    (cond ((eq? env '()) (error "unbound variable"))
          (else
           ((lambda (vcell)
              (cond ((eq? vcell '())
                     (lookup sym
                             (cdr env)))
                    (else (cdr vcell))))
            (assq sym (car env)))))))

assq

(define assq
  (lambda (sym alist)
    (cond ((eq? alist '()) '())
          ((eq? sym (caar alist))
           (car alist))
          (else
           (assq sym (cdr alist))))))

3 Step by step

To gain a better understanding of how an evaluation functions, let's take it slow.

(eval '(((lambda (x) (lambda (y) (+ x y))) 3) 4) <e0>)

e0 is a global environment containing the procedures + * - / eq? cons cdr car etc.

(apply (eval '((lambda (x) (lambda (y) (+ x y))) 3) <e0>)
       (evlist '(4) <e0>))
(apply (eval '((lambda (x) (lambda (y) (+ x y))) 3) <e0>)
       (cons (eval 4 <e0>)
             (evlist '() <e0>)))
(apply (eval '((lambda (x) (lambda (y) (+ x y))) 3) <e0>)
       (cons 4 '() ))
(apply (eval '((lambda (x) (lambda (y) (+ x y))) 3) <e0>)
       '(4))
(apply (apply (eval '(lambda (x) (lambda (y) (+ x y))) <e0>)
              '(3))
       '(4))
(apply (apply '(closure ((lambda (y) (+ x y))) <e0>)
              '(3))
       '(4))

A new environment e1 is created at this point with bind. x = 3.

(apply (eval '(lambda (y) (+ x y)) <e1>)
       '(4))
(apply '(closure ((y) (+ x y)) <e1>)
       '(4))

A new environment e2 is created at this point with bind. y = 4.

(eval '(+ x y) <e2>)
(apply (eval '+ <e2>)
       (evlist '(x y) <e2>))
(apply + '(3 4))
7

4 Fixed points

How is building an interpreter for a language we are already able to interpret not completely vacuous? Let's revisit the exponential function and describe what happens when a function is defined in terms of itself.

(define expt
  (lambda (x n)
    (cond ((= n 0) 1)
          (else
           (* x (expt x (- n 1)))))))

Now let's take a look from a mathematical perspective.

From the below equations, we can see that the 1st and 2nd equation have an infinite number of solutions in x 𝑥 x and y 𝑦 y , equations 2 and 3 have a unique solution, and the final two have no solutions.

2 x + 2 y = 6 2 𝑥 2 𝑦 6 2x+2y=6 x + y = 3 𝑥 𝑦 3 x+y=3 x - y = 1 𝑥 𝑦 1 x-y=1 x - y = 2 𝑥 𝑦 2 x-y=2

The second and third equation can be rewritten in terms of x 𝑥 x and y 𝑦 y as so.

x = 3 - y 𝑥 3 𝑦 x=3-y y = x - 1 𝑦 𝑥 1 y=x-1

< x , y >= T < x , y > formulae-sequence formulae-sequence absent 𝑥 𝑦 𝑇 𝑥 𝑦 absent <x,y>=T<x,y>

The solution is a fixed point of the T 𝑇 T . Applying this logic to expt, we obtain a procedure, call it F.

F

(lambda (g)
  (lambda (x n)
    (cond ((= n 0) 1)
          (else
           (* x
              (g x (- n 1)))))))

expt is the fixed point of F. There's a problem that there might be more than one fixed point or no fixed points.

E0 = 1
E1 = (lambda (x n)
       (cond ((= n 0) 1)
             (else
              (* x (E0 x (- n 1))))))
E2 = (lambda (x n)
       (cond ((= n 0) 1)
             (else
              (* x (E1 x (- n 1))))))
E3 = (lambda (x n)
       (cond ((= n 0) 1)
             (else
              (* x (E2 x (- n 1))))))
...

We will assert that 𝚎𝚡𝚙𝚝 = lim n E n 𝚎𝚡𝚙𝚝 subscript 𝑛 subscript 𝐸 𝑛 \texttt{expt}=\lim_{n\to\infty}E_{n} . The proof is horribly difficult, and best left for denotational semanticists.

𝚎𝚡𝚙𝚝 = ( F ( F ( F ( F ( F < x > ) ) ) ) ) 𝚎𝚡𝚙𝚝 𝐹 𝐹 𝐹 𝐹 𝐹 expectation 𝑥 \texttt{expt}=(F(F(F(F...(F<x>)...))))

5 Y combinator

How can we express infinity? The simplest inifinite loop is:

((lambda (x) (x x)) (lambda (x) (x x)))

Curry's paradoxical combinator of Y allows a function to apply itself to itself.

Y

(lambda (f)
  ((lambda (x) (f (x x)))
   (lambda (x) (f (x x)))))

(Y F)

((lambda (x) (F (x x)))
 (lambda (x) (F (x x)))))
(F ((lambda (x) (F (x x))) (lambda (x) (F (x x)))))

By applying Y to F, we produce an infinite series of F​s.

(Y F) = (F (Y F)) (Y F) (F (Y F)) \texttt{(Y F)}=\texttt{(F (Y F))}

Y is a magical procedure which, when applied to some function, produces an object which is the fixed point of that function, if it exists.

6 Trouble with infinity

u = 1 + 1 2 + 1 4 + 1 8 + 𝑢 1 1 2 1 4 1 8 u=1+\frac{1}{2}+\frac{1}{4}+\frac{1}{8}+... u - 1 = 1 2 + 1 4 + 1 8 + 𝑢 1 1 2 1 4 1 8 u-1=\frac{1}{2}+\frac{1}{4}+\frac{1}{8}+... 2 ( u - 1 ) = 1 + 1 2 + 1 4 + 1 8 + 2 𝑢 1 1 1 2 1 4 1 8 2(u-1)=1+\frac{1}{2}+\frac{1}{4}+\frac{1}{8}+... 2 ( u - 1 ) = u 2 𝑢 1 𝑢 2(u-1)=u u = 2 𝑢 2 u=2

This is correct. However, the below conclusion is false.

v = 1 + 2 + 4 + 8 𝑣 1 2 4 8 v=1+2+4+8... v - 1 = 2 + 4 + 8 𝑣 1 2 4 8 v-1=2+4+8... ( v - 1 ) / 2 = 1 + 2 + 4 + 8 𝑣 1 2 1 2 4 8 (v-1)/2=1+2+4+8... ( v - 1 ) / 2 = v 𝑣 1 2 𝑣 (v-1)/2=v v = - 1 𝑣 1 v=-1

When we play with limits, arguments which may work in one case do not necessarily generalise to other cases.

For more information, read Joe Stoy's Denotational Semantics: The Scott-Strachey Approach to Programming Language Semantics.