merge sort for array

Stream: general

[Asei Inoue]

variable {α : Type}
variable (le : α → α → Prop) [DecidableRel le]

local infixl:50 " ≼ " => le

def merge (xs ys : Array α) : Array α := Id.run do
  let mut i := 0
  let mut j := 0
  let mut result := Array.empty
  while h : i < xs.size && j < ys.size do
    have : i < xs.size := by grind
    have : j < ys.size := by grind
    if xs[i] ≼ ys[j] then
      result := (dbgTraceIfShared "at merge" result).push xs[i]
      i := i + 1
    else
      result := (dbgTraceIfShared "at merge" result).push ys[j]
      j := j + 1
  return result ++ xs.extract (start := i) ++ ys.extract (start := j)

#guard merge (fun x y : Nat => x ≤ y) #[] #[] = #[]
#guard merge (fun x y : Nat => x ≤ y) #[1, 2] #[] = #[1, 2]
#guard merge (fun x y : Nat => x ≤ y) #[] #[1, 2] = #[1, 2]
#guard merge (fun x y : Nat => x ≤ y) #[3, 4, 5] #[1, 2] = #[1, 2, 3, 4, 5]

def mergeSort (xs : Array α) : Array α := Id.run do
  if h : xs.size ≤ 1 then
    return xs
  else
    let mid := xs.size / 2
    let left := mergeSort <| (dbgTraceIfShared "at mergeSort" xs).extract (start := 0) (stop := mid)
    let right := mergeSort <| (dbgTraceIfShared "at mergeSort" xs).extract (start := mid) (stop := xs.size)
    return merge le left right

#guard mergeSort (fun x y : Nat => x ≤ y) #[1, 6, 2, 3, 4, 5, 7] = #[1, 2, 3, 4, 5, 6, 7]

def mergeSortOrd [Ord α] (xs : Array α) : Array α :=
  mergeSort (le := fun x y => (Ord.compare x y).isLE) xs

def getLines : IO (Array String) := do
  let stdin ← IO.getStdin
  let lines ← stdin.lines
  return lines

def mainUnique (process : Array String → Array String) : IO Unit := do
  let lines ← getLines
  for line in process lines do
    IO.println line

def mainShared (process : Array String → Array String) : IO Unit := do
  let lines ← getLines
  IO.println "--- Reversed lines: ---"
  for line in process lines do
    IO.println line

  IO.println ""
  IO.println "--- Original data: ---"
  for line in lines do
    IO.println line

def main (args : List String) : IO UInt32 := do
  match args with
  | ["--shared"] =>
    mainShared (process := mergeSortOrd)
    pure 0
  | ["--unique"] =>
    mainUnique (process := mergeSortOrd)
    pure 0
  | _ =>
    IO.println "Expected single argument, either \"--shared\" or \"--unique\""
    pure 1

[Asei Inoue]

When I run the mergeSort function implemented above, a lot of shared RCs are displayed.
How can I implement it in-place without making unnecessary copies of the array?

[Kim Morrison]

Implementing merge sort for arrays should probably not actually ever merge arrays. You should just be doing permutations in place in a fixed array (or maybe moving back and forth between two arrays), pretending that certain subarrays are the "arrays you are merging". You might look at the implementation of Array.qsort.

[Shreyas Srinivas]

Mergesort is not done in-place unlike quicksort.

[Shreyas Srinivas]

There are variations on merge sort that try to reduce space usage while retaining the O(n log n) complexity, but these are substantially different algorithms from an implementation standpoint.

[Kim Morrison]

Looking forward to seeing it. :-)

[Shreyas Srinivas]

Seeing what?

[(deleted)]

Yeah, merge sort has O(n) space complexity. It is my favorite algorithm. I think your algorithm is already as good as it can be.

[(deleted)]

You should consider implementing heap sort.

[(deleted)]

Sorry, just did a quick read. Looks like there's a way to just allocate 1 extra array for the merging process. So you don't have to allocate many small arrays and destroy them.

[Shreyas Srinivas]

Huỳnh Trần Khanh said:

Sorry, just did a quick read. Looks like there's a way to just allocate 1 extra array for the merging process. So you don't have to allocate many small arrays and destroy them.

This is true and it is still going to take O(n) extra space unlike docs#Array.qsort . @Asei Inoue you will definitely need one extra array. There are complicated variations on merge sort that would save you this extra space but some of those aren’t even technically called merge sort. See block sort or glide sort for example.

To be clear you can do a naive merge in-place in your merge sort but this algorithm is technically not merge sort and more concretely it will have O(n^2 log n) running time

[Kim Morrison]

Shreyas Srinivas said:

Seeing what?

An implementation of Array.mergeSort that is practical to run.

[Michael MacLeod]

If it's at all useful to anyone, here's an implementation of Array.mergeSort that only allocates one auxiliary array and does USize indexing instead of Nat indexing (for maximum performance.) It contains a termination proof and proofs that all array accesses are in-bounds [but no proof that it correctly sorts the array]. I'm not really that happy, though, with the length of the code. I think a lot could be done to improve it, especially since it was written before grind. I have been trying to rewrite it but progress has been slow and I have been sidetracked by needing to look for a job.

Some performance testing:
image.png

[Shreyas Srinivas]

Kim Morrison said:

Shreyas Srinivas said:

Seeing what?

An implementation of Array.mergeSort that is practical to run.

My point was that such an implementation wouldn’t be called merge sort. There are variants that accomplish reduction in extra space usage which have different names. I was confused by your suggestion of merging arrays in-place (especially the comparison with qsort). Textbook mergesort necessarily uses at least one extra array.

[Shreyas Srinivas]

I started a repository for implementing efficient sort procedures. I will push algorithms in pieces over time. Currently I have compiled a (most certainly incomplete) list of recent algorithms in roughly dependency order, so it really helps to follow the sequence. I have excluded timsort since powersort supercedes it. Most of the algorithms I have included in the list are either stable merge sort variants or hybrids of mergesort with quicksort variants and insertion sort.

PRs are always welcome.

Link : https://github.com/Shreyas4991/Sorting-in-Lean

[Shreyas Srinivas]

The goal is not to prove much but engineer algorithms that work best in lean. The algorithms in the list are not lean focussed. They have been implemented in C, rust, or python. But they might be good starting points. Suggestions welcome.

[Kim Morrison]

Nice!

One note: Array.qsort is implemented in Lean, not Mathlib. It also has a problem, that it is slow for already sorted lists, because it uses a pretty basic qsort algorithm. It is easy to fix at the algorithm level, less easy to replace the existing verification that qsort is correct (which, if I recall correctly, only lives in Lean's test suite rather than its library).

Fixing the implementation (e.g. splitting in three blocks, below the pivot, equal to the pivot, above the pivot) would be nice; I can dig up the code somewhere but it's pretty trivial. I would love to see this verified using the new monad verification framework.

[Kim Morrison]

Insertion sort is implemented in Mathlib in Mathlib.Data.List.Sort, and also proved correct and stable. It would be good to move this upstream to Lean at some point, because as you say it is a component of many fast algorithms.

[Kim Morrison]

Another great direction for the "work best in Lean" would be a tunable wrapper for qsort+insertion sort, which starts with qsort but drops to insertion sort below some length (often 4-8?). This tends to be the practical winner, if you can get insertion sort on fixed length very short lists/arrays to compile exactly as you want.