| id: |
λx. x |
| true: |
λt. λf. t |
| false: |
λt. λf. f |
| Y: |
λf. (λx. f (x x)) (λx. f (x x)) |
| n: |
Church-Numeral n (e.g. 0 = λs. λz. z, 1 = λs. λz. s z) |
| succ: |
λn. λs. λz. s (n s z) |
| pred: |
λn. λs. λz. n (λg. λh. h (g s)) (λu. z) (λu. u) |
| plus: |
λm. λn. λf. λx. m f (n f x) |
| minus: |
λm. λn. (n pred) m |
| mult: |
λm. λn. λf. m (n f) |
| isZero: |
λn. n (λx. false) true |
| leq: |
λm. λn. isZero (minus m n) |
| lt: |
λn. λm. leq n m (leq m n false true) false) |
| divides: |
λn. λm. Y (λdivides. λa. λb. isZero b true (lt b a false (divides a (minus b a)))) n m |
| isPrime: |
λn. isZero (pred n) false (Y (λisPrimeUpTo. λn. λacc. isZero (pred acc) true (divides acc n false (isPrimeUpTo n (pred acc)))) n (pred n)) |