Lecture 4: A Syntactic Interpreter for LC |
|
|
|
|
Recall the syntax of our LC language modeling a core functional subset of Scheme. To make LC slighty more realistic, 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)
A proper LC program is an LC expression M that is closed, i,e., contains no free variables. An LC program is any LC expression. Think of LC as being a sub-language of Scheme. For the moment, we will confine our attention to proper programs.
The set R of abstract representations is defined bv the equation:
R = (make-var Sym) | (make-const Num) | (make-proc Sym R) | (make-app R R) | (make-add R R)
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))
and the primitive type Sym consisting of all sequences of letters and digits beginning with a letter and excluding lambda and the primitive type Num consisting of the set of all integers ..., -2, -1, 0, 1, 2, ...
Recall that in Comp 211, 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: Given an application of the binary operator + to two arguments that are values, replace the application by the sum of the two arguments. |
| Rule 2: Given an application of a lambda-expression to an argument, substitute the argument for the parameter in the body. |
If M has the form (lambda (x) N), to what does it evaluate?
Does the argument to a lambda-expression in Rule 2 have to be a value? As stated above Rule 2 does not impose this requirement. But in LC, we will impose this requirement. Scheme does the same as do nearly all pproduction languages. A few functional languages used primarily for specification (e.g., Haskell) do not.
What happens when we require the argument to be a value? More computations diverge (never terminate). Consider
((lambda (y) 5) ((lambda (x) (x x)) (lambda (x) (x x))))
In nearly all production languages (e.g., Java, Scheme) this computation diverges. The argument
((lambda (x) (x x)) (lambda (x) (x x)))
does not reduce to a value. This lambda term has such an important role int the lambda-caculus that is has a greek letter as its name, capital Omega. In Haskell, the computation
((lambda (y) 5) ((lambda (x) (x x)) (lambda (x) (x x))))
converges because Omega is never evaluated. The application reduces to 5.
Hence, we "patch" Rule 2 to read:
| Rule 2: Given an application of a lambda-expression to a value, 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,
| Rule 2: Given an application of a lambda-expression to a value, substitute the value of the argument for all free occurrences of the parameter in the body. |
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.
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))
Is this reduction correct? No! What happened? The free occurrence of x in the application bound by the inner (lambda (x) ...). This anomaly called "capture of a free variable" is clearly not what we intended. Our evaluation rules will produce legitimate answers (integer values) for some improper programs that should produce run-time errors. Even worse, if we try to use the reduction of applications as a transformation rule to simplify programs, we can change the meaning of programs.
| Exercise 1: Devise a closed LC program P where reducing an application (using unsafe substitution) inside a lambda produces a program P' that is not semantically equivalent to P (P' produces different answers for some inputs than P does). |
There are two ways out of this conundrum:
In a language like Scheme with global definitions
(define x ...)
functions frequently refer to free variables with global definitions. As a result, the only viable option in defining a substitution semantics for such a language is to force substitutions to be hygienic. In the absence of global definitions, however, free variables serve no useful purpose in functional languages like LC. For this reason, we simply ban free variables from LC programs, permitting us to avoid the issue of safe substitution.
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.
| Puzzle: What are the equivalent evaluation rules for LC programs that have been converted to static distance (deBruijn) notation? What is the analog of capture when the application rule is used to simplify programs? |
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) is true
(Apply
(Eval (app-rator M))
(Eval (app-rand M)))))))
(define Apply
(lambda (a-proc a-value)
(Eval (substitute a-value ; 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
From the perspective of implementation efficiency, our evaluator (Eval) has some problems. Consider its behavior on an input like
((lambda (x) <big-proc>) 5)
Assume that <big-proc> consists of many uses of x. The evaluator must step through this entire procedure body, replacing every occurrence of x by the value 5. The new tree produced by this process has the same size as the original tree (since we traversed the entire tree, and replaced an identifier with a value). What does eval do next? It walks once again over the entirety of the new tree that it just produced after substitution, for the purpose of evaluating it. This two phase process is clearly very wasteful, particularly since it involves copying the original abstract syntax tree for <big-proc>.
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.
| Exercise 2: Devise a simple example, where the environment at the point of application contains a WRONG substutition for the body of the procedure being applied. Hint: use the same variable name as a free variable in a function being passed as an argument and in the function it is being passsed to. |
The process of building a procedure representation that includes the correct environment is called "building a closure" or "closing over the environment of the procedure". For this reason, procedure [function] values in programming languages are often called closures.
Unfortunately, many programming languages with procedures as arguments have historically failed to recognize the need to construct closures. Keeping track of the environment for a procedure requires a lot of extra machinery if the interpreter is written in low level language like C. In addition, many language implementors unfamiliar with functions as arguments have failed to realize that failing to keep track of the procedures "lexical" environment is inconsistent with the standard substitution based evaluation rules.
If procedures are not closed, the interpreter will implement an ugly semantic model called "dynamic scoping". The history of programming languages is replete with languages that fail to construct closures and hence implement dynamic scoping. They include SNOBOL, APL, some early dialects of LISP, and TCL. To finish our environment-based interpreter we need to choose representations for environments and closures and then fill in the gaps in the template above. For the moment, we will make the simplest, most pedestrian representational choices. In the next lecture, we will consider alternatives. An environment is a table mapping variables to substitutions. A simple choice for a representation is a list of pairs. Similarly a simple representation for a closure is a structure containing the procedure text and the environment. Given these choices our interpreter becomes:
(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
(let ((body (closure-body fn)))
(Eval body
(extend (closure-env fn) (proc-param body) arg)))))
(define lookup
(lambda (var env)
(if (null? env)
(error ...)
(if (eq? var (pair-var (first env)))
(pair-val (first env))
(lookup var (rest env))))))
(define extend
(lambda (env var val) (cons (make-pair var val) env)))
(define emptyEnv '())
At the top level, a complete LC program P is evaluated by calling (Eval P emptyEnv). Since there are no free variables in a complete program, emptyEnv contains all of the environment information (bindings of free variables) required to evaluate it.
We have
Let the form
(let (v M) N)}
abbreviate the LC expression
((lambda (v) N) M)
This abbreviation makes LC code much easier to read.
1. Consider the program
(let (y 2)
(let (f (lambda (x) (* x y)))
(let (g (lambda (y) (f (+ y y))))
(g (+ y y)))))
which abbreviates the LC program
((lambda (y)
((lambda (f)
((lambda (g) (g (+ y y)))))
(lambda (y) (f (+ y y))))
(lambda (x) (* x y)))
2)
The program evaluates to 16.
If we naively substitute (lambda (x) (* x y)) for f in the expression
(let (g (lambda (y) (f (+ y y)))) (g (+ y y)))
we get
(let (g (lambda (y) ((lambda (x) (* x y)) (+ y y)))) (g (+ y y)))
With this transformation, the program reduces to 32. After the transformation, the free occurrence of y in the value of f refers to the formal parameter y in the definition of g rather than the y introduced in the outermost let.
2. If an LC evaluator does not build closures to represent procedure values, it will compute the wrong answer for the following program:
(let (y 17)
(let (f (lambda (x) (+ y y)))
(let (y 2)
(f 0))))
This program abbreviates the LC program
((lambda (y)
((lambda (f)
((lambda (y)
(f 0))
2))
(lambda (x) (+ y y)))
17))
Given this program, a closure-based LC interpreter will
(let f ...)in the resulting environment
(y = 17)
(let (y 2) ...)in the extended environment
(f = [(lambda (x) (+ y y)), (y = 17)]; y = 17)
(f 0)in the extended environment
((y = 2; f = [(lambda (x) (+ y y)), (y = 17)]; y = 17)
[(lambda (x) (+ y y)), (y = 17)]and evaluate this closure applied to the value 0
(x = 0; y = 17)
An incorrect interpreter that fails to build closures will perform the following computation for the same program:
(let f ...)in the resulting environment
(y = 17)
(let (y 2) ...)in the extended environment
(f = (lambda (x) (+ y y); y = 17)
(f 0)in the extended environment
(y = 2; f = (lambda (x) (+ y y)); y = 17)
(lambda (x) (+ y y))and evaluate this expression applied to the value 0 in the environment
(y = 2; f = (lambda (x) (+ y y)); y = 17)
(x = 0; y = 2; f = (lambda (x) (+ y y)); y = 17)
In class we considered several lambda terms and discussed what they should evaluate to. Most interesting discussions revolved around whether we should evaluate under lambda or not (what should be done for application seemed untuitively clear). Ultimately, we agreed that to model traditional languages we should not evaluate under lambda. It was also noted that evaluating under lambda could be used to model optimizations that a compiler could perform. However, given that we are after the simplest possible semantics for this language, we decided not to worry about specifying optimizations for now.
Our attention then moved to how to precisely specify what should be done to evaluate an application. It was suggested that we use a table (or environment) to keep track of what values are bound to what variables, but we decided to focus on a simpler way of specifying semantics, namely, substitution. We are still discussion how to define substitution on lambda expressions...
In the mean time, we will consider the highly illuminating question of how to perform substition and evaluation of terms represented using de Bruijn indeces.
type debruijn =
Cn of int
| Vr of int
| Lm of debruijn
| Ap of debruijn * debruijn
let rec plus e m =
match e with
Cn i -> Cn i
| Vr n -> Vr (if n < m then n else n+1)
| Ap (e1,e2) -> Ap (plus e1 m, plus e2 m)
| Lm (e) -> Lm (plus e (m+1))
let rec subst i v e =
match e with
Cn i -> Cn i
| Vr n -> (if n==i then v
else if n>i then Vr (n-1)
else Vr n)
| Ap (e1,e2) -> Ap (subst i v e1, subst i v e2)
| Lm (e) -> Lm (subst (i+1) (plus v 0) e)
Evaluation will be exactly the same as with the name-based representation:
exception Error of string;;
let rec ev0 e =
match e with
Cn i -> Cn i
| Vr x ->
raise (Error "Unbound variable")
| Lm e' -> e
| Ap (e1,e2) ->
(match (ev0 e1) with
Lm e ->
let v = ev0 e2 in
ev0 (subst 0 v e)
| _ -> raise (Error "Applying non-function"))
In class, we discuss how to describe these rules at a higher-level using mathematical notation. A question was raised about the rule for application, and it was noted that there are two reasonable ways of defining application, Call-by-value (CBV) and Call-by-name (CBN). The rule used above is Call-by-value. To get a finer-grained model of how a program is evaluation, we started looking at small-step semantics (in contrast to the above big-step semnatics). We derived together a definition for such a semantics based on how several example terms should be evaluated. It was noted that the definition of the small-step semantics is particularly unusually, in that it is not defined on constants, variables, or lambdas, because they involve no additional work. It was also noted that this unusual "partiality" of the small-step semantics also contributes to the fact that it can be defined quite consicely. In what follows is an example implementation of such a small-step semantics in OCaml:
let rec step e =
match e with
Ap (Lm e, Cn i) ->
subst 0 (Cn i) e
| Ap (Lm e1, Lm e2) ->
subst 0 (Lm e2) e1
| Ap (Lm e1, e2) ->
Ap (Lm e1, step e2)
| Ap (e1, e2) ->
Ap (step e1, e2)
| _ -> raise (Error "Nothing to evaluate here")
let rec ev1 e =
match e with
Cn i -> Cn i
| Lm e -> Lm e
| _ -> ev1 (step e)
Notice, again, that the mathematical definition was even more consice than the code above :) Now we will consider how substitution is implemented. Everytime we perform and application with the big-step semantics, we perform a substitution. But substitution (as defined above) traverses the whole body of the function we are applying. If we had a program 3,000,000 line program, the application would take a very long time, even if the first line raised an exception that terminated the program. To implement substitution more efficiently, we discussed the use of environments that would remember the substitutions that we want to perform, and then perform them only when they are needed. If we are working with de Bruijn indices, here is how an implementation that uses a list as an environment would look like:
type debValue =
V_Cn of int
| V_Lm of (debValue list) * debruijn
let rec ev3 env e =
match e with
Cn i -> V_Cn i
| Vr 0 ->
(match env with
v::vs -> v
| _ -> raise (Error "Unbound variable"))
| Vr n ->
(match env with
v::vs -> ev3 vs (Vr (n-1))
| _ -> raise (Error "Unbound variable"))
| Lm e' -> V_Lm (env, e')
| Ap (e1,e2) ->
(match (ev3 env e1) with
(V_Lm (env',e)) ->
let v = ev3 env e2 in
ev3 (v::env') e
| _ -> raise (Error "Applying non-function"))
We will call this the big-step semantics with environments, or just the environment semantics for short. First, notice the similarity between this implementation and the big-step semnatics: We are still performing a match on the term being evaluated, and the main kinds of errors that can occur are still being raised in the different cases. Also, with the exception of the variable case, all cases follow the same structure as with the big-step semantics. Even in the variable case, we still (under more constrained conditions) raise the same error that we raise in the big-step semantics. Now for the differences: First, we have also introduce a new type for values, and the function now always returns values of this type. In contrast, the big-step semantics just returned expressions. Second, the variable case is split into two cases. The are very similar, and essentially serve to look up the variable in the environment by its index. Third, the lambda case constructs a closure, rather than just returning a lambda. As we said in class, the closure is very much like a let-expression of a somewhat restricted form. Finally, application no longer performs a substition, but rather, extends the environment for the body of the closure with the new binding, and then evaluates that body in the extended environment.