1
$\begingroup$

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?
Improve this question
$\endgroup$

2 Answers 2

Reset to default
7
$\begingroup$

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.

Improve this answer
$\endgroup$
6
  • $\begingroup$ 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? $\endgroup$
    – wlnirvana
    Mar 16, 2017 at 8:06
  • $\begingroup$ @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? $\endgroup$
    – Damiano Mazza
    Mar 16, 2017 at 12:14
  • 5
    $\begingroup$ By the way, I still think your questions are better suited for CS StackExchange (i.e., they are not research-level). $\endgroup$
    – Damiano Mazza
    Mar 16, 2017 at 12:15
  • $\begingroup$ 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. $\endgroup$
    – Andrej Bauer
    Mar 16, 2017 at 20:43
  • $\begingroup$ @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. $\endgroup$
    – wlnirvana
    Mar 18, 2017 at 3:09
3
$\begingroup$

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

Improve this answer
$\endgroup$
2
  • 1
    $\begingroup$ 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? $\endgroup$
    – Damiano Mazza
    Mar 17, 2017 at 9:29
  • $\begingroup$ 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? $\endgroup$
    – Damiano Mazza
    Mar 17, 2017 at 9:31

Not the answer you're looking for? Browse other questions tagged or ask your own question.