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

Joe Fredette jfredett at gmail.com
Mon Oct 12 15:33:26 EDT 2009

```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
>
> _______________________________________________