[Haskell-cafe] is proof by testing possible?

[Joe Fredette]

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 <jfredett at gmail.com>:
>> 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 <ekirpichov at gmail.com>:
>>>>
>>>> It is possible for functions with compact domain, not just finite.
>>>>
>>>> 2009/10/12 Joe Fredette <jfredett at gmail.com>:
>>>>>
>>>>> 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
>>>>>> Haskell-Cafe at haskell.org
>>>>>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>>>>
>>>>> _______________________________________________
>>>>> Haskell-Cafe mailing list
>>>>> Haskell-Cafe at haskell.org
>>>>> 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