+
+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 = <<fun y _ -> y>>
+let f = <<fun _ n -> n>>
+let b = <<fun f g x -> f (g x)>>
+let k = << $t$ >>
+let get1 = << $t$ >>
+let get2 = << $f$ >>
+let id = <<fun x -> x>>
+let w = <<fun f -> f f>>
+let w' = <<fun f n -> f f n>>
+let pair = <<fun x y theta -> theta x y>>
+
+let zero = <<fun s z -> z>>
+let succ = <<fun n s z -> 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 = <<fun n -> n (fun u v -> v (u $succ$)) ($k$ $zero$) $id$ >>
+*)
+let pred = <<fun n s z -> n (fun u v -> v (u s)) ($k$ z) $id$ >>
+(* ifzero n withp whenz *)
+let ifzero = <<fun n -> 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 = (* <n,_> -> <n+1,n> *)
+ <<fun d -> d (fun d1 _ -> $pair$ ($succ$ d1) d1) >> in
+ <<fun n -> n $shift$ ($pair$ $zero$ $zero$) $get2$ >>
+
+
+
+let add = <<fun m n -> n $succ$ m>>
+(* let add = <<fun m n -> 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$ *)
+ <<fun m n -> n $mtail$ (m $msucc$ $mzero$) $get1$ >>
+
+let min' = <<fun m n -> $sub$ m ($sub$ m n) >>
+let max' = <<fun m n -> $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$ *)
+ <<fun n m -> 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$ *)
+ <<fun m n -> 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$ *)
+ <<fun m n -> 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' = <<fun n d -> $divmod'$ n d $get1$ >>
+let mod' = <<fun n d -> $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' = <<fun n d -> $divmod'$ n d $get1$ >>
+let mod' = <<fun n d -> $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 = <<fun phi z n -> 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 = <<fun z withp m -> $bernays$ (fun x p -> withp x) z m>>
+let ifzero = <<fun z withp m -> m ($k$ (withp ($pred$ m))) z>>
+*)
+
+let y = <<fun f -> (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 f -> (fun u -> f (fun n -> u u n)) (fun u -> f (fun n -> u u n))>>
+(*
+let y'' = <<fun f -> (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 <<fun n -> $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_ = <<fun s z -> z>>;;
+let succ_ = <<fun m s z -> 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_ = <<fun n -> n (fun n' _ -> n') $zero_$ >>
+let add_ = <<fun m n -> n (fun _ f' -> $succ_$ f') m>>
+let mul_ = <<fun m n -> n (fun _ f' -> $add_$ m f') $zero_$ >>
+(* let pow_ = *)
+
+let sub_ = <<fun m n -> n (fun _ f' -> $pred_$ f') m>>
+let min_ = <<fun m n -> $sub_$ m ($sub_$ m n)>> (* m-max(m-n,0) = m+min(n-m,0) = min(n,m) *)
+let max_ = <<fun m n -> $add_$ n ($sub_$ m n)>> (* n+max(m-n,0) = max(m,n) *)
+
+let eq_ = <<fun m -> m (fun _ fm' n -> n (fun n' _ -> fm' n') $f$) (fun n -> n (fun _ _ -> $f$) $t$)>>
+let lt_ = <<fun m n -> ($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_ = <<fun n d -> $divmod_$ n d $get1$ >>
+let mod_ = <<fun n d -> $divmod_$ n d $get2$ >>
+