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



Hi Peter and Stephan,

just let me add a few comments. We have not done this yet because the collections framework reuses as much as possible from the Isabelle/HOL library, e.g. red-black trees and associative lists. Since HOL equality is ubiquitous in there, all this would have to be generalised to arbitrary equivalence classes. Unfortunately, HOL equality is not a type class parameter as the comparison operators are. Hence, we cannot even exploit locale hackery to avoid redoing a lot. But it's not just copying and replaying the proofs, the simplifier as is does not support rewriting w.r.t. equivalence classes. Thus, we expect that many proofs have to be rewritten.

An alternative approach would be to move the multiple representation problem from the logic to in the code generator setup. For example, you could quotient your favorite data structure for sets w.r.t. the equivalence relation induced by the abstraction function and use the new type to represent the inner sets. The challenge then is to set up the code equations for the quotient type. However, this only works for operations whose result does not depend on the different representation of equal sets. For example, iteration over distinct lists would no longer be executable because iterating over [2, 1] visits 2 before 1, over [1, 2] visits 1 before 2. For red-black-trees, this would be an option because they implement totally ordered sets, for which iteration is uniquely specified.

This second approach is similar to the Cset approach in HOL/Library. 'a cset is isomorphic to 'a set, but has backing implementations with lists, distinct lists and red black trees. However, it does not support underspecified operations like iteration, as the collections framework does. the quotient construction above differs from Cset in that it is not isomorphic to set and adds the additional structure of the backing implementation (actually, only the structure of ordered lists) such that a few more code equations are provable.

Andreas

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.


However, we know that problem and have already discussed it. I think
that the result was that it is, in principle, possible. The set
implementation would then store custom equals (and hashcode, compare,
etc.) functions,
that have to be specified, e.g. on construction of a set
(empty-operation). The data structure invariant (and the precondition of
the empty-operation) would require that the custom equals, hashcode,
compare, etc functions are sensible.
A default empty-operation, setting the functions to default values (e.g.
op =, op<), would still be possible.



Best,
   Peter


--
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.