[isabelle] Fwd: Collections: problems with sets of sets



Forwarding the helpful reply from Andreas who apparently forgot to reply to the list as well as to me -- since others may be interested as well.

Thanks Andreas!

Stephan

Begin forwarded message:

> From: Andreas Lochbihler <andreas.lochbihler at kit.edu>
> Date: 11 July 2011 08:54:01 CEST
> To: Stephan Merz <Stephan.Merz at loria.fr>
> Subject: Re: [isabelle] Collections: problems with sets of sets
> 
> Dear Stephan,
> 
> the code generator setup for equality of dlist is currently broken, but you can fix it easily. Just add
> 
> declare equal_dlist_def [code]
> 
> to your theory and everything should work fine.
> 
> One of the Isabelle developers might also add the above declaration to HOL/Library/Dlist. In there, the [code nbe] declaration removes the default code equation from the definition.
> 
> The collections framework supports nesting of data structures in a very limited way: For sets of sets, equality on the data structure for the sets inside the sets should be equivalent to set equality, i.e., the abstraction function should be injective, but dlist is *not*. For example, "[1, 2]" and "[2, 1]" represent the same set, but they are unequal. Hence, if you put them into another set, it will contain *two* elements, both of which represent the same set. If this is problematic for your use case, you must define your own set implementation for this, e.g., distinct, ordered lists. Unfortunately, the collections framework does not provide any such implementation.
> 
> A more general solution would be to abstract over the equality operator in the set's locales such that user-defined equalities could be used. However, neither Peter nor me have attempted to do that yet.
> 
> Andreas
> 
> Am 10.07.2011 12:44, schrieb Stephan Merz:
>> Dear all,
>> 
>> I have been playing with the Collection framework lately and having trouble when trying to set up executable sets of sets. The theory below illustrates the problem: the function maxima is meant to compute the maximal sets contained in a set of sets. Using the value command, I can evaluate the function for the empty and for singleton sets, but evaluation fails for any argument containing two or more element sets.
>> 
>> I've then exported ML code computing the maxima of a two-element set. When trying to evaluate this code, exception "Fail" is raised, and sure enough the code contains
>> 
>>   fun equal_dlista _ _ _ = raise Fail "equal_dlist";
>> 
>> which is responsible for this. However, looking into theory DList I find
>> 
>>   instantiation dlist :: (equal) equal
>> 
>> so I presumed that appropriate code for checking equality of two dlists would be generated. (I haven't looked much further, though, how this code would be set up.)
>> 
>> Am I doing something wrong here, or is this a known limitation?
>> 
>> NB: When I try to replace lists ('a ls) by hash sets ('a hs), I get the more sensible error message
>> 
>>   No type arity HashMap.hashmap :: hashable
>> 
>> for the definition of maxima -- I can understand that there is no hash function set up for hash sets themselves.
>> 
>> Thanks,
>> Stephan
>> 
> 
> -- 
> Karlsruher Institut für Technologie
> IPD Snelting
> 
> Andreas Lochbihler
> wissenschaftlicher Mitarbeiter
> Adenauerring 20a, Geb. 50.41, Raum 031
> 76131 Karlsruhe
> 
> Telefon: +49 721 608-47399
> Fax: +49 721 608-48457
> E-Mail: andreas.lochbihler at kit.edu
> http://pp.info.uni-karlsruhe.de
> KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft






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