X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=exercises%2Fassignment7.mdwn;h=719057d4e96698331c1a4cf686dc2fc14e3d307d;hp=ddee5f7ae2d48b3cd18750796d012b46edf1ab82;hb=HEAD;hpb=8b5f17b3b2c71d443362d7f629dec6cd82b4fb59 diff --git a/exercises/assignment7.mdwn b/exercises/assignment7.mdwn index ddee5f7a..719057d4 100644 --- a/exercises/assignment7.mdwn +++ b/exercises/assignment7.mdwn @@ -1,8 +1,8 @@ -# Assignment 7 - There is no separate assignment 6. (There was a single big assignment for weeks 5 and 6, and we're going to keep the assignment numbers in synch with the weeks.) +[[!toc]] + ## Evaluation order in Combinatory Logic 1. Give a term that the lazy evaluators (either [[the Haskell @@ -45,7 +45,7 @@ add the last pieces to make the program function. You can find the skeleton code [[here|/code/untyped_evaluator.ml]]. The first place you need to add code is in the `free_in` function. You already -wrote such a function [[in a previous homework|assignment5#occurs_free]], so this +wrote such a function [[in a previous homework|exercises/assignment5-6#occurs_free]], so this part should be easy. The intended behavior is for the function to return results like this: @@ -83,138 +83,20 @@ This part of the exercise is the "VB" part of that code. You'll see that in the `eval` function, a new kind of value `Closure (ident) (term) (env)` is used. What's that about? -The `Closure`s are for handling the binding of terms that have locally free variables in them. Let's -see how this works. For exposition, I'll pretend that the code you're working with has -primitive numbers in it, though it doesn't. (But the fuller code it's simplified from does; see below.) -Now consider: - - term environment - ---- ----------- - (\w.(\y.y) w) 2 [] - (\y.y) w [w->2] - y [y->w, w->2] - -In the first step, we bind `w` to the term `2`, by saving this association in our environment. In the second step, we bind `y` to the term `w`. In the third step, we would like to replace `y` with whatever its current value is according to our scorecard/environment. But a naive handling of this would replace `y` with `w`; and that's not the right result, because `w` should itself be mapped onto `2`. On the other hand, in: - - term environment - ---- ----------- - (\x w. x) w 2 [] - (\w. x) 2 [x->w] - x [w->2, x->w] - -Now our final term _should_ be replaced with `w`, not with `2`. So evidently it's not so simple as just recursively re-looking up variables in the environment. - -A good strategy for handling these cases would be not to bind `y` to the term `w`, but rather to bind it to _what the term `w` then fully evaluates to_. Then in the first case we'd get: - -
```-term                             environment
-----                             -----------
-(\w.(\y.y) w) 2                  []
-(\y.y) w                         [w->2]
-y                                [y->2, w->2]
-```
- -And at the next step, `y` will evaluate directly to `2`, as desired. In the other example, though, `x` gets bound to `w` when `w` is already free. (In fact the code skeleton we gave you won't permit that to happen; it refuses to perform any applications except when the arguments are "result values", and it doesn't count free variables as such. As a result, other variables can never get bound to free variables.) - -So far, so good. - -But now consider the term: - - (\f. x) ((\x y. y x) 0) - -Since the outermost head `(\f. x)` is already a `Lambda`, we begin by evaluating the argument `((\x y. y x) 0)`. This results in: - - term environment - ---- ----------- - (\f. x) (\y. y x) [x->0] - -But that's not right, since it will result in the variable `x` in the head also being associated with the argument `0`. Instead, we want the binding of `x` to `0` to be local to the argument term `(\y. y x)`. For the moment, let's notate that like this: - -
```-term                             environment
-----                             -----------
-(\f. x)1 (\y. y x)2              []1   [x->0]2
-```
- -Now, let's suppose the head is more complex, like so: - - (\f. (\x. f x) I) ((\x y. y x) 0) - -That might be easier to understand if you transform it to: - - let f = (let x = 0 in \y. y x) in - let x = I in - f x - -Since the outermost head `(\f. (\x. f x) I)` is already a `Lambda`, we begin by evaluating the argument `((\x y. y x) 0)`. This results in: - -
```-term                             environment
-----                             -----------
-(\f. (\x. f x) I)1 (\y. y x)2    []1 [x->0]2
-```
- -Now the argument is not itself any longer an `App`, and so we are ready to evaluate the outermost application, binding `f` to the argument term. So we get: - -
```-term                             environment
-----                             -----------
-((\x. f x) I)1                   [f->(\y. y x)2]1 [x->0]2
-```
- -Next we bind `x` to the argument `I`, getting: - -
```-term                             environment
-----                             -----------
-(f x)1                           [x->I, f->(\y. y x)2]1 [x->0]2
-```
- -Now we have to apply the value that `f` is bound to to the value that `x` is bound to. But notice there is a free variable `x` in the term that `f` is bound to. How should we interpret that term? Should the evaluation proceed: - -
```-(\y. y x1) x1                    [x->I, ...]1 [x->0]2
-y x1                             [y->I, x->I, ...]1 [x->0]2
-I I
-I
-```
- -using the value that `x` is bound to in context1, _where the `f` value is applied_? Or should it proceed: - -
```-(\y. y x2) x1                    [x->I, ...]1 [x->0]2
-y x2                             [y->I, x->I, ...]1 [x->0]2
-I 0
-0
-```