まず、4章は充填率が高いというか、手加減がないというか、前章で作った用語が入り乱れて記述されているので、刻んで読んでいくことすら難しい。なので自分なりにいろいろ展開して見える化しないと、私はとても理解できなかった。展開したものをここに書く。読書メモじゃなくて、そういうものなので、誤りを含んでいる可能性も高いと思う。
* 4 ホーア論理詳説
自分なりのポイントを自分なりに書く。
まず、ホーア論理を理解するために形式的理論を振り返っ
てみる。
** 形式的理論の骨組
形式的理論の骨組をできるだけシンプルに書く。
形式的理論を組み立てていく標準的な順番に沿って書く。
一階述語論理とする。
- 語彙を決める。
- 変数
- 定数
- 関数記号
- 記号
- アリティ
- 述語記号
- 記号
- アリティ
- 論理記号
整理の関係でここに書いたが論理記号は汎用的に
決まっているのでそれをそのまま採用するだけ。
- 構文を決める。
- 無手勝流 (自分で決める)
- 項の構文
- 論理式の構文
- 一階述語論理 (汎用的に決まっている)
- 項の構文
- 論理式の構文
- 語彙の解釈を決める。
- 真理値集合：{True,False}が存在するとする。こ
れはお約束。
- 領域：領域を決める。
- 定数：領域の要素と定数を紐付ける。
- 関数記号：領域上の関数と関数記号を紐付ける。
- 述語記号：領域上の述語と述語記号を紐付ける。
- 述語記号"="は必ず領域における等価関数に紐付
けること。
- 形式的理論の公理を決める。
ここがAIMAと違う。AIMAはこれらを伴意と真理値表
から導き出す。プログラム検証論は公理として与え
る。
- 公理(I群) (論理的公理)
- これは、一階述語論理としては確定している。お
約束。
- 公理(II群) (非論理的公理)
- これは、今構築している内容に合わせて定義す
る。これは構文で許される範囲で、理論を構築
するものが自由に選ぶものである。自由に選ぶ
というのは、この時点では特定の解釈との整合
性は求められていないから。それは理論を作っ
た後の検査課題である。
- 推論規則
- これは一階述語論理としては確定している。お約
束。
- 形式的証明の方法を決める。
- プログラム検証論ではヒルベルトの方法を採用し
ている。
- 他に自然演繹などがある。
** 形式的理論のトピック
前項で形式的理論の骨組が整理できた。ここでは、この
上でどのようなトピックがあるのか、列記する。
- 環境と項の解釈
- 項の解釈には環境を使う。
- 論理式Aは解釈Iと環境pに対して正しい、ということ
を、
I,p |= A
と書く。
- 論理式Aは解釈Iと任意の環境に対して正しい(伴意?)
ということを、
I |= A
と書く。
- トートロジー。任意の解釈Iに対して I |= A が成立
するとき、Aをトートロジーと呼ぶ。
- 形式的に証明可能
- 形式的理論Tにおいて、形式的証明によって論理式
を証明できたとき、
T |- その論理式
と書く。
- 形式的理論Tが解釈Iにおいて完全性と持つというこ
とは、
任意の論理式Fに対して、I |= F ならば、T |- F と
なる
ということである。すなわち意味論としての正しさ
があるものは、統語論としての正しさも証明できる
ことが保証されているということ。
- 形式的理論Tが解釈Iに対して健全であるとは、
任意の論理式Fに対して、T |- F ならば、I |= F と
なる
ということである。すなわち統語論をベースに証明
されたものは、意味論としても正しい、ことが保証
されているということ。
- 形式的理論として一階述語論理を採用した場合
- 次の2つのことが重要。
- 一階述語論理の論理的公理はすべてトートロジー
である。
- 一階述語論理の推論規則は、前提が真ならば結論
も真である。
- これらゆえ、次が言える。
- 一階述語論理に基づく形式的理論Tが解釈Iに対し
て健全である必要十分条件は、Tの非論理的公理
のすべてにてついて(今そのひとつをFとする)に
対して、I |= Fが成り立つことである。
- 一階述語論理自身の健全性と完全性
- 一階述語論理をつかって作った形式的理論の健全
性/完全性と、一階述語論理自身の健全性/完全性
とは別の概念である。
- 一階述語論理の健全性とは、一階述語論理の公理
およびそれから推論される論理式(定理)はすべて
トートロジである、ということ。
- 一階述語論理の完全性とは、 一階述語論理の定理
の証明は、一階述語論理以外の情報を必要としな
い、ということ。
- ゲーデルの不完全性定理
形式的理論が次のふたつを満すならば、それが健全
かつ完全となるような解釈は存在しない。
- 自然数の理論を含む。
- 論理式が非論理的公理であるかどうかを決定可能
(turing decidable)である。
** 形式的理論としてホーア論理を組み立てる
前項の一階述語論理の組み立てを頭のすみにおきつつ、
ホーア論理を形式的に組み立てる。
前置きを少々。部分正当性ホーア論理をPHL、完全正当
性ホーア論理をTHLと書く。ここではPHLをやる。結論か
ら先に言うと、PHLを決めるということは、PV,AV,Sを決
めるということにほぼ等しい。よって、特定化されたホー
ア論理のことをPHL(PV,AV,S)と書く。
- ホーア論理の語彙を決める。
- プログラムの語彙(PV)を決める。
- ただし、プログラムの語彙の論理記号は限量子
を含まない。
- これは、ユニークなものではない。すなわち、
いろいろなPVを考えることができて、それぞれ
がそのプログラミング言語の(を使った)ホーア
論理となる。
- 実践的に言うと、プログラムの語彙は、2つの部
分で構成される。ひとつは数やそれに関する関数
記号/述語記号を定めるもの。もうひとつは、そ
れらを組み込みつつプログラムを表現するための
プログラミング言語を定めるもの。例えば、整数
に関する問題しか解かなないのであれば、前者は
整数の語彙を採用する。例えば、浮動小数点数に
関する問題を解くならば、浮動小数点の語彙を採
用する。どちらでもプログラミング言語は同じも
の、というのもありえる。また、前者が同じだが、
プログラミング言語がPascal 風であったりLisp
風であったりいう形で、トータルでは別のもので
あることもある。
- 表明の語彙(AV)を決める。
- AVはPVの拡張でなければならない。
- AVの変数記号はPVと同じでなければならない。
- ホーア論理の構文を決める。
- プログラムの構文を決める。
- 項の構文を決める。これが式となる。
- 論理式の構文を決める。これがブール式となる。
- 表明の構文を決める。
- 表明付きプログラムの構文を決める。
- 表明の非論理的公理を決める。
- これは、あたりまえだが、AVを語彙とする論理式の
集合Fml(AV)の部分集合である。それをSと呼ぶ。
- 非論理的公理は表明付きプログラムの前後部分に
ある表明を指定するために使われる。
- 非論理的公理は、公理といいつつ、解釈まで降り
ていって決める。
- 推論規則を決める。
- 形式的証明の方法は決まっている。
- 次のものに固定されているようだ。
---
ホーア論理の形式的証明
PHL(PV,AV,S)が特定されているとする。そのPHLにおけ
る形式的証明とは、行番号、表明付きプログラムAP、コ
メントCからなる行を並べたもので、次の条件を満たす
ものをいう。
1. i行目のコメントCiが公理の番号であるとき、その行
の表明付きプログラムAPiはその公理である。
2. i行目のコメントCiが推論規則の番号と数の列
R,j1,...,jmであるときは、j1,...,jm < i であり、
APj1,...,APjm
---------------
APi
が、その推論規則Rとなる。
---
- ここまでで統語論の構築が完了。これに続き意味論の
構築が存在する。(それは次章のようだ)
** とあるホーア論理をこの手順に従って組み立ててみる
GCDプログラムの検証につかえるホーア論理を構築する。
ここでは統語論を扱う。(意味論的なことも、ちょろっ
と出てくる)
- ホーア論理の語彙を決める。
- プログラムの語彙(PV)を決める。
---
整数の語彙(VZ)
変数：a,b,c,aa,ac,a0,b01,ac123,... .
定数：0,1.
関数記号：+,*,-.mod.
述語記号：=,<=.
---
- ただし、プログラムの語彙の論理記号は限量子
を含まない。
- アリティはすべて2。
- 表明の語彙(AV)を決める。
- AVはPVの拡張でなければならない。
---
AVはPVに次の語彙を加えたものとする。
関数記号：gcd,abs.
述語記号：<.
gcd,<はアリティ2。absはアリティ1。
---
- ホーア論理の構文を決める。
- プログラムの構文を決める。
- 項の構文を決める。これが式となる。
- 論理式の構文を決める。これがブール式となる。
---
Term(PV)、Fml(PV)は一階述語論理の項の統語論を採用する。
---
---
プログラミング言語 Min(PV)
変数 ::= 語彙PVの変数.
式 ::= Term(PV)の項.
ブール式 ::= Fml(PV)の原子論理式 | ブール式 ^ ブール式 |
ブール式 v ブール式 | ブール式 => ブール式 |
¬ブール式.
文 ::= skip | 変数 := 式 | begin 文 { ";" 文 } end |
if ブール式 then 文 else 文 fi |
while ブール式 do 文 od.
プログラム ::= 文.
---
- 余談：ここで、beginとかifとかはあくまでプログ
ラミング言語の構文要素であり、式ではない！ 非
Lisp系の言語にてどういう事情や文脈にて式ではな
い構文要素が出てくるのだろうかとモヤモヤしてい
たが、ここでの出現は、その必然性をこの文脈にお
いて感じさせるものだ。この気づきはありがたい。
---
PHL(PV,AV,S)の公理と推論規則
公理
Aas(代入文の公理)
{A[t/x]} x := t {A}
Ask(スキップ文の公理)
{A} skip {A}
推論規則
Rif(条件文の規則)
{C^A}P{B} {¬C^A}Q{B}
-----------------------------
{A} if C then P else Q fi {B}
Rwh(while文の規則)
{C^A}P{A}
-----------------------------
{A} while C do P od {¬C ^ A}
Rcp(複合文の規則)
{A}P1{S1}...{Sn-1}Pn{B}
-----------------------------
{A} begin P1;...; Pn end {B}
Rcs(帰結規則)
{B}P{C}
---------
{A}P{D}
ただし、S |- A => B かつ S |- C => D であるとする。
---
- 表明の構文を決める。
- 表明付きプログラムの構文を決める。
---
表明と表明付きプログラムの定義
表明 ::= Fml(AV)の論理式.
表明付きプログラム ::= "{" 表明 "}" プログラム "{" 表明 "}".
ただし、Term(AV),Fml(AV)については一階述語論理の項
の統語論を採用する。
---
- 表明の非論理的公理を決める。
- これは、あたりまえだが、AVを語彙とする論理式の
集合Fml(AV)の部分集合である。それをSと呼ぶ。
- 非論理的公理は表明付きプログラムの前後部分に
ある表明を指定するために使われる。
- 非論理的公理は、公理といいつつ、解釈まで降り
ていって決める。
---
まず、PVの語彙の解釈を決める。
領域: D=N.Nは自然数の集合を表す。
定数: I[0]=0, I[1]=1.
関数記号: I[+]="+", I[*]="*",
I[mod](a,b) =
0 b = 0のとき
aをbで割ったときの余り それ以外のとき.
述語記号: I[=]="=", I[<=],
次に、これをベースにAVで追加したものの解釈を決める。
これでAVの解釈が構築完了となる。
関数記号:
I[gcd](a,b) =
0 a=b=0であるとき
aとbの最大公約数 それ以外のとき.
I[abs](a) = aの絶対値
I[<](a,b) =
True a < bであるとき
False それ以外のとき
最後に非論理的公理を決める。これは、この解釈にて正
しい論理式全てである。集合表記すると次のとおり。
{F| I |= F}
これをSと呼ぶ。
---
** ホーア論理を組み立てた後の話
- ここまで組み立てるとP90にあるGCDプログラムの形
式的証明をすんなり読むことができる。
これ以降は後日。
こつこつ。
