X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2Fweek2_lambda_intro.mdwn;h=4b0917529eb8041f64e6e43f42de0c2cad17de54;hp=3718d317134eab8993ec3684dc644e4bae948ca4;hb=020566910974049e4cd9cbc9279a781768e1817c;hpb=a9aa00567a448746beece0fd605b29fadb64686c

diff --git a/topics/week2_lambda_intro.mdwn b/topics/week2_lambda_intro.mdwn
index 3718d317..4b091752 100644
--- a/topics/week2_lambda_intro.mdwn
+++ b/topics/week2_lambda_intro.mdwn
@@ -228,7 +228,12 @@ abbreviates:
 
     ((\x (\y (x y))) x)
 
-We didn't have to insert any parentheses around the inner body of `\y. (x y)` because they were already there.
+The outermost parentheses were added because we have an application. `(\x. \y.
+...)` became `(\x (\y. ...))` because of the rule for dots. We didn't have to
+insert any parentheses around the inner body of `\y. (x y)` because they were
+already there. That is, in expressions of the form `\y. (...)`, the dot abbreviates
+nothing. It's harmless to write such a dot, though, and it can be conceptually
+helpful especially in light of the next convention...
 
 
 **Merging lambdas** An expression of the form `(\x (\y M))`, or equivalently, `(\x. \y. M)`, can be abbreviated as:
@@ -270,7 +275,7 @@ For some lambda terms, it is easy to see what function they represent:
 simply returns `M`: `((\x x) M) ~~> M`.
 
 > `(\x (x x))` duplicates its argument (applies it to itself):
-`((\x (x x)) M) ~~> (M M)` <!-- **M** or &omega;; W is \uv.uvv -->
+`((\x (x x)) M) ~~> (M M)` <!-- **M** or &omega;; W is \uv.uvv, L is \uv.u(vv) -->
 
 > `(\x (\y (y x)))` reorders its two arguments:
 `(((\x  (\y (y x))) M) N) ~~> (N M)` <!-- **T**; C is \uvx.uxv -->
@@ -312,7 +317,7 @@ are distinct lambda expressions:
 
     (\z z)
 
-yet when applied to any argument M, all of these will always return M. So they
+yet when applied to any argument `M`, all of these will always return `M`. So they
 have the same extension. It's also true, though you may not yet be in a
 position to see, that no other function can differentiate between them when
 they're supplied as an argument to it. However, these expressions are all
@@ -432,7 +437,7 @@ 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
+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.