-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$ >>