The answer is that QuickCheck can't correctly constructively verify an existential condition without a constructive mechanism to generate the existential (i.e. the Skolem function mentioned before).
If you think about it from a plausible reasoning and constructive logic sense, QuickCheck should not be able to answer the question you desire. After all it runs a bounded number of tests, if it didn'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. A QuickCheck merely provides support for the plausibility of a universally quantified statement, much like how an experiment can't prove a model in physics, it can merely provide support for it. (see Polya's Mathematics and Plausible Reasoning). The scientific method can never prove anything. QuickCheck never gives you a false negative, but that one-sided error dooms your quest. You can assert that something doesn'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. 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 'expectFailure' 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. And to me at least the value of QuickCheck is that it never cries wolf. -Ed On Tue, Oct 14, 2008 at 6:36 PM, Norman Ramsey <[EMAIL PROTECTED]> wrote: > > > But how do I use QuickCheck to check an existential? > > > > The "standard" method in QuickCheck is to be constructive, and > > actually implement the function that constructs for the value. So, > > instead of > > > > forAll x . exists y . P(x,y) > > > > you write > > > > forAll x . P(x, find_y(x)) > > > Interesting. For A-E properties I can see where this approach would > be helpful, especially if it's not too hard to think of a good skolem > function. In my case x is empty and so I'm left with > > 'find a y such that P(y)' > > or a bit more exactly > > 'find an x in the four-dimensional unit cube such that 0.9 < f(x)' > > I've already written f and I'd really rather not write f-inverse; > I want the computer to do some of the work for me. So perhaps > SmallCheck would be a better way to go. > > It does seem a pity, as almost all the QuickCheck machinery would be > useful in such a search. On the other hand there are similar > scenarios on which I've already given up in despair, such as writing a > generator for creating well-typed terms in a nontrivial language. > > Anyway, thanks for suggesting a skolem function---I'm sure I'll find > use for one sooner or later. > > > Norman > _______________________________________________ > Haskell mailing list > [email protected] > http://www.haskell.org/mailman/listinfo/haskell >
_______________________________________________ Haskell mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell
