情報証明論 第5章 ハードウェアの意味論的正しさ

第3節 場合の数が多すぎるときは証明を

目次


第1節 状態遷移方程式

 第2節 カウンタ回路の正しさ

 第3節 場合の数が多すぎるときは証明を


テスト

Logをみる

Back
 

第5章 ハードウェアの意味論的正しさ 第3節 場合の数が多すぎるときは証明を

 前節での手法は、場合の数が64個位でしたら適用できます。しかし例えば32bitのカウンターのような場合は現実的ではありません。そのようなときは、場合の数が多すぎるので、証明が必要になります。

 今まで紹介してきた手法は、Mizarを使っても、使用者が証明をしなければならない、ということはなく、単に式を記述してチェックするだけのものでした。

 この節では実際に証明をつける場合を紹介します。

 そのためには

 BINARITH

という名の論文(ファイル)が役立ちます。そこではn桁の2進数を

 Tuple of n,BOOLEAN

という型で表します。これは要素が0か1(Boolean値という)である、n次元のベクトルです。b が Tuple of n,BOOLEAN という型であるとき、b/.i というのは i番目の要素の値を表します。

 今Flip−Flopを32個あるいはそれ以上並べるとします。そして4bitのときと同じような結線をするとしましょう。各Flip−Flopの状態 s0,s1,s2,s3,...は一つの変数s で表せます。

 reserve s for Tuple of n,BOOLEAN

またand ゲートは n-1 個必要です。しかし1bit余計にとっておいて、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;

という3つの定理が証明できるはずです。

 TH1は、入力Tが0ならば、次の状態は変わらない、ということを言っています。

 TH2は、この3つの中で一番証明がむずかしいと思われるものです。Absvalというのは BINARITH の中で定義された関数で、n桁の2進数を、負で無い自然数に自然な方法で対応させるものです。このカウンターはその値がオール1のときを除いて入力Tが1なら次の状態の列の表す数(新カウント値)は、は前の状態の列が表す数(旧カウント値)に1を加えたものである、というまさにカウンタの機能を証明するものです。

 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;
しかしここまできて、結論式を直接証明するのはむずかしそうだ、と気づきます。一般のnについて証明するには多くの場合数学的帰納法を使わなければなりません。数学的帰納法はMizarでは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];

即ち,命題Pが0についていえることと、kについて言えれば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というのは命題Pを定義するものです。パラメータの型はNat、そのパラメータは右辺では$1(最初のパラメータという意味。2番目があれば$2)で表せます。

上の証明中でA3:とA4:のラベルの式2つを証明すれば先ほどのschemeが使えます。 A4:の式の証明はm

    A4: for m being Nat st P[m] holds P[m+1]
     proof let m be Nat;
      assume P[m];
       now per cases;
       case m=n;
       end;
       end;
      hence P[m+1];
     end;

 A4:の証明が終わらないうちに、全体の考え方がいいのかどうか、数学的帰納法を使った部分(A5:)を書き、それを使った結論式の証明も書いてみます。そしてMizarチェッカーにかけてみます。

 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];
       now per cases;
       case m                *4
       end;
       case m>=n;
        hence P[m+1];
::>                *4
       end;
       end;
      hence P[m+1];
     end;
    A5: for i being Nat holds P[i] from NAT_1:sch 1(A3,A4);
    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 by A5;
     end;
  end;

上では2つだけのエラーですので、全体としてはこの考え方でいいようです。

最終結果を示します。これはtrivdemoというようなMizarに添付された証明整形用のソフトを使って無駄な証明を取り除いたりしています(relprem,inacc,chklab,irrvoc,irrths も使って整形している)。

environ
 vocabulary MIDSP_3, MARGREL1, FINSEQ_4, GATE_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS,
      XCMPLX_0, XREAL_0, REAL_1, NAT_1, MARGREL1, FINSEQ_1, FINSEQ_2,
      FINSEQ_4, MIDSP_3, GATE_1, BINARITH;
 constructors MONOID_0 , FINSEQ_4 ,BINARITH;
 clusters INT_1, MARGREL1;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
 theorems AXIOMS,NAT_1,REAL_1;
 schemes NAT_1;

begin
reserve T for set;
reserve n for Nat;
reserve s,sp,a for Tuple of n,BOOLEAN;

 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  assume A0: ((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 by AXIOMS:22;then
    A3: P[0];
    A4: for m being Nat st P[m] holds P[m+1]
     proof let m be Nat;
      assume B0: P[m];then
       B1: for j being Nat st 1<=j & j<=n & j<=m holds sp/.j=0;
       now per cases;
       case C0: m=m+1;then
             C3: k=m+1 by D0,AXIOMS:21;
             C9: ($(sp/.(m+1)) iff $(s/.(m+1)) & not $(a/.(m+1))
              or not $(s/.(m+1)) & $(a/.(m+1))) &
                       ($(a/.(m+1+1)) iff $(s/.(m+1)) & $(a/.(m+1))) 
                       by A0,C5,C6b;
             now per cases;
             case C4: m>=1;
               C6: ($(sp/.m) iff
                 $(s/.m) & not $(a/.m) or not $(s/.m) & $(a/.m)) &
                       ($(a/.(m+1)) iff $(s/.m) & $(a/.m) )
                       by A0,C0,C4;
               C11: sp/.(m)=0 by B1,C4,C0;
               s/.(m+1)=1 by A0,C5,C6b;then
               C8b: $(s/.(m+1));
               C10: s/.(m)=1 by A0,C4,C0;then
               C8: $(s/.(m));
               C12: $(a/.(m+1)) iff $(a/.m) by C6,C10;
               $(a/.m) by C6,C11,C8;then
               $(a/.(m+1)) by C12;then
               not $(sp/.(m+1)) by C9,C8b;then
               sp/.(m+1)=0;
              hence sp/.k=0 by C3;
             end;
             case m<1;then m+1<=1 by NAT_1:38;then m+1<=0+1;then
               C5: m<=0 by REAL_1:53;
               m>=0 by NAT_1:18;then
               C13: m=0 by C5,AXIOMS:21;
               C14: $(sp/.1) iff not $(s/.1) by A0;
               0=n;
         hereby let k be Nat;
          assume D0: 1<=k & k<=n & k<=m+1;then k<=m by C0,AXIOMS:22;
          hence sp/.k=0 by B0,D0;
         end;
        hence P[m+1];
       end;
       end;
      hence P[m+1];
     end;
     for i being Nat holds P[i] from NAT_1:sch 1(A3,A4);
    hence for k being Nat st 1<=k & k<=n holds sp/.k=0;
  end;
C6b:の直後にherebyも使われています。

上の証明はこの種の証明として標準的なものですので、参考になると思います。

 とにかく何ビットであろうがこの種のカウンターは正しく動作するということが示されたわけです。勿論andゲートを何段も使っていますのでビットが多くなると信号の伝播遅れが生じ、実用にならなくなるでしょう。しかし回路の論理的構成としてはバグが無いことが証明されたのです。

 これは偉大なことなのです。デバッグはいかに多くのデータでチェックしてもその数はたかが知れているのです。「数学は無限を扱う学問である」という諺がありますが、無限でないまでも天文学的に大きな数でも扱えるのです。

 一般的な場合のアルゴリズム(回路を生成する)は貴重です。それは描画時にバグが混入し難い、ということを表します。このように上手に一般化することが適応範囲が広い上にバグの少ないシステムの制作に通じるのです。

 ただ、最初から一般化を狙ってもなかなかうまくいきません。ここでの説明でも4ビットのものから始めましたが、具体的なケースの考察はとても大切です。

 具体的なケースと一般化理論の間を上手に行き来できる技術者が求められています。