X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2Fweek2_encodings.mdwn;h=091fb4c5e19d8069a851375db8dc7d28fdfa794a;hp=290cd5d82f85bda88464c44990dd154b5e75dbb3;hb=a4d2693effe839524592f4427465ff8d97625302;hpb=aaf2ff6a5405de529d0272a4692557c5a55e822a diff --git a/topics/week2_encodings.mdwn b/topics/week2_encodings.mdwn index 290cd5d8..091fb4c5 100644 --- a/topics/week2_encodings.mdwn +++ b/topics/week2_encodings.mdwn @@ -231,6 +231,7 @@ That will evaluate to whatever this does: f (f (f (z, 10), 20), 30) + With a commutative operator like `(+)`, it makes no difference whether you say `fold_right ((+), z) xs` or `fold_left ((+), z) xs`. But with other operators it will make a difference. We can't say `fold_left ((&), []) [10, 20, 30]`, since that would start by trying to evaluate `[] & 10`, which would crash. But we could do this: let @@ -397,6 +398,8 @@ In fact, there's a way of looking at this that makes it look incredibly natural. \x. f (g x) +For example, the operation that maps a number `n` to `n2+1` is the composition of the successor function and the squaring function (first we square, then we take the successor). + The composition of a function `f` with itself, namely: \x. f (f x) @@ -415,13 +418,13 @@ we are proposing to encode it as: And indeed this is the Church encoding of the numbers: -`0 ≡ \f z. I z         ; or \f z. f0 z` -`1 ≡ \f z. f z         ; or \f z. f1 z` -`2 ≡ \f z. f (f z)     ; or \f z. f2 z` -`3 ≡ \f z. f (f (f z)) ; or \f z. f3 z` +`0 ≡ \f z. z   ; <~~> \f z. I z, or \f z. f0 z` +`1 ≡ \f z. f z                 ; or \f z. f1 z` +`2 ≡ \f z. f (f z)             ; or \f z. f2 z` +`3 ≡ \f z. f (f (f z))         ; or \f z. f3 z` `...` -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. +The encoding for `0` is what we 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.