Remembering that I is the identity combinator, this could also be written:
-<pre><code>(I) z<p>
-(s) z<p>
-(s ∘ s) z<p>
-(s ∘ s ∘ s) z<p>
+<pre><code>(I) z
+(s) z
+(s ∘ s) z
+(s ∘ s ∘ s) z
...</code></pre>
And we might adopt the following natural shorthand for this:
-<pre><code>s<sup>0</sup> z<p>
-s<sup>1</sup> z<p>
-s<sup>2</sup> z<p>
-s<sup>3</sup> z<p>
+<pre><code>s<sup>0</sup> z
+s<sup>1</sup> z
+s<sup>2</sup> z
+s<sup>3</sup> z
...</code></pre>
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:
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 <code>s<sup><em>n</em></sup> z</code> as a result. In other words:
-<pre><code>zero ≡ \s z. s<sup>0</sup> z ≡ \s z. z<p>
-one ≡ \s z. s<sup>1</sup> z ≡ \s z. s z<p>
-two ≡ \s z. s<sup>2</sup> z ≡ \s z. s (s z)<p>
-three ≡ \s z. s<sup>3</sup> z ≡ \s z. s (s (s z))<p>
+<pre><code>zero ≡ \s z. s<sup>0</sup> z ≡ \s z. z
+one ≡ \s z. s<sup>1</sup> z ≡ \s z. s z
+two ≡ \s z. s<sup>2</sup> z ≡ \s z. s (s z)
+three ≡ \s z. s<sup>3</sup> z ≡ \s z. s (s (s z))
...</code></pre>
This is a very elegant idea. Implementing numbers this way, we'd let the successor function be:
-<pre><code>succ ≡ \n. \s z. s (n s z)</code><pre>
+<pre><code>succ ≡ \n. \s z. s (n s z)</code></pre>
So, for example:
-<pre><code> succ two<p>
- ≡ (\n. \s z. s (n s z)) (\s z. s (s z))<p>
-~~> \s z. s ((\s z, s (s z)) s z)<p>
+<pre><code> 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))</code></pre>
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:
How would we tell whether a number was 0? Well, look again at the implementations of the first few numbers:
-<pre><code>zero ≡ \s z. s<sup>0</sup> z ≡ \s z. z<p>
-one ≡ \s z. s<sup>1</sup> z ≡ \s z. s z<p>
-two ≡ \s z. s<sup>2</sup> z ≡ \s z. s (s z)<p>
-three ≡ \s z. s<sup>3</sup> z ≡ \s z. s (s (s z))<p>
+<pre><code>zero ≡ \s z. s<sup>0</sup> z ≡ \s z. z
+one ≡ \s z. s<sup>1</sup> z ≡ \s z. s z
+two ≡ \s z. s<sup>2</sup> z ≡ \s z. s (s z)
+three ≡ \s z. s<sup>3</sup> z ≡ \s z. s (s (s z))
...</code></pre>
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: