From: Jim Date: Sun, 1 Feb 2015 08:13:22 +0000 (-0500) Subject: update week1 notes X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=d791500ac0e00266296de236cc2d804fd61aedcb update week1 notes --- diff --git a/week1.mdwn b/week1.mdwn index f2d4aebb..734bd654 100644 --- a/week1.mdwn +++ b/week1.mdwn @@ -568,5 +568,29 @@ It may be helpful to contrast these recursive-style definitons to the way one wo                                       `in n` `in length` -Here ... +Here there is no recursion. Rather what happens is that we *initialize* the variable `n` with the value `0`, and then so long as our sequence variable `xs` is non-empty, we *increment* that variable `n`, and *overwrite* the variable `xs` with the tail of the sequence that it is then bound to, and repeat in a loop (the `while ... do ... end` construction). This is similar to what happens in our second definition of `length`, using `aux`, but here it happens using *mutation* or *overwriting* the values of variables, and a special looping construction, whereas in the preceding definitions we achieved the same effect instead with recursion. + +We will be looking closely at mutation later in the term. For the time being, our focus will instead be on the recursive and *immutable* style of doing things. Meaning no variables get overwritten. + +It's helpful to observe that in expressions like: + + let + x match 0; + y match x + 1; + x match x + 1; + z match 2 * x + in (y, z) + +the variable `x` has not been *overwritten* (mutated). Rather, we have *two* variables `x` and its just that the second one is *hiding* the first so long as its scope is in effect. Once its scope expires, the original variable `x` is still in place, with its orginal binding. A different example should help clarify this. What do you think this: + + let + x match 0; + (y, z) match let + x match x + 1 + in (x, 2*x) + in ([y, z], x) + +evaluates to? Well, the right-hand side of the second binding will evaluate to `(1, 2)`, because it uses the outer binding of `x` to `0` for the right-hand side of its own binding `x match x + 1`. That gives us a new binding of `x` to `1`, which is in place when we evaluate `(x, 2*x)`. That's why the whole right-hand side of the second binding evaluates to `(1, 2)`. So `y` gets bound to `1` and `z` to `2`. But now what is `x` bound to in the final line? The binding of `x` to `1` was in place only until we got to `(x, 2*x)`. After that its scope expired, and the original binding of `x` to `0` reappears. So the final line evaluates to `([1, 2], 0)`. + +This is very like what happens in ordinary predicate logic if you say: &exists; `x. F x and (` ∀ `x. G x ) and H x`. The `x` in `F x` and in `H x` are governed by the outermost quantifier, and only the `x` in `G x` is governed by the inner quantifier.