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

[Heinrich Apfelmus]

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