+The first two expressions are *convertible*: in particular the first
+reduces to the second via a single instance of beta reduction. So they
+can be regarded as proof-theoretically equivalent even though they're
+not syntactically identical. However, the proof theory we've given so
+far doesn't permit you to reduce the second expression to the
+third. So these lambda expressions are non-equivalent.
+
+To use a linguistic analogy, you can think of what we're calling
+"proof theory" as a kind of syntactic transformation. That is, the
+sentences *John saw Mary* and *Mary was seen by John* are not
+syntactically identical, yet (on some theories) one can be derived
+from the other. The key element in the analogy is that this kind of
+syntactic derivation is supposed to preserve meaning, so that the two
+sentence mean (roughly) the same thing.
+
+There's an extension of the proof-theory we've presented so far which
+does permit this further move. And in that extended proof theory, all
+computable functions with the same extension do turn out to be
+equivalent (convertible). However, at that point, we still wouldn't be
+working with the traditional mathematical notion of a function as a
+set of ordered pairs. One reason is that the fully general
+mathematical notion permits many uncomputable functions, but the
+lambda calculus is capable of expressing only computable functions. A
+second reason is that the full mathematical notion prohibits
+functions from applying to themselves, but in the lambda calculus,
+it is permitted for a function to take itself as an argument (for
+instance, there is nothing wrong with applying the identity function
+to itself, thus: `(\x x)(\x x)`. This is a redex that reduces to the
+identity function (of course).
+
+
+The analogy with `let`
+----------------------
+
+In our basic functional programming language, we used `let`
+expressions to assign values to variables. For instance,
+
+ let x match 2
+ in (x, x)
+
+evaluates to the ordered pair (2, 2). It may be helpful to think of
+a redex in the lambda calculus as a particular sort of `let`
+construction.
+
+ ((\x M) N) is analogous to
+
+ let x match N
+ in M
+
+This analogy should be treated with caution. For one thing, our
+`letrec` allowed us to define recursive functions in which the name of
+the function appeared within the expression `N`; we're not ready to
+deal with recursive functions in the lambda calculus yet. For
+another, we defined `let` in terms of values, and at this point, the
+lambda calculus doesn't have values, it only has other expressions.
+So it might be better to translate `((\x M) N)` as `let x be replaced
+by N in M`, or some such. Most problematically, in the lambda
+calculus, an abstract such as `(\x (x x))` is perfectly well-formed
+and coherent, but it is not possible to write a `let` expression that
+does not have an argument (here, `N`) explicitly present.
+
+Nevertheless, the correspondence is close enough that it can spur
+intuition.