[Haskell-cafe] Re: is proof by testing possible?
Heinrich Apfelmus
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
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
More information about the Haskell-Cafe
mailing list