Re: [isabelle] Sorting algorithms in the AFP



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.

--
  Peter





On Wed, 2021-06-16 at 13:19 +0200, Florian Haftmann wrote:
> 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:  Automat
> > > ic_Refinement.Misc
> > > 	thys/Separation_Logic_Imperative_HOL/ROOT:19:    Automatic_Refi
> > > nement.Misc
> > > 	thys/IP_Addresses/WordInterval_Sorted.thy:3:        Automatic_R
> > > efinement.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_Refineme
> > > nt.Misc
> > > 	thys/Network_Security_Policy_Verification/Lib/Efficient_Distinc
> > > t.thy:3:  Automatic_Refinement.Misc (*mergesort*)
> > > 	thys/Collections/Lib/Dlist_add.thy:5:  Automatic_Refinement.Mis
> > > c
> > > 	thys/Collections/Lib/Sorted_List_Operations.thy:3:imports Main
> > > Automatic_Refinement.Misc
> > > 	thys/Collections/Iterator/SetIterator.thy:8:  Automatic_Refinem
> > > ent.Misc 
> > > 	thys/LOFT/LinuxRouter_OpenFlow_Translation.thy:3:  Automatic_Re
> > > finement.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
> 





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