Lecture 4, Comp 311

A Syntactic Interpreter for LC

Recall the syntax of LC. We will add one primitive binary operator, +, to the language, giving the following syntax for terms in the language:

M :== x | n | (lambda (x) M) | (M M) | (+ M M)

We similarly extend our abstract syntax for LC to include addition as a primitive application. The set AR of abstract representations is defined bv the equation:

AR = (make-var Var)
   | (make-const Num)
   | (make-proc Var AR) 
   | (make-app AR AR)
   | (make-add AR AR)

given the data definitions:

(define-struct var (name))
(define-struct const (number))
(define-struct proc (param body))
(define-struct app (rator rand))
(define-struct add (left right))

Recall that in Comp 210, we formulated the semantics of Scheme as an extension to the familiar algebraic calculation process. Consider (+ (+ 3 4) (+ 7 5)). To evaluate this, we first determine the value of (+ 3 4) and of (+ 7 5). Why? Because these are not values and + can only add two values (numbers).

What is a value? Intuitively, it is any expression that can be returned as the "answer" produced by a computation. We must understand this concept in detail before we can explain the process of evaluation. Let's consider the various possible forms for expression and determine which are values.

First, lambda expressions are values. Are numbers values? Yes, they are. Are identifiers values? No, they stand for values. Are applications values? No, they are not; they trigger an evaluation. Are primitive applications (+ M M) values? No, they also trigger an evaluation. In summary, (M M) and (+ M M) are computations, (lambda ...) and numbers are values, and identifiers are neither (they are not computations because they do not trigger evaluation in our interpreter for LC and they are not values because they are not legitimate "answers" for computations). Let us return to our example, (+ (+ 3 4) (+ 7 5)). By following the regular rules of evaluation for Scheme, we determine that the expression above yields the value 19. Let us review the rules of evaluation for the LC subset of Scheme.

Rules of Evaluation

Rule 1: For +-expressions, evaluate the operands, then add them.

Rule 2: For applications of the binary operator + to two arguments that are values, replace the application by the sum of the two arguments.

Rule 3: For applications of lambda-expressions to values, substitute the argument for the parameter in the body. Does this argument have to be a value? In LC, we will impose this requirement. Scheme does the same. Some other functional languages (e.g., Haskell) do not.

((lambda (y) 5) ((lambda (x) (x x)) (lambda (x) (x x))))

Hence, we ``patch'' our application rule to read: For lambda applications, substitute the value of the argument for the parameter in the body. This revision, however, still isn't quite satisfactory. Consider the procedure (lambda (x) (lambda (x) x)). When this procedure is applied, we do not want the inner x to be substituted; that should happen only when the inner procedure is applied. Hence, we amend our rule to read,

For lambda applications, substitute the value of the argument for all free instances of the parameter in the body.

Combining the Rules of Evaluation

Given an LC expression, we evaluate it by repeatedly applying the preceding rules until we get an answer. What happens when we encounter an expression to which more than one rule applies? In Rice Scheme and LC, the leftmost rule always takes priority.

Potential Complications

As long as we only evaluate proper programs (closed expressions), the preceding evaluation rules are satisfactory. But they will fail if we try to evaluate arbitrary programs (expressions that may contain free variables) or if we try to use the evaluation rule for lambda applications as a transformation rule to simplify programs. Consider the following reduction of an expression with the free variable x:

  ((lambda (y) (lambda (x) y)) (lambda (z) x))
= (lambda (x) (lambda (z) x))

There are two ways out of this conundrum:

• We can institute a rule that programs cannot contain free variables.
• We can once again redefine our notion of substitution: our final amendment will require that we rename all binding occurrences (and their corresponding bound occurrences) before we perform the substitution. The new name chosen should be one that cannot yield such inadvertent capture (such as, say, a name not found anywhere else in the program). This technique is called ``clean substitution'', ``hygienic substitution'', or ``safe substitution''.

(define x ...)

Note: many languages avoid the capture problem by prohibiting functions (procedures) as arguments. In such a language, lambda expressions are not values and are never substituted for variables.

An Evaluator

Now we can translate our rules into a program. Here is a sketch of the evaluator:

(define Eval
  (lambda (M)
    (cond
      ((var? M) (impossible ...))
      ((const? M) M)
      ((proc? M) M)
      ((add? M) (add-num
		  (Eval (add-left M))
		  (Eval (add-right M))))
      (else ; (app? M) ==> #t
	(Apply
	  (Eval (app-rator M))
	  (Eval (app-rand M)))))))

(define Apply
  (lambda (a-proc a-value)
    (Eval (substitute a-val ; for
	    (proc-param a-proc) ; in
	    (proc-body a-proc)))))

(define substitute
  (lambda (v x M)
    (cond ; M
      ... cases go here ...
      )))

The key property of this evaluator is that it only manipulates (abstract) syntax. It specifies the meaning of LC by mechanically transforming the syntactic representation of a program. This approach only assigns meaning to complete LC programs, not to individual components of an LC program (such as particular lambda expressions embedded in the program). Such an evaluator is called is a purely syntactic method for describing meaning of programs

Toward Assigning Meaning to Embedded Expressions

From the perspective of implementation efficiency, our evaluator (Eval) has some problems. Consider its behavior on an input like

((lambda (x) <big-proc>) 5)

To be more frugal, eval could instead do the following: it could merge the two traversals into one, which is carried out when evaluating the (as yet unsubstituted) tree. During this traversal, it could carry along a table of the necessary substitutions, which it could then perform just before evaluating an identifier. This table of delayed substitutions is called an environment.

Hence, our evaluator now takes two arguments: the expression and an environment. The environment env contains a list of the identifiers that are free in the body, and the values associated with them.

(define Eval
  (lambda (M env)
    (cond
      ((var? M) lookup M's name in env)
      ((const? M) ...)
      ((proc? M) ... what do we do here? ...)
      ((add? M) ...)
      (else ... ))))

The interesting clause in this definition is the code for evaluating procedures. To preserve the semantics of our evaluation rules, we must keep track of the environment active at the time the procedure was evaluated. Why? Because this environment contains the correct substitutions. When the procedure is finally applied (possibly more than once), the current environment will generally contain the WRONG substitutions.

(define-struct pair (var val))
(define-struct closure (body env))


(define Eval
  (lambda (M env)
    (cond
      ((var? M) (lookup M env))
      ((const? M) M)
      ((proc? M) (make-closure M env))
      ((add? M) (add (Eval (add-left M) env) (Eval (add-right M) env)))
      (else (Apply (Eval (app-rator M) env) (Eval (app-rand M) env))))))
         
(define Apply
  (lambda (fn arg) ; fn must be a closure
    (Eval (proc-body (closure-body fn)) 
          (extend (closure-env fn) (proc-param (closure-body)) arg))))

(define lookup
  (lambda (var env)
    (if (null? env) 
        (error ...)
        (if (eq? var (pair-var (car env)))
            val
            (lookup var (cdr env)))))) 

Summary

We have

• presented the rudiments of a syntactic evaluation theory, and
• shown how optimizing the evaluation process leads to the representation of procedures as data structures (closures) instead of program text.

Solutions to Exercises

(let (v M) N)}

((lambda (v) N) M)