+`in length`
+
+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, consider the right-hand side of the second binding:
+
+ let
+ x match x + 1
+ in (x, 2*x)
+
+This expression evaluates 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 thing evaluates to `(1, 2)`. So now returning to the outer expression, `y` gets bound to `1` and `z` to `2`. But now what is `x` bound to in the final line,`([y, z], x)`? 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:
+
+∃ `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.
+
+### That's enough ###
+
+This was a lot of material, and you may need to read it carefully and think about it, but none of it should seem profoundly different from things you're already accustomed to doing. What we worked our way up to was just the kind of recursive definitions of `factorial` and `length` that you volunteered in class, before learning any programming.
+
+You have all the materials you need now to do this week's [[assignment|assignment1]]. Some of you may find it easy. Many of you will not. But if you understand what we've done here, and give it your time and attention, we believe you can do it.
+
+There are also some [[advanced notes|week1 advanced notes]] extending this week's material.