I am using the following definitions in the notation of Haskell. In case it matters, I would like to use only the $\alpha,\beta,\eta$ reductions rather than the Haskell evaluation rules.
-- boolean constants true = \x y -> x false = \x y -> y -- 0 and increment (successor) zero = \f x -> x inc n = \f x -> f (n f x) -- IS THIS iszero SOUND AND COMPLETE? iszero = \n -> n (\x -> false) true
It seems to me that
iszero needs to check if two functions are identical. Since the equivalence of two arbitrary Turing Machines are undecidable, I am wondering if the it really works. In particular,
- Soundness: are all functions for which
- Completeness: for any arbitrary function $f$, can
iszerocorrectly determine if $f$ is equal