X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=lists_and_numbers.mdwn;fp=lists_and_numbers.mdwn;h=e3dd1fba08336938185db88db6e1a4ff38b5cca5;hp=73decb27029677ed1c5291dbaaef4953620887c8;hb=17563aceb6428a31d42d58726ca73dda2fd2e8b5;hpb=6912c9938c2edb3ecbd90d57ce286662942b3090 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: