X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2Fweek2_encodings.mdwn;fp=topics%2Fweek2_encodings.mdwn;h=6adafda04b2cab617a43baac9d0bdb1b36548586;hp=290cd5d82f85bda88464c44990dd154b5e75dbb3;hb=3303e8c15d71c68c58c6eec5d6dc7c03e3d6d7bd;hpb=588916b85952d356b51cccea0fb38b8cc1582174
diff --git a/topics/week2_encodings.mdwn b/topics/week2_encodings.mdwn
index 290cd5d8..6adafda0 100644
--- a/topics/week2_encodings.mdwn
+++ b/topics/week2_encodings.mdwn
@@ -397,6 +397,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,10 +417,10 @@ 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.