+
+## Substitution and Alpha-Conversion ##
+
+Intuitively, (a) and (b) express the application of the same function to the argument `y`:
+
+<OL type=a>
+<LI><code>(\x. \z. z x) y</code>
+<LI><code>(\x. \y. y x) y</code>
+</OL>
+
+One can't just rename variables freely. (a) and (b) are different than what's expressed by:
+
+<OL type=a start=3>
+<LI><code>(\z. (\z. z z) y</code>
+</OL>
+
+
+Substituting `y` into the body of (a) `(\x. \z. z x)` is unproblematic:
+
+ (\x. \z. z x) y ~~> \z. z y
+
+However, with (b) we have to be more careful. If we just substituted blindly,
+then we might take the result to be `\y. y y`. But this is the self-application
+function, not the function which accepts an arbitrary argument and applies that
+argument to the free variable `y`. In fact, the self-application function is
+what (c) reduces to. So if we took (b) to reduce to `\y. y y`, we'd wrongly be
+counting (b) to be equivalent to (c), instead of (a).
+
+To reduce (b), then, we need to be careful to that no free variables in what
+we're substituting in get captured by binding λs that they shouldn't be
+captured by.
+
+In practical terms, you'd just replace (b) with (a) and do the unproblematic substitution into (a).
+
+How should we think about the explanation and justification for that practical procedure?
+
+One way to think about things here is to identify expressions of the lambda
+calculus with *particular alphabetic sequences*. Then (a) and (b) would be
+distinct expressions, and we'd have to have an explicit rule permitting us to
+do the kind of variable-renaming that takes us from (a) to (b) (or vice versa).
+This kind of renaming is called "alpha-conversion." Look in the standard
+treatments of the lambda calculus for detailed discussion of this.
+
+Another way to think of it is to identify expressions not with particular
+alphabetic sequences, but rather with *classes* of alphabetic sequences, which
+stand to each other in the way that (a) and (b) do. That's the way we'll talk.
+We say that (a) and (b) are just typographically different notations for a
+*single* lambda formula. As we'll say, the lambda formula written with (a) and
+the lambda formula written with (b) are literally syntactically identical.
+
+A third way to think is to identify the lambda formula not with classes of
+alphabetic sequences, but rather with abstract structures that we might draw
+like this:
+
+<pre><code>
+ (λ. λ. _ _) y
+ ^ ^ | |
+ | |__| |
+ |_______|
+</code></pre>
+
+Here there are no bound variables, but *bound positions* remain. We can
+regard formula like (a) and (b) as just helpfully readable ways to designate
+these abstract structures.
+
+A version of this last approach is known as [de Bruijn notation](http://en.wikipedia.org/wiki/De_Bruijn_index) for the lambda calculus.
+
+It doesn't seem to matter which of these approaches one takes; the logical
+properties of the systems are exactly the same. It just affects the particulars
+of how one states the rules for substitution, and so on. And whether one talks
+about expressions being literally "syntactically identical," or whether one
+instead counts them as "equivalent modulu alpha-conversion."
+
+(Linguistic trivia: some linguistic discussions do suppose that
+alphabetic variance has important linguistic consequences; see Ivan Sag's
+dissertation.)
+
+Next week, we'll discuss other systems that lack variables. Those systems will
+not just lack variables in the sense that de Bruijn notation does; they will
+furthermore lack any notion of a bound position.
+
+
+## Review: syntactic equality, reduction, convertibility ##
+
+Define N to be `(\x. x y) z`. Then N and `(\x. x y) z` are syntactically equal,
+and we're counting them as syntactically equal to `(\z. z y) z` as well. We'll express
+all these claims in our metalanguage as:
+
+<pre><code>N ≡ (\x. x y) z ≡ (\z. z y) z
+</code></pre>
+
+This:
+
+ N ~~> z y
+
+means that N beta-reduces to `z y`. This:
+
+ M <~~> N
+
+means that M and N are beta-convertible, that is, that there's something they both reduce to in zero or more steps.
+
+The symbols `~~>` and `<~~>` aren't part of what we're calling "the Lambda
+Calculus". In our mouths, they're just part of our metatheory for talking about it. In the uses of
+the Lambda Calculus as a formal proof theory, one or the other of these
+symbols (or some notational variant of them) is added to the object language.
+
+See Hankin Sections 2.2 and 2.4 for the proof theory using `<~~>` (which he
+writes as `=`). He discusses the proof theory using `~~>` in his Chapter 3.
+This material is covered in slightly different ways (different organization and
+some differences in terminology and notation) in Chapters 1, 6, and 7 of the
+Hindley & Seldin.