Email Gateway (Aug 19 2022 at 13:40): Email Gateway (Aug 19 2022 at 13:40):From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear all,
I recently played around with the available code-equations for multisets.
(I wanted to get rid of manual data refinement in our formalization)
Here, the current problem is that the code for comparing multisets is non-terminating:
E.g., equality is implemented via two calls to <=,
and <= is implemented via intersection and equality.
Hence, even
value[code] "{#} = {#}"
does not terminate.
To solve this problem, I wrote a tiny implementation for comparisons.
Everybody can use it, and it would be nice, if
this algorithm or another proper implementation would find its
way into the distribution in src/HOL/Library/Multiset.thy.
Kind regards,
René
Multiset_Code.thy
Email Gateway (Aug 19 2022 at 13:40):From: "Jens-D. Doll" <jd@cococo.de>
Hello René,
could you explain the results for code comparison from conventional theory
a little? Aren't there some undecidable areas? And which results do we
have on normal forms and reducability?
Jens
------------------- René Thiemann wrote: -----------------
... the current problem is that the code for comparing multisets is
non-terminating: ...
Email Gateway (Aug 19 2022 at 13:40):From: René Thiemann <rene.thiemann@uibk.ac.at>
Hi Jens,
could you explain the results for code comparison from conventional theory a little?
The problem is easily explained. At the end of Multiset.thy, multisets are implemented via (not necessarily sorted) lists.
I.e., now all multiset-operations must be implemented on lists, where multiset_of is seen as a constructor.
E.g., it would be possible to implement membership via the lemma
lemma [code]: "(x :# multiset_of xs) = (x : set xs)"
Pattern matching on multiset_of is however not required. It is perfectly fine to implement multiset-equality via
the multiset subset-relation in general, i.e., without any specialization on the implementation type:
lemma[code]: "(A = (B :: 'a multiset)) = (A <= B & B <= A)"
However, the problem in Multiset.thy is, that the subset-relation is again implemented via equality:
lemma[code]: "(A <= B) = (inf_multiset A B = A)
Then, when trying to evaluate "A = B" we immediately invoke "A <= B" which in turn
invokes "inf_multiset A B = A" which invokes "<=", etc.
So, at least "=" or "<=" must be implemented directly, which is what I did in the previously attached theory.
Of course, one can think of smarter representations for multisets, like sorted lists,
or maps "'a => nat" which store the multiplicity of each element, but this is a bit more effort
than just fixing the current implementation of multisets by lists which is provided in Multiset.thy.
Aren't there some undecidable areas? And which results do we have on normal forms and reducability?
Can you be more precise? The above problems at least have nothing to do with undecidability!
Cheers,
René
Email Gateway (Aug 19 2022 at 13:41):From: "Jens-D. Doll" <jd@cococo.de>
If you consider code comparison of a phrase structure language or subsets
of it you will find intractables and undicidables; at least the current
theory says so.
D'accord?
Jens
Email Gateway (Aug 19 2022 at 13:41):From: René Thiemann <rene.thiemann@uibk.ac.at>
Maybe, but I do not see the connection between the "code comparison of a phrase structure language" and my topic, the implementation of finite multisets.
René
Email Gateway (Aug 19 2022 at 13:42):From: Tobias Nipkow <nipkow@in.tum.de>
René, thanks for your implementation, it is "in" now. I have defined your
auxiliary function List.extract (which may be of general interest for list
manipulators) via takeWhile and dropWhile, but the implementation is still via
your code equations.
Note that there is actually a faster implementation of multisets in
Library/DAList_Multiset.thy. Nevertheless it is nice that the default one
terminates more often now ;-)
Tobias
Email Gateway (Aug 19 2022 at 13:58):From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear Tobias,
your implementation is "in" now.
Thanks for taking care of it.
Note that there is actually a faster implementation of multisets in
Library/DAList_Multiset.thy.
This is true, but actually also this implementation lacks some implementations, namely
none of the following constants are executable after loading DAList_Multiset:
set_of, msetsum, msetprod, mcard, image_mset
To this end, it might be nice to merge the attached theory into DAList_Multiset: it implements
all of the above constants via a generic DA_List_Multiset_fold constant.
Maybe someone else also requires a more complete implementation.
Cheers,
René
Multiset_Code.thy
Email Gateway (Aug 19 2022 at 13:58):From: Tobias Nipkow <nipkow@in.tum.de>
I have added your contributions, thank you!
Tobias
Last updated: Apr 20 2024 at 12:26 UTC