On 10/27/2011 02:50 PM, Florian Haftmann wrote:
Hi Christian,
please find attached the formalization of the merge-sort algorithm as
used in GHC's standard library. See also:
http://hackage.haskell.org/packages/archive/base/latest/doc/html/src/Data-List.html#sort
interesting to read that comment. The exiting quicksort implementation
in HOL is indeed taken from Isabelle's ML library. Don't know what the
ancient motivation for quicksort has been (maybe others can comment on
this).
As far as I understand, mergesort is even worst-case faster on purely
functional lists. Unfortunately I cannot justify my claim (since it is
only what I've heard by others).
A critical question: according to the comment, this should easily
generalize to a stable sort_key implementation (as also the current
quicksort does). Have you undertaken this?
Indeed, that would be the obvious next step. I have not tried yet but
would not expect too hard difficulties. If this is of general interest I
can try.
cheers
chris
All the best,
Florian
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
