[isabelle-dev] Merge-Sort Implementation

[Florian Haftmann]

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

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?

All the best,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20111027/5f7262eb/attachment.sig>