2009/2/2 Joachim Breitner <m...@joachim-breitner.de>
> 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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
