is proof by testing possible?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
32 messages Options
12
Reply | Threaded
Open this post in threaded view
|

is proof by testing possible?

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

Re: is proof by testing possible?

jfredett
In general? No- If we had an implementation of the `sin` function, how  
can testing a finite number of points along it determine
if that implementation is correct for every point?

For specific functions (particularly those with finite domain), it is  
possible. If you know the 'correct' output of every input, then  
testing each input and ensuring correct output will work. Consider the  
definition of the `not` function on booleans. The domain only has two  
elements (True and False) and the range has only two outputs (True and  
False), so if I test every input, and insure it maps appropriately to  
the specified output, we're all set.

Basically, if you can write your function as a big case statement that  
covers the whole domain, and that domain is finite, then the function  
can be tested to prove it's correctness.

Now, I should think the Muad'Dib would know that, perhaps you should  
go back to studying with the Mentats. :)

/Joe



On Oct 12, 2009, at 1:42 PM, muad 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.
>
> --
> View this message in context: http://www.nabble.com/is-proof-by-testing-possible--tp25860155p25860155.html
> Sent from the Haskell - Haskell-Cafe mailing list archive at  
> Nabble.com.
>
> _______________________________________________
> 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
Reply | Threaded
Open this post in threaded view
|

Re: is proof by testing possible?

Eugene Kirpichov
It is possible for functions with compact domain, not just finite.

2009/10/12 Joe Fredette <[hidden email]>:

> In general? No- If we had an implementation of the `sin` function, how can
> testing a finite number of points along it determine
> if that implementation is correct for every point?
>
> For specific functions (particularly those with finite domain), it is
> possible. If you know the 'correct' output of every input, then testing each
> input and ensuring correct output will work. Consider the definition of the
> `not` function on booleans. The domain only has two elements (True and
> False) and the range has only two outputs (True and False), so if I test
> every input, and insure it maps appropriately to the specified output, we're
> all set.
>
> Basically, if you can write your function as a big case statement that
> covers the whole domain, and that domain is finite, then the function can be
> tested to prove it's correctness.
>
> Now, I should think the Muad'Dib would know that, perhaps you should go back
> to studying with the Mentats. :)
>
> /Joe
>
>
>
> On Oct 12, 2009, at 1:42 PM, muad 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.
>>
>> --
>> View this message in context:
>> http://www.nabble.com/is-proof-by-testing-possible--tp25860155p25860155.html
>> Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
>>
>> _______________________________________________
>> 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
>



--
Eugene Kirpichov
Web IR developer, market.yandex.ru
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: is proof by testing possible?

Eugene Kirpichov
For example, it is possible to prove correctness of a function
"negatedHead :: [Bool] -> Bool" by testing it on "True:undefined" and
"False:undefined".

2009/10/12 Eugene Kirpichov <[hidden email]>:

> It is possible for functions with compact domain, not just finite.
>
> 2009/10/12 Joe Fredette <[hidden email]>:
>> In general? No- If we had an implementation of the `sin` function, how can
>> testing a finite number of points along it determine
>> if that implementation is correct for every point?
>>
>> For specific functions (particularly those with finite domain), it is
>> possible. If you know the 'correct' output of every input, then testing each
>> input and ensuring correct output will work. Consider the definition of the
>> `not` function on booleans. The domain only has two elements (True and
>> False) and the range has only two outputs (True and False), so if I test
>> every input, and insure it maps appropriately to the specified output, we're
>> all set.
>>
>> Basically, if you can write your function as a big case statement that
>> covers the whole domain, and that domain is finite, then the function can be
>> tested to prove it's correctness.
>>
>> Now, I should think the Muad'Dib would know that, perhaps you should go back
>> to studying with the Mentats. :)
>>
>> /Joe
>>
>>
>>
>> On Oct 12, 2009, at 1:42 PM, muad 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.
>>>
>>> --
>>> View this message in context:
>>> http://www.nabble.com/is-proof-by-testing-possible--tp25860155p25860155.html
>>> Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
>>>
>>> _______________________________________________
>>> 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
>>
>
>
>
> --
> Eugene Kirpichov
> Web IR developer, market.yandex.ru
>



--
Eugene Kirpichov
Web IR developer, market.yandex.ru
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: is proof by testing possible?

jfredett
In reply to this post by Eugene Kirpichov
Really? How? That sounds very interesting, I've got a fair knowledge  
of basic topology, I'd love to see an application
to programming...




On Oct 12, 2009, at 1:55 PM, Eugene Kirpichov wrote:

> It is possible for functions with compact domain, not just finite.
>
> 2009/10/12 Joe Fredette <[hidden email]>:
>> In general? No- If we had an implementation of the `sin` function,  
>> how can
>> testing a finite number of points along it determine
>> if that implementation is correct for every point?
>>
>> For specific functions (particularly those with finite domain), it is
>> possible. If you know the 'correct' output of every input, then  
>> testing each
>> input and ensuring correct output will work. Consider the  
>> definition of the
>> `not` function on booleans. The domain only has two elements (True  
>> and
>> False) and the range has only two outputs (True and False), so if I  
>> test
>> every input, and insure it maps appropriately to the specified  
>> output, we're
>> all set.
>>
>> Basically, if you can write your function as a big case statement  
>> that
>> covers the whole domain, and that domain is finite, then the  
>> function can be
>> tested to prove it's correctness.
>>
>> Now, I should think the Muad'Dib would know that, perhaps you  
>> should go back
>> to studying with the Mentats. :)
>>
>> /Joe
>>
>>
>>
>> On Oct 12, 2009, at 1:42 PM, muad 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.
>>>
>>> --
>>> View this message in context:
>>> http://www.nabble.com/is-proof-by-testing-possible--tp25860155p25860155.html
>>> Sent from the Haskell - Haskell-Cafe mailing list archive at  
>>> Nabble.com.
>>>
>>> _______________________________________________
>>> 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
>>
>
>
>
> --
> Eugene Kirpichov
> Web IR developer, market.yandex.ru

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: is proof by testing possible?

Eugene Kirpichov
In reply to this post by Eugene Kirpichov
Also google "seemingly impossible functional programs".

2009/10/12 Eugene Kirpichov <[hidden email]>:

> For example, it is possible to prove correctness of a function
> "negatedHead :: [Bool] -> Bool" by testing it on "True:undefined" and
> "False:undefined".
>
> 2009/10/12 Eugene Kirpichov <[hidden email]>:
>> It is possible for functions with compact domain, not just finite.
>>
>> 2009/10/12 Joe Fredette <[hidden email]>:
>>> In general? No- If we had an implementation of the `sin` function, how can
>>> testing a finite number of points along it determine
>>> if that implementation is correct for every point?
>>>
>>> For specific functions (particularly those with finite domain), it is
>>> possible. If you know the 'correct' output of every input, then testing each
>>> input and ensuring correct output will work. Consider the definition of the
>>> `not` function on booleans. The domain only has two elements (True and
>>> False) and the range has only two outputs (True and False), so if I test
>>> every input, and insure it maps appropriately to the specified output, we're
>>> all set.
>>>
>>> Basically, if you can write your function as a big case statement that
>>> covers the whole domain, and that domain is finite, then the function can be
>>> tested to prove it's correctness.
>>>
>>> Now, I should think the Muad'Dib would know that, perhaps you should go back
>>> to studying with the Mentats. :)
>>>
>>> /Joe
>>>
>>>
>>>
>>> On Oct 12, 2009, at 1:42 PM, muad 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.
>>>>
>>>> --
>>>> View this message in context:
>>>> http://www.nabble.com/is-proof-by-testing-possible--tp25860155p25860155.html
>>>> Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
>>>>
>>>> _______________________________________________
>>>> 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
>>>
>>
>>
>>
>> --
>> Eugene Kirpichov
>> Web IR developer, market.yandex.ru
>>
>
>
>
> --
> Eugene Kirpichov
> Web IR developer, market.yandex.ru
>



--
Eugene Kirpichov
Web IR developer, market.yandex.ru
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: is proof by testing possible?

jfredett
In reply to this post by Eugene Kirpichov
Oh- thanks for the example, I suppose you can disregard my other  
message.

I suppose this is a bit like short-circuiting. No?


On Oct 12, 2009, at 1:56 PM, Eugene Kirpichov wrote:

> For example, it is possible to prove correctness of a function
> "negatedHead :: [Bool] -> Bool" by testing it on "True:undefined" and
> "False:undefined".
>
> 2009/10/12 Eugene Kirpichov <[hidden email]>:
>> It is possible for functions with compact domain, not just finite.
>>
>> 2009/10/12 Joe Fredette <[hidden email]>:
>>> In general? No- If we had an implementation of the `sin` function,  
>>> how can
>>> testing a finite number of points along it determine
>>> if that implementation is correct for every point?
>>>
>>> For specific functions (particularly those with finite domain), it  
>>> is
>>> possible. If you know the 'correct' output of every input, then  
>>> testing each
>>> input and ensuring correct output will work. Consider the  
>>> definition of the
>>> `not` function on booleans. The domain only has two elements (True  
>>> and
>>> False) and the range has only two outputs (True and False), so if  
>>> I test
>>> every input, and insure it maps appropriately to the specified  
>>> output, we're
>>> all set.
>>>
>>> Basically, if you can write your function as a big case statement  
>>> that
>>> covers the whole domain, and that domain is finite, then the  
>>> function can be
>>> tested to prove it's correctness.
>>>
>>> Now, I should think the Muad'Dib would know that, perhaps you  
>>> should go back
>>> to studying with the Mentats. :)
>>>
>>> /Joe
>>>
>>>
>>>
>>> On Oct 12, 2009, at 1:42 PM, muad 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.
>>>>
>>>> --
>>>> View this message in context:
>>>> http://www.nabble.com/is-proof-by-testing-possible--tp25860155p25860155.html
>>>> Sent from the Haskell - Haskell-Cafe mailing list archive at  
>>>> Nabble.com.
>>>>
>>>> _______________________________________________
>>>> 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
>>>
>>
>>
>>
>> --
>> Eugene Kirpichov
>> Web IR developer, market.yandex.ru
>>
>
>
>
> --
> Eugene Kirpichov
> Web IR developer, market.yandex.ru

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: is proof by testing possible?

Dan Piponi-2
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
Reply | Threaded
Open this post in threaded view
|

Re: is proof by testing possible?

jfredett
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
Reply | Threaded
Open this post in threaded view
|

Re: is proof by testing possible?

Dan Piponi-2
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.9875

You 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
Reply | Threaded
Open this post in threaded view
|

Re: is proof by testing possible?

Eugene Kirpichov
In reply to this post by jfredett
What do you mean under short-circuiting here, and what is the connection?
The property that allows to deduce global correctness from correctness
on under-defined inputs is just continuity in the topological sense.

2009/10/12 Joe Fredette <[hidden email]>:

> Oh- thanks for the example, I suppose you can disregard my other message.
>
> I suppose this is a bit like short-circuiting. No?
>
>
> On Oct 12, 2009, at 1:56 PM, Eugene Kirpichov wrote:
>
>> For example, it is possible to prove correctness of a function
>> "negatedHead :: [Bool] -> Bool" by testing it on "True:undefined" and
>> "False:undefined".
>>
>> 2009/10/12 Eugene Kirpichov <[hidden email]>:
>>>
>>> It is possible for functions with compact domain, not just finite.
>>>
>>> 2009/10/12 Joe Fredette <[hidden email]>:
>>>>
>>>> In general? No- If we had an implementation of the `sin` function, how
>>>> can
>>>> testing a finite number of points along it determine
>>>> if that implementation is correct for every point?
>>>>
>>>> For specific functions (particularly those with finite domain), it is
>>>> possible. If you know the 'correct' output of every input, then testing
>>>> each
>>>> input and ensuring correct output will work. Consider the definition of
>>>> the
>>>> `not` function on booleans. The domain only has two elements (True and
>>>> False) and the range has only two outputs (True and False), so if I test
>>>> every input, and insure it maps appropriately to the specified output,
>>>> we're
>>>> all set.
>>>>
>>>> Basically, if you can write your function as a big case statement that
>>>> covers the whole domain, and that domain is finite, then the function
>>>> can be
>>>> tested to prove it's correctness.
>>>>
>>>> Now, I should think the Muad'Dib would know that, perhaps you should go
>>>> back
>>>> to studying with the Mentats. :)
>>>>
>>>> /Joe
>>>>
>>>>
>>>>
>>>> On Oct 12, 2009, at 1:42 PM, muad 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.
>>>>>
>>>>> --
>>>>> View this message in context:
>>>>>
>>>>> http://www.nabble.com/is-proof-by-testing-possible--tp25860155p25860155.html
>>>>> Sent from the Haskell - Haskell-Cafe mailing list archive at
>>>>> Nabble.com.
>>>>>
>>>>> _______________________________________________
>>>>> 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
>>>>
>>>
>>>
>>>
>>> --
>>> Eugene Kirpichov
>>> Web IR developer, market.yandex.ru
>>>
>>
>>
>>
>> --
>> Eugene Kirpichov
>> Web IR developer, market.yandex.ru
>
>



--
Eugene Kirpichov
Web IR developer, market.yandex.ru
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: is proof by testing possible?

Dan Piponi-2
In reply to this post by Dan Piponi-2
I'm making the same mistake repeatedly. In both my mails there are
places where I said (a,b) or (b,a) when I meant (a,a).
--
Dan

On Mon, Oct 12, 2009 at 11:09 AM, Dan Piponi <[hidden email]> wrote:

> 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.9875
>
> You 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
Reply | Threaded
Open this post in threaded view
|

Re: is proof by testing possible?

jfredett
In reply to this post by Eugene Kirpichov
I mean that, like in the definition of `||`

     True || _ = True
     False || x = x

If you generalize this to `or`-ing a list of inputs, eg:


     foldr (||) False list_of_bools

you can 'short-circuit' the test as soon as you find a 'True' value.  
This is actually not the greatest example, since you can't actually  
test it in finite number of tests, but you can test "half" the  
function by testing a that lists like [True:undefined] or [False,  
False, False, ... , True , undefined] return "True".

It's "short-circuiting" in the sense that it (like the `||` function)  
doesn't need to see (necessarily) all of it's arguments to return a  
correct result.

/Joe


On Oct 12, 2009, at 2:11 PM, Eugene Kirpichov wrote:

> What do you mean under short-circuiting here, and what is the  
> connection?
> The property that allows to deduce global correctness from correctness
> on under-defined inputs is just continuity in the topological sense.
>
> 2009/10/12 Joe Fredette <[hidden email]>:
>> Oh- thanks for the example, I suppose you can disregard my other  
>> message.
>>
>> I suppose this is a bit like short-circuiting. No?
>>
>>
>> On Oct 12, 2009, at 1:56 PM, Eugene Kirpichov wrote:
>>
>>> For example, it is possible to prove correctness of a function
>>> "negatedHead :: [Bool] -> Bool" by testing it on "True:undefined"  
>>> and
>>> "False:undefined".
>>>
>>> 2009/10/12 Eugene Kirpichov <[hidden email]>:
>>>>
>>>> It is possible for functions with compact domain, not just finite.
>>>>
>>>> 2009/10/12 Joe Fredette <[hidden email]>:
>>>>>
>>>>> In general? No- If we had an implementation of the `sin`  
>>>>> function, how
>>>>> can
>>>>> testing a finite number of points along it determine
>>>>> if that implementation is correct for every point?
>>>>>
>>>>> For specific functions (particularly those with finite domain),  
>>>>> it is
>>>>> possible. If you know the 'correct' output of every input, then  
>>>>> testing
>>>>> each
>>>>> input and ensuring correct output will work. Consider the  
>>>>> definition of
>>>>> the
>>>>> `not` function on booleans. The domain only has two elements  
>>>>> (True and
>>>>> False) and the range has only two outputs (True and False), so  
>>>>> if I test
>>>>> every input, and insure it maps appropriately to the specified  
>>>>> output,
>>>>> we're
>>>>> all set.
>>>>>
>>>>> Basically, if you can write your function as a big case  
>>>>> statement that
>>>>> covers the whole domain, and that domain is finite, then the  
>>>>> function
>>>>> can be
>>>>> tested to prove it's correctness.
>>>>>
>>>>> Now, I should think the Muad'Dib would know that, perhaps you  
>>>>> should go
>>>>> back
>>>>> to studying with the Mentats. :)
>>>>>
>>>>> /Joe
>>>>>
>>>>>
>>>>>
>>>>> On Oct 12, 2009, at 1:42 PM, muad 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.
>>>>>>
>>>>>> --
>>>>>> View this message in context:
>>>>>>
>>>>>> http://www.nabble.com/is-proof-by-testing-possible--tp25860155p25860155.html
>>>>>> Sent from the Haskell - Haskell-Cafe mailing list archive at
>>>>>> Nabble.com.
>>>>>>
>>>>>> _______________________________________________
>>>>>> 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
>>>>>
>>>>
>>>>
>>>>
>>>> --
>>>> Eugene Kirpichov
>>>> Web IR developer, market.yandex.ru
>>>>
>>>
>>>
>>>
>>> --
>>> Eugene Kirpichov
>>> Web IR developer, market.yandex.ru
>>
>>
>
>
>
> --
> Eugene Kirpichov
> Web IR developer, market.yandex.ru

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: is proof by testing possible?

Neil Brown-7
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
Reply | Threaded
Open this post in threaded view
|

Re: is proof by testing possible?

Jochem Berndsen-3
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
Reply | Threaded
Open this post in threaded view
|

Re: is proof by testing possible?

Dan Piponi-2
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
Reply | Threaded
Open this post in threaded view
|

Re: is proof by testing possible?

Ben Franksen
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
Reply | Threaded
Open this post in threaded view
|

Re: is proof by testing possible?

Ketil Malde-5
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
Reply | Threaded
Open this post in threaded view
|

Re: Re: is proof by testing possible?

jfredett
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
Reply | Threaded
Open this post in threaded view
|

Re: is proof by testing possible?

Dan Weston
In reply to this post by Dan Piponi-2
Could that nice precise formulation simply be Scott continuity, which in
turn preserves compactness through composition and under application?

Dan Piponi wrote:

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

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
12