2009/2/2 Joachim Breitner <span dir="ltr"><<a href="mailto:mail@joachim-breitner.de">mail@joachim-breitner.de</a>></span><br><div class="gmail_quote"><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
Hi,<br>
<br>
Am Montag, den 02.02.2009, 11:06 -0700 schrieb Luke Palmer:<br>
<div class="Ih2E3d"><br>
> That question has kind of a crazy answer.<br>
><br>
> In mathematics, Nat -> Bool is uncountable, i.e. there is no function<br>
> Nat -> (Nat -> Bool) which has every function in its range.<br>
><br>
> But we know we are dealing with computable functions, so we can just<br>
> enumerate all implementations. So the computable functions Nat -><br>
> Bool are countable.<br>
><br>
> However! If we have a function f : Nat -> Nat -> Bool, we can<br>
> construct the diagonalization g : Nat -> Bool as: g n = not (f n n),<br>
> with g not in the range of f. That makes Nat -> Bool "computably<br>
> uncountable".<br>
<br>
</div>That argument has a flaw. Just because we have a function in the<br>
mathematical sense that sends ℕ to (Nat -> Bool) does not mean that we<br>
have Haskell function f of that type that we can use to construct g.</blockquote><div><br>What argument? What was I trying to prove?<br><br>But I admit that my notation is confusing; I am not distinguishing between Haskell types and their denotations. I'll be more precise:<br>
<br>I will use N for the set of naturals, Nat for the Haskell type of (strict) naturals, 2 for the set {0,1}, Bool for the Haskell type True|False, (->) for a mathematical function, (~>) for a <i>total</i> computable function in Haskell.<br>
<br>N -> 2 is uncountable, meaning there is no surjection N -> (N -> 2).<br><br>Nat ~> Bool is countable, meaning there is a surjection N -> (Nat ~> Bool). Enumerate all program source codes (which is countable, so N -> SourceCode), and pick out the ones which denote a total computable function Nat ~> Bool.<br>
<br>But Nat ~> Bool is <i>computably</i> uncountable, meaning there is no injective function Nat ~> (Nat ~> Bool), by the diagonal argument above.<br><br>That's what I meant.<br><br>Luke<br></div></div>