[Haskell-cafe] natural mergesort in Data.List
c.sternagel at gmail.com
Tue Sep 18 08:21:14 UTC 2018
some years ago I formalized the mergesort implementation  from
(as far as I can tell it didn't change since 2012) in the proof
assistant Isabelle/HOL .
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
sequences xs = [xs]
ascending a as  = let !x = as [a] in [x]
ascending a as bs = let !x = as [a] in x : sequences bs
descending a as  = [a:as]
descending a as bs = (a:as) : sequences bs
More information about the Haskell-Cafe