On Mon, Feb 2, 2009 at 3:41 PM, Dan Piponi <span dir="ltr"><<a href="mailto:dpiponi@gmail.com">dpiponi@gmail.com</a>></span> wrote:<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;">
<div class="Ih2E3d">2009/2/2 Luke Palmer <<a href="mailto:lrpalmer@gmail.com">lrpalmer@gmail.com</a>>:<br>
<br>
</div>> But Nat ~> Bool is computably uncountable, meaning there is no injective (surjective?)<br>
<div class="Ih2E3d">> function Nat ~> (Nat ~> Bool), by the diagonal argument above.<br>
<br>
</div>Given that the Haskell functions Nat -> Bool are computably<br>
uncountable, you'd expect that for any Haskell function (Nat -> Bool)<br>
-> Nat there'd always be two elements that get mapped to the same<br>
value.<br>
<br>
So here's a programming challenge: write a total function (expecting<br>
total arguments) toSame :: ((Nat -> Bool) -> Nat) -> (Nat -> Bool,Nat<br>
-> Bool) that finds a pair that get mapped to the same Nat.<br>
<br>
Ie. f a==f b where (a,b) = toSame f</blockquote><div><br>Presumably under the condition that a /= b.<br><br>It's unlikely that you can. At least you can't use Escardo's trick, because while the space of pairs of cantor spaces (cantor space = Nat -> Bool) is compact, the space of pairs of <i>different</i> cantors spaces is not. This is witnessed by the following function:<br>
<br>f (a,b) = length (takeWhile id (zipWith (==) a b))<br><br>This function finds the first index at which they differ. Since they are guaranteed to be different, this function is total. Thus, if the space of nonequal cantor spaces were compact, then so too would be Nat, which we know is not the case.<br>
<br>Luke<br></div></div><br>