Re: [isabelle] Problems with linear orders and strings





Peter Lammich schrieb:
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?
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.

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

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.

Andreas


--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 023
76131 Karlsruhe

Telefon: +49 721 608-48352
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.