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.