+Given all these tools, we're (almost) in a position to define functions like the `factorial` and `length` functions we defined in class.
+
+Here's an attempt to define the `factorial` function:
+
+`let`
+ `factorial match` λ `n. if n == 0 then 1 else n * factorial (n-1)`
+`in factorial`
+
+or, using `case`:
+
+`let`
+ `factorial match` λ `n. case n of 0 then 1; _ then n * factorial (n - 1) end`
+`in factorial`
+
+But there's a problem here. What value does `factorial` have when evaluating the expression `factorial (n - 1)`?
+
+As we said in class, the natural precedent for this with non-function variables would go something like this:
+
+ let
+ x match 0;
+ y match x + 1;
+ x match x + 1;
+ z match 2 * x
+ in (y, z)
+
+We'd expect this to evaluate to `(1, 2)`, and indeed it does. That's because the `x` in the `x + 1` on the right-hand side of the third binding (`x match x + 1`) is evaluated under the scope of the first binding, of `x` to `0`.
+
+We should expect the `factorial` variable in the right-hand side of our attempted definition to behave the same way. It will evaluate to whatever value it has before reaching this `let`-expression. We actually haven't said what is the result of trying to evaluate unbound variables, as in:
+
+ let
+ x match y + 0
+ in x
+
+Let's agree not to do that. We can consider such expressions only under the implied understanding that they are parts of larger expressions that assign a value to `y`, as for example in:
+
+ let
+ y match 1
+ in let
+ x match y + 0
+ in x
+
+Hence, let's understand our attempted definition of `factorial` to be part of such a larger expression:
+
+`let`
+ `factorial match` λ `n. n`
+`in let`
+ `factorial match` λ `n. case n of 0 then 1; _ then n * factorial (n - 1) end`
+`in factorial 4`
+
+This would evaluate to what `4 * factorial 3` does, but with the `factorial` in the expression bound to the identity function λ `n. n`. In other words, we'd get the result `12`, not the correct answer `24`.
+
+For the time being, we will fix this solution by just introducing a special new construction `letrec` that works the way we want. Now in:
+
+`let`
+ `factorial match` λ `n. n`
+`in letrec`
+ `factorial match` λ `n. case n of 0 then 1; _ then n * factorial (n - 1) end`
+`in factorial 4`
+
+the initial binding of `factorial` to the identity function gets ignored, and the `factorial` in the right-hand side of our definition is interpreted to mean the very same function that we are hereby binding to `factorial`. Exactly how this works is a deep and exciting topic, that we will be looking at very closely in a few weeks. For the time being, let's just accept that `letrec` does what we intuitively want when defining functions recursively.
+
+**It's important to make sure you say letrec when that's what you want.** You may not *always* want `letrec`, though, if you're ever re-using variables (or doing other things) that rely on the bindings occurring in a specified order. With `letrec`, all the bindings in the construction happen simultaneously. This is why you can say, as Jim did in class:
+
+`letrec`
+ `even? match` λ `n. case n of 0 then 'true; _ then odd? (n-1) end`
+ `odd? match` λ `n. case n of 0 then 'false; _ then even? (n-1) end`
+`in (even?, odd?)`
+
+Here neither the `even?` nor the `odd?` pattern is matched before the other. They, and also the `odd?` and the `even?` variables in their right-hand side expressions, are all bound at once.
+
+As we said, this is deep and exciting, and it will make your head spin before we're done examining it. But let's trust `letrec` to do its job, for now.
+