Re: [isabelle] Problems with linear orders and strings
Peter Lammich schrieb:
There is no theoretical problem to parametrise ordering, equality,
hash-functions, etc. However, the current state results from what has been
available before: The Isabelle Collections Framework reuses various existing
formalisations, e.g. red black trees (RBT), associative and distinct lists from
HOL/Library. All of them have been phrased in terms of type class operators ("op
<=" and "op <" for rbts) or HOL equality "op =". If one of these is to be
parametrised, these developments must first be changed or replicated. Thus, this
is mainly an engineering problem.
Unfortunately, the ICF interfaces are currently not parameterizable by
the used order, hash-function, equality-operator, ...
@Andreas: What was the state of discussion there, is it possible/worth
the effort to parameterize?
In fact, a few weeks ago, I changed the red black tree development on my local
copy such that the type class constraint vanishes and the ordering can now be a
parameter. It was not a big deal, but the new version is not backward-compatible
(w.r.t. HOL/Library/RBT_Impl), because I had to rename operations to avoid
name clashes. The key was to shift the definitions and lemmas in RBT_Impl from
the theory context with sort constraint linorder to the locale context
ord/order/linorder that is associated with the respective type class.
The locale context takes the order as parameter, i.e. only few changes are
necessary to the rbt formalisation (except for name clashes, etc.).
Since the ICF supports explicit invariants, different order implementations for
different RBTs should be relatively easy: In addition to the RBT itself, each
map also stores the comparison operation. Upon the first creation of the (empty)
map, one has to decide which order to use and stick with that. Even operations
on multiple RBTs like union and intersection are no problems if they are
implemented via iterators.
However, the ICF currently builds on the type RBT.rbt from HOL/Library/RBT,
which hides the data structure invariant of the raw implementation RBT_Impl.rbt
in a typedef. Hence, the red black tree implementation from the ICF requires
*no* invariants. If one wants to hide the invariant from one's formalisation,
there are two options:
Either, one introduces a typedef of its own for each order operation of
interest. This scales only to a few and requires to replicate HOL/Library/RBT
for each of them.
Or, one defines the type of all well-formed red black trees together with their
ordering, and adapts HOL/Library/RBT once for this more general type. But now,
equality tests via "op =" are no longer computable because equality of the order
operations is not. Thus, one would also have to replace "op =" with a
user-defined equality operation and redo all the above. With "op =", however, it
does not suffice to shift definitions from the theory context to a locale
context because "op =" is a HOL constant, not a type class parameter. Hence,
everything that depends on "op =" would have to be generalised w.r.t. an
explicit equality operator. Since "op =" is at the very core of HOL, this would
probably be a lot of work.
All the above should work fine for the ICF. HOL/Library also contains Mapping
and Cset as isomorphic types for 'a => 'b option and 'a set, and a setup to
implement these types via associative lists and red black trees. If you want to
take the above approach to Mapping and Cset, this would require even more work
To sum everything up: I think it would be no big deal to provide a map and set
implementation for a variant of red black trees where the user can specify his
own ordering of the keys. User-specified equality would be a much bigger task.
Karlsruher Institut für Technologie
Adenauerring 20a, Geb. 50.41, Raum 023
Telefon: +49 721 608-48352
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