Re: [isabelle] Wellsortedness error in Quickcheck



Hi Yuhui,


Quickcheck tries to execute this proposition using the code generation facility.
The functions (alpha => bool) are translated to functions in ML.
To allow to check for function equality, it requires that the type of the domain is finite (and enumerable, being of type class enum).

For the obvious finite types (unit and bool), we provide instantiations.
To polymorphic types, we check with small finite types that are of class enum.

Infinite types, such as int and nat, are not enumerable, and we cannot check for function equality (for the chosen translation above).

The solution to enable execution of this proposition even with an infinite type is to choose a different representation for functions (and sets). Different on-going discussions and effort by the developers will soon enable that this is possible, but right now, we are at the unlucky stage that none of them are fully automatic and could be applied by quickcheck behind the scenes.

NB: I am still not happy with the error message. It is the honest truth, why quickcheck cannot execute the proposition, but admittedly users might struggle understanding its explanation.


Lukas

On 09/11/2011 11:14 PM, Yuhui Lin wrote:
Hi All:

I met a problem when I try to use test_term in Quickcheck. The lemma is
showed below

*lemma "(f::int =>  bool) Un (h::int =>  bool) = h Un f"

*It pops up the following error
***************************************
*** Wellsortedness error:
*** Type int  =>   bool not of sort equal
*** No type arity int :: enum
***************************************

If I change the type from "int =>  bool"  to "' 'a =>  bool", then it's fine.
but "nat =>  bool" is not OK,  "bool =>  bool" is OK.

Thanks for reading.


Best
Yuhui Lin






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.