The `x + 1` that is evaluated to give the value that `y` gets bound to uses the (more local) binding of `x` to `5`, not the (previous, less local) binding of `x` to `0`. By the way, the parentheses in that displayed expression were just to focus your attention. It would have parsed and meant the same without them.
-Now we can allow ourselves to introduce λ-expressions in the following way. If a λ-expression is applied to an argument, as in: `(`λ `x.` φ`) M`, for any (simple or complex) expressions φ and `M`, this means the same as: `let x be M in` φ. That is, the argument to the λ-expression provides (when evaluated) a value for the variable `x` to be bound to, and then the result of the whole thing is whatever φ evaluates to, under that binding to `x`.
+Now we can allow ourselves to introduce λ-expressions in the following way. If a λ-expression is applied to an argument, as in: `(`λ `x.` φ`) M`, for any (simple or complex) expressions φ and `M`, this means the same as: `let x be M in` φ. That is, the argument `M` to the λ-expression provides (when evaluated) a value for the variable `x` to be bound to, and then the result of the whole thing is whatever φ evaluates to, under that binding to `x`.
If we restricted ourselves to only that usage of λ-expressions, that is when they were applied to all the arguments they're expecting, then we wouldn't have moved very far from the decidable fragment of arithmetic we began with.
For the time being, these are the only patterns we'll allow. But since the definition of patterns is recursive, this permits very complex patterns. What would this evaluate to:
let
- ([x, y], [z:zs, w]) match ([[], 'true], [[10, 20, 30], 'false])
+ ([x, y], [z:zs, w]) match ([[], [1]], [[10, 20, 30], [0]])
in (z, y)
Also, we will permit complex patterns in λ-expressions, too. So you can write: