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=091e1234dbaef36e5cd163b03bacad2eac19dbc1;hb=a4d2693effe839524592f4427465ff8d97625302;hpb=b6e2ba40d18b2c1efb84e764d0e07d7f97d57319 diff --git a/topics/week2_lambda_intro.mdwn b/topics/week2_lambda_intro.mdwn index 091e1234..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 @@ -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`