+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 +