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

観変化のための証明関数

観変化 (view-change) という言いまわしは、関数を一連の観の証明に適用してそれらを別の観の証明に変換することを意味しています。この関数自身も証明関数なので、観変化それぞれに関連する実行時のコストはありません。例えば、どこかのアドレス L について駐観 int32@L の証明は4つの駐観: int8@L, int8@L+1, int8@L+2, int8@L+3 からなるタプルに変化できます。このとき int32 と int8 はそれぞれ32ビットと8ビット整数の型です。より興味深い観変化が証明関数としてそれぞれ定義されています。この章の残りではそのようないくつかの例を紹介します。

配列の添字操作を O(1) 時間で実装するには、1つの配列の観を2つの隣接した配列の観に変換する証明関数と、その逆の変換を行なう別の証明関数が必要です。形式的に言うと、次の2つの証明関数 array_v_split と array_v_unsplit を作る必要があるのです:

//
prfun
array_v_split
  {a:t@ype}
  {l:addr}{n,i:nat | i <= n}
(
  pfarr: array_v (a, l, n)
) : (array_v (a, i, l), array_v (a, n-i, l+i*sizeof(a)))
//
prfun
array_v_unsplit
  {a:t@ype}
  {l:addr}{n1,n2:nat}
(
  pf1arr: array_v (a, l, n1), pf2arr: array_v (a, l+n1*sizeof(a), n2)
) : array_v (a, l, n1+n2)
//

array_v_split の実装は次のように与えられます:

primplmnt
array_v_split
  {a}{l}{n,i}(pfarr) = let
  prfun split
    {l:addr}{n,i:nat | i <= n} .<i>.
  (
    pfarr: array_v (a, l, n)
  ) : (
    array_v (a, l, i)
  , array_v (a, l+i*sizeof(a), n-i)
  ) =
    sif i > 0 then let
      prval array_v_cons (pf1, pf2arr) = pfarr
      prval (pf1res1, pf1res2) = split{..}{n-1,i-1} (pf2arr)
    in
      (array_v_cons (pf1, pf1res1), pf1res2)
    end else let
      prval EQINT () = eqint_make{i,0}((*void*))
    in
      (array_v_nil (), pfarr)
    end // end of [sif]
in
  split (pfarr)
end // end of [array_v_split]

(implement の代わりに) キーワード primplement は証明関数の実装に使われることに注意してください。明確に、証明関数 split は数学的帰納法を使って証明を直接エンコードしています。 array_v_unsplit の実装を次に示します:

primplmnt
array_v_unsplit
  {a}{l}{n1,n2}
  (pf1arr, pf2arr) = let
  prfun unsplit
    {l:addr}{n1,n2:nat} .<n1>.
  (
    pf1arr: array_v (a, l, n1)
  , pf2arr: array_v (a, l+n1*sizeof(a), n2)
  ) : array_v (a, l, n1+n2) =
    sif n1 > 0 then let
      prval
      array_v_cons (pf1, pf1arr) = pf1arr
      prval pfres = unsplit (pf1arr, pf2arr)
    in
      array_v_cons (pf1, pfres)
    end else let
      prval array_v_nil () = pf1arr in pf2arr
    end // end of [sif]
in
  unsplit (pf1arr, pf2arr)
end // end of [array_v_unsplit]

証明関数 unsplit もまた数学的帰納法を用いて証明を直接エンコードしています。

ここで観変化を行なうより興味深い証明関数を見てみましょう。証明関数 array_v_takeout のインターフェイスは次のように与えられます:

//
prfun
array_v_takeout
  {a:t@ype}
  {l:addr}{n,i:nat | i < n}
(
  pfarr: array_v (a, l, n)
) : (a @ l+i*sizeof(a), a @ l+i*sizeof(a) -<lin,prf> array_v (a, l, n))
//

次の型は、駐観の証明を取り配列観の証明を返すような線形証明関数を表わすことに注意してください:

a @ l+i*sizeof(a) -<lin,prf> array_v (a, l, n)

そのような関数は1つ要素が欠けた配列を本質的に表わし、単純に array_v_takeout は配列の観を (1つの要素に対する) 駐観と配列の残りを表わす観に変更すると、表現することができます。 array_v_takeout を使うことで、arrget に別の実装を与えることができます:

implement
{a}(*tmp*)
arrget{l}{n,i}
  (pf | p, i) = x where {
  prval (pf1, fpf2) =
  array_v_takeout{a}{l}{n,i} (pf)
  val x = ptr_get1<a> (pf1 | ptr_add<a> (p, i))
  prval () = pf := fpf2 (pf1) // putting the cell and the rest together
} (* end of [arrget] *)

証明関数 array_v_takeout は次のように実装できます:

primplmnt
array_v_takeout
  {a}{l}{n,i}(pfarr) = let
  prfun takeout
    {l:addr}{n,i:nat | i < n} .<i>.
  (
    pfarr: array_v (a, l, n)
  ) : (
    a @ l+i*sizeof(a)
  , a @ l+i*sizeof(a) -<lin,prf> array_v (a, l, n)
  ) = let
    prval array_v_cons (pf1at, pf1arr) = pfarr
  in
    sif i > 0 then let
      prval (pfres, fpfres) = takeout{..}{n-1,i-1}(pf1arr)
    in
      (pfres, llam (pfres) => array_v_cons (pf1at, fpfres (pfres)))
    end else let
      prval EQINT () = eqint_make{i,0}((*void*))
    in
      (pf1at, llam (pf1at) => array_v_cons (pf1at, pf1arr))
    end // end of [sif]
  end // end of [takeout]
in
  takeout{l}{n,i}(pfarr)
end // end of [array_v_takeout]

llam は線形関数を作るキーワードであることに注意してください。線形関数が適用されるとそれは消費されてその内にリソースを作り、そしてもし未回収ならば、それが返す結果の中に移動します。

これまで示してきた観変化のための証明関数は全て配列観の操作でした。次のコードはこれらとは異なり、片方向リストを表わす2つの観を1つに結合するものと考えることができます:

//
prfun
slseg_v_unsplit
  {a:t@ype}
  {l1,l2,l3:addr}{n1,n2:nat}
(
  pf1lst: slseg_v (a, l1, l2, n1), pf2lst: slseg_v (a, l2, l3, n2)
) : slseg_v (a, l1, l3, n1+n2)
//

slseg_v_unsplit の型は、長さ N1 の L1 から L2 へのリスト片と長さ N2 の L2 から L3 への別のリスト片は、長さ N1+N2 の L1 から L3 へのリスト片であると考えることができることを本質的に表わしています。次の slseg_v_unsplit の実装は array_v_unsplit の実装とおおまかに類似しています:

primplmnt
slseg_v_unsplit
  {a}(pf1lst, pf2lst) = let
  prfun unsplit
    {l1,l2,l3:addr}{n1,n2:nat} .<n1>.
  (
    pf1lst: slseg_v (a, l1, l2, n1), pf2lst: slseg_v (a, l2, l3, n2)
  ) : slseg_v (a, l1, l3, n1+n2) =
    sif n1 > 0 then let
      prval slseg_v_cons (pf1at, pf1lst) = pf1lst
    in
      slseg_v_cons (pf1at, unsplit (pf1lst, pf2lst))
    end else let
      prval slseg_v_nil () = pf1lst in pf2lst
    end // end of [sif]
in
  unsplit (pf1lst, pf2lst)
end // end of [slseg_v_unsplit]

興味深くも slseg_v_unsplit を使って slist_ptr_append を実装できることに読者は気が付くかもしれえません。

オンラインのファイル array.dats と slist.dats からこの章で紹介したコードを入手できます。

Prev	Home	Next
片方向リストのデータ観	Up	線形データ型としてのデータ観型 (dataviewtype)