From 3303e8c15d71c68c58c6eec5d6dc7c03e3d6d7bd Mon Sep 17 00:00:00 2001 From: jim Date: Sat, 14 Feb 2015 17:01:00 -0500 Subject: [PATCH] alignment --- topics/week2_encodings.mdwn | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) 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. -- 2.11.0