``successor ∘ square``
- -and in general: - -
``(s ∘ f) z``
- -should be understood as: - - s (f z) - -Now consider the following series: - - z - s z - s (s z) - s (s (s z)) - ... - -Remembering that I is the identity combinator, this could also be written: - -
``````(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
-...``````
- -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: - - z - s z - s (s z) - s (s (s z)) - ... - -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))
-...``````
- -This is a very elegant idea. Implementing numbers this way, we'd let the successor function be: - -
``succ ≡ \n. \s z. s (n s z)``
- -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)
-~~> \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: - - \m \n. m succ n - -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))
-...``````