``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))
...```

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:

some-number (\x. false) true

If some-number is zero, this will evaluate to the base value true. If some-number is non-zero, then it will evaluate to the result of applying (\x. false) to the result of applying ... to the result of applying (\x. false) to the base value true. But the result of applying (\x. false) to any argument is always false. So when some-number is non-zero, this expressions evaluates to false.

Perhaps not as elegant as addition, but still decently principled.

Multiplication is even more elegant. Consider that applying an arbitrary function s to a base value z *m × n* times is a matter of applying s to z *n* times, and then doing that again, and again, and so on...for *m* repetitions. In other words, it's a matter of applying the function (\z. n s z) to z *m* times. In other words, *m × n* can be represented as:

\s z. m (\z. n s z) z
~~> \s z. m n s z

which eta-reduces to:

m n

Isn't that nice?

However, at this point the elegance gives out. The predecessor function is substantially more difficult to construct on this implementation. As with all of these operations, there are several ways to do it, but they all take at least a bit of ingenuity. If you're only first learning programming right now, it would be unreasonable to expect you to be able to figure out how to do it.

However, if on the other hand you do have some experience programming, consider how you might construct a predecessor function for numbers implemented in this way. Using only the resources we've so far discussed. (So you have no general facility for performing recursion, for instance.)

(list?)
nil
cons
nil?, (pair?)
tail

Chris's lists:
nil = (t,N)  = \f. f true N
[a] = (f,(a,nil))
[b,a] = (f,(b,[a]))

isnil = get-first
tail = L get-second get-second

Lists 2:
nil = false
[a] = (a,nil)

L (\h\t.K deal_with_h_and_t) if-nil

We've already seen enumerations: true | false, red | green | blue
What if you want one or more of the elements to have associated data? e.g. red | green | blue

could handle like this:
the-value if-red if-green (\n. handler-if-blue-to-degree-n)

then red = \r \g \b-handler. r
green = \r \g \b-handler. g
make-blue = \degree. \r \g \b-handler. b-handler degree

A list is basically: empty | non-empty

empty = \non-empty-handler \if-empty. if-empty = false
cons = \h \t. \non-empty-handler \if-empty. non-empty-handler h t

so [a] = cons a empty = \non-empty-handler \_. non-empty-handler a empty

Lists 3:
[a; tl] isnil == (\f. f a tl) (\h \t.false) a b ~~> false a b

nil isnil == (\f. M) (\h \t. false) a b ~~> M[f:=isnil] a b == a

so M could be \a \b. a, i.e. true
so nil = \f. true == K true == K K = \_ K

nil = K true
[a] = (a,nil)
[b,a] = (b,[a])

isnil = (\x\y.false)

nil tail = K true tail = true = \x\y.x = \f.f? such that f? = Kx. there is no such.

Church figured out how to encode integers and arithmetic operations
using lambda terms.  Here are the basics:

0 = \f\x.fx
1 = \f\x.f(fx)
2 = \f\x.f(f(fx))
3 = \f\x.f(f(f(fx)))
...

Adding two integers involves applying a special function + such that
(+ 1) 2 = 3.  Here is a term that works for +:

+ = \m\n\f\x.m(f((n f) x))

So (+ 0) 0 =
(((\m\n\f\x.m(f((n f) x))) ;+
\f\x.fx)                 ;0
\f\x.fx)                 ;0

~~>_beta targeting m for beta conversion

((\n\f\x.[\f\x.fx](f((n f) x)))
\f\x.fx)

\f\x.[\f\x.fx](f(([\f\x.fx] f) x))

\f\x.[\f\x.fx](f(fx))

\f\x.\x.[f(fx)]x

\f\x.f(fx)

let t = < y>>
let f = < n>>
let b = < f (g x)>>
let k = << \$t\$ >>
let get1 = << \$t\$ >>
let get2 = << \$f\$ >>
let id = < x>>
let w = < f f>>
let w' = < f f n>>
let pair = < theta x y>>

let zero = < z>>
let succ = < s (n s z)>>
let one = << \$succ\$ \$zero\$ >>
let two = << \$succ\$ \$one\$ >>
let three = << \$succ\$ \$two\$ >>
let four = << \$succ\$ \$three\$ >>
let five = << \$succ\$ \$four\$ >>
let six = << \$succ\$ \$five\$ >>
let seven = << \$succ\$ \$six\$ >>
let eight = << \$succ\$ \$seven\$ >>
let nine = << \$succ\$ \$eight\$ >>

(*
let pred = < n (fun u v -> v (u \$succ\$)) (\$k\$ \$zero\$) \$id\$ >>
*)
let pred = < n (fun u v -> v (u s)) (\$k\$ z) \$id\$ >>
(* ifzero n withp whenz *)
let ifzero = < n (fun u v -> v (u \$succ\$)) (\$k\$ \$zero\$) (fun n' withp
whenz -> withp n') >>

let pred' =
let iszero = << fun n -> n (fun _ -> \$f\$) \$t\$ >> in
<< fun n -> n ( fun f z' -> \$iszero\$ (f \$one\$) z' (\$succ\$ (f z')) ) (\$k\$ \$zero\$) \$zero\$ >>

(*
so n = zero ==> (k zero) zero
n = one  ==> f=(k zero) z'=zero  ==> z' i.e. zero
n = two  ==> g(g (k zero)) zero
f = g(k zero) z'=zero
f = fun z'->z'  z'=zero  ==> succ (f z') = succ(zero)
n = three ==> g(g(g (k zero))) zero
f = g(g(k zero)) z'=zero
f = fun z' -> succ(i z')  z'=zero
==> succ (f z') ==> succ(succ(z'))
*)

let pred'' =
let shift = (*  ->  *)
< d (fun d1 _ -> \$pair\$ (\$succ\$ d1) d1) >> in
< n \$shift\$ (\$pair\$ \$zero\$ \$zero\$) \$get2\$ >>

let add = < n \$succ\$ m>>
(* let add = < fun s z -> m s (n s z) >> *)
let mul = << fun m n -> n (fun z' -> \$add\$ m z') \$zero\$ >>

(* we create a pairs-list of the numbers up to m, and take the
* head of the nth tail. the tails are in the form (k tail), with
* the tail of mzero being instead (id). We unwrap the content by:
*      (k tail) tail_of_mzero
* or
*      (id) tail_of_mzero
* we let tail_of_mzero be the mzero itself, so the nth predecessor of
* zero will still be zero.
*)

let sub =
let mzero = << \$pair\$ \$zero\$ \$id\$ >> in
let msucc = << fun d -> d (fun d1 _ -> \$pair\$ (\$succ\$ d1) (\$k\$ d)) >> in
let mtail = << fun d -> d \$get2\$ d >> in (* or could use d \$get2\$ \$mzero\$ *)
< n \$mtail\$ (m \$msucc\$ \$mzero\$) \$get1\$ >>

let min' = < \$sub\$ m (\$sub\$ m n) >>
let max' = < \$add\$ n (\$sub\$ m n) >>

let lt' =
let mzero = << \$pair\$ \$zero\$ \$id\$ >> in
let msucc = << fun d -> d (fun d1 _ -> \$pair\$ (\$succ\$ d1) (\$k\$ d)) >> in
let mtail = << fun d -> d \$get2\$ d >> in (* or could use d \$get2\$ \$mzero\$ *)
< n \$mtail\$ (m \$msucc\$ \$mzero\$) \$get1\$ (fun _ -> \$t\$) \$f\$ >>

let leq' =
let mzero = << \$pair\$ \$zero\$ \$id\$ >> in
let msucc = << fun d -> d (fun d1 _ -> \$pair\$ (\$succ\$ d1) (\$k\$ d)) >> in
let mtail = << fun d -> d \$get2\$ d >> in (* or could use d \$get2\$ \$mzero\$ *)
< n \$mtail\$ (m \$msucc\$ \$mzero\$) \$get1\$ (fun _ -> \$f\$) \$t\$ >>

let eq' =
(* like leq, but now we make mzero have a self-referential tail *)
let mzero = << \$pair\$ \$zero\$ (\$k\$ (\$pair\$ \$one\$ \$id\$))  >> in
let msucc = << fun d -> d (fun d1 _ -> \$pair\$ (\$succ\$ d1) (\$k\$ d)) >> in
let mtail = << fun d -> d \$get2\$ d >> in (* or could use d \$get2\$ \$mzero\$ *)
< n \$mtail\$ (m \$msucc\$ \$mzero\$) \$get1\$ (fun _ -> \$f\$) \$t\$ >>

(*
let divmod' = << fun n d -> n
(fun f' -> f' (fun d' m' ->
\$lt'\$ (\$succ\$ m') d (\$pair\$ d' (\$succ\$ m')) (\$pair\$ (\$succ\$ d') \$zero\$)
))
(\$pair\$ \$zero\$ \$zero\$) >>
let div' = < \$divmod'\$ n d \$get1\$ >>
let mod' = < \$divmod'\$ n d \$get2\$ >>
*)

let divmod' =
let triple = << fun d1 d2 d3 -> fun sel -> sel d1 d2 d3 >> in
let mzero = << \$triple\$ \$succ\$ (\$k\$ \$zero\$) \$id\$ >> in
let msucc = << fun d -> \$triple\$ \$id\$ \$succ\$ (\$k\$ d) >> in
let mtail = (* open in dhead *)
<< fun d -> d (fun dz mz df mf drest ->
fun sel -> (drest dhead) (sel (df dz) (mf mz))) >> in
<< fun n divisor ->
( fun dhead -> n \$mtail\$ (fun sel -> dhead (sel \$zero\$ \$zero\$)) )
(divisor \$msucc\$ \$mzero\$ (fun _ _ d3 -> d3 _))
(fun dz mz _ _ _ -> \$pair\$ dz mz) >>

let div' = < \$divmod'\$ n d \$get1\$ >>
let mod' = < \$divmod'\$ n d \$get2\$ >>

(*
ISZERO = lambda n. n (lambda x. false) true,

LE =  lambda x. lambda y. ISZERO (MONUS x y),
{ ? x <= y ? }

MONUS = lambda a. lambda b. b PRED a,
{NB. assumes a >= b >= 0}

DIVMOD = lambda x. lambda y.
let rec dm = lambda q. lambda x.
if LE y x then {y <= x}
dm (SUCC q) (MONUS x y)
else pair q x
in dm ZERO x,
*)

(* f n =def. phi n_prev f_prev *)
let bernays = < n (fun d -> \$pair\$ (d (fun n_prev f_prev -> \$succ\$ n_prev)) (d phi)) (\$pair\$ \$zero\$ z) (fun n f -> f)>>

(*
let pred_b = << \$bernays\$ \$k\$ \$zero\$ >>
let fact_b = << \$bernays\$ (fun x p -> \$mul\$ (\$succ\$ x) p) \$one\$ >>

(* if m is zero, returns z; else returns withp (pred m) *)
let ifzero = < \$bernays\$ (fun x p -> withp x) z m>>
let ifzero = < m (\$k\$ (withp (\$pred\$ m))) z>>
*)

let y = < (fun u -> f (u u)) (fun u -> f (u u))>>
(* strict y-combinator from The Little Schemer, Crockford's http://www.crockford.com/javascript/little.html *)
let y' = < (fun u -> f (fun n -> u u n)) (fun u -> f (fun n -> u u n))>>
(*
let y'' = < (fun u n -> f (u u n)) (fun u n -> f (u u n))>>
*)

let turing = <<(fun u f -> f (u u f)) (fun u f -> f (u u f))>>
let turing' = <<(fun u f -> f (fun n -> u u f n)) (fun u f -> f (fun n -> u u f n))>>

let fact_w = << \$w\$ (fun f n -> \$ifzero\$ n (fun p -> \$mul\$ n (f f
p)) \$one\$)>>
let fact_w' = <<(fun f n -> f f n) (fun f n -> \$ifzero\$ n (fun p ->
\$mul\$ n (f f p)) \$one\$)>>
let fact_w'' = let u = <<(fun f n -> \$ifzero\$ n (fun p -> \$mul\$ n (f f
p)) \$one\$)>> in < \$u\$ \$u\$ n>>

let fact_y = << \$y\$ (fun f n -> \$ifzero\$ n (fun p -> \$mul\$ n (f p)) \$one\$)>>
let fact_y' = << \$y'\$ (fun f n -> \$ifzero\$ n (fun p -> \$mul\$ n (f p)) \$one\$)>>

let fact_turing = << \$turing\$ (fun f n -> \$ifzero\$ n (fun p -> \$mul\$ n (f p)) \$one\$)>>
let fact_turing' = << \$turing'\$ (fun f n -> \$ifzero\$ n (fun p -> \$mul\$ n (f p)) \$one\$)>>

let zero_ = < z>>;;
let succ_ = < s m (m s z)>>;;
let one_ = << \$succ_\$ \$zero_\$ >>;;
let two_ = << \$succ_\$ \$one_\$ >>;;
let three_ = << \$succ_\$ \$two_\$ >>;;
let four_ = << \$succ_\$ \$three_\$ >>;;
let five_ = << \$succ_\$ \$four_\$ >>;;
let six_ = << \$succ_\$ \$five_\$ >>;;
let seven_ = << \$succ_\$ \$six_\$ >>;;
let eight_ = << \$succ_\$ \$seven_\$ >>;;
let nine_ = << \$succ_\$ \$eight_\$ >>;;

let pred_ = < n (fun n' _ -> n') \$zero_\$ >>
let add_ = < n (fun _ f' -> \$succ_\$ f') m>>
let mul_ = < n (fun _ f' -> \$add_\$ m f') \$zero_\$ >>
(* let pow_ = *)

let sub_ = < n (fun _ f' -> \$pred_\$ f') m>>
let min_ = < \$sub_\$ m (\$sub_\$ m n)>>  (* m-max(m-n,0) = m+min(n-m,0) = min(n,m) *)
let max_ = < \$add_\$ n (\$sub_\$ m n)>>  (* n+max(m-n,0) = max(m,n) *)

let eq_ = < m (fun _ fm' n -> n (fun n' _ -> fm' n') \$f\$) (fun n -> n (fun _ _ -> \$f\$) \$t\$)>>
let lt_ = < (\$sub_\$ n m) (fun _ _ -> \$t\$) \$f\$ >>
let leq_ = << fun m n -> (\$sub_\$ m n) (fun _ _ -> \$f\$) \$t\$ >>

let divmod_ = << fun n d -> n
(fun _ f' -> f' (fun d' m' ->
\$lt_\$ (\$succ_\$ m') d (\$pair\$ d' (\$succ_\$ m')) (\$pair\$ (\$succ_\$ d') \$zero_\$)
))
(\$pair\$ \$zero_\$ \$zero_\$) >>
let div_ = < \$divmod_\$ n d \$get1\$ >>
let mod_ = < \$divmod_\$ n d \$get2\$ >>

```