caml-list - the Caml user's mailing list
 help / Atom feed
From: Kazuhiko Sakaguchi <pi8027@gmail.com>
To: Christophe Raffalli <christophe@raffalli.eu>
Cc: caml-list@inria.fr
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: <CANPWVwmgT-sc6e73k4Yjrr03e1OYn-ktYXRv0zzGtLw5HX+GRg@mail.gmail.com> (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:
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

      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:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

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

  git send-email \
    --in-reply-to=CANPWVwmgT-sc6e73k4Yjrr03e1OYn-ktYXRv0zzGtLw5HX+GRg@mail.gmail.com \
    --to=pi8027@gmail.com \
    --cc=caml-list@inria.fr \
    --cc=christophe@raffalli.eu \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* 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 https://inbox.ocaml.org/caml-list

AGPL code for this site: git clone https://public-inbox.org/ public-inbox