Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Problems with linear orders and strings

view this post on Zulip Email Gateway (Aug 18 2022 at 17:19):

From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear Florian and Peter,

thanks again. However, there now seems to be an incompatibility of Char_ord with RBTMapImpl from the AFP:

If I try to load both modules (to use RBTMaps with strings as keys), then there is class conflict
since the dependent theories of Char_ord and RBTMapImpl both define the ordering on pairs
(Product_ord and AFP/common/Misc).

Peter, can you remove the pair-ordering in common/Misc and load Product_ord instead (it is the same definition)?

I have the following workaround, but of course this should be fixed in a better way.

theory Linorders
imports List_lexord Char_nat (* but not Char_prod *)
begin

instantiation char :: linorder
begin
fun less_eq_char :: "char \<Rightarrow> char \<Rightarrow> bool" where "less_eq_char c d = (nat_of_char c \<le> nat_of_char d)"
fun less_char :: "char \<Rightarrow> char \<Rightarrow> bool" where "less_char c d = (nat_of_char c < nat_of_char d)"

instance
proof
fix x y :: char
assume "x \<le> y" and "y \<le> x"
hence "nat_of_char x = nat_of_char y" (is "?x = ?y") by auto
hence "char_of_nat ?x = char_of_nat ?y" by simp
thus "x = y" unfolding char_of_nat_of_char .
qed auto
end

Afterwards strings are in class linorder, code-generation works also after Code_Char_chr,
and I can use RBTMapImpl as there is no conflict between Misc and Product_ord.

Cheers,
René

view this post on Zulip Email Gateway (Aug 18 2022 at 17:19):

From: Peter Lammich <peter.lammich@uni-muenster.de>

Peter, can you remove the pair-ordering in common/Misc and load Product_ord instead (it is the same definition)?

If it is the same definition, and Product_ord is in the Isabelle
standard library, it should of course be changed to avoid duplication
and clashes!
@Rene: For the first time, you should change it in your local copy. If
you are using the stable version, there is no other way.
For the development version, someone (probably me or some of the
afp maintainers) should setup a development snapshot, do the change,
test if nothing breaks, and push it into the hg-repository.

Otherwise, it highlights some general problem with type classes:
If there is more than one way to say order a datatype, which one
should go into the typeclass.
I think there is such a problem for multisets, where there are two
orderings that are both "the natural" one when viewed from the right
perspective.
And, if formalizations get large, there may be parts where one order
is the "natural" one, and other parts where the other order is the
"natural" one, and
then things seems to clash ...

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?

Best,
Peter

I have the following workaround, but of course this should be fixed in a better way.

theory Linorders
imports List_lexord Char_nat (* but not Char_prod *)
begin

instantiation char :: linorder
begin
fun less_eq_char :: "char \<Rightarrow> char \<Rightarrow> bool" where "less_eq_char c d = (nat_of_char c \<le> nat_of_char d)"
fun less_char :: "char \<Rightarrow> char \<Rightarrow> bool" where "less_char c d = (nat_of_char c < nat_of_char d)"

instance
proof
fix x y :: char
assume "x \<le> y" and "y \<le> x"
hence "nat_of_char x = nat_of_char y" (is "?x = ?y") by auto
hence "char_of_nat ?x = char_of_nat ?y" by simp
thus "x = y" unfolding char_of_nat_of_char .
qed auto
end

Afterwards strings are in class linorder, code-generation works also after Code_Char_chr,
and I can use RBTMapImpl as there is no conflict between Misc and Product_ord.

Cheers,
René

view this post on Zulip Email Gateway (Aug 18 2022 at 17:19):

From: Jeremy Siek <jeremy.siek@colorado.edu>
2011/3/4 Peter Lammich <peter.lammich@uni-muenster.de>

Peter, can you remove the pair-ordering in common/Misc and load
Product_ord instead (it is the same definition)?

If it is the same definition, and Product_ord is in the Isabelle
standard library, it should of course be changed to avoid duplication
and clashes!
@Rene: For the first time, you should change it in your local copy. If
you are using the stable version, there is no other way.
For the development version, someone (probably me or some of the
afp maintainers) should setup a development snapshot, do the change,
test if nothing breaks, and push it into the hg-repository.

Otherwise, it highlights some general problem with type classes:
If there is more than one way to say order a datatype, which one
should go into the typeclass.
I think there is such a problem for multisets, where there are two
orderings that are both "the natural" one when viewed from the right
perspective.
And, if formalizations get large, there may be parts where one order
is the "natural" one, and other parts where the other order is the
"natural" one, and
then things seems to clash ...

Can't help but comment on this... there are alternative designs for
type classes in which instance declarations are lexically scoped.
This allows different instance declarations to be in effect for different
scopes.

@inproceedings{Siek:2005:ELS:1065010.1065021,
author = {Siek, Jeremy G. and Lumsdaine, Andrew},
title = {Essential language support for generic programming},
booktitle = {Proceedings of the 2005 ACM SIGPLAN conference on
Programming language design and implementation},
series = {PLDI '05},
year = {2005},
isbn = {1-59593-056-6},
location = {Chicago, IL, USA},
pages = {73--84},
numpages = {12},
url = {http://doi.acm.org/10.1145/1065010.1065021},
doi = {http://doi.acm.org/10.1145/1065010.1065021},
acmid = {1065021},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {C++, Haskell, generic programming, polymorphism, standard ML},

}

@inproceedings{Dreyer:2007:MTC:1190216.1190229,
author = {Dreyer, Derek and Harper, Robert and Chakravarty, Manuel M.
T. and Keller, Gabriele},
title = {Modular type classes},
booktitle = {Proceedings of the 34th annual ACM SIGPLAN-SIGACT
symposium on Principles of programming languages},
series = {POPL '07},
year = {2007},
isbn = {1-59593-575-4},
location = {Nice, France},
pages = {63--70},
numpages = {8},
url = {http://doi.acm.org/10.1145/1190216.1190229},
doi = {http://doi.acm.org/10.1145/1190216.1190229},
acmid = {1190229},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {modules, type classes, type inference, type systems},
}

Cheers,
Jeremy

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?

Best,
Peter

I have the following workaround, but of course this should be fixed in a
better way.

theory Linorders
imports List_lexord Char_nat (* but not Char_prod *)
begin

instantiation char :: linorder
begin
fun less_eq_char :: "char \<Rightarrow> char \<Rightarrow> bool" where
"less_eq_char c d = (nat_of_char c \<le> nat_of_char d)"
fun less_char :: "char \<Rightarrow> char \<Rightarrow> bool" where
"less_char c d = (nat_of_char c < nat_of_char d)"

instance
proof
fix x y :: char
assume "x \<le> y" and "y \<le> x"
hence "nat_of_char x = nat_of_char y" (is "?x = ?y") by auto
hence "char_of_nat ?x = char_of_nat ?y" by simp
thus "x = y" unfolding char_of_nat_of_char .
qed auto
end

Afterwards strings are in class linorder, code-generation works also
after Code_Char_chr,
and I can use RBTMapImpl as there is no conflict between Misc and
Product_ord.

Cheers,
René

view this post on Zulip Email Gateway (Aug 18 2022 at 17:20):

From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear all,

the problem I have is as follows:

unfortunately, neither char nor list are contained in the linorder class.
So here I have three questions:

1) are there already theories which make char and string members of linorder

2) I have defined my own class instance for char as follows:

fun nibble_to_nat :: "nibble => nat" where
"nibble_to_nat Nibble0 = 0"
| "nibble_to_nat Nibble1 = 1"
...

fun char_to_nat :: "char => nat" where
"char_to_nat (Char n1 n2) = (16 * nibble_to_nat n1 + nibble_to_nat n2)"

fun less_eq_char :: "char => char => bool"
where "less_eq_char c d = (char_to_nat c <= char_to_nat d)"

and then proven that this implementation satisfies the class conditions.
Unfortunately, after loading Code_Char_chr I cannot export the code anymore
since it is complains as follows:
*** Illegal character expression,
*** in equation char_to_nat (Char ?n1.0 ?n2.0) \<equiv>
*** plus_nat_inst.plus_nat
*** (times_nat_inst.times_nat
*** (nat (number_int_inst.number_of_int
*** (Int.Bit0 (Int.Bit0 (Int.Bit0 (Int.Bit0 (Int.Bit1 Int.Pls)))))))
*** (nibble_to_nat ?n1.0))
*** (nibble_to_nat ?n2.0)

3) In reality I need linorder not only for strings, but also for more
complex datatypes like the following for labeled symbols:

datatype ('f,'l)lab =
Lab "('f,'l)lab" 'l
| Funlab "('f,'l)lab" "('f,'l)lab list"
| Unlab 'f

The generation of an arbitrary linearization of each
datatype is trivial via a lexicographic comparison. However, the proof
obligations are tedious to prove. Is there some automatic way to
let Isabelles generate a linearization?

Best regards,
René

view this post on Zulip Email Gateway (Aug 18 2022 at 17:21):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi René,

1) are there already theories which make char and string members of linorder

there are theories in HOL/Library, e.g. Char_ord and List_lexord and
List_Prefix -- note that strings are just char lists, no type on their own

2) I have defined my own class instance for char as follows:

and then proven that this implementation satisfies the class conditions.
Unfortunately, after loading Code_Char_chr I cannot export the code anymore
since it is complains as follows:

Does this persists if you use the »official« Char_ord theory?

Hope this helps,
Florian
signature.asc

view this post on Zulip Email Gateway (Aug 18 2022 at 17:24):

From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
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.

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

view this post on Zulip Email Gateway (Aug 18 2022 at 17:25):

From: René Thiemann <rene.thiemann@uibk.ac.at>

1) are there already theories which make char and string members of linorder

there are theories in HOL/Library, e.g. Char_ord and List_lexord and
List_Prefix

thanks Florian for the pointers.

2) I have defined my own class instance for char as follows:

and then proven that this implementation satisfies the class conditions.
Unfortunately, after loading Code_Char_chr I cannot export the code anymore
since it is complains as follows:

Does this persists if you use the »official« Char_ord theory?

Unfortunately: yes.

theory Test
imports Char_ord Code_Char_chr
begin

definition f where "f x \<equiv> (x :: char) <= x"
export_code f in Haskell file -

yields a similar error message as my own definition of <= on characters.

view this post on Zulip Email Gateway (Aug 18 2022 at 17:27):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hallo René,

Does this persists if you use the »official« Char_ord theory?

Unfortunately: yes.

theory Test
imports Char_ord Code_Char_chr
begin

definition f where "f x \<equiv> (x :: char) <= x"
export_code f in Haskell file -

yields a similar error message as my own definition of <= on characters.

the key issue is that the code lemmas for less_eq, less on char should
use nat_of_char rather than relying on the exact representation of nats.

lemma [code]:
"c1 \<le> c2 \<longleftrightarrow> nat_of_char c1 \<le> nat_of_char c2"

lemma [code]:
"c1 < c2 \<longleftrightarrow> nat_of_char c1 < nat_of_char c2"

I would appreciate if these would go to the Char_ord theory.

Hope this helps,
Florian
signature.asc

Last updated: Nov 21 2024 at 12:39 UTC