(* Definitions *) let church n = lam_list 2 (iter (fun t -> App(Rel 1,t)) (Rel 0) n);; let succ = lam_list 3 (App(Rel 1, bin_app (Rel 2) (Rel 1) (Rel 0)));; let plus = lam_list 4 (bin_app (Rel 3) (Rel 1) (bin_app (Rel 2) (Rel 1) (Rel 0)));; let mult = lam_list 4 (bin_app (Rel 3) (App(Rel 2, Rel 1)) (Rel 0));; let pair x y = Lam (bin_app (Rel 0) (lift 1 0 x) (lift 1 0 y));; let fst = Lam (App(Rel 0, lam_list 2 (Rel 1)));; let snd = Lam (App(Rel 0, lam_list 2 (Rel 0)));; let mkfst p = App(fst,p);; let mksnd p = App(snd,p);; let pred = Lam (mksnd(bin_app (Rel 0) (Lam (pair (App(succ, mkfst (Rel 0))) (mkfst (Rel 0)))) (pair (church 0) (church 0)))) ;; (* cbv *) let pred' = Lam (mksnd(bin_app (Rel 0) (Lam (App (Lam (pair (App(succ, Rel 0)) (Rel 0)), mkfst (Rel 0)))) (pair (church 0) (church 0)))) ;; (* Test functions *) let tplus f m n = f (bin_app plus (church m) (church n));; let tmult f m n = f (bin_app mult (church m) (church n));; let tpred f n = f (App(pred, church n));; let zero n = bin_app (church n) pred (church n);; let zero' n = bin_app (church n) pred' (church n);; let ident n = bin_app (church n) pred (bin_app plus (church n) (church n));; let tuple k = Lam (bin_app (church k) (Lam (pair (Rel 0) (Rel 1))) (Rel 0));; let ttu f k n = f (App(tuple k, zero n));; let ttu' f k n = f (App(tuple k, ident n));;