On Mon, Feb 2, 2009 at 4:18 PM, Reid Barton <span dir="ltr"><<a href="mailto:rwbarton@math.harvard.edu">rwbarton@math.harvard.edu</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">> 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<br>
<br>
</div>(Warning: sketchy argument ahead.) Let f :: (Nat -> Bool) -> Nat be a<br>
total function and let g0 = const True. The application f g0 can<br>
only evaluate g0 at finitely many values, so f g0 = f (< k) for any k<br>
larger than all these values. So we can write<br>
<br>
> toSame f = (const True, head [ (< k) | k <- [1..], f (const True) == f (< k) ])<br>
<br>
and toSame is total on total inputs.</blockquote><div><br>Well done! That's not sketchy at all! There is always such a k (when the result type of f has decidable equality) and it is the "modulus of uniform continuity" of f. This is computable directly, but the implementation you've provided might come up with a smaller one that still works (since you only need to differentiate between const True, not all other streams).<br>
<br>I guess I should hold off on conjecturing the impossibility of things... :-)<br><br>Luke<br></div></div><br>