[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