refine notes

[lambda.git] / topics / week2_lambda_advanced.mdwn

diff --git a/topics/week2_lambda_advanced.mdwn b/topics/week2_lambda_advanced.mdwn
index 1372e43..dbc62e7 100644 (file)
--- a/topics/week2_lambda_advanced.mdwn
+++ b/topics/week2_lambda_advanced.mdwn
@@ -1,4 +1,4 @@
-## Fine points concerning the lambda calculus ##
+## Advanced notes on the Lambda Calculus ##
 
 Hankin uses the symbol
 <code><big><big>&rarr;</big></big></code> for one-step contraction,
@@ -7,10 +7,7 @@ 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>.
 
-As we said in the main notes, 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 write that like
-this:
+As we said in the main notes, 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 write that like this:
 
     M <~~> N
 
@@ -31,11 +28,11 @@ 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)`.
+> `T` is defined to be `(M N)`.
 
 or:
 
-> Let T be `(M N)`.
+> Let `T` be `(M N)`.
 
 We'll regard the following two expressions:
 
@@ -92,7 +89,7 @@ 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 &lambda;s that they shouldn't be
+we're substituting in get "captured" by binding &lambda;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).
@@ -147,7 +144,7 @@ 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,
+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:
 
@@ -158,16 +155,16 @@ This:
 
     N ~~> z y
 
-means that N beta-reduces to `z y`. This:
+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.
+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.
+symbols (or some notational variant of them) is added to the object language. But only in outermost contexts. It's like the "sequent" symbol (written `=>` or <code>&vdash;</code>) in [Gentzen-style proof systems](https://en.wikipedia.org/wiki/Sequent_calculus) for logic. You can't embed the `~~>` or `<~~>` symbol inside lambda terms.
 
 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.