2009/2/2 Joachim Breitner
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