Effective ATS:
線形リストのソート

この記事では、線形リストをソートするためのマージソートの実装を紹介します。 配列のソートをするのにマージソートよりもクイックソートがしばしば好まれますが、リストのソートには前者が好まれます。 配列のソートにおいて、マージソートの深刻な弱点はマージ操作を行なうために (その配列のサイズに比例した) 追加のメモリが必要になってしまうことです。 リストに対するマージソートにこの弱点はありません。 マージソートのいくつかの強みは、それが安定なソートアルゴリズムであり、その (最悪) 時間的計算量が O(n(log(n)) であることです。

線形リストの抽象インターフェイス

ATS では、[list_vt] は片方向リスト (singly-linked list) を表わす dataviewtype (つまり線形のデータ型) として宣言されています。 けれども、私はここで [list_vt] を直接使いたくありません。 抽象的な線形リストをソートするマージソートの実装を作りたいのです。 そこで、まずはじめにこの実装で使う線形リストに対する抽象インターフェイスを導入します。

次のような2つの抽象型を導入します: 

absvtype mynode(l:addr) = ptr(l)
absvtype mylist(l:addr, n:int) = ptr(l)
NULL ではないアドレス L が与えられた時、型 [mynode(L)] は L に配置されたリストノードを表わします。 NULL ではないアドレス L と整数 N が与えられた時、型 [mylist(L, N)] は最初のノードが L に配置されるような長さ N のリストを表わします。 [mylist] のパラメータの性質は次の2つの証明関数によって捕捉されます: 
praxi
lemma_mylist_param
  {l:addr}{n:int}
  (xs: !mylist(l, n)): [l >= null; n >= 0] void
//
praxi
lemma_mylist_param2
  {l:addr}{n:int}
(
  xs: !mylist(l, n)
) : [(l==null && n==0) || (l > null && n > 0)] void
標準的な2つのリストのコンストラクタには次の型が割り当てられます: 
//
fun
mylist_nil ()
  : mylist(null, 0) = "mac#atspre_ptr_null"
//
fun{}
mylist_cons
  {l1,l2:addr}{n:nat}
(
  !mynode(l1) >> mylist(l1,n+1), mylist(l2, n)
) :<!wrt> void // end of [mylist_cons]
//
(1番目の引数である) ノードと (2番目の引数である) リストを繋げるために、[mylist_cons] がなんらかのメモリ割り当てをする必要があるのは明確です。 ときどき、与えられたノードとリストが既に繋がっていて、割り当てが不要なこともあるでしょう。 次の証明関数 [_mylist_cons] はそのような場合を正確に扱うために導入されています: 
//
prfun
_mylist_cons
  {l1,l2:addr}{n:nat}
(
  !mynode(l1) >> mylist(l1, n+1), mylist(l2, n)
) :<prf> void // end of [_mylist_cons]
//
また、[mylist_cons] の変形として [mylist_cons2] も導入されます: 
//
fun{}
mylist_cons2
  {l1,l2:addr}{n:nat}
  (x_hd: mynode(l1), xs_tl: mylist(l2, n)):<!wrt> mylist(l1, n+1)
//
[mylist] に対する、コンストラクタと正反対の動作をするデコンストラクタ (deconstructor) が次のように宣言されます: 
//
prfun
mylist_unnil
  {l:addr} (mylist(l,0)): void
//
fun{}
mylist_uncons
  {l:addr}
  {n:int | n > 0}
(
  xs: !mylist(l, n) >> mynode(l)
) : mylist(n-1) // end-of-fun
//
[mylist_unnil] と [mylist_uncons] の意味は、それらに割り当てられた型からすぐに推察できるでしょう。 [mylist_uncons] の変種として [mylist_uncons2] が次のように与えられます: 
//
fun{}
mylist_uncons2
  {l:addr}
  {n:int | n > 0}
  (xs: mylist(l, n)): (mynode(l), mylist(n-1))
//
[mylist] に対するこのコンストラクタとデコンストラクタの使い方を理解するために、与えられたリストの長さを計算する関数テンプレート [mylist_length] を実装してみましょう: 
//
fun{}
mylist_length{n:int} (xs: !mylist(n)): int(n)
//
[mylist] の具体的な表現が選択された後でのみ [mylist_cons] と [mylist_uncons] の実装は有効なので、[mylist_cons] もしくは [mylist_uncons] を呼び出す関数も当然コンパイルできません。 従って (そのインスタンスをコンパイルできるように) 関数テンプレートとして [mylist_length] を宣言することが重要になります。 [mylist_length] の実装は次のように与えられます: 
implement
{}(*tmp*)
mylist_length (xs) = let
//
fun loop
  {i,j:nat} .<i>.
(
  xs: !mylist(i), j: int(j)
) : int(i+j) =
if
isneqz (xs)
then let
  val xs2 = mylist_uncons (xs)
  val res = loop (xs2, j + 1)
  prval () = _mylist_cons (xs, xs2)
in
  res
end // end of [then]
else (j) // end of [else]
//
prval () = lemma_mylist_param (xs)
//
in
  loop (xs, 0)
end // end of [mylist_length]
記号 [isneqz] は次の関数でオーバーロードされていることに注意してください: 
fun
mylist_isnot_nil
  {l:addr}{n:int}
  (xs: !mylist(l,n)): bool(n > 0) = "mac#atspre_ptr_isnot_null"
ここで紹介した線形リストに対する抽象インターフェイスの全体は mylist.dats から入手できます。

抽象線形リストをソートするマージソート

次の関数テンプレート [mylist_mergesort] は (線形リストを表わす) mylist 値をマージソートします: 
fun{}
mylist_mergesort{n:int} (xs: mylist(n)): mylist(n)
また [mylist_mergesort] の実装は次のようになります: 
implement
{}(*tmp*)
mylist_mergesort
  (xs) = let
//
val n = mylist_length (xs)
//
in
  mylist_msort (xs, n)
end // end of [mylist_mergesort]
このとき [mylist_msort] は次の方で宣言されています: 
fun{}
mylist_msort{n:int}
  (xs: mylist(n), n: int(n)): mylist(n)
[mylist_msort] の実装は次のように与えられます: 
implement
{}(*tmp*)
mylist_msort
  (xs, n) = let
in
//
if n >= 2
  then let
//
    val n1 = half (n)
//
    val (xs1, xs2) = mylist_split (xs, n1)
//
    val xs1 = mylist_msort (xs1, n1)
    and xs2 = mylist_msort (xs2, n-n1)
//
  in
    mylist_merge (xs1, xs2)
  end // end of [then]
  else xs // end of [else]
// end of [if]
end // end of [mylist_msort]
このとき [mylist_split] はリストを2つに分割し、[mylist_merge] は2つのソート済みリストを1つのリストにマージします。

関数テンプレート [mylist_split] は次のように宣言されます: 

//
fun{}
mylist_split
  {n:int}{k:nat | k <= n}
  (xs: mylist(n), k: int(k)): (mylist(k), mylist(n-k))
//
また [mylist_split] の実装は次のようになります: 
implement
{}(*tmp*)
mylist_split
  (xs, k) = let
in
//
if
k = 0
then (mylist_nil (), xs)
else let
  val xs_tl =
    mylist_uncons (xs)
  val (xs1, xs2) =
    mylist_split (xs_tl, k-1)
in
  (mylist_cons2 (xs, xs1), xs2)
end // end of [else]
//
end // end of [mylist_split]

関数テンプレート [mylist_merge] は次のように宣言されます: 

//
fun{}
mylist_merge
  {n1,n2:int}
  (xs1: mylist(n1), xs2: mylist(n2)): mylist(n1+n2)
//
また次のコードは [mylist_merge] を実装しています: 
implement
{}(*tmp*)
mylist_merge
  (xs1, xs2) = let
//
prval () = lemma_mylist_param (xs1)
prval () = lemma_mylist_param (xs2)
//
in
//
if
isneqz(xs1)
then (
if
isneqz(xs2)
then let
  val xs1_tl = mylist_uncons (xs1)
  val xs2_tl = mylist_uncons (xs2)
  val sgn = compare_mynode_mynode (xs1, xs2)
in
  if sgn <= 0
    then let
      prval () = _mylist_cons (xs2, xs2_tl)
    in
      mylist_cons2 (xs1, mylist_merge (xs1_tl, xs2))
    end // end of [then]
    else let
      prval () = _mylist_cons (xs1, xs1_tl)
    in
      mylist_cons2 (xs2, mylist_merge (xs1, xs2_tl))
    end // end of [else]
end // end of [then]
else let
  prval () = mylist_unnil (xs2) in xs1
end // end of [else]
) (* end of [then] *)
else let
  prval () = mylist_unnil (xs1) in xs2
end // end of [else]
//
end // end of [mylist_merge]
[compare_mynode_mynode] は与えられた2つのリストノードに保存されている値を比較する関数テンプレートであることに注意してください。

ここでは [merge_split] と [mylist_merge] のどちらも末尾再帰関数として実装されていないことを指摘したいと思います。 ここでの主な目的はより受け入れやすい表現を得ることでした。 けれども、[merge_split] と [mylist_merge] 双方を末尾再帰関数で再実装することは興味深くやりがいのある課題でしょう。

ここで紹介した抽象線形リストに対するマージソートの実装の全体は mylist_mergesort.dats から入手できます。

片方向リストをソートするマージソート

具体的な表現のリストをマージソートするためには、その表現を用いて [mylist_cons] と [mylist_uncons] を実装する必要があります。 また、リストノードに一致する表現を用いて [compare_mynode_mynode] も実装する必要があります。

[mylist] を [list_vt] として解釈した場合については、mergesort_list_vt.dats を参照してください。 また、[mylist] を [sllist] として解釈した場合については、mergesort_sllist.dats を参照してください。

片方向リストのクイックソートについて

線形リストのクイックソートに興味のある読者には、次のファイルにあるコードから学習することをすすめます: 
mylist_quicklist.dats
quicksort_list_vt.dats
quicksort_sllist.dats
これらはここで紹介したマージソートの実装に沿っています。

この記事は Hongwei Xi によって書かれ、 Japan ATS User Group によって翻訳されています。