On Mon, Feb 2, 2009 at 4:18 PM, Reid Barton <span dir="ltr">&lt;<a href="mailto:rwbarton@math.harvard.edu">rwbarton@math.harvard.edu</a>&gt;</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">&gt; So here&#39;s a programming challenge: write a total function (expecting<br>
&gt; total arguments) toSame :: ((Nat -&gt; Bool) -&gt; Nat) -&gt; (Nat -&gt; Bool,Nat<br>
&gt; -&gt; Bool) that finds a pair that get mapped to the same Nat.<br>
&gt;<br>
&gt; Ie. f a==f b where (a,b) = toSame f<br>
<br>
</div>(Warning: sketchy argument ahead.) &nbsp;Let f :: (Nat -&gt; Bool) -&gt; Nat be a<br>
total function and let g0 = const True. &nbsp;The application f g0 can<br>
only evaluate g0 at finitely many values, so f g0 = f (&lt; k) for any k<br>
larger than all these values. &nbsp;So we can write<br>
<br>
&gt; toSame f = (const True, head [ (&lt; k) | k &lt;- [1..], f (const True) == f (&lt; k) ])<br>
<br>
and toSame is total on total inputs.</blockquote><div><br>Well done!&nbsp; That&#39;s not sketchy at all!&nbsp; There is always such a k (when the result type of f has decidable equality) and it is the &quot;modulus of uniform continuity&quot; of f.&nbsp; This is computable directly, but the implementation you&#39;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>