[Haskell-cafe] is proof by testing possible?
Dan Piponi
dpiponi at gmail.com
Mon Oct 12 14:00:03 EDT 2009
On Mon, Oct 12, 2009 at 10:42 AM, muad <muad.dib.space at gmail.com> wrote:
>
> Is it possible to prove correctness of a functions by testing it? I think the
> tests would have to be constructed by inspecting the shape of the function
> definition.
not True==False
not False==True
Done. Tested :-)
Less trivially, consider a function of signature
swap :: (a,b) -> (b,a)
We don't need to test it at all, it can only do one thing, swap its
arguments. (Assuming it terminates.)
But consider:
swap :: (a,a) -> (a,a)
If I find that swap (1,2) == (2,1) then I know that swap (x,y)==(y,x)
for all types a and b. We only need one test.
The reason is that we have a free theorem that says that for all
functions, f, of type (a,a) -> (a,a) this holds:
f (g a,g b) == let (x,y) = f (a,b) in (g x',g y')
For any x and y define
g 1 = x
g 2 = y
Then f(x,y) == f (g 1,g 2) == let (x',y') == f(1,2) in (g x',g y') ==
let (x',y') == (2,1) in (g x',g y') == (g 2,g 1) == (y,x)
In other words, free theorems can turn an infinite amount of testing
into a finite test. (Assuming termination.)
--
Dan
More information about the Haskell-Cafe
mailing list