ATSプログラミング入門:
Prev	Chapter 14. 線形なデータ命題としてのデータ観 (dataview)	Next

片方向リストのデータ観

次のデータ観 slseg_v は片方向リストの部分の概念を捕捉しています:

dataview
slseg_v (
  a:t@ype+ // covariant argument
, addr(*beg*)
, addr(*end*)
, int(*length*)
) = // slseg_v
  | {l:addr}
    slseg_v_nil (a, l, l, 0) of ()
  | {l_fst:agz}{l_nxt,l_end:addr}{n:nat}
    slseg_v_cons (a, l_fst, l_end, n+1) of
      ((a, ptr l_nxt) @ l_fst, slseg_v (a, l_nxt, l_end, n))
// end of [slseg]_v

slseg_v に関連する2つの証明コンストラクタ slseg_v_nil と slseg_v_cons があり、それらに割り当てられた型は次のようになります:

//
slseg_v_nil :
  {a:t@ype}{l:addr} () -> slseg_v (a, l, l, 0)
//
slseg_v_cons :
  {a:t@ype}{l_fst:agz}{l_nxt,l_end:addr}{n:nat}
  ((a, ptr l_nxt) @ l_fst, slseg_v (a, l_nxt, l_end, n)) -> slseg_v (a, l_fst, l_end, n+1)
//

agz は NULL ではないアドレスのサブセット種であることに注意してください。型 T, 2つのアドレス L1 と L2, 自然数 N が与えられた時、観 slseg_v(T, L1, L2, N) は L1 からはじまり L2 で終わるような型 T の N 個の要素を含む片方向リストの部分を表わします。 L2 が NULL ポインタである場合、このリスト部分は次に形式的に定義されるリストと考えられます:

viewdef slist_v
  (a:t@ype, l:addr, n:int) = slseg_v (a, l, null, n)
// end of [slist_v]

型 T が与えられた時、L を指すポインタと自然数 N について観 slist_v(T, L, N) の証明は、C言語において次に宣言された構造体型 slist_struct へのポインタと本質的に同じです:

typedef
struct slist {
  T data ; /* [T] matches the corresponding type in ATS */
  struct slist *next ; /* pointing to the tail of the list */
} slist_struct ;

ここで片方向リストを使った単純な例を見てみましょう:

fn{a:t@ype}
slist_ptr_length
  {l:addr}{n:nat}
(
  pflst: !slist_v (a, l, n) | p: ptr l
) : int (n) = let
  fun loop
    {l:addr}{i,j:nat} .<i>.
  (
    pflst: !slist_v (a, l, i) | p: ptr l, j: int (j)
  ) : int (i+j) =
    if p > 0 then let
      prval slseg_v_cons (pfat, pf1lst) = pflst
      val res = loop (pf1lst | !p.1, j+1) // !p.1 points to the tail
      prval () = pflst := slseg_v_cons (pfat, pf1lst)
    in
      res
    end else let // the length of a null list is 0
      prval slseg_v_nil () = pflst in pflst := slseg_v_nil (); j
    end (* end of [if] *)
  // end of [loop]
in
  loop (pflst | p, 0)
end // end of [slist_ptr_length]

関数テンプレート slist_ptr_length は与えられた片方向リストの長さを計算します。内部の関数 loop が末尾再帰であることに注意してください。 slist_ptr_length の上記の実装はC言語における次の実装と本質的に一致します:

int
slist_ptr_length
(
  slist_struct *p
) {
  int res = 0 ;
  while (p != NULL) { res = res + 1 ; p = p->next ; }
  return res ;
} // end of [slist_ptr_length]

もう一つの例として、次の関数テンプレート slist_ptr_reverse は与えられた連結リストを逆順にします:

fn{a:t@ype}
slist_ptr_reverse
  {l:addr}{n:nat}
(
  pflst: slist_v (a, l, n) | p: ptr l
) : [l:addr] (slist_v (a, l, n) | ptr l) = let
  fun loop
    {n1,n2:nat}
    {l1,l2:addr} .<n1>. (
    pf1lst: slist_v (a, l1, n1)
  , pf2lst: slist_v (a, l2, n2)
  | p1: ptr l1, p2: ptr l2
  ) : [l:addr] (slist_v (a, l, n1+n2) | ptr l) =
    if p1 > 0 then let
      prval slseg_v_cons (pf1at, pf1lst) = pf1lst
      val p1_nxt = !p1.1
      val () = !p1.1 := p2
    in
      loop (pf1lst, slseg_v_cons (pf1at, pf2lst) | p1_nxt, p1)
    end else let
      prval slseg_v_nil () = pf1lst in (pf2lst | p2)
    end // end of [if]
in
  loop (pflst, slseg_v_nil | p, the_null_ptr)
end // end of [slist_ptr_reverse]

末尾再帰関数 loop を while ループに翻訳すれば、ATS における slist_ptr_reverse の実装を次のようなC言語の実装にたやすく変換できるでしょう:

slist_struct*
slist_ptr_reverse
(
  slist_struct *p
) {
  slist_struct *tmp, *res = NULL ;
  while (p != NULL) {
    tmp = p->next ; p->next = res ; res = p ; p = tmp ;
  }
  return res ;
} // end of [slist_ptr_reverse]

また別の例を見てみましょう。様々なリストにおいてリストの連結は共通した操作です。ここで、まずはじめにC言語でリストの連結を実装してみましょう:

slist_struct*
slist_ptr_append
  (slist_struct *p, slist_struct *q) {
  slist_struct *p1 = p ;
  if (p1 == NULL) return q ;
  while (p1->next != NULL) p1 = p1->next ; p1->next = q ;
  return p ;
} // end of [slist_ptr_append]

素直なアルゴリズムです。もし p が NULL だった場合、q が返されます。そうでなければ、はじめに p で指し示されたリストの最後のノードを見つけて、そのノードの next フィールドは q に置換されます。 C言語における slist_ptr_append のこの実装は、次のような ATS の実装に直接変換できます:

fn{a:t@ype}
slist_ptr_append
  {l1,l2:addr}{n1,n2:nat}
(
  pf1lst: slist_v (a, l1, n1)
, pf2lst: slist_v (a, l2, n2)
| p1: ptr l1, p2: ptr l2
) : [l:addr] (slist_v (a, l, n1+n2) | ptr l) = let
  fun loop
    {n1,n2:nat}
    {l1,l2:addr | l1 > null} .<n1>. (
    pf1lst: slist_v (a, l1, n1)
  , pf2lst: slist_v (a, l2, n2)
  | p1: ptr l1, p2: ptr l2
  ) : (slist_v (a, l1, n1+n2) | void) = let
    prval slseg_v_cons (pf1at, pf1lst) = pf1lst
    val p1_nxt = !p1.1
  in
    if p1_nxt > 0 then let
      val (pflst | ()) = loop (pf1lst, pf2lst | p1_nxt, p2)
    in
      (slseg_v_cons (pf1at, pflst) | ())
    end else let
      val () = !p1.1 := p2
      prval slseg_v_nil () = pf1lst
    in
      (slseg_v_cons (pf1at, pf2lst) | ())
    end (* end of [if] *)
  end // end of [loop]
in
  if p1 > 0 then let
    val (pflst | ()) = loop (pf1lst, pf2lst | p1, p2)
  in
    (pflst | p1)
  end else let
    prval slseg_v_nil () = pf1lst in (pf2lst | p2)
  end (* end of [if] *)
end // end of [slist_ptr_append]

上記の例では、ATS のコードがC言語の該当するコードよりも冗長であることは明らかです。けれども、前者は後者よりも次の点でより堅牢です: もし ATS のコードに小さな変更 (例: 識別子の名前変更、関数の引数の並べ替え) を加えた場合、変更したコードは型検査されておそらく型エラーが発生します。他方、C言語で書かれたコードについては同じことは起きません。例えば、次のようなC言語における slist_ptr_reverse の誤った実装はもちろん正しい型です:

/*
** This implementation is *incorrect* but type-correct:
*/
slist_struct*
slist_ptr_reverse
  (slist_struct *p)
{
  slist_struct *tmp, *res = NULL ;
  while (p != NULL) {
    tmp = p->next ; res = p ; p->next = res ; p = tmp ;
  }
  return res ;
} // end of [slist_ptr_reverse]

ここで宣言したデータ観 slseg_v はリストのノードを確保/解放する問題に対処していないことを指摘しておこうと思います。これは複雑な表現を避けることを意図しています。確保と解放を扱うような片方向リストのデータ観もまた ATS で宣言することができます。しかしデータ観型 (dataviewtype) で宣言することでそのようなリストをより使い易くすることができます。けれども、データ観は根本的にデータ観型よりも一般的で柔軟です。多くの一般的なデータ構造 (例: 双方向リスト) は ATS においてデータ観を用いてのみ適切に取り扱うことができます。

Prev	Home	Next
線形文字列のデータ観	Up	観変化のための証明関数