# Is iszero of the untyped lambda calculus sound and complete? [closed]

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,

1. Soundness: are all functions for which iszero returns true really zero?
2. Completeness: for any arbitrary function $f$, can iszero correctly determine if $f$ is equal zero?

No, iszero does not have to test whether two functions are equal. It only has to detect a difference between them, i.e., extract enough information to tell whether the given function represents a 0 or not.

You could ask the same question about equality testing. It is possible to implement an equality test eq for numbers (exercise, but implement predecessor first). Isn't it the case that eq is comparing functions for equality? No. First of all, eq does not compare arbitrary functions but only those that happen to encode numbers. Second, even when comparing two function n and m that encode numbers, it does not answer the question "are n and m equal function?" but rather "do n and m encode the same number?" These are two different questions.

• That sounds kinda tricky and reminds me of the metaphors in GEB by Hofstadter. Yet I am still confused. Aren't difference and equality the same (or exactly opposite, like the complement set) thing? Or put differently, is the difference-detection of iszero sound and complete? – wlnirvana Mar 16 '17 at 8:06
• @Andrej is perfectly right (of course). I have the feeling that you are still confused because you are somehow looking at $\lambda$-terms in the wrong way (I don't understand exactly how though). If I answered that $\mathtt{ifzero}$ is neither sound nor complete according to your notion of soundness or completeness (in which I understand "being $\mathtt{zero}$" and "being equal to $\mathtt{zero}$" as both meaning syntactic equality), would that make things clearer? – Damiano Mazza Mar 16 '17 at 12:14
• By the way, I still think your questions are better suited for CS StackExchange (i.e., they are not research-level). – Damiano Mazza Mar 16 '17 at 12:15
• Oh my, I never noticed this was cstheory. Yes, these questions are from a beginner who does not understand the basic concepts (there's nothing wrong with being a beginner and asking questions, but in an appropriate forum). They belong to cs.stackexchange.com. – Andrej Bauer Mar 16 '17 at 20:43
• @DamianoMazza Sorry I didn't know there are two separate forums for theoretical questions. Your comment is indeed helpful. I guess my understanding for "equality" is somewhat vague as well. – wlnirvana Mar 18 '17 at 3:09
1. The iszero function is sound, in the sense that it returns true only for functions which are $\beta\eta$ equal to the $\bf{zero}$ function.

2. The iszero function is only complete modulo termination: there is no finite method to determine for an arbitrary f whether iszero f is going to return true, false or simply run forever. This is where undecidability rears its head. However if it returns false, then (by Böhm's theorem) f is not $\beta\eta$ equal to $\bf{zero}$.

• Sorry @cody, I think point 1 is wrong: take $M:=\lambda x.\lambda y.\mathtt{true}$. Then $M\not\simeq_{\beta\eta}\mathtt{zero}$ and yet $\mathtt{iszero}\,M\to^\ast\mathtt{true}$. Like I said in my comment above, $\mathtt{iszero}$ is neither sound nor complete, whatever meaning one gives to "being equal to" in the OP's definition of "sound and complete". Am I missing something? – Damiano Mazza Mar 17 '17 at 9:29
• Also, when you write "it returns zero only for functions which are $\beta\eta$ equal to the $\mathbf{zero}$ function", I think you mean "it returns true". Right? – Damiano Mazza Mar 17 '17 at 9:31