From: Jim Pryor Date: Fri, 17 Sep 2010 00:52:09 +0000 (-0400) Subject: tweak lists_and_numbers X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=17563aceb6428a31d42d58726ca73dda2fd2e8b5 tweak lists_and_numbers Signed-off-by: Jim Pryor --- diff --git a/lists_and_numbers.mdwn b/lists_and_numbers.mdwn index 73decb27..e3dd1fba 100644 --- a/lists_and_numbers.mdwn +++ b/lists_and_numbers.mdwn @@ -230,18 +230,18 @@ Now consider the following series: Remembering that I is the identity combinator, this could also be written: -
(I) z

-(s) z

-(s ∘ s) z

-(s ∘ s ∘ s) z

+
(I) z
+(s) z
+(s ∘ s) z
+(s ∘ s ∘ s) z
 ...

 
 And we might adopt the following natural shorthand for this:
 
-
s0 z

-s1 z

-s2 z

-s3 z

+
s0 z
+s1 z
+s2 z
+s3 z
 ...

 
 We haven't introduced any new constants 0, 1, 2 into the object language, nor any new form of syntactic combination. This is all just a metalanguage abbreviation for:
@@ -254,10 +254,10 @@ We haven't introduced any new constants 0, 1, 2 into the object language, nor an
 
 Church had the idea to implement the number *n* by an operation that accepted an arbitrary function `s` and base value `z` as arguments, and returned sn z as a result. In other words:
 
-
zero ≡ \s z. s0 z ≡ \s z. z

-one ≡ \s z. s1 z ≡ \s z. s z

-two ≡ \s z. s2 z ≡ \s z. s (s z)

-three ≡ \s z. s3 z ≡ \s z. s (s (s z))

+
zero ≡ \s z. s0 z ≡ \s z. z
+one ≡ \s z. s1 z ≡ \s z. s z
+two ≡ \s z. s2 z ≡ \s z. s (s z)
+three ≡ \s z. s3 z ≡ \s z. s (s (s z))
 ...

 
 This is a very elegant idea. Implementing numbers this way, we'd let the successor function be:
@@ -266,9 +266,9 @@ This is a very elegant idea. Implementing numbers this way, we'd let the success
 
 So, for example:
 
-
    succ two

-  ≡ (\n. \s z. s (n s z)) (\s z. s (s z))

-~~> \s z. s ((\s z, s (s z)) s z)

+
    succ two
+  ≡ (\n. \s z. s (n s z)) (\s z. s (s z))
+~~> \s z. s ((\s z, s (s z)) s z)
 ~~> \s z. s (s (s z))
 
 
 Adding *m* to *n* is a matter of applying the successor function to *n* *m* times. And we know how to apply an arbitrary function s to *n* *m* times: we just give that function s, and the base-value *n*, to *m* as arguments. Because that's what the function we're using to implement *m* *does*. Hence **add** can be defined to be, simply:
@@ -279,10 +279,10 @@ Isn't that nice?
 
 How would we tell whether a number was 0? Well, look again at the implementations of the first few numbers:
 
-
zero ≡ \s z. s0 z ≡ \s z. z

-one ≡ \s z. s1 z ≡ \s z. s z

-two ≡ \s z. s2 z ≡ \s z. s (s z)

-three ≡ \s z. s3 z ≡ \s z. s (s (s z))

+
zero ≡ \s z. s0 z ≡ \s z. z
+one ≡ \s z. s1 z ≡ \s z. s z
+two ≡ \s z. s2 z ≡ \s z. s (s z)
+three ≡ \s z. s3 z ≡ \s z. s (s (s z))
 ...

 
 We can see that with the non-zero numbers, the function s is always applied to an argument at least once. With zero, on the other hand, we just get back the base-value. Hence we can determine whether a number is zero as follows: