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
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 big
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 to do
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
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
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
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
It is possible for functions with compact domain, not just finite.
2009/10/12 Joe Fredette jfred...@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 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 ekirpic...@gmail.com:
It is possible for functions with compact domain, not just finite.
2009/10/12 Joe Fredette
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
Also google seemingly impossible functional programs.
2009/10/12 Eugene Kirpichov ekirpic...@gmail.com:
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
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
On Mon, Oct 12, 2009 at 10:42 AM, muad muad.dib.sp...@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
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.sp...@gmail.com
wrote:
Joe,
On Mon, Oct 12, 2009 at 11:03 AM, Joe Fredette jfred...@gmail.com 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:
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 jfred...@gmail.com:
Oh- thanks for the example, I suppose
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 dpip...@gmail.com wrote:
Joe,
On Mon, Oct 12, 2009 at 11:03 AM, Joe Fredette jfred...@gmail.com wrote:
I completely
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,
Dan Piponi wrote:
On Mon, Oct 12, 2009 at 10:42 AM, muad muad.dib.sp...@gmail.com 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
Neil Brown wrote:
Dan Piponi wrote:
On Mon, Oct 12, 2009 at 10:42 AM, muad muad.dib.sp...@gmail.com 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
On Mon, Oct 12, 2009 at 11:31 AM, Neil Brown nc...@kent.ac.uk 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.
Neil Brown nc...@kent.ac.uk 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
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 nc...@kent.ac.uk wrote:
swap = undefined
Terminates and does not swap its arguments
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
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
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
On Mon, Oct 12, 2009 at 8:15 PM, Joe Fredette jfred...@gmail.com 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
27 matches
Mail list logo
