author jim Sun, 8 Feb 2015 21:37:27 +0000 (16:37 -0500) committer Linux User Sun, 8 Feb 2015 21:37:27 +0000 (16:37 -0500)

index eca1514..ac92202 100644 (file)
@@ -8,8 +8,7 @@ we've become acquainted with.

## Booleans ##

## Booleans ##

-We'll start with the `if ... then
-... else...` construction we saw last week:
+We'll start with the `if ... then ... else ...` construction we saw last week:

if M then N else L

if M then N else L

@@ -55,7 +54,7 @@ Sucess! In the same spirit, `'false` could be **K I**, which reduces to `(\y x.
~~> ((\x x) L)
~~> L

~~> ((\x x) L)
~~> L

-So have seen our first major encoding in the Lambda Calculus:
+So we have seen our first major encoding in the Lambda Calculus:
"true" is represented by **K**, and "false" is represented by **K I**.
We'll be building up a lot of representations in the weeks to come,
and they will all maintain the discipline that if a expression is
"true" is represented by **K**, and "false" is represented by **K I**.
We'll be building up a lot of representations in the weeks to come,
and they will all maintain the discipline that if a expression is
@@ -316,7 +315,7 @@ Now we saw above how to define `map` in terms of `fold_right`. In Kapulet syntax

In our Lambda Calculus encoding, `fold_right (f, z) xs` gets translated to `xs f z`. That is, the list itself is the operator, just as we saw triples being. So we just need to know how to represent `lambda (x, zs). g x & zs`, on the one hand, and `[]` on the other, into the Lambda Calculus, and then we can also express `map`. Well, in the Lambda Calculus we're working with curried functions, and there's no infix syntax, so we'll replace the first by `lambda x zs. cons (g x) zs`. But we just defined `cons`, and the lambda is straightforward. And we also just defined `[]`. So we already have all the pieces to do this. Namely:

In our Lambda Calculus encoding, `fold_right (f, z) xs` gets translated to `xs f z`. That is, the list itself is the operator, just as we saw triples being. So we just need to know how to represent `lambda (x, zs). g x & zs`, on the one hand, and `[]` on the other, into the Lambda Calculus, and then we can also express `map`. Well, in the Lambda Calculus we're working with curried functions, and there's no infix syntax, so we'll replace the first by `lambda x zs. cons (g x) zs`. But we just defined `cons`, and the lambda is straightforward. And we also just defined `[]`. So we already have all the pieces to do this. Namely:

-    map (g, z) xs
+    map g xs

in Kapulet syntax, turns into this in our lambda evaluator:

in Kapulet syntax, turns into this in our lambda evaluator:

@@ -403,7 +402,7 @@ And indeed this is the Church encoding of the numbers:
<code>3 &equiv; \f z. f (f (f z)) ;  or \f z. f<sup>3</sup> z</code>
<code>...</code>

<code>3 &equiv; \f z. f (f (f z)) ;  or \f z. f<sup>3</sup> z</code>
<code>...</code>

-The encoding for `0` can also be written as `\f z. z`, which we've also proposed as the encoding for `[]` and for `false`. Don't read too much into this.
+The encoding for `0` is equivalent to `\f z. z`, which we've also proposed as the encoding for `[]` and for `false`. Don't read too much into this.

Given the above, can you figure out how to define the `succ` function? We already worked through the definition of `cons`, and this is just a simplification of that, so you should be able to do it. We'll make it a homework.

Given the above, can you figure out how to define the `succ` function? We already worked through the definition of `cons`, and this is just a simplification of that, so you should be able to do it. We'll make it a homework.