[Haskell-cafe] Re: is proof by testing possible?

[Ben Franksen]

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