That has got to be the single awesomest thing I have ever seen ever... The first time I tried to read through the "Seemingly Impossible Functional Programs" post, I understood none of it. Now it seems obviously. I Love Math... Thanks for the explanation! /Joe On Oct 12, 2009, at 3:22 PM, Ben Franksen wrote:
Joe Fredette wrote:
Really? How? That sounds very interesting, I've got a fair knowledge of basic topology, I'd love to see an application to programming...
Compactness is one of the most powerful concepts in mathematics, because on the one hand it makes it possible to reduce many infinite problems to finite ones (inherent in its definition: for every open cover there is a finite subcover), on the other hand it is often easy to prove compactness due to Tychonoff's theorem (any product of compact spaces is compact). The connection to computing science is very nicely explained in
http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/
I found this paragraph particularly enlightening:
"""
modulus :: (Cantor -> Integer) -> Natural modulus f = least(\n -> forevery(\a -> forevery(\b -> eq n a b --> (f a == f b))))
This [...] finds the modulus of uniform continuity, defined as the least natural number `n` such that `forall alpha,beta. alpha =_n beta implies f(alpha)=f(beta),` where `alpha =_n beta iff forall i< n. alpha_i = beta_i.`
What is going on here is that computable functionals are continuous, which amounts to saying that finite amounts of the output depend only on finite amounts of the input. But the Cantor space is compact, and in analysis and topology there is a theorem that says that continuous functions defined on a compact space are uniformly continuous. In this context, this amounts to the existence of a single `n` such that for all inputs it is enough to look at depth `n` to get the answer (which in this case is always finite, because it is an integer). """
Cheers
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe