# is proof by testing possible? Classic List Threaded 32 messages 12
Open this post in threaded view
|

## is proof by testing possible?

 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.
Open this post in threaded view
|

## Re: is proof by testing possible?

Open this post in threaded view
|

## Re: is proof by testing possible?

Open this post in threaded view
|

## Re: is proof by testing possible?

Open this post in threaded view
|

## Re: is proof by testing possible?

Open this post in threaded view
|

## Re: is proof by testing possible?

Open this post in threaded view
|

## Re: is proof by testing possible?

Open this post in threaded view
|

## Re: is proof by testing possible?

 In reply to this post by muad On Mon, Oct 12, 2009 at 10:42 AM, muad <[hidden email]> 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

## Re: is proof by testing possible?

 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 <[hidden email]>   > 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 > [hidden email] > http://www.haskell.org/mailman/listinfo/haskell-cafe_______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

## Re: is proof by testing possible?

 Joe, > On Mon, Oct 12, 2009 at 11:03 AM, Joe Fredette <[hidden email]> wrote: > 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. There is Wadler's paper but I do find it tricky: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.9875You can play with the generator here: http://linux.tcs.inf.tu-dresden.de/~voigt/ft/The results can look unreadable at first, but I find that if I copy them onto paper and do all of the remaining substitutions manually (like I had to do with (a,b) -> (b,a)) you end up with something readable. If you keep doing this you'll get a good intuition for what the free theorem for a type will look like. -- Dan _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

## Re: is proof by testing possible?

Open this post in threaded view
|

## Re: is proof by testing possible?

Open this post in threaded view
|

## Re: is proof by testing possible?

Open this post in threaded view
|

## Re: is proof by testing possible?

 In reply to this post by Dan Piponi-2 Dan Piponi wrote: > On Mon, Oct 12, 2009 at 10:42 AM, muad <[hidden email]> wrote: >   >> Is it possible to prove correctness of a functions by testing it? >>     > 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.) >   swap = undefined Terminates and does not swap its arguments :-)  What do free theorems say about this, exactly -- do they just implicitly exclude this possibility? Neil. _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

## Re: is proof by testing possible?

 Neil Brown wrote: > Dan Piponi wrote: >> On Mon, Oct 12, 2009 at 10:42 AM, muad <[hidden email]> wrote: >>   >>> Is it possible to prove correctness of a functions by testing it?     >> 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.) >>   > swap = undefined > > Terminates and does not swap its arguments :-)  What do free theorems > say about this, exactly -- do they just implicitly exclude this > possibility? Normally, one presumes that "undefined" (id est, calling "error") is equivalent to looping, except that calling "error" is pragmatically speaking better: it is nicer to the caller of your function (they/you get to see a somewhat more descriptive error message instead of 100% CPU without any results). Regards, Jochem -- Jochem Berndsen | [hidden email] | jochem@牛在田里.com _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

## Re: is proof by testing possible?

 In reply to this post by Neil Brown-7 On Mon, Oct 12, 2009 at 11:31 AM, Neil Brown <[hidden email]> wrote: > swap = undefined > > Terminates and does not swap its arguments :-)  What do free theorems say > about this, exactly -- do they just implicitly exclude this possibility? I'm terrible at reasoning about functions with bottoms (ie. undefined or non-termination). But I suspect that a property like this holds: if the type signature of a function f is polymorphic in a, and it doesn't produce bottom for one particular value x of type a, for some particular type a, f can never produce bottom for any choice of x in any choice of type a. (Which is not to say it might not fail, but that the failure will be an issue with x, not f.) The intuition behind this is that if a function is polymorphic in a then it never examines the a. So even if a is bottom, the function can never know it. But it could fail because f additionally accepts as argument a polymorphic function that itself accepts a's, and that fails. But then it wouldn't be f's fault, it'd be the fault of the function you passed in. This is very poor of me. There's probably a nice precise formulation of what I've just said :-) -- Dan _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

## Re: is proof by testing possible?

 In reply to this post by jfredett Joe Fredette wrote: > Really? How? That sounds very interesting, I've got a fair knowledge > of basic topology, I'd love to see an application > to programming... Compactness is one of the most powerful concepts in mathematics, because on the one hand it makes it possible to reduce many infinite problems to finite ones (inherent in its definition: for every open cover there is a finite subcover), on the other hand it is often easy to prove compactness due to Tychonoff's theorem (any product of compact spaces is compact). The connection to computing science is very nicely explained in  http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/I found this paragraph particularly enlightening: """ > modulus :: (Cantor -> Integer) -> Natural > modulus f = least(\n -> forevery(\a -> forevery(\b -> eq n a b --> (f a == f b))))  This [...] finds the modulus of uniform continuity, defined as the least natural number `n` such that  `forall alpha,beta. alpha =_n beta implies f(alpha)=f(beta),`  where  `alpha =_n beta iff forall i< n. alpha_i = beta_i.`  What is going on here is that computable functionals are continuous, which amounts to saying that finite amounts of the output depend only on finite amounts of the input. But the Cantor space is compact, and in analysis and topology there is a theorem that says that continuous functions defined on a compact space are uniformly continuous. In this context, this amounts to the existence of a single `n` such that for all inputs it is enough to look at depth `n` to get the answer (which in this case is always finite, because it is an integer). """ Cheers _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

## Re: is proof by testing possible?

 In reply to this post by Neil Brown-7 Neil Brown <[hidden email]> writes: >> 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.) > swap = undefined > Terminates and does not swap its arguments :-) I think this counts as non-termination, and that for semantic purposes, any bottom value -- infinite loops, exceptions, undefined -- is treated equally. -k -- If I haven't seen further, it is by standing in the footprints of giants _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

## Re: Re: is proof by testing possible?

 In reply to this post by Ben Franksen That has got to be the single awesomest thing I have ever seen ever...   The first time I tried to read through the "Seemingly Impossible   Functional Programs" post, I understood none of it. Now it seems   obviously. I Love Math... Thanks for the explanation! /Joe On Oct 12, 2009, at 3:22 PM, Ben Franksen wrote: > Joe Fredette wrote: >> Really? How? That sounds very interesting, I've got a fair knowledge >> of basic topology, I'd love to see an application >> to programming... > > Compactness is one of the most powerful concepts in mathematics,   > because on > the one hand it makes it possible to reduce many infinite problems to > finite ones (inherent in its definition: for every open cover there   > is a > finite subcover), on the other hand it is often easy to prove   > compactness > due to Tychonoff's theorem (any product of compact spaces is   > compact). The > connection to computing science is very nicely explained in > > http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/> > I found this paragraph particularly enlightening: > > """ >> modulus :: (Cantor -> Integer) -> Natural >> modulus f = least(\n -> forevery(\a -> forevery(\b -> eq n a b -->   >> (f a == > f b)))) > > This [...] finds the modulus of uniform continuity, defined as the   > least > natural number `n` such that > `forall alpha,beta. alpha =_n beta implies f(alpha)=f(beta),` > where > `alpha =_n beta iff forall i< n. alpha_i = beta_i.` > > What is going on here is that computable functionals are continuous,   > which > amounts to saying that finite amounts of the output depend only on   > finite > amounts of the input. But the Cantor space is compact, and in   > analysis and > topology there is a theorem that says that continuous functions   > defined on > a compact space are uniformly continuous. In this context, this   > amounts to > the existence of a single `n` such that for all inputs it is enough   > to look > at depth `n` to get the answer (which in this case is always finite, > because it is an integer). > """ > > Cheers > > _______________________________________________ > Haskell-Cafe mailing list > [hidden email] > http://www.haskell.org/mailman/listinfo/haskell-cafe_______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe