+Finally, we're in a position to revisit the two definitions of `length` that Jim presented in class. Here is the first:
+
+`letrec`
+ `length match` λ `xs. case xs of [] then 0; _:ys then 1 + length ys end`
+`in length`
+
+This function accept a sequence `xs`, and if its empty returns `0`, else it says that its length is `1` plus whatever is the length of its remainder when you take away the first element. In programming circles, this remainder is commonly called the sequence's "tail" (and the first element is its "head").
+
+Thus if we evaluated `length [10, 20, 30]`, that would give the same result as `1 + length [20, 30]`, which would give the same result as `1 + (1 + length [30])`, which would give the same result as `1 + (1 + (1 + length []))`. But `length []` is `0`, so our original expression evaluates to `1 + (1 + (1 + 0))`, or `3`.
+
+Here's another way to define the `length` function:
+
+`letrec`
+ `aux match` λ `(n, xs). case xs of [] then n; _:ys then aux (n + 1, ys) end`
+`in` λ `xs. aux (0, xs)`
+
+This may be a bit confusing. What we have here is a helper function `aux` (for "auxiliary") that accepts *two* arguments, the first being a counter of how long we've counted in the sequence so far, and the second argument being how much more of the sequence we have to inspect. If the sequence we have to inspect is empty, then we're finished and we can just return our counter. (Note that we don't return `0`.) If not, then we add `1` to the counter, and proceed to inspect the tail of the sequence, ignoring the sequence's first element. After the `in`, we can't just return the `aux` function, because it expects two arguments, whereas `length` should just be a function of a single argument, the sequence whose length we're inquiring about. What we do instead is return a λ-generated function, that expects a single sequence argument `xs`, and then returns the result of calling `aux` with that sequence together with an initial counter of `0`.
+
+So for example, if we evaluated `length [10, 20, 30]`, that would give the same result as `aux (0, [10, 20, 30])`, which would give the same result as `aux (1, [20, 30])`, which would give the same result as `aux (2, [30])`, which would give the same result as `aux(3, [])`, which would give `3`. (This should make it clear why when `aux` is called with the empty sequence, it returns the result `n` rather than `0`.)
+
+Programmers will sometimes define functions in the second style because it can be evaluated more efficiently than the first style. You don't need to worry about things like efficiency in this seminar. But you should become acquainted with, and comfortable with, both styles of recursive definition.
+
+It may be helpful to contrast these recursive-style definitons to the way one would more naturally define the `length` function in an imperatival language. This uses some constructs we haven't explained yet, but I trust their meaning will be intuitively clear enough.
+
+`let`
+ `empty? match` λ `xs.` *this definition left as an exercise*;
+ `tail match` λ `xs.` *this definition left as an exercise*;
+ `length match` λ `xs. let`
+ `n := 0;`
+ `while not (empty? xs) do`
+ `n := n + 1;`
+ `xs := tail xs`
+ `end`
+ `in n`
+`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.