Luke, sorry for being offtopic, but you are more and more intriguing me with topology. I wonder if any stuff from it has, apart from applications in computability/complexity, also computational applications as useful as monoids or rings do (i.e. parallel prefix sums).
2009/2/3 Luke Palmer <lrpal...@gmail.com>: > On Mon, Feb 2, 2009 at 4:18 PM, Reid Barton <rwbar...@math.harvard.edu> > wrote: >> >> > So here's a programming challenge: write a total function (expecting >> > total arguments) toSame :: ((Nat -> Bool) -> Nat) -> (Nat -> Bool,Nat >> > -> Bool) that finds a pair that get mapped to the same Nat. >> > >> > Ie. f a==f b where (a,b) = toSame f >> >> (Warning: sketchy argument ahead.) Let f :: (Nat -> Bool) -> Nat be a >> total function and let g0 = const True. The application f g0 can >> only evaluate g0 at finitely many values, so f g0 = f (< k) for any k >> larger than all these values. So we can write >> >> > toSame f = (const True, head [ (< k) | k <- [1..], f (const True) == f >> > (< k) ]) >> >> and toSame is total on total inputs. > > 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). > > I guess I should hold off on conjecturing the impossibility of things... :-) > > Luke > > > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe