【検証論】4 ホーア論理詳説 （その2）

** GCDプログラムの形式的証明を読む
 - 読みました。。。
 - 2ページ、証明的にいうと19行ですが、2時間かかり
   ました。。。
 - これは、慣れればかなり高速化が期待できますが、
   ホーア論理の専門家になるのでなければ、慣れるこ
   ともないように思います。
 - 読む際のヒントをいくつか。
   - 演算子優先度が普通に使われているので、Lisper
     な人は、はじめに表明について括弧を補完した方が
     読み易いです。
   - [c/b][b/a][a/c]というのは、いわゆる変数の値の
     スワップの表明代入版です。
   - 13行のb /= 0は誤植かと。正しくは¬b = 0です。

     
** 再び、ホーア論理を組み立てた後の話

 - 実際にGCDプログラムの証明を読んでみるとはっきり
   わかるのですが、ホーア論理の要は帰結規則です。

 - この帰結規則のところで、プログラムの正しさが、表
   明が含意でつなげるかどうか(検証条件)ということ次
   第である、という別れ目になります。

 - すなわち、プログラムの正しさが、論理の問題に変
   わるポイントなわけです。

 - で、帰結規則というのは、先日掲載したとおりSにて
   証明可能な検証条件は推論を進めてOKというものです。

 - で、Sは、ホーア論理構築時に作成した解釈Iのもと
   で正しい論理式の集合ということなので、なんのこ
   とはない、解釈Iで検証条件が正しいかどうかを確認
   することがやるべきことである。

 - なので、非論理的公理を解釈Iから構築する場合は、
   ホーア論理は、PV,AV,Iにて確定する。それゆえ、
   
     PHL(PV,AV,I) ≡PHL(PV,AV,{F| I |= F})
   
   と書くことにする。

 - ヒルベルトの形式的証明の方法は、行同士が参照し
   ている。これを図示すると木構造になる。

 - この木構造を「証明の木 (proof tree)」と言う。

 - 証明の木の葉を部品(コンポーネント)と言う。

 - 証明の木の節を部分プログラムと言う。

 - 証明の木の帰結規則でつながる部分を潰したものを
   「構文木 (syntax tree)」と言う。

こつこつ。