|
|
情報証明論 第５章 ハードウェアの意味論的正しさ
第３節 場合の数が多すぎるときは証明を |
|
目次
第１節 状態遷移方程式 第３節 場合の数が多すぎるときは証明を
|
前節での手法は、場合の数が６４個位でしたら適用できます。しかし例えば３２ｂｉｔのカウンターのような場合は現実的ではありません。そのようなときは、場合の数が多すぎるので、証明が必要になります。 今まで紹介してきた手法は、Ｍｉｚａｒを使っても、使用者が証明をしなければならない、ということはなく、単に式を記述してチェックするだけのものでした。 この節では実際に証明をつける場合を紹介します。 そのためには BINARITH という名の論文（ファイル）が役立ちます。そこではｎ桁の２進数を Tuple of n,BOOLEAN という型で表します。これは要素が０か１（Ｂｏｏｌｅａｎ値という）である、ｎ次元のベクトルです。b が Tuple of n,BOOLEAN という型であるとき、b/.i というのは i番目の要素の値を表します。 今Ｆｌｉｐ−Ｆｌｏｐを３２個あるいはそれ以上並べるとします。そして４ｂｉｔのときと同じような結線をするとしましょう。各Ｆｌｉｐ−Ｆｌｏｐの状態 s0,s1,s2,s3,...は一つの変数s で表せます。 reserve s for Tuple of n,BOOLEAN またand ゲートは n-1 個必要です。しかし１ｂｉｔ余計にとっておいて、a も Tuple of n,BOOLEAN という型をもつとした方が単純でいいでしょう。 次の状態はspという変数で表します。その型もsと同じです。すると
theorem TH1: not $T & ($(sp/.1) iff $(s/.1) & not $T or not $(s/.1) & $T) & ($(a/.1) iff $s/.1 & $T) & for i being Nat st 1<=i & i<=n holds ($(sp/.i) iff $(s/.i) & not $(a/.i) or not $(s/.i) & $(a/.i)) & ($(a/.(i+1)) iff $(s/.i) & $(a/.i)) implies s=sp; theorem TH2: ( not (for k being Nat st 1<=k & k<=n holds s/.k=1)& $T & ($(sp/.1) iff $(s/.1) & not $T or not $(s/.1) & $T) & ($(a/.1) iff $s/.1 & $T) & for i being Nat st 1<=i & i<=n holds ($(sp/.i) iff $(s/.i) & not $(a/.i) or not $(s/.i) & $(a/.i)) & ($(a/.(i+1)) iff $(s/.i) & $(a/.i)) ) implies Absval(sp)=Absval(s)+1; theorem TH3: ((for k being Nat st 1<=k & k<=n holds s/.k=1)& $T & ($(sp/.1) iff $(s/.1) & not $T or not $(s/.1) & $T) & ($(a/.1) iff $s/.1 & $T) & for i being Nat st 1<=i & i<=n holds ($(sp/.i) iff $(s/.i) & not $(a/.i) or not $(s/.i) & $(a/.i)) & ($(a/.(i+1)) iff $(s/.i) & $(a/.i)) ) implies for k being Nat st 1<=k & k<=n holds sp/.k=0; という３つの定理が証明できるはずです。 TH1は、入力Ｔが０ならば、次の状態は変わらない、ということを言っています。 TH2は、この３つの中で一番証明がむずかしいと思われるものです。Absvalというのは BINARITH の中で定義された関数で、ｎ桁の２進数を、負で無い自然数に自然な方法で対応させるものです。このカウンターはその値がオール１のときを除いて入力Ｔが１なら次の状態の列の表す数（新カウント値）は、は前の状態の列が表す数（旧カウント値）に１を加えたものである、というまさにカウンタの機能を証明するものです。 TH3 は旧カウント値が1111...1なら新カウント値は0000...0となる、というものです。 ここでは定理TH3 を証明してみましょう。 まずtheorem の命題の後に（セミコロンを取って）proof end; を付け加えます。このように必要なendは先に書いておいたほうが後で楽です。
theorem TH3: ((for k being Nat st 1<=k & k<=n holds s/.k=1)&
$T &
($(sp/.1) iff $(s/.1) & not $T or not $(s/.1) & $T) &
($(a/.1) iff $s/.1 & $T) &
for i being Nat st 1<=i & i<=n holds
($(sp/.i) iff $(s/.i) & not $(a/.i) or not $(s/.i) & $(a/.i)) &
($(a/.(i+1)) iff $(s/.i) & $(a/.i)) )
implies
for k being Nat st 1<=k & k<=n holds sp/.k=0
proof
end;
次に定理の命題の式そのものをproof と end の間にコピーします。
proof ((for k being Nat st 1<=k & k<=n holds s/.k=1)&
$T &
($(sp/.1) iff $(s/.1) & not $T or not $(s/.1) & $T) &
($(a/.1) iff $s/.1 & $T) &
for i being Nat st 1<=i & i<=n holds
($(sp/.i) iff $(s/.i) & not $(a/.i) or not $(s/.i) & $(a/.i)) &
($(a/.(i+1)) iff $(s/.i) & $(a/.i)) )
implies
for k being Nat st 1<=k & k<=n holds sp/.k=0
end;
ここで前提となる式の頭にassume をつけ、結論となる式の頭にthus かhence をつけます。もし全称記号が定理命題の全体にかかっているときは、for x being ...をlet x be ...をproof の後につけます。
proof assume ((for k being Nat st 1<=k & k<=n holds s/.k=1)&
$T &
($(sp/.1) iff $(s/.1) & not $T or not $(s/.1) & $T) &
($(a/.1) iff $s/.1 & $T) &
for i being Nat st 1<=i & i<=n holds
($(sp/.i) iff $(s/.i) & not $(a/.i) or not $(s/.i) & $(a/.i)) &
($(a/.(i+1)) iff $(s/.i) & $(a/.i)) );
thus for k being Nat st 1<=k & k<=n holds sp/.k=0;
end;
結論式に全称記号がついていますので、それを証明するのがいいと考え、そこにもproof end; を付けます。
proof assume ((for k being Nat st 1<=k & k<=n holds s/.k=1)&
$T &
($(sp/.1) iff $(s/.1) & not $T or not $(s/.1) & $T) &
($(a/.1) iff $s/.1 & $T) &
for i being Nat st 1<=i & i<=n holds
($(sp/.i) iff $(s/.i) & not $(a/.i) or not $(s/.i) & $(a/.i)) &
($(a/.(i+1)) iff $(s/.i) & $(a/.i)) );
thus for k being Nat st 1<=k & k<=n holds sp/.k=0
proof
end;
end;
またproof end; の中も次のように書きこみます。
proof assume ((for k being Nat st 1<=k & k<=n holds s/.k=1)&
$T &
($(sp/.1) iff $(s/.1) & not $T or not $(s/.1) & $T) &
($(a/.1) iff $s/.1 & $T) &
for i being Nat st 1<=i & i<=n holds
($(sp/.i) iff $(s/.i) & not $(a/.i) or not $(s/.i) & $(a/.i)) &
($(a/.(i+1)) iff $(s/.i) & $(a/.i)) );
thus for k being Nat st 1<=k & k<=n holds sp/.k=0
proof let k be Nat;
assume 1<=k & k<=n;
hence sp/.k=0;
end;
end;
しかしここまできて、結論式を直接証明するのはむずかしそうだ、と気づきます。一般のｎについて証明するには多くの場合数学的帰納法を使わなければなりません。数学的帰納法はＭｉｚａｒではscheme（スキーム）という概念で表現されます。schemeは一種の定理ですが、高階の述語論理（すべての命題について、というように述語変数としてより一般の変数を許す論理）を使わなければいけないような場合に使うものです。数学的帰納法に関するschemeはNAT_1 の中にあります。
scheme :: NAT_1:sch 1
Ind { P[Nat] } :
for k being Nat holds P[k]
provided
P[0] and
for k being Nat st P[k] holds P[k + 1];
即ち，命題Ｐが０についていえることと、ｋについて言えればｋ＋１について言える、ということから、全ての自然数について言える、ということです。
proof assume ((for k being Nat st 1<=k & k<=n holds s/.k=1)&
$T &
($(sp/.1) iff $(s/.1) & not $T or not $(s/.1) & $T) &
($(a/.1) iff $s/.1 & $T) &
for i being Nat st 1<=i & i<=n holds
($(sp/.i) iff $(s/.i) & not $(a/.i) or not $(s/.i) & $(a/.i)) &
($(a/.(i+1)) iff $(s/.i) & $(a/.i)) );
defpred P[Nat] means
for k being Nat st 1<=k & k<=n & k<=$1 holds sp/.k=0;
for k being Nat st 1<=k & k<=n & k<=0 holds sp/.k=0
proof let k be Nat;
assume B1: 1<=k & k<=n & k<=0;then
1<=0 by AXIOMS:22;
hence sp/.k=0;
end;then
A3: P[0];
A4: for m being Nat st P[m] holds P[m+1]
proof let m be Nat;
assume P[m];
hence P[m+1];
end;
thus for k being Nat st 1<=k & k<=n holds sp/.k=0;
end;
defpredというのは命題Ｐを定義するものです。パラメータの型はＮａｔ、そのパラメータは右辺では＄１（最初のパラメータという意味。２番目があれば＄２）で表せます。
上の証明中でＡ３：とＡ４：のラベルの式２つを証明すれば先ほどのschemeが使えます。 Ａ４：の式の証明はm
Ａ４：の証明が終わらないうちに、全体の考え方がいいのかどうか、数学的帰納法を使った部分（Ａ５：）を書き、それを使った結論式の証明も書いてみます。そしてＭｉｚａｒチェッカーにかけてみます。
上では２つだけのエラーですので、全体としてはこの考え方でいいようです。
最終結果を示します。これはtrivdemoというようなＭｉｚａｒに添付された証明整形用のソフトを使って無駄な証明を取り除いたりしています（relprem,inacc,chklab,irrvoc,irrths も使って整形している）。
上の証明はこの種の証明として標準的なものですので、参考になると思います。
とにかく何ビットであろうがこの種のカウンターは正しく動作するということが示されたわけです。勿論andゲートを何段も使っていますのでビットが多くなると信号の伝播遅れが生じ、実用にならなくなるでしょう。しかし回路の論理的構成としてはバグが無いことが証明されたのです。
これは偉大なことなのです。デバッグはいかに多くのデータでチェックしてもその数はたかが知れているのです。「数学は無限を扱う学問である」という諺がありますが、無限でないまでも天文学的に大きな数でも扱えるのです。
一般的な場合のアルゴリズム（回路を生成する）は貴重です。それは描画時にバグが混入し難い、ということを表します。このように上手に一般化することが適応範囲が広い上にバグの少ないシステムの制作に通じるのです。
ただ、最初から一般化を狙ってもなかなかうまくいきません。ここでの説明でも４ビットのものから始めましたが、具体的なケースの考察はとても大切です。
具体的なケースと一般化理論の間を上手に行き来できる技術者が求められています。
|