Hi,

Am Montag, den 02.02.2009, 11:06 -0700 schrieb Luke Palmer:

> That question has kind of a crazy answer.
>
> In mathematics, Nat -> Bool is uncountable, i.e. there is no function
> Nat -> (Nat -> Bool) which has every function in its range.
>
> But we know we are dealing with computable functions, so we can just
> enumerate all implementations. So the computable functions Nat ->
> Bool are countable.
>
> However! If we have a function f : Nat -> Nat -> Bool, we can
> construct the diagonalization g : Nat -> Bool as: g n = not (f n n),
> with g not in the range of f. That makes Nat -> Bool "computably
> uncountable".

That argument has a flaw. Just because we have a function in the
mathematical sense that sends ℕ to (Nat -> Bool) does not mean that we
have Haskell function f of that type that we can use to construct g.

What argument? What was I trying to prove?

But I admit that my notation is confusing; I am not distinguishing between Haskell types and their denotations. I'll be more precise:

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 total computable function in Haskell.

N -> 2 is uncountable, meaning there is no surjection N -> (N -> 2).

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.

But Nat ~> Bool is computably uncountable, meaning there is no injective function Nat ~> (Nat ~> Bool), by the diagonal argument above.

That's what I meant.

Luke