pred.ml

(* このプログラムの本質的なアイディアは、塚田武志先生にご教示頂きました *)

let succ n s z = s (n s z)

let pred n s z =
  let r = ref true in
  let s' m =
    if !r then (r := false; m)
    else s m
  in n s' z

let church_to_num n = n (fun x -> x + 1) 0
let rec num_to_church x =
  if x = 0 then (fun s -> fun z -> z)
  else succ (num_to_church (x - 1))

let apply f x =	church_to_num (f (num_to_church	x))

(* Example *)
(* apply pred 3 ==> 2 *)
(* apply pred 0 ==> 0 *)