On 2009-11-10 08:24 + (Tue), Conor McBride wrote:
> On 10 Nov 2009, at 05:52, Curt Sampson wrote:
>
> This is sometimes described as the "reflective" proof method: express
> problem in language capturing decidable fragment; hit with big stick.
Well, that's pretty sweet. *And* you get to use a
On 10 Nov 2009, at 05:52, Curt Sampson wrote:
On 2009-11-09 14:22 -0800 (Mon), muad wrote:
Proof: True for n = 0, 1, 2, 3, 4 (check!), hence true for all n.
QED.
...
Actually, the test is that it's true for 0 through 4 is not sufficient
for a proof;
It's enough testing...
you also nee
On 2009-11-09 14:22 -0800 (Mon), muad wrote:
> > Proof: True for n = 0, 1, 2, 3, 4 (check!), hence true for all n. QED.
> > ...
Actually, the test is that it's true for 0 through 4 is not sufficient
for a proof; you also need to prove in some way that you need do no
further tests. Showing that pa
I have come across an example:
> However, the following proof of the lovely identity:
> sum . map (^3) $ [1..n] = (sum $ [1..n])^2 is perfectly rigorous.
>
> Proof: True for n = 0, 1, 2, 3, 4 (check!), hence true for all n. QED.
>
> In order to turn this into a full-fledged proof, all you have
Joe Fredette wrote:
I fiddled with my previous idea -- the NatTrans class -- a bit, the results
are here[1], I don't know enough really to know if I got the NT law
right, or
even if the class defn is right.
Any thoughts? Am I doing this right/wrong/inbetween? Is there any use
for a class
like
On Mon, Oct 12, 2009 at 8:15 PM, Joe Fredette wrote:
> Sadly not enough, I understand the basics, but the whole "proof <=> this
> diagram commutes" thing still seems like
> voodoo to me. There is a section coming up in my Topology ISP that will be
> on CT. So I hope that I will be able to
> gain s
I fiddled with my previous idea -- the NatTrans class -- a bit, the
results
are here[1], I don't know enough really to know if I got the NT law
right, or
even if the class defn is right.
Any thoughts? Am I doing this right/wrong/inbetween? Is there any use
for a class
like this? I listed a
Sadly not enough, I understand the basics, but the whole "proof <=>
this diagram commutes" thing still seems like
voodoo to me. There is a section coming up in my Topology ISP that
will be on CT. So I hope that I will be able to
gain some purchase on the subject, at least enough to build up a
Do you know any category theory? What helped me finally grok free
theorems is that in the simplest cases, the free theorem for a
polymorphic function is just a naturality condition. For example, the
free theorem for
flatten :: Tree a -> [a]
is precisely the statement that flatten is a natural
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 wrote:
swap = undefined
Terminates and does not swap its arguments :-) What do free t
Neil Brown 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 purpose
On Mon, Oct 12, 2009 at 11:31 AM, Neil Brown 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
Neil Brown wrote:
> Dan Piponi wrote:
>> On Mon, Oct 12, 2009 at 10:42 AM, muad 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, s
Dan Piponi wrote:
On Mon, Oct 12, 2009 at 10:42 AM, muad 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 termin
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, sin
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 wrote:
> Joe,
>
>> On Mon, Oct 12, 2009 at 11:03 AM, Joe Fredette wrote:
>> I completely forgot about free theorems! Do yo
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 :
> Oh- thanks for the example, I suppose you can disregard
Joe,
> On Mon, Oct 12, 2009 at 11:03 AM, Joe Fredette 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://citeseer
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
wrote:
Is it possible to prove
On Mon, Oct 12, 2009 at 10:42 AM, 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.
not True==False
not False==True
Done. Tested :-)
Less trivially, consider a
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 "
Also google "seemingly impossible functional programs".
2009/10/12 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 :
>> It is possible fo
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 :
In gen
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 :
> It is possible for functions with compact domain, not just finite.
>
> 2009/10/12 Joe Fredette :
>> In general? No
It is possible for functions with compact domain, not just finite.
2009/10/12 Joe Fredette :
> 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 fun
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 o
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 Haskel
27 matches
Mail list logo
