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
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.
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,
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.
Karlsruher Institut für Technologie
Adenauerring 20a, Geb. 50.41, Raum 031
Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
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