caps

[lambda.git] / topics / week2_lambda_intro.mdwn

diff --git a/topics/week2_lambda_intro.mdwn b/topics/week2_lambda_intro.mdwn
index 091e123..6bbb539 100644 (file)
--- a/topics/week2_lambda_intro.mdwn
+++ b/topics/week2_lambda_intro.mdwn
@@ -198,9 +198,7 @@ and:
     z (\x (x y))
 
 
     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))
 
 
     \x (\y (x y))
 


@@ -228,7 +226,15 @@ abbreviates:
 
     ((\x (\y (x y))) x)
 
 
     ((\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:
 
 
 **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
 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
 
 In order to count as a *function* (rather
 than as merely a more general *relation*), we require that the graph not contain two


@@ -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
 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)`
 
 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)
 
 
     (\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
 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`
 ## 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
 
     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.
 
 a redex in the lambda calculus as a particular sort of `let`
 construction.
 


@@ -440,7 +446,7 @@ construction.
 
 is analogous to
 
 
 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`
     in BODY
 
 This analogy should be treated with caution.  For one thing, our `letrec`