[Haskell-cafe] is proof by testing possible?

[Conor McBride]

On 10 Nov 2009, at 05:52, Curt Sampson wrote:

> On 2009-11-09 14:22 -0800 (Mon), muad wrote:
>
>>> Proof: True for n = 0, 1, 2, 3, 4 (check!), hence true for all n.  
>>> QED.
>>> ...
>
> Actually, the test is that it's true for 0 through 4 is not sufficient
> for a proof;

It's enough testing...

> you also need to prove in some way that you need do no
> further tests.

...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.)

> Showing that particular point in this case appears to me
> to lie outside the realm of testing.

You need to appeal to a general theorem about expressions
of a particular form, but if that theorem is in the
library, the only work you need do is to put the
expressions in that form. This is sometimes described
as the "reflective" proof method: express problem in
language capturing decidable fragment; hit with big stick.

There are lots of other examples of this phenomenon. The
zero-one principle for sorting networks is a favourite of
mine. I'm sure there's more to be found here. It smells
a bit of theorems for free: the strength comes from
knowing what you don't.

All the best

Conor