X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2Fweek2_lambda_intro.mdwn;h=6bbb53991b855a73c57de344a56d24c0756ea83b;hp=3718d317134eab8993ec3684dc644e4bae948ca4;hb=6228f0758c13ed2d5d2d70a858a474f5c70bba68;hpb=a9aa00567a448746beece0fd605b29fadb64686c;ds=sidebyside
diff --git a/topics/week2_lambda_intro.mdwn b/topics/week2_lambda_intro.mdwn
index 3718d317..6bbb5399 100644
--- a/topics/week2_lambda_intro.mdwn
+++ b/topics/week2_lambda_intro.mdwn
@@ -198,9 +198,7 @@ and:
z (\x (x y))
-**Dot notation** Dot means "assume a left paren here, and the matching right
-paren as far to the right as possible without creating unbalanced
-parentheses". So:
+**Dot notation** Dot means "Insert a left parenthesis here, and the matching right parenthesis as far to the right as possible without creating unbalanced parentheses---so long as doing so would enclose an application or abstract not already wrapped in parentheses." Thus:
\x (\y (x y))
@@ -228,7 +226,15 @@ 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
+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.
+
+Similarly, we permit `\x. x`, which is shorthand for `\x x`, not for `\x (x)`, which
+our syntax forbids. (The [[lambda evaluator|/code/lambda_evaluator]] however tolerates such expressions.)
**Merging lambdas** An expression of the form `(\x (\y M))`, or equivalently, `(\x. \y. M)`, can be abbreviated as:
@@ -247,7 +253,7 @@ function? One popular answer is that a function can be represented by
a set of ordered pairs. This set is called the **graph** of the
function. If the ordered pair `(a, b)` is a member of the graph of `f`,
that means that `f` maps the argument `a` to the value `b`. In
-symbols, `f: a` ↦ `b`, or `f (a) == b`.
+symbols, `f: a` ↦ `b`, or `f (a) == b`.
In order to count as a *function* (rather
than as merely a more general *relation*), we require that the graph not contain two
@@ -270,7 +276,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)`
+`((\x (x x)) M) ~~> (M M)`
> `(\x (\y (y x)))` reorders its two arguments:
`(((\x (\y (y x))) M) N) ~~> (N M)`
@@ -283,7 +289,7 @@ lambda calculus, note that duplicating, reordering, and deleting
elements is all that it takes to simulate the behavior of a general
word processing program. That means that if we had a big enough
lambda term, it could take a representation of *Emma* as input and
-produce *Hamlet* as a result.
+produce *Hamlet* as a result.
Some of these functions are so useful that we'll give them special
names. In particular, we'll call the identity function `(\x x)`
@@ -312,7 +318,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
@@ -427,12 +433,12 @@ reasons sketched above.
## The analogy with `let` ##
In our basic functional programming language, we used `let`
-expressions to assign values to variables. For instance,
+expressions to assign values to variables. For instance,
let x match 2
- in (x, x)
+ 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.
@@ -440,7 +446,7 @@ construction.
is analogous to
- let x match ARG
+ let x match ARG
in BODY
This analogy should be treated with caution. For one thing, our `letrec`