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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
