この記事では、2つの異なる基本的な種 bool と prop の関係の具体例を通じて、ATS の2つの定理証明のスタイルを示そうと思います。 この記事で用いるコード全体は bool-vs-prop.dats から入手できます。
例からはじめましょう。 関数 fib は次のようなフィボナッチ数を計算します:
fib(0) = 0 fib(1) = 1 fib(n+2) = fib(n) + fib(n+1) for n >= 0次のコードは上記に対する直接的な実装に ATS の関数を用いています:
fun fib ( n: int ) : int = if n >= 2 then fib (n-2) + fib (n-1) else n // end of [fib]明確に、これは時間複雑性の点で恐しく非効率な実装です。 C言語における fib の実装は線形の時間複雑性を持つ次のようなものです:
int fibc (int n) { int tmp, f0 = 0, f1 = 1 ; while (n-- > 0) { tmp = f1 ; f1 = f0 + f1 ; f0 = tmp ; } ; return f0 ; } // end of [fibc]もし ATS に翻訳するなら、関数 fibc は本質的に次のように実装できます:
fun fibc ( n: int ) : int = let fun loop (n: int, f0: int, f1: int) = if n > 0 then loop (n-1, f1, f0+f1) else f0 // end of [loop] in loop (n, 0, 1) end // end of [fibc]fib の定義と fibc で具体化された実装の間には、明らかに論理的ギャップがあります。
ATS では、fib の実装にこのギャップに対する橋をかけることができます。 そのおために、次のデータ命題の宣言で満たされるような fib の仕様を ATS にエンコードする必要があります。
// dataprop fib_p(int, int) = | fib_p_bas0(0, 0) of () | fib_p_bas1(1, 1) of () | {n:nat}{r0,r1:int} fib_p_ind2(n+2, r0+r1) of (fib_p(n, r0), fib_p(n+1, r1)) //fib_p は prop コンストラクタで、証明を表わす型 を意味することに注意してください。 2つの静的な整数項 N と R が与えられたとき、fib_p は fib(N) が R に等しいことを意味する prop fib_p(N, R) を作ります。
fib_p に相当する述語 fib_b があります:
// stacst fib_b : (int, int) -> bool //2つの静的な整数項 N と R が与えられたとき、bool 項 fib_b(N, R) は prop fib_p(N, R) に相当します。 また次の3つの証明関数は、fib_p に関連した3つの証明コンストラクタに相当します。
// // Note: unit_p is the unit prop // extern praxi fib_b_bas0() : [fib_b(0, 0)] unit_p extern praxi fib_b_bas1() : [fib_b(1, 1)] unit_p extern praxi fib_b_ind2 {n:nat}{r0,r1:int}(): [fib_b(n, r0)&&fib_b(n+1, r1) ->> fib_b(n+2, r0+r1)] unit_p //fib_b_ind2 に割り当てられたインターフェイスの構文には少し説明が必要でしょう: fib_b_ind2 は、あらゆる自然数 n と整数 r0 と r1 において、fib_b(n, r0) と fib_b(n+1, r1) を前提として fib_b(n+2, r0+r1) を主張する証明関数です。
次のコードは、上記で示した fib 関数の検証された実装です:
// extern fun f_fib_p {n:nat} (n: int(n)): [r:int] (fib_p(n, r) | int(r)) // implement f_fib_p{n}(n) = let // fun loop { i:nat | i < n } { r0,r1:int } ( pf0: fib_p(i, r0) , pf1: fib_p(i+1, r1) | i: int(i) , r0: int(r0), r1: int(r1) ) : [r:int] (fib_p(n,r) | int(r)) = let // in // if i+1 < n then loop(pf1, fib_p_ind2(pf0, pf1) | i+1, r1, r0+r1) else (pf1 | r1) // end // end of [loop] // prval pf0 = fib_p_bas0() prval pf1 = fib_p_bas1() // in if n >= 1 then loop(pf0, pf1 | 0, 0, 1) else (pf0 | 0) end // end of [f_fib_p] //f_fib_p のインターフェイスは、f_fib_p が自然数 n を取り、整数 r と prop fib_p(n, r) の証明のペアを返すことを示しています。 別の言い方をすると、自然数 n に対する f_fib_p 呼び出しの返り値は、常に fib の値に等しい整数になります。
f_fib_p の実装における定理証明のスタイルは、しばしば明示的なとか、明示的な証明の使用と呼ばれます。 ATS でサポートされる定理証明の別のスタイルは (明示的な証明を使わないので) 暗黙的と呼ばれることがあります。 例えば、次のコードは定理証明が暗黙的に行なわれた fib 関数の検証された別の実装です:
// extern fun f_fib_b {n:nat} (n: int(n)) : [r:int] (fib_b(n, r) && int(r)) // implement f_fib_b{n}(n) = let // prval() = $solver_assert(fib_b_bas0) prval() = $solver_assert(fib_b_bas1) // fun loop { i:nat | i < n } { r0,r1:int | fib_b(i,r0); fib_b(i+1,r1) } ( i: int(i) , r0: int(r0), r1: int(r1) ) : [r:int | fib_b(n,r)] int(r) = let // prval() = $solver_assert(fib_b_ind2{i}) // in // if i+1 < n then loop(i+1, r1, r0+r1) else r1 // end // end of [loop] // in if n >= 1 then loop(0, 0, 1) else 0 end // end of [f_fib_b] //キーワード $solver_assert を証明に適用することで、その証明の prop を (同じ意味の) 静的な bool 項に変化させ、その項を前提に追加することを表わします。 (この前提は同じスコープで生成された後続の制約を解決するのに制約ソルバよって使われます。) 1つ目と2つ目の $solver_assert 呼び出しは、それぞれ fib_b(0, 0) と fib_b(1, 1) を追加します。 3つ目は次の前提を追加します:
{r0,r1:int} fib_b(i, r0)&&fib_b(i+1, r1) ->> fib_b(i+2, r0+r1)これは、あらゆる整数ペア r0 と r1 においても、fib_b(i, r0) と fib_b(i+1, r1) を前提として fib_b(i+2, r0+r1) を主張しています。 i は自由変数で、ここでは量化されていないことに注意してください。
現時点では、f_fib_b の実装の型検査で生成される制約は ATS/Postiats のビルトインの制約ソルバでは解決できません。 1つの選択肢はそれらの制約をエクスポートして、それからコマンド patsolve_z3 を呼び出してそれらを解かせることです。 この patsolve_z3 は、ATS ソースコードを型検査して得られる制約を解決するために Z3 を使うユーティリティです。 より多くの例が Makefile に見つかります。
定理証明のスタイルはどちらが望ましいのでしょうか: 明示的?暗黙的? これは何を証明すべきかに依存しています。 個人的な意見では、後者は "簡単" に使うことでき、前者は "難解" であるということです。 熟練してから明示的な定理証明にはじめに挑戦するのを強く推奨します。