I := λx.x
0 := λf.λx.x
1 := λf.λx.f x
TRUE := λx.λy.x
FALSE := λx.λy.y
PRED := λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u)
ISZERO := λn.n (λx.FALSE) TRUE
The identity function λx.x
is Eta equivalent to church numeral 1 λf.λx.f x
. The Fn below will return FALSE
for any function that does not evaluate to a church numeral zero (λf.λx.x
) after being passed through the predicate function.
λx.(ISZERO (PRED x)) TRUE FALSE
There may exist a function BAD that behaves as such:
λx.(ISZERO (PRED x)) TRUE FALSE BAD := TRUE
BAD != I