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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
