Email Gateway (Aug 18 2022 at 18:05): Email Gateway (Aug 18 2022 at 18:05):From: Stephan Merz <Stephan.Merz@loria.fr>
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
Maxima.thy
Email Gateway (Aug 18 2022 at 18:06):From: Alexander Krauss <krauss@in.tum.de>
Hi Stephan,
There seems to be a problem with the setup of type Dlist. I reduced your
example to a minimal one, which does not use the Collection framework.
The problem goes away when I remove the [code nbe] declaration that
comes after the instance proof of equal in Dlist.thy
(http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2011/src/HOL/Library/Dlist.thy#l128).
I don't know about the precise semantics of [code nbe] wrt. normal code
equations, but it seems to override the previous code equation.
Maybe Florian can comment...
Alex
Email Gateway (Aug 18 2022 at 18:06):From: Stephan Merz <Stephan.Merz@loria.fr>
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:
Email Gateway (Aug 18 2022 at 18:06):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,
all [code …] declarations simply override any default equation.
Btw. the explicit declaration is currently tested for addition.
Cheers,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 18:07):From: Peter Lammich <peter.lammich@uni-muenster.de>
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
Email Gateway (Aug 18 2022 at 18:07):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
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
Last updated: Apr 25 2024 at 20:15 UTC