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

例: ブラウンツリーの性質を確立する

この本で以前示したように、空であるか、もしくは左と右の子がブラウンツリーでなおかつ左の子のサイズから右の子のサイズを引くと0もしくは1なら、そのような二分木はブラウンツリーです。形式的には、ブラウンツリーの概念を捕捉するために、次のデータ命題 isBraun を宣言できます:

dataprop
isBraun (tree) =
  | isBraunE (E) of ()
  | {tl,tr:tree}
    {sl,sr:nat | sr <= sl; sl <= sr + 1}
    isBraunB (
      B(tl, tr)) of (isBraun tl, isBraun tr, SZ (tl, sl), SZ (tr, sr)
    ) // end of [isBraunB]
// end of [isBraun]

与えられたどんなサイズのブラウンツリーも存在することをはじめに証明しましょう。この性質は ATS では次のようにエンコードできます:

prfun
lemma_existence{n:nat}(): [t:tree] (isBraun (t), SZ (t, n))

事実上、lemma_existence に割り当てられた型は t がブラウンツリーで t のサイズが n であるような自然数 n が与えられた時、木 t が存在することを意味しています。次のコードは lemma_existence の実装です:

primplement
lemma_existence
  {n}((*void*)) = let
//
prfun
lemma{n:nat} .<n>.
(
  // argless
) : [t:tree] (isBraun (t), SZ (t, n)) =
  sif n==0
    then (isBraunE (), SZE ())
    else let
      stadef nl = n / 2
      stadef nr = n - 1 - nl
      val (pfl1, pfl2) = lemma{nl}((*void*))
      and (pfr1, pfr2) = lemma{nr}((*void*))
    in
      (isBraunB (pfl1, pfr1, pfl2, pfr2), SZB (pfl2, pfr2))
    end // end of [else]
  // end of [sif]
//
in
  lemma{n}((*void*))
end // end of [lemma_existence]

stadef は、名前と (なんらかの種の) 静的な項の間に静的な束縛を導入するための ATS のキーワードであることに注意してください。もし望めば、このキーワードは typedef で置き換えることもできます (名前と種 t@ype の静的な項を束縛します)。

次に、同じサイズの2つのブラウンツリーが同一であることを示します。この性質は次のようにエンコードできます:

prfun
lemma_unicity
  {n:nat}{t1,t2:tree}
(
  pf1: isBraun t1, pf2: isBraun t2, pf3: SZ (t1, n), pf4: SZ (t2, n)
) : EQ (t1, t2) // end of [lemma_unicity]

EQ は次のデータ命題宣言で導入されている命題コンストラクタです:

dataprop EQ (tree, tree) =
  | EQE (E, E) of ()
  | {t1l,t1r:tree}{t2l,t2r:tree}
    EQB (B (t1l, t1r), B (t2l, t2r)) of (EQ (t1l, t2l), EQ (t1r, t2r))
// end of [EQ]

EQ が木の等式を帰納的に定義していることは明確です。証明関数 lemma_unicity の実装は次のようになります:

primplement
lemma_unicity
  (pf1, pf2, pf3, pf4) = let
  prfun lemma{n:nat}{t1,t2:tree} .<n>.
  (
    pf1: isBraun t1, pf2: isBraun t2, pf3: SZ (t1, n), pf4: SZ (t2, n)
  ) : EQ (t1, t2) =
    sif n==0
      then let
        prval SZE () = pf3 and SZE () = pf4
        prval isBraunE () = pf1 and isBraunE () = pf2
      in
        EQE ()
      end // end of [then]
      else let
        prval SZB (pf3l, pf3r) = pf3
        prval SZB (pf4l, pf4r) = pf4
        prval isBraunB (pf1l, pf1r, pf1lsz, pf1rsz) = pf1
        prval isBraunB (pf2l, pf2r, pf2lsz, pf2rsz) = pf2
        prval () = SZ_istot (pf1lsz, pf3l) and () = SZ_istot (pf1rsz, pf3r)
        prval () = SZ_istot (pf2lsz, pf4l) and () = SZ_istot (pf2rsz, pf4r)
        prval pfeql = lemma (pf1l, pf2l, pf3l, pf4l)
        prval pfeqr = lemma (pf1r, pf2r, pf3r, pf4r)
      in
        EQB (pfeql, pfeqr)
      end // end of [else]
    // end of [sif]
in
  lemma (pf1, pf2, pf3, pf4)
end // end of [lemma_unicity]

lemma_unicity のこの実装内の証明関数 SZ_istot は次のインターフェイスを持つことに注意してください:

prfun
SZ_istot{t:tree}{n1,n2:int}
  (pf1: SZ (t, n1), pf2: SZ (t, n2)): [n1==n2] void

これは SZ がその最初のパラメータに関して関数的な関係であることを単純に表わしています。つまり、SZ によって関係付けられた t と n があるとき、どのような t が与えられても高々1つの n が存在します。明確に、この実装に対応する数学的証明は与えられた2つの木 t1 と t2 のサイズ n に対する帰納法で証明されます。 n が 0 の基底部では、t1 と t2 は両方とも空の木なので等しくなります。 n > 0 の場合、帰納的に、それぞれ t1 と t2 の左の子のサイズである n1l と n2l が同じ値であることを証明します; 同様に、それぞれ t1 と t2 の右の子のサイズである n1r と n2r が同じ値であることを証明します; n1l について帰納法の仮定から、t1 と t2 の左の子は同じです; n1r について帰納法の仮定から、t1 と t2 の右の子は同じです; 木の等式の定義 (EQ にエンコードされています) から、t1 と t2 は同じです。

比較として、次のコードは lemma_unicity の別の実装ですが、少し独特のスタイルです:

primplement
lemma_unicity
  (pf1, pf2, pf3, pf4) = let
//
prfun
lemma{n:nat}{t1,t2:tree} .<t1>.
(
  pf1: isBraun t1, pf2: isBraun t2, pf3: SZ (t1, n), pf4: SZ (t2, n)
) : EQ (t1, t2) =
  case+ (pf1, pf2) of
//
  | (isBraunE (), isBraunE ()) => EQE ()
//
  | (isBraunB (pf11, pf12, pf13, pf14),
     isBraunB (pf21, pf22, pf23, pf24)) => let
//
      prval SZB (pf31, pf32) = pf3
      prval SZB (pf41, pf42) = pf4
//
      prval () = SZ_istot (pf13, pf31)
      prval () = SZ_istot (pf23, pf41)
//
      prval () = SZ_istot (pf14, pf32)
      prval () = SZ_istot (pf24, pf42)
//
      prval pfeq1 = lemma (pf11, pf21, pf31, pf41)
      prval pfeq2 = lemma (pf12, pf22, pf32, pf42)
    in
      EQB (pfeq1, pfeq2)
    end
//
  | (isBraunE _, isBraunB _) =/=>
    let prval SZE _ = pf3 and SZB _ = pf4 in (*none*) end
  | (isBraunB _, isBraunE _) =/=>
    let prval SZB _ = pf3 and SZE _ = pf4 in (*none*) end
//
in
  lemma (pf1, pf2, pf3, pf4)
end // end of [lemma_unicity]

この実装は与えられた木 t1 の構造に対する帰納法の証明に対応します。特殊記号 =/=> の使用に注意してください。これは ATS のキーワードで、パターンマッチに含まれる節が 到達不能 であることを ATS の型検査器に指示します; 節の右辺で偽を証明するのはプログラマの責務です。上記のコード全体はオンラインから入手できます。

Prev	Home	Next
代数的なデータ種 (datasort)	Up	プログラマ中心の定理証明