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

[Joe Fredette]

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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe