= Solution
Split the list into two contiguous halves, sort each recursively, and use the <merge algorithm> from part (a):
``
fun mergesort [] = []
| mergesort [x] = [x]
| mergesort xs =
let
val k = List.length xs div 2
val left = List.take (xs, k)
val right = List.drop (xs, k)
in
merge (mergesort left, mergesort right)
end;
``
`List.length` counts elements, `List.take(xs,k)` returns the first $k$ elements and `List.drop(xs,k)` returns the remaining suffix. Since $0<k<n$ when $n\ge2$, both recursive inputs are smaller and differ in length by at most one. <Mathematical induction> on length proves that each half is sorted without losing elements, and the correctness of the <merge algorithm> proves the same for the combined result. Contiguous splitting and left-biased equal-key merging preserve the original relative order of equal keys. \b[This is a stable top-down <merge sort>.]
Back to article page
