Re: [Caml-list] O(n ln k) sorting for ocaml on github and a challenge

[Kazuhiko Sakaguchi <pi8027@gmail.com>]

Hi Christophe,

If I understand correctly, that's called "smooth sort" problem in
Paulson's "ML for the Working Programmer" book:
https://www.cl.cam.ac.uk/~lp15/MLbook/PDF/chapter3.pdf

I have tail-recursive smooth mergesort implemented (and verified) in Coq here:
https://github.com/pi8027/stablesort/blob/04a1441d36a379c31ea0221ace27ead1e93fc39e/theories/stablesort.v#L662-L685
Indeed, I can extract OCaml code from the Coq implementation, although
it is hard to read:
https://github.com/pi8027/stablesort/blob/benchmark-results/benchmark/ocaml/mergesort_coq.ml#L1285-L1364
Here are the benchmark results. Although I didn't use native integers,
my implementation seems to outperform List.stable_sort of OCaml:
https://github.com/pi8027/stablesort/blob/benchmark-results/output/main.pdf

This does not answer the initial question (challenge) since my
implementation targets lists rather than arrays. But, I think that the
`merge_sort_push` and `merge_sort_pop` functions are worth
understanding. It was initially devised to work around the termination
checker of Coq, but it is also useful to prevent stack overflow.
https://sympa.inria.fr/sympa/arc/coq-club/2009-04/msg00040.html

I hope it helps.

Best,
Kazuhiko

2021年10月9日(土) 13:06 Christophe Raffalli <christophe@raffalli.eu>:
>
> Hello,
>
> I just pushed on https://github.com/craff/block_sort.git an old piece of code: a
> stable sorting algorithm which is in O(n ln k) where n is the size of the list
> and k the number of changes of direction.  It is often much faster than
> List.sort, on my tests, never more than 10% slower.  The tests are available on
> github.
>
> If people are interested I could provide a version for arrays.
>
> A challenge would be to provide a O(n ln k) sorting on list that is always
> faster than List.sort. Any ideas ?
>
> Cheers,
> Christophe