JavaScript λ-term Evaluator
K = \x.\y. x. S = \x y z. x z (y z). I = \x. x. Ω = (\x. x x) (\x. x x). Y = \f. (\x. f (x x)) (\x. f (x x)). succ = \n s z. s (n s z). add = \n m. \s z. n s (m s z). mul = \n m. \s z. n (m s) z. true = \x y. x. false = \x y. y. pair = \x y k. k x y. fst = \p. p true. snd = \p. p false. pred = \n s z. fst (n (\p. p (\x y k. k y (s y))) (\k. k z z)). sub = \n m. m pred n. iszero = \n. n (\x. false) true. sum = Y (\f n. iszero n 0 (add n (f (pred n)))). sum' = \n. n (\p. p (\x y k. k (succ x) (add (succ x) y))) (\k. k 0 0) false. sum'' = \n s z. n (\p. p (\x y k. k (\z. s (x z)) (s (x y)))) (\k. k I z) false.