[Haskell-cafe] natural mergesort in Data.List
Christian Sternagel
c.sternagel at gmail.com
Tue Sep 18 08:21:14 UTC 2018
Dear Cafe,
some years ago I formalized the mergesort implementation [1] from
http://hackage.haskell.org/package/base-4.11.1.0/docs/src/Data.OldList.html#sort
(as far as I can tell it didn't change since 2012) in the proof
assistant Isabelle/HOL [2].
More specifically, I proved its functional correctness (the result is
sorted and contains all elements of the input with exactly the same
multiplicities) and that it is a stable sorting algorithm.
Very recently I also formalized a complexity result in Isabelle/HOL,
namely that the number of comparisons is bounded from above by
n + n * ⌈log 2 n⌉
for lists of length n.
For this proof I had to change the definition of "sequences",
"ascending", and "descending" slightly.
Now here is my question: Does anyone now of reasons why the current
implementation of "sequences" is allowed to produce spurious empty lists
in its result? The version I used in my formalization only differs in
the following three spots:
sequences [x] = [[x]] -- this is the only important change, since
sequences [] = [] -- then the result does not contain empty lists
instead of
sequences xs = [xs]
and
ascending a as [] = let !x = as [a] in [x]
instead of
ascending a as bs = let !x = as [a] in x : sequences bs
and
descending a as [] = [a:as]
instead of
descending a as bs = (a:as) : sequences bs
[1] https://www.isa-afp.org/entries/Efficient-Mergesort.html
[2] http://isabelle.in.tum.de/
More information about the Haskell-Cafe
mailing list