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

4章のつづき。

** 証明アウトライン
 - コメント付きプログラム
   - 表明付きプログラムは、プログラムの前後に表明が
     付くだけであり、プログラムに混在して表明は書
     けない。
   - 証明の木では、プログラムの各コンポーネントの前後
     に表明がある。
   - そこで、証明の木の各コンポーネントの表明付き
     プログラムを証明の木の構造に従って合体して、
     プログラムと表明が混在したものを書いちゃえ、
     というアイデア。それをコメント付きプログラム
     と言う。
   - BNFで構文定義あり。ここに再掲はしない。
 - 証明の木からコメント付きプログラムを作るときのア
   ルゴリズムが掲載されている。これが、なんだかわか
   りにくい。間違っているのでは？と思って、他の記
   述を探したがなかなか見付からない。
 - ただ、実際に証明木からコメント付きプログラムを生
   成したり、変換したりするのは簡単であり、間違って
   いないようだ。実体は理解できているのかもしれな
   い。
 - 証明の木の全ての表明を含んでいるものを完全証明ア
   ウトライン、それから表明をさっぴいたものを証明ア
   ウトラインという。さっぴきかたにルールはない。
   さっぴきすぎると証明の木の復元が困難になる。

** プログラム変数と仕様変数
 - 代入文の左辺に表れる変数はプログラム変数。表れ
   ないのは仕様変数(論理変数とも)。
 - プログラム変数はR/W。仕様変数はRead Only。
 - 表明付きプログラムのプログラム本体部分の詳細が
   不明なときであっても、仕様変数が何であるかの情
   報があれば、表明の理解の助けになる。

** 整礎関係
 - well-founded : 基礎のしっかりした
 - 整礎関係の説明のところ、すっと入ってこない。私
   の頭が悪いのだろう。。。
 - Wikipedia: 無限降下列が存在しない2項関係を整礎関
   係と言う。
 - これはわかるこれをもとに自分なりに確認する。
 - 述語<は自然数において整礎関係である。
   x1<x0 ^ x2<x1 ^ x3<x2 ^ ... ^ xi+1<xi ^ ...
   i.e. <(x1,x0) ^ <(x2,x1) ^ <(x3,x2) ^ ...
   となる無限数列は存在しない。
 - 述語>は自然数において整礎関係ではない。
   x1>x0 ^ x2>x1 ^ x3>x2 ^ ... ^ xi+1>xi ^ ...
   i.e. >(x1,x0) ^ >(x2,x1) ^ >(x3,x2) ^ ...
   となる無限数列は存在しない。
 - これでよしとする。

** 整礎表明
 - 整礎表明の説明もすっと入ってこない。。。私の頭
   が悪いのだろう。
 - Web上でシンプルな説明をみつけた。これにて理解を
   試みる。
 - 。。。
 - だめだ。シンプルすぎる。

 - うーん。この完全ホーア理論の部分、どうもわかり
   にくいと思い調べてみると、説明に誤りがあるとか、
   不適切であるという指摘がWeb上に多少あった。
 - ホーア論理についての情報がこの本以外ではほとん
   どないのが現状。そこで巻末の参考文献をいくつか
   取り寄せることにした。
 - この部分はそれらの本が調達された後に再度チャレ
   ンジしようと思う。

こつこつ。