[Haskell-cafe] Re: is proof by testing possible?
apfelmus at quantentunnel.de
Tue Nov 10 05:46:08 EST 2009
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
sum . map (^3) $ [1..n] = (sum $ [1..n])^2
in the first place. But once proven, the former can be reused ad libitum.
More information about the Haskell-Cafe