caml-list - the Caml user's mailing list
 help / Atom feed
From: Kazuhiko Sakaguchi <>
To: Christophe Raffalli <>
Subject: Re: [Caml-list] O(n ln k) sorting for ocaml on github and a challenge
Date: Fri, 22 Oct 2021 13:42:46 +0900
Message-ID: <> (raw)
In-Reply-To: <20211009040533.chu7kqqk27r5wcok@oulala>

Hi Christophe,

If I understand correctly, that's called "smooth sort" problem in
Paulson's "ML for the Working Programmer" book:

I have tail-recursive smooth mergesort implemented (and verified) in Coq here:
Indeed, I can extract OCaml code from the Coq implementation, although
it is hard to read:
Here are the benchmark results. Although I didn't use native integers,
my implementation seems to outperform List.stable_sort of OCaml:

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.

I hope it helps.


2021年10月9日(土) 13:06 Christophe Raffalli <>:
> Hello,
> I just pushed on 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

      parent reply index

Thread overview: 6+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2021-10-09  4:05 Christophe Raffalli
2021-10-09  8:58 ` Mario Pereira
2021-10-09 19:59   ` Christophe Raffalli
2021-10-11 11:46     ` Niols
2021-10-11 21:27       ` Mario Pereira
2021-10-22  4:44 ` Kazuhiko Sakaguchi [this message]

Reply instructions:

You may reply publically to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \ \ \ \ \

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link

caml-list - the Caml user's mailing list

Archives are clonable: git clone --mirror

AGPL code for this site: git clone public-inbox