[Haskell] Abusing quickcheck to check existential properties

[Edward Kmett]

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 <nr at cs.tufts.edu> 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
> Haskell at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell/attachments/20081014/f774e86e/attachment-0001.htm