[isabelle-dev] Merge-Sort Implementation

[Makarius]

On Thu, 27 Oct 2011, Florian Haftmann wrote:

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

In ancient times, the Isabelle/ML library had a really slow insertion 
sort.  I replaced that by quicksort according to the discussion of sorting 
algorithms in Larry's "ML for the working programmer" (1st edition), when 
I was a young student. Later the implementation was slightly tuned in 
conjunction with a lot of profiling on the real applications in the system 
-- the most critical one being normalization of sorts, which often happens
in the inference kernel.

In recent years, mergesort definitely gained more popularity than 
quicksort in general public.  Norbert Schirmer was the first to look at 
this again in ML, but he did not find a significant difference to the 
existing Isabelle/ML implementation. I've occasionally reconsidered the 
question myself, but there was never the critical mass to make a change to 
this important detail of the trusted code base.


 	Makarius