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
