[Haskell-cafe] is proof by testing possible?

[Joe Fredette]

I completely forgot about free theorems! Do you have some links to  
resources -- I tried learning about them a while
ago, but couldn't get a grasp on them... Thanks.

/Joe



On Oct 12, 2009, at 2:00 PM, Dan Piponi wrote:

> 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
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe