以前の章 implementation of mergesort on lists でコンストラクタ list0_nil と list0_cons を使ってリストのマージソートを実装しました。 この章では コンストラクタ list_nil と list_cons を使ってリストのマージソートを実装します。 この実装は以前の章と同じアルゴリズムを用いています。 しかし、長さを保持するよう関数を保証するために、実装したソート関数に型を割り当てます。 つまり、この関数はソートする前のリストと同じ長さのリストを常に返します。
次に定義する関数 merge は2つの整列済みリストを連結して1つの整列済みリストにします:
// typedef lte (a:t@ype) = (a, a) -> bool // fun{ a:t@ype } merge {m,n:nat} .<m+n>. ( xs0: list (a, m), ys0: list (a, n), lte: lte a ) : list (a, m+n) = case+ xs0 of | list_nil() => ys0 | list_cons(x, xs1) => ( case+ ys0 of | list_nil() => xs0 | list_cons(y, ys1) => if x lte y then list_cons (x, merge (xs1, ys0, lte)) else list_cons (y, merge (xs0, ys1, lte)) // end of [if] ) // end of [list_cons] // end of [merge] //
次に定義する関数 mergesort は与えられた順序付けでリストをマージソートします:
fun{ a:t@ype } mergesort{n:nat} ( xs: list (a, n), lte: lte a ) : list (a, n) = let // fun msort {n:nat} .<n,n>. ( xs: list (a, n), n: int n, lte: lte a ) : list (a, n) = if n >= 2 then split (xs, n, lte, half(n), list_nil) else xs // end of [if] // end of [msort] and split {n:int | n >= 2}{i:nat | i <= n/2} .<n,i>. ( xs: list (a, n-n/2+i) , n: int n, lte: lte a, i: int i, xsf: list (a, n/2-i) ) : list (a, n) = if i > 0 then let val+ list_cons (x, xs) = xs in split (xs, n, lte, i-1, list_cons (x, xsf)) end else let val n2 = half(n) val xsf = list_reverse<a> (xsf) // make sorting stable! val xsf = list_of_list_vt (xsf) // linear list -> nonlinear list val xsf = msort (xsf, n2, lte) and xs = msort (xs, n-n2, lte) in merge (xsf, xs, lte) end // end of [if] // end of [split] // in msort(xs, list_length<a>(xs), lte) end // end of [mergesort]
この章のコード全体と追加のテストコードは オンライン から入手できます。