-term environment ----- ----------- -(\w.(\y.y) w) 2 [] -(\y.y) w [w->2] -y [- -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: - -y->2, w->2] -

-term environment ----- ----------- -(\f. x)- -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: - -_{1}(\y. y x)_{2}[]_{1}[x->0]_{2}-

-term environment ----- ----------- -(\f. (\x. f x) I)- -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: - -_{1}(\y. y x)_{2}[]_{1}[x->0]_{2}-

-term environment ----- ----------- -((\x. f x) I)- -Next we bind `x` to the argument `I`, getting: - -_{1}[f->(\y. y x)_{2}]_{1}[x->0]_{2}-

-term environment ----- ----------- -(f x)- -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: - -_{1}[x->I, f->(\y. y x)_{2}]_{1}[x->0]_{2}-

-(\y. y- -using the value that `x` is bound to in contextx) x_{1}_{1}[x->I, ...]_{1}[x->0]_{2}-y x_{1}[y->I, x->I, ...]_{1}[x->0]_{2}-I I -I -

-(\y. y- -using the value that `x` was bound to in contextx) x_{2}_{1}[x->I, ...]_{1}[x->0]_{2}-y x_{2}[y->I, x->I, ...]_{1}[x->0]_{2}-I 0 -0 -