[Haskell-cafe] Re: type metaphysics
benjovi at gmx.net
Mon Feb 2 18:55:08 EST 2009
Ryan Ingram schrieb:
> 2009/2/2 Luke Palmer <lrpalmer at gmail.com>:
>> 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".
> This is making my head explode. How is g not in the range of f?
> In particular, f is a program, which I can easily implement; given:
f is 'easy to implement' if it enumerates all functions, not just total
ones. Otherwise, f is hard to implement ;)
In the first case, if we have (f n n) = _|_, then g n = not (f n n) =
_|_ as well, so the diagonalization argument does not hold anymore.
But I do agree that proofs by contradiction do not map well to haskell ...
> compiler :: String -> Maybe (Nat -> Bool)
> mkAllStrings :: () -> [String] -- enumerates all possible strings
> I can write f as
> f n = validPrograms () !! n
> validPrograms = map fromJust . filter isJust . map compiler . mkAllStrings
> Now, in particular, mkAllStrings will generate the following string at
> some index, call it "stringIndexOfG":
> <source code for compiler>
> <source code for mkAllStrings>
> <source code for f>
> g n = not (f n n)
> This is a valid program, so the compiler will compile it successfully,
> and therefore there is some index "validProgramIndexOfG" less than or
> equal to "stringIndexOfG" which generates this program.
> But your argument seems to hold as well, so where is the contradiction?
> -- ryan
More information about the Haskell-Cafe