<div dir="ltr"><div>The answer is that QuickCheck can&#39;t correctly constructively verify an existential condition without a constructive mechanism to generate the existential (i.e. the Skolem function mentioned before).</div>
<div><br></div>If you think about it from a plausible reasoning and constructive logic sense, QuickCheck should not be able to answer the question you desire.&nbsp;After all it runs a bounded number of tests, if it didn&#39;t find your case in that number of checks its not definitive. It may have been looking in the wrong spots at the wrong cases.<div>
<br></div><div>A QuickCheck merely provides support for the plausibility of a universally quantified statement, much like how an experiment can&#39;t prove a model in physics, it can merely provide support for it. (see Polya&#39;s Mathematics and Plausible Reasoning). The scientific method can never prove anything.<div>
<br></div><div>QuickCheck never gives you a false negative, but that one-sided error dooms your quest.</div><div><br></div><div>You can assert that something doesn&#39;t exist with QuickCheck, but asserting that something always holds is the domain of mathematics, not experiment, unless you can exhaustively enumerate the universe of discourse, which is why SmallCheck _can_ handle existential claims.</div>
<div><br></div><div>Now that said, if you can strengthen the existential to a probabalistic claim about the odds of a random sample satisfying a given property are greater than some fixed known positive real number, then you can abuse the known QuickCheck sample size to say something about the odds of your &#39;expectFailure&#39; style trick failing to substantiate your claim, but unfortunately this costs you the invariant that when quickcheck says something is wrong that something really is wrong.&nbsp;</div>
<div><br></div><div>And to me at least the value of QuickCheck is that it never cries wolf.</div><div><br></div><div>-Ed</div><div><div><br></div><div><div><div class="gmail_quote">On Tue, Oct 14, 2008 at 6:36 PM, Norman Ramsey <span dir="ltr">&lt;<a href="mailto:nr@cs.tufts.edu">nr@cs.tufts.edu</a>&gt;</span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;"><div class="Ih2E3d">&nbsp;&gt; &gt; But how do I use QuickCheck to check an existential?<br>
&nbsp;&gt;<br>
&nbsp;&gt; The &quot;standard&quot; method in QuickCheck is to be constructive, and<br>
&nbsp;&gt; actually implement the function that constructs for the value. So,<br>
&nbsp;&gt; instead of<br>
&nbsp;&gt;<br>
&nbsp;&gt; &nbsp; forAll x . exists y . P(x,y)<br>
&nbsp;&gt;<br>
&nbsp;&gt; you write<br>
&nbsp;&gt;<br>
&nbsp;&gt; &nbsp; forAll x . P(x, find_y(x))<br>
<br>
<br>
</div>Interesting. &nbsp;For A-E properties I can see where this approach would<br>
be helpful, especially if it&#39;s not too hard to think of a good skolem<br>
function. &nbsp;In my case x is empty and so I&#39;m left with<br>
<br>
 &nbsp;&#39;find a y such that P(y)&#39;<br>
<br>
or a bit more exactly<br>
<br>
 &nbsp;&#39;find an x in the four-dimensional unit cube such that 0.9 &lt; f(x)&#39;<br>
<br>
I&#39;ve already written f and I&#39;d really rather not write f-inverse;<br>
I want the computer to do some of the work for me. &nbsp;So perhaps<br>
SmallCheck would be a better way to go.<br>
<br>
It does seem a pity, as almost all the QuickCheck machinery would be<br>
useful in such a search. &nbsp;On the other hand there are similar<br>
scenarios on which I&#39;ve already given up in despair, such as writing a<br>
generator for creating well-typed terms in a nontrivial language.<br>
<br>
Anyway, thanks for suggesting a skolem function---I&#39;m sure I&#39;ll find<br>
use for one sooner or later.<br>
<font color="#888888"><br>
<br>
Norman<br>
</font><div><div></div><div class="Wj3C7c">_______________________________________________<br>
Haskell mailing list<br>
<a href="mailto:Haskell@haskell.org">Haskell@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell" target="_blank">http://www.haskell.org/mailman/listinfo/haskell</a><br>
</div></div></blockquote></div><br></div></div></div></div></div>