--- /dev/null
+Fine points concerning the lambda calculus
+==========================================
+
+Hankin uses the symbol
+<code><big><big>→</big></big></code> for one-step contraction,
+and the symbol <code><big><big>↠</big></big></code> for
+zero-or-more step reduction. Hindley and Seldin use
+<code><big><big><big>⊳</big></big></big><sub>1</sub></code> and
+<code><big><big><big>⊳</big></big></big></code>.
+
+When M and N are such that there's some P that M reduces to by zero or
+more steps, and that N also reduces to by zero or more steps, then we
+say that M and N are **beta-convertible**. We'll write that like this:
+
+ M <~~> N
+
+This is what plays the role of equality in the lambda calculus. Hankin
+uses the symbol `=` for this. So too do Hindley and
+Seldin. Personally, I keep confusing that with the relation to be
+described next, so let's use this notation instead. Note that `M <~~>
+N` doesn't mean that each of `M` and `N` are reducible to each other;
+that only holds when `M` and `N` are the same expression. (Or, with
+our convention of only saying "reducible" for one or more reduction
+steps, it never holds.)
+
+In the metatheory, it's also sometimes useful to talk about formulas
+that are syntactically equivalent *before any reductions take
+place*. Hankin uses the symbol <code>≡</code> for this. So too
+do Hindley and Seldin. We'll use that too, and will avoid using `=`
+when discussing the metatheory. Instead we'll use `<~~>` as we said
+above. When we want to introduce a stipulative definition, we'll write
+it out longhand, as in:
+
+> T is defined to be `(M N)`.
+
+We'll regard the following two expressions:
+
+ (\x (x y))
+
+ (\z (z y))
+
+as syntactically equivalent, since they only involve a typographic
+change of a bound variable. Read Hankin section 2.3 for discussion of
+different attitudes one can take about this.
+
+Note that neither of those expressions are identical to:
+
+ (\x (x w))
+
+because here it's a free variable that's been changed. Nor are they identical to:
+
+ (\y (y y))
+
+because here the second occurrence of `y` is no longer free.
+
+There is plenty of discussion of this, and the fine points of how
+substitution works, in Hankin and in various of the tutorials we've
+linked to about the lambda calculus. We expect you have a good
+intuitive understanding of what to do already, though, even if you're
+not able to articulate it rigorously.
+
+* [More discussion in week 2 notes](/week2/#index1h1)
+