Re: [isabelle] Sorting algorithms in the AFP

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,



* 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.


Am 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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.