[Haskell-cafe] Re: is proof by testing possible?
Conor McBride wrote: and you can calculate how much testing is enough by computing an upper bound on the polynomial degree of the expression. (The summation operator increments degree, the difference operator decreases it, like in calculus.) This is sometimes described as the reflective proof method: express problem in language capturing decidable fragment; hit with big stick. The fact that summation maps polynomials to polynomials needs to be proven, of course, and I guess that this proof is not much simpler than proving sum . map (^3) $ [1..n] = (sum $ [1..n])^2 in the first place. But once proven, the former can be reused ad libitum. Regards, apfelmus -- http://apfelmus.nfshost.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: is proof by testing possible?
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
Re: [Haskell-cafe] Re: is proof by testing possible?
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
