From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by c5ff346549e7 (Postfix) with ESMTP id 4C50D5D5 for ; Fri, 22 Oct 2021 04:44:13 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.84,326,1620684000"; d="scan'208";a="396912617" Received: from prod-listesu18.inria.fr (HELO sympa.inria.fr) ([128.93.162.160]) by mail3-relais-sop.national.inria.fr with ESMTP; 22 Oct 2021 06:44:07 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id 01C91E0C70; Fri, 22 Oct 2021 06:44:07 +0200 (CEST) Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 5DFCBE0015 for ; Fri, 22 Oct 2021 06:44:01 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=pi8027@gmail.com; spf=Pass smtp.mailfrom=pi8027@gmail.com; spf=None smtp.helo=postmaster@mail-ua1-f43.google.com IronPort-PHdr: =?us-ascii?q?A9a23=3AKmzTnBEG+nEAwzeMDMCyYZ1Gf61MhN3EVzX9CrI?= =?us-ascii?q?Zgr5DOp6u447ldBSGo6k31BmYBM6GtLptsKn/i+jYQ2sO4JKM4jgpUadncFs7s?= =?us-ascii?q?/gQhBEqG8WfCEf2f7bAZi0+G9leBhc+pynoeUdaF9zjaFLMv3a88SAdGgnlNQp?= =?us-ascii?q?yO+/5BpPeg9642uys55HfeQFFiCeybb5yLhi9sBncuNQRjYZ+MKg61wHHomFPe?= =?us-ascii?q?+RYxGNoIUyckhPh7cqu/5Bt7jpdtes5+8FPTav1caI4TadFDDs9KGA6+NfrtRj?= =?us-ascii?q?YQgSR4HYXT3gbnQBJAwjB6xH6Q4vxvy7nvedzxCWWIcv7Rq0vVD+886lkVgPni?= =?us-ascii?q?CYfNz447m7XjNBwjLlGqx6lvhBz3pLYbJ2QOPd4Y6jTf84VRXBZU8leWSxOAIO?= =?us-ascii?q?yYYUMAeQcI+hXs4bzqkASrRunHwSgGP/jxiNKi3LwwKY00/4hEQbD3AE4GtwBq?= =?us-ascii?q?nXVrMj1NKcTUuC1y7TDwyjZYPNVwzj955XIfQwhofGNQLl9dtLRyUgsGg/ZkFm?= =?us-ascii?q?dq5foPzyQ1usXsmib6/BsWv6oi24isgx8pCWkycgwhIfTnI0V1kzE+jtjwIYzP?= =?us-ascii?q?dC1Sk12bNyrHZZNtiyXNY97T8AtTW11vCs3xaMLt56ncCUOxpoqxRzSZuKafoa?= =?us-ascii?q?G4x/uSuafLDV3iXxldryxiQi//E69wePyUcm01UxFritDktTUqn8CzRnT5tKdR?= =?us-ascii?q?fRh5EuhxDWP2xjc6uFFPUA0lbfbJIU7zrEskZoTtFzPHi7wmEXsja+ZbF8o+ua?= =?us-ascii?q?y6+nhf77opYecOpdqhg3iNqkigM+yDOQiPgQQQWSX5/6w2bLt8ED/Xb5ElOc5k?= =?us-ascii?q?rPDv5DfPckbprC2AwtS0os77hawFTam0NABkXkaNl1JZQuLj4bmNlzAOvz4AvC?= =?us-ascii?q?/g1OjkDdv2f/KJKHuApLILnTbkbfhe6hy61JExQYt0dxS44hYB7IBLf7pREP9q?= =?us-ascii?q?sLUAgU2PgG62+rnDc9y1oIaWWKBGK+ZN6bSvEeQ5uIuIOSAeJEZtTTmJvgq4v7?= =?us-ascii?q?hl345mVsHcaa12psXbWi0Hu56LEWBfXrsntABHH8WsQUkSezqjESOUTpSZ3apQ?= =?us-ascii?q?6Ix/So7CYKjDYfbXI+hmr2B3CGhHp1XfG9KEF6MEW27P7mDDtwMciOJPsh5kjF?= =?us-ascii?q?Mb7GvRYYl0RDm4AT60bt8Mu3M+iAwr5vt2tFx4+yVmAxkphJuCMHI8GifUmF1n?= =?us-ascii?q?WRAfDY11a9iqkx8ggOb0Pgg2aNwGtla5vcPWQA/Y82Ph9dmAsz/D1qSNuyCT0y?= =?us-ascii?q?rF5D/WWlZpjMZxtYPZwNgEozngEyYmSWtBLARmvqAA5lmqso0MFD+Is98zzDN0?= =?us-ascii?q?6xz1jHOp+NAMGSnguh08A2BX+b0?= IronPort-HdrOrdr: =?us-ascii?q?A9a23=3AGqyL36wVblussG9JT7JJKrPwFb1zdoMgy1kn?= =?us-ascii?q?xilNoNJuHfBw9vre+cjzuiWftN98YhwdcJW7WZVoIkmsl6Kdg7N+AV7KZmCP01?= =?us-ascii?q?dAbrsD0WKI+UyCJ8SKzJ8l6U4WSdkZNDSfNzRHZL7BkW6F+oEbsb26zJw=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0ARAwASaxphfyveVdFaFnOEMAE8DlY7M?= =?us-ascii?q?YRHj0lTBwEBAQaBPgOKRCqBA4VOjCgLAQMBDTkIBAEBhGECgmsCHQcBBDQTAQI?= =?us-ascii?q?EFQEBBQEBAQIBAwMEARMBAQ0LEAg4JoVoDYI1KQGDZAIBAQISER0BGx0BAwwGA?= =?us-ascii?q?wILDwImAgIiAREBBQEcBhMigk8BglQBAwkmD4tijxeBBD2LMoEVBRcTboIIBoE?= =?us-ascii?q?/AQMCgycKGSgNaIFXAgEGEn4qhCuBRRNASoZmJ4EZgRCBS4JvPoJiAQEBAYFeg?= =?us-ascii?q?xeCZASFRgYCgQU+AhUEgQAZVgEBAZ88iwCSEwkBBgJSgTpuDSOKPZQVK4Nlkie?= =?us-ascii?q?QaaJPk1cthHMQIxKBQoF9TSNQMW2BS1AZDpISgT6GPIJzNS8CAQgtAgYBCgEBA?= =?us-ascii?q?wmJdQEB?= X-IPAS-Result: =?us-ascii?q?A0ARAwASaxphfyveVdFaFnOEMAE8DlY7MYRHj0lTBwEBAQa?= =?us-ascii?q?BPgOKRCqBA4VOjCgLAQMBDTkIBAEBhGECgmsCHQcBBDQTAQIEFQEBBQEBAQIBA?= =?us-ascii?q?wMEARMBAQ0LEAg4JoVoDYI1KQGDZAIBAQISER0BGx0BAwwGAwILDwImAgIiARE?= =?us-ascii?q?BBQEcBhMigk8BglQBAwkmD4tijxeBBD2LMoEVBRcTboIIBoE/AQMCgycKGSgNa?= =?us-ascii?q?IFXAgEGEn4qhCuBRRNASoZmJ4EZgRCBS4JvPoJiAQEBAYFegxeCZASFRgYCgQU?= =?us-ascii?q?+AhUEgQAZVgEBAZ88iwCSEwkBBgJSgTpuDSOKPZQVK4NlkieQaaJPk1cthHMQI?= =?us-ascii?q?xKBQoF9TSNQMW2BS1AZDpISgT6GPIJzNS8CAQgtAgYBCgEBAwmJdQEB?= X-IronPort-AV: E=Sophos;i="5.84,326,1620684000"; d="scan'208";a="396912549" X-MGA-submission: =?us-ascii?q?MDGjoY3hofRE9KobT9MsPHuXuxlfaEW1rs8NEf?= =?us-ascii?q?tBVvYhzoKcyR08IpROXhK5Fuy7B+z1QDgDKIJiVc1fu/YbCBVz7sobmr?= =?us-ascii?q?XyI9L9ILjzi210AlQyzmy7eXtM0PIjffxSsNdzWOaxxV8Hd/521EeG6X?= =?us-ascii?q?ITZJ7W1Nn8xhzMRAvimAM4Tg=3D=3D?= Received: from mail-ua1-f43.google.com ([209.85.222.43]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES256-GCM-SHA384; 22 Oct 2021 06:43:59 +0200 Received: by mail-ua1-f43.google.com with SMTP id a17so5304408uax.12 for ; Thu, 21 Oct 2021 21:43:59 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=1X/AbJ6QWbAEzlZmIwaAwoFKLwB0FNMSs/w4BJ7F70o=; b=T6VrBFP/5EVc3D2p0kptbdQECiKTeHzxHHTd4oxYMM2fwyoHYt79glkuAXDXK4JoJ6 IFrV+7BXEeIOtiqud7piDO91lwY5XsE+oSiXRJNV1orXAsjFIcfqBQCV26l66wt2pwIp nv1eZl1UAcq2b15Yd3qw1e5h3YFBjTJksmdPTo2WHjVyea+xqVCuQXH/Ydnig333CQ98 GGKMOWNyZX72Mwe1zpiuT40cBfFNUVwOLcX1q5G2aforoqGwuxY5rqje/4KJJjXQM/Af K02zJS2hLREGdlL6vCVlKOnbxOjlNDBPMGPZ3JMR/r204SSlzXrXGtQ7+KvPE2x3iwep fYJQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:mime-version:references:in-reply-to:from:date :message-id:subject:to:cc:content-transfer-encoding; bh=1X/AbJ6QWbAEzlZmIwaAwoFKLwB0FNMSs/w4BJ7F70o=; b=sr3RwqEXozdxccAoYxTc/SyqoraxvvHsoyL1jI3VdZ3t1Dg3sb6ROpsFk9VrQfHCmB fB65uLTi471u/ZXidTjzt/0bx922y5bw+EFADzkz/LlfHRk7SQfELqI41iZFfNltyJCG WW2Cem85dnNxe2FtJSuAV42t+mSOVzMnSViJ62TXE+n5qxiXs6nmQyb5+v132AviUiAi GggiU5Ia2eHArhuLHkCDIc5QWCWNnOINpEJGHtFBQLL40Gdu8rH7XDhj6XMnOjYQUUPq Yf3890vLXg0+3B32K7tPEFY4mVP7iyMQ30QP0m/GHix9OMgTPI8doIum13QSTe/QP+pk 8Kug== X-Gm-Message-State: AOAM532to7ZOOFqLYMmXcqpcun41Z+1eDcM9KKLhqbFVNKP3keG1Ug+/ I2Hh9abZmAIdxbAdkIUii8Mj9ppaJbYXUqdUXLkLYhwtxkg= X-Google-Smtp-Source: ABdhPJyHW6myZAI4ejG8Wf2T1ir7FlAVA37IrOBlG4lESXsbZUD3XaMLGR54YDbEDAAcI2SmR2f5GIvoEbHKfJZp+Zg= X-Received: by 2002:a67:d289:: with SMTP id z9mr12520549vsi.39.1634877777828; Thu, 21 Oct 2021 21:42:57 -0700 (PDT) MIME-Version: 1.0 References: <20211009040533.chu7kqqk27r5wcok@oulala> In-Reply-To: <20211009040533.chu7kqqk27r5wcok@oulala> From: Kazuhiko Sakaguchi Date: Fri, 22 Oct 2021 13:42:46 +0900 Message-ID: To: Christophe Raffalli Cc: caml-list@inria.fr Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Subject: Re: [Caml-list] O(n ln k) sorting for ocaml on github and a challenge Reply-To: Kazuhiko Sakaguchi X-Loop: caml-list@inria.fr X-Sequence: 18607 Errors-To: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Help: List-Subscribe: List-Unsubscribe: List-Post: List-Owner: List-Archive: Archived-At: 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 he= re: https://github.com/pi8027/stablesort/blob/04a1441d36a379c31ea0221ace27ead1e= 93fc39e/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=E5=B9=B410=E6=9C=889=E6=97=A5(=E5=9C=9F) 13:06 Christophe Raffalli : > > 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 availa= ble 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 alway= s > faster than List.sort. Any ideas ? > > Cheers, > Christophe