(* Church Numerals *) val zero = fn f => fn x => x; val succ = fn n => fn f => fn x => (f ((n f) x)); val add = fn m => fn n => fn f => fn x => ((((m succ) n) f) x); val mult = fn f => fn g => fn x => (f (g x)); val power = fn f => fn g => (f g); (* Church Numerals *) val one = (succ zero); val two = (succ one); val inc = fn n => n+1; (* More Church Numerals *) val four = (add one (add one (add one (add one zero)))); val three = ((add one) two); val five = ((add three) two); val six = ((mult three) two); val nine = ((power two) three); val ten = ((mult two) five); (* A test to show what a Church Numeral does *) ((zero inc) 0); ((five inc) 0); ((ten inc) 0); val first = fn x => fn y => x; val second = fn x => fn y => y; val third = fn x => fn y => fn z => z; val iszero = fn n => ((n third) first); (* Predicate, is a Church Numeral zero? *) val pair = fn x => fn y => fn f => ((f x) y); val prefn = fn f => fn p => ((pair (f (p first))) (p first)); val pred = fn n => fn f => fn x => (((n (prefn f))(pair x x)) second); (* predecessor function *) val eight = (pred nine);