ChurchNumerals.ml

(* church booleans *)
fun True x y = x;
fun False x y = y;

(*conditionals*)
fun If b x y = b x y;
fun Or b1 b2 x y	= b1 x (b2 x y);
fun Xor b1 b2 x y	= b1 (b2 y x) (b2 x y);
fun And b1 b2 x y	= b1 (b2 x y) y;
fun Nand b1 b2 x y	= b1 (b2 y x) x;
fun Not b x y		= b y x;

(* church numerals *)
fun Zero f x = x;
fun One f x = f x;
fun Two f x = f (f x);

fun Succ n f x = f (n f x);
fun Add m n f x = m f (n f x);
fun Multiply m n f x = m (n f) x;
fun Exp m n f x = n m f x;
(* swap them or we end up doing n^m *)

fun IsZero n = n (fn(x) => False) True;

(* predecessor and subtraction, translated from lamba notation in IB notes *)
fun Pair x y f = f x y;
fun First p = p True;
fun Second p = p False;

fun Prefn f p = Pair(f(First p)) (First p);
fun Pre n f x = Second(n(Prefn f)(Pair x x));

fun Sub m n = n Pre m;

(* nicer predecessor using normal pairs based on above *)
fun Prefn2 f (a,b) = (b,f b);
fun Pre2 n f x = 
let
	val (a,b) = (n (Prefn2 f) (x,x))
in
	a
end;

(* conversion  of numbers *)
fun Churchify 0 f x = x
  | Churchify n f x = f(Churchify (n-1) f x);
fun DeChurchify n = n (fn(x) => x+1) 0;

(* conversion of booleans *)
fun ChurchifyBool true = True;
  | ChurchifyBool false = False
fun DeChurchifyBool n = n true false;