Email Gateway (Jun 16 2021 at 11:20): Email Gateway (Jun 16 2021 at 11:20):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear all,
I stumbled over a fundamental structural issue in the AFP (referring to
the 2021 release):
There is entry Efficient_Merge_Sort, with obvious content.
There is theory Automatic_Refinement.Misc, which provides both a quick
sort and a merge sort specification tailored for efficient execution.
There are a couple of references to Automatic_Refinement.Misc
throughout the AFP:
I have not yet visited all of them in detail but already this overview
suggests that a significant amount of those references makes use of the
sorting algorithms.
It seems worth a try whether those applications can be changed to use
session Efficient_Merge_Sort instead. But maybe the authors /
maintainers of Automatic_Refinement can say more on this.
In any case, the sorting part of Automatic_Refinement.Misc should be
made more explicit using a separate theory.
Cheers,
Florian
OpenPGP_signature
Email Gateway (Jun 16 2021 at 11:58):From: Peter Lammich <lammich@in.tum.de>
The quicksort and mergesort algorithms in AFP have been developed by
Thomas Tuerk, for the CAVA model checker.
It is slightly different from the mergesort afp entry:
Efficient_Merge_Sort uses a key function ('a => 'key::linorder), while
the Automatic_Refinement version accepts a relation. While this is
theoretically the same (both define weak linear orderings), practically
the introduction of an additional linearly ordered key type and type-
class can be cumbersome. In CAVA, we have had type-class conflicts
before, which do not affect our typeclass-less sorting definitions.
The efficiency of the existing algorithms should be benchmarked. To my
knowledge, we have never benchmarked our sorting algorithms.
The comments in Efficient_Merge_Sort suggests, however, that the
performance may also be language independent.
Email Gateway (Jun 16 2021 at 23:01):From: Gerwin Klein <kleing@unsw.edu.au>
Hi Florian,
I don't understand what the fundamental issue is there.
Do you mean that all entries should use only one specific sort implementation? (Why?) Or is it that the one in Automatic_Refinement is hard to reference?
Cheers,
Gerwin
signature.asc
Email Gateway (Jun 24 2021 at 07:21):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear all,
after Peter’s and Gerwin’s replies I recognize that there is a
significant difference between the sort implementations in
Automatic_Refinement and that in Efficient_Merge_Sort.
So the situation appears to me as follows:
The implementation in Efficient_Merge_Sort depends on a type class,
which is not general enough for all applications.
The implementations in Automatic_Refinement.Misc should be made
available more explicitly, either a) using a specific theory name or b)
seperately in a distinct AFP entry.
In the long run, analysis and potential unification of the algorithms
could be undertaken.
Hopefully this clarifies the situation.
Cheers,
Florian
OpenPGP_signature
Email Gateway (Jul 09 2021 at 18:20):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Florian,
On 6/24/21 9:20 AM, Florian Haftmann wrote:
Dear all,
after Peter’s and Gerwin’s replies I recognize that there is a
significant difference between the sort implementations in
Automatic_Refinement and that in Efficient_Merge_Sort.So the situation appears to me as follows:
- The implementation in Efficient_Merge_Sort depends on a type class,
which is not general enough for all applications.
Well, there is a key-function that maps elements into a linorder. That
is, in my opinion not as severe a dependency as directly depending on a
type class. Anyway
sorry for the late reply,
cheers
chris
The implementations in Automatic_Refinement.Misc should be made
available more explicitly, either a) using a specific theory name or b)
seperately in a distinct AFP entry.In the long run, analysis and potential unification of the algorithms
could be undertaken.
That would be nice.
Hopefully this clarifies the situation.
Cheers,
FlorianAm 16.06.21 um 13:19 schrieb Florian Haftmann:
Dear all,
I stumbled over a fundamental structural issue in the AFP (referring to
the 2021 release):
There is entry Efficient_Merge_Sort, with obvious content.
There is theory Automatic_Refinement.Misc, which provides both a quick
sort and a merge sort specification tailored for efficient execution.There are a couple of references to Automatic_Refinement.Misc
throughout the AFP:thys/AI_Planning_Languages_Semantics/PDDL_STRIPS_Semantics.thy:7: "Automatic_Refinement.Misc"
thys/CAVA_Automata/Digraph_Basic.thy:4: "Automatic_Refinement.Misc"
thys/Kruskal/UGraph.thy:5: "Automatic_Refinement.Misc"
thys/Kruskal/Kruskal_Misc.thy:5: "Automatic_Refinement.Misc"
thys/Separation_Logic_Imperative_HOL/Assertions.thy:7: Automatic_Refinement.Misc
thys/Separation_Logic_Imperative_HOL/ROOT:19: Automatic_Refinement.Misc
thys/IP_Addresses/WordInterval_Sorted.thy:3: Automatic_Refinement.Misc (Mergesort. TODO: dependnecy! we need a mergesort afp entry!!)
thys/IP_Addresses/ROOT:9: Automatic_Refinement.Misc (* mergesort *)
thys/Refine_Imperative_HOL/Lib/Pf_Add.thy:2:imports Automatic_Refinement.Misc "HOL-Library.Monad_Syntax"
thys/DFS_Framework/Misc/DFS_Framework_Misc.thy:2:imports Automatic_Refinement.Misc
thys/Flow_Networks/Lib/Fofu_Abs_Base.thy:5: Automatic_Refinement.Misc
thys/Network_Security_Policy_Verification/Lib/Efficient_Distinct.thy:3: Automatic_Refinement.Misc (mergesort)
thys/Collections/Lib/Dlist_add.thy:5: Automatic_Refinement.Misc
thys/Collections/Lib/Sorted_List_Operations.thy:3:imports Main Automatic_Refinement.Misc
thys/Collections/Iterator/SetIterator.thy:8: Automatic_Refinement.Misc
thys/LOFT/LinuxRouter_OpenFlow_Translation.thy:3: Automatic_Refinement.Misc (TODO@Peter: rename and make available at better place :))
thys/Tree-Automata/Ta.thy:7:imports Main Automatic_Refinement.Misc Tree
thys/Iptables_Semantics/Primitive_Matchers/Ipassmt.thy:6: Automatic_Refinement.Misc (dependnecy!)I have not yet visited all of them in detail but already this overview
suggests that a significant amount of those references makes use of the
sorting algorithms.It seems worth a try whether those applications can be changed to use
session Efficient_Merge_Sort instead. But maybe the authors /
maintainers of Automatic_Refinement can say more on this.In any case, the sorting part of Automatic_Refinement.Misc should be
made more explicit using a separate theory.Cheers,
Florian
Last updated: Jul 15 2022 at 23:21 UTC