X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2F_week2_lambda_calculus_fine_points.mdwn;fp=topics%2F_week2_lambda_calculus_fine_points.mdwn;h=2176f359dac72fb6f197fca9dd23411b5302921f;hp=0000000000000000000000000000000000000000;hb=e171fd1236da1479e08f7753a0802c4cd6b5efa8;hpb=6465fb1a7d6eefd49c2fcef866359cf03089906d

diff --git a/topics/_week2_lambda_calculus_fine_points.mdwn b/topics/_week2_lambda_calculus_fine_points.mdwn
new file mode 100644
index 00000000..2176f359
--- /dev/null
+++ b/topics/_week2_lambda_calculus_fine_points.mdwn
@@ -0,0 +1,63 @@
+Fine points concerning the lambda calculus
+==========================================
+
+Hankin uses the symbol
+<code><big><big>&rarr;</big></big></code> for one-step contraction,
+and the symbol <code><big><big>&#8608;</big></big></code> for
+zero-or-more step reduction. Hindley and Seldin use
+<code><big><big><big>&#8883;</big></big></big><sub>1</sub></code> and
+<code><big><big><big>&#8883;</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>&equiv;</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)
+