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

この本で以前示したように、空であるか、もしくは左と右の子がブラウンツリーでなおかつ左の子のサイズから右の子のサイズを引くと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 の型検査器に指示します; 節の右辺に嘘を書くのはプログラマの責務です。 上記のコード全体は オンライン から入手できます。