Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Sorting algorithms in the AFP


view this post on Zulip 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):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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:

Hopefully this clarifies the situation.

Cheers,
Florian
OpenPGP_signature

view this post on Zulip 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:

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

That would be nice.

Hopefully this clarifies the situation.

Cheers,
Florian

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):

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: Sep 25 2021 at 09:17 UTC