[isabelle-dev] Merge-Sort Implementation

[Christian Sternagel]

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
>