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

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

CC BY-SA 3.0
2017-03-16T08:06:32.860Z
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
CC BY-SA 3.0
2017-03-16T12:14:14.213Z
@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
CC BY-SA 3.0
2017-03-16T12:15:29.977Z
By the way, I still think your questions are better suited for [CS StackExchange](http://cs.stackexchange.com/) (i.e., they are *not* research-level).
Damiano Mazza
CC BY-SA 3.0
2017-03-16T20:43:57.817Z
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
CC BY-SA 3.0
2017-03-18T03:09:29.300Z
@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
CC BY-SA 3.0
2017-03-18T08:33:09.293Z
No problem, I'm glad it was helpful.  However, I wanto to make sure you got the main message of Andrej's answer: asking whether `iszero` is "sound" and/or "complete" (according to your definition) is not a good question. `iszero` correctly implements test for zero for the representation of integers you gave; the failure of the properties you mention (which you'll never have in the pure $\lambda$-calculus) is irrelevant.
Damiano Mazza
CC BY-SA 3.0
2017-03-16T07:27:59.913Z
2017-03-16T07:27:59.913Z
Andrej Bauer
<ol>
<li><p>The <code>iszero</code> function is sound, in the sense that it returns <code>true</code> only for functions which are $\beta\eta$ equal to the $\bf{zero}$ function.</p></li>
<li><p>The <code>iszero</code> function is only complete <strong>modulo termination</strong>: there is no <strong>finite</strong> method to determine for an arbitrary <code>f</code> whether <code>iszero f</code> is going to return <code>true</code>, <code>false</code> or simply run forever. This is where undecidability rears its head. However <em>if</em> it returns <strong>false</strong>, then (by Böhm's theorem) <code>f</code> is not $\beta\eta$ equal to $\bf{zero}$.</p></li>
</ol>

CC BY-SA 3.0
2017-03-17T09:29:22.073Z
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
CC BY-SA 3.0
2017-03-17T09:31:27.673Z
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
CC BY-SA 3.0
2017-03-16T13:21:32.537Z
2017-03-18T14:56:37.453Z
2017-03-18T14:56:37.453Z
cody
<p>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.</p>

<pre><code>-- boolean constants
true = \x y -&gt; x
false = \x y -&gt; y

-- 0 and increment (successor)
zero = \f x -&gt; x
inc n = \f x -&gt; f (n f x)

-- IS THIS iszero SOUND AND COMPLETE?
iszero = \n -&gt; n (\x -&gt; false) true
</code></pre>

<p>It seems to me that <code>iszero</code> 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,</p>

<ol>
<li>Soundness: are all functions for which <code>iszero</code> returns <code>true</code> really <code>zero</code>?</li>
<li>Completeness: for any arbitrary function $f$, can <code>iszero</code> correctly determine if $f$ is equal <code>zero</code>?</li>
</ol>

<lambda-calculus><turing-machines><reductions><equivalence>
Is iszero of the untyped lambda calculus sound and complete?
wlnirvana
# Is iszero of the untyped lambda calculus sound and complete?

(Asked by: username_0 on 2017-03-16)

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 iszero returns true really zero?
Completeness: for any arbitrary function $f$, can iszero correctly determine if $f$ is equal zero?

**Tags:** lambda-calculus, turing-machines, reductions, equivalence

---

## 2 answers

### Answer by username_1 on 2017-03-16. Score: 7 | Accepted answer

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.

> **Comments:**
> **username_0**: 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?  
> **username_2**: @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?  
> **username_2**: By the way, I still think your questions are better suited for [CS StackExchange](http://cs.stackexchange.com/) (i.e., they are *not* research-level).  
> **username_1**: 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.  
> **username_0**: @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.  
> **username_2**: No problem, I'm glad it was helpful.  However, I wanto to make sure you got the main message of Andrej's answer: asking whether `iszero` is "sound" and/or "complete" (according to your definition) is not a good question. `iszero` correctly implements test for zero for the representation of integers you gave; the failure of the properties you mention (which you'll never have in the pure $\lambda$-calculus) is irrelevant.  

---

### Answer by username_3 on 2017-03-16. Score: 3

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}$.

> **Comments:**
> **username_2**: 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?  
> **username_2**: 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?  

---

