ATSプログラミング入門:
Prev	Chapter 11. ATS/LF を使った定理証明	Next

代数的なデータ種 (datasort)

データ種 (datasort) はデータ型 (datatype) に少し似ています。けれども、後者は ATS の動的な宣言ですが、前者は ATS の静的な宣言です。データ種の典型的な用途を見るために、 s と h がそれぞれ与えられた二分木のサイズと高さであるなら、s がきっちり 2^h より小さくなることを示す定理を ATS でエンコードしてみましょう。二分木を静的に表わすために、まず次のデータ種を宣言しましょう:

datasort tree = E of () | B of (tree, tree)

宣言したデータ種の名前は tree で、関連する2つのコンストラクタがあります: それは E と B で、E は空の木を作り、B は与えられた2つの木を結合した木を作ります。例えば、B(E(), E()) は種 tree の静的な項で、シングルトン木を表わしています。つまりノードが1つしかない木です。 E と B で作った木は全くデータを保持しない骨だけの木であることに注意してください。

次のように木のサイズと高さの概念を捕捉するために2つのデータ命題を宣言しましょう:

//
dataprop
SZ (tree, int) =
  | SZE (E (), 0) of ()
  | {tl,tr:tree}{sl,sr:nat}
    SZB (B (tl, tr), 1+sl+sr) of (SZ (tl, sl), SZ (tr, sr))
// end of [SZ]
//
dataprop
HT (tree, int) =
  | HTE (E (), 0) of ()
  | {tl,tr:tree}{hl,hr:nat}
    HTB (B (tl, tr), 1+max(hl,hr)) of (HT (tl, hl), HT (tr, hr))
// end of [HT]
//

木 t と整数 s が与えられた時、SZ(t, s) は t のサイズが s に等しいという関係をエンコードします。同様に、木 t と整数 h が与えられた時、HZ(t, h) は t の高さが h に等しいという関係をエンコードします。

2を底にした累乗関数は ATS の静的な部分にはないので、それを捕捉する次のデータ命題を宣言します:

dataprop
POW2 (int, int) =
  | POW2bas (0, 1)
  | {n:nat}{p:int} POW2ind (n+1, p+p) of POW2 (n, p)
// end of [POW2]

2つの整数 h と p が与えられた時、POW2 (h, p) は 2^h が p に等しいという関係をエンコードします。

s と h が与えられた二分木のサイズと高さである時、 s がきっちり 2^h より小さくなることを表わす定理を、次の証明関数のインターフェイスがエンコードしていることは明確でしょう:

prfun
lemma_tree_size_height
  {t:tree}{s,h:nat}{p:int}
(
  pf1: SZ (t, s), pf2: HT (t, h), pf3: POW2 (h, p)
) : [s < p] void // end of [prfun]

この証明関数の実装を次のようにコンストラクトしてみましょう。

はじめに、2を底にした累乗関数のいくつかの基本的な性質を作ります:

prfun
pow2_istot
  {h:nat} .<h>. (): [p:int] POW2 (h, p) =
  sif h==0
    then POW2bas () else POW2ind (pow2_istot {h-1} ())
  // end of [sif]
// end of [pow2_istot]

prfun
pow2_pos
  {h:nat}{p:int} .<h>.
  (pf: POW2 (h, p)): [p > 0] void =
  case+ pf of
  | POW2bas () => () | POW2ind (pf1) => pow2_pos (pf1)
// end of [pow2_pos]

prfun
pow2_inc
  {h1,h2:nat | h1 <= h2}{p1,p2:int} .<h2>.
  (pf1: POW2 (h1, p1), pf2: POW2 (h2, p2)): [p1 <= p2] void =
  case+ pf1 of
  | POW2bas () => pow2_pos (pf2)
  | POW2ind (pf11) => let
      prval POW2ind (pf21) = pf2 in pow2_inc (pf11, pf21)
    end // end of [POW2ind]
// end of [pow2_inc]

明確に、pow2_istot はデータ命題 POW2 にエンコードされた関係が全域な関係であることを表わしています; pow2_pos は自然数の累乗が正の数になることを証明しています; pow2_inc は累乗関数が単調増加であることを証明しています。

関数 lemma_tree_size_height は次のように実装できます:

primplement
lemma_tree_size_height
  (pf1, pf2, pf3) = let
//
prfun
lemma{t:tree}
  {s,h:nat}{p:int} .<t>.
(
  pf1: SZ (t, s)
, pf2: HT (t, h)
, pf3: POW2 (h, p)
) : [p > s] void =
(
  scase t of
  | E () => let
      prval SZE () = pf1
      prval HTE () = pf2
      prval POW2bas () = pf3
   in
     // nothing
   end // end of [E]
  | B (tl, tr) => let
      prval SZB (pf1l, pf1r) = pf1
      prval HTB {tl,tr}{hl,hr} (pf2l, pf2r) = pf2
      prval POW2ind (pf31) = pf3
      prval pf3l = pow2_istot {hl} ()
      prval pf3r = pow2_istot {hr} ()
      prval () = lemma (pf1l, pf2l, pf3l)
      prval () = lemma (pf1r, pf2r, pf3r)
      prval () = pow2_inc (pf3l, pf31)
      prval () = pow2_inc (pf3r, pf31)
    in
      // nothing
    end // end of [B]
) (* end of [lemma] *)
//
in
  lemma (pf1, pf2, pf3)
end // end of [lemma_tree_size_height]

内部の関数 lemma は、種 tree の静的な項で構成されている停止性メトリクスを持ちます。またこの関数は二分木 t に関連する構造的な帰納法の証明に対応しています。 2つの項 t1 と t2 が種 tree として与えられ、t1 が t2 より小さい構造であるなら、t1 はきっちり t2 より小さくなります。明らかに、これは根拠の確かな順序です。キーワード scase は (宣言されたデータ種に関連するコンストラクタで構築される) 静的な項のcase判定をする動的な式を作るのに使われます。そのため、sif と scase の関係は if と case の関係と同じです。上記のコード全体はオンラインから入手できます。

Prev	Home	Next
例: 乗法の交換法則	Up	例: ブラウンツリーの性質を確立する