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 and , equations 2 and 3 have a unique solution, and the final two have no solutions.
The second and third equation can be rewritten in terms of and as so.
The solution is a fixed point of the
. 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 . The proof is horribly difficult, and best left for denotational semanticists.
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
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
This is correct. However, the below conclusion is false.
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.