2009年8月1日土曜日

【検証論】5 ホーア論理の数学 (その4)


**** whileについて考える

- 形式的理論の構築に沿って、whileの理解を深めてみ
たい。
- まず、ホーア論理の言語の構成部品のひとつである
プログラムの文法を定める。それをプログラミング
言語Minと呼ぶ。Minの中でwhile構文が定義されてい
る。
- 定義はこのとおり。

文 ::= while ブール式 do 文 od.

文となるものはこの他にもあるが抜き出して書いた。

- 続いて推論規則の定義にwhileが表れる。

Rwh(while文の規則)
{C^A}P{A}
----------------------------
{A} while C do P od {¬C^A}

- 推論規則は形式的証明に使うものであり、第一義に
は意味は無い。このような形の変形が許されるとい
うことだけだ。もちろん、この形の変形を推論規則
に選んだことに、意味論を見越した意図や狙いはあ
るのだが、今は分離して進める。
- しかし、この規則、不思議な形をしているよなぁ。
- ここまでが統語論と証明論?。

- 続いて意味論。
- まずラベル付きプログラムを導入する。その文法を
定義する。その中にwhileが表れる。

<A> ::= ラベル ":" while ブール式 do <A> od ラベル ":".

ラベルは他の語彙と衝突せず相互に識別できて無限個
あるなら何でもよくて、ここではl0,l1,...とする。
- あるプログラムPの意味を考えるときは、そのままで
は駄目であり、それをラベル付きプログラムに変換
するという手順。
- プログラムの意味というのは、このラベルをカウン
タが移動していくにあたってどういう風に状態が変
わるの、ということで数学的に形式化される。
- なので、Min言語の意味論とは、Min言語の文のラベ
ル付きのものにおいて、ラベルと状態(あわせて状況)が
どのように遷移するかを定義することにあたる。そ
こで、whileはどうなっているかというと、次のよう。
- ラベル付きプログラム

l0 : while C do l1 : P l2 : od l3 :

を考える。状況をと表し、初期状況を<p,l0>と
する。IPpを、「環境pにおけるプログラムの語彙PVに
対する解釈」を表す記号とする。

するとこのラベル付きプログラムの意味論は次のよ
うになる。

- <p,l0> (初期状況)
- l0からの遷移。while構文が統制している。
- IPp[C]がTrueならば、<p,l1>に遷移する。
- IPp[C]がFalseならば、<p,l3>に遷移する。
- l1からの遷移。
- <p,l1>を初期状態といて、Pの実行に入る。
- Pの実行が終わると、状態の詳細はPの内容により
けりだがいずれにしてもなんらなかの状態にな
るのでそれをp'とする。すると状況は、<p',l2>
となる。
- l2からの遷移。
- 状態を維持したままカウンタをl0にする。l1か
らの流れでいうと、状況は<p',l0>となる。
- ふむ。これはnaiveな定義だな。
- 続いて、実行関係というものを導入する。
- 実行関係とは何か。
- ここで採用している意味論においては、プログラム
の結果というのは、もしくはプログラムの実行の結
果または効果というは状態の変化しか無い。実行に
おいては、プログラムカウンタが構文に従って動き
回るということがおこるが、それは過程であって、
結果には結びつかない。(もちろんリアルな言語で副
作用がある場合は、そのプログラムカウンタの移動
に付随して別の結果をもたらすこともある)
- なので、プログラムPによって状態pが状態p'になっ
た、ということは、プログラムカウンタの動きの子
細を省きつつ、このプログラムの意味(論)を捉えて
いる。そこでこれを、

Exec(P,p,p')

と書き、実行関係と呼ぶ。これを実行関係というのは、
このExecを述語と捉えれば、Exec(P,a,b)がTrueなら
ば、aとbはPの実行関係であり、FalseならaとbはPの
実行関係ではない、などと運用できるからだ。

- では、Min言語の基本的な構文達の実行関係とはどの
ようなものかという興味がわく。すなわちプログラ
ムPにたいしてExec(P,a,b)がTrueとなるaとbの関係
というのは論理式であらわすとどうなるかというこ
とだ。
- ここでwhileの実行関係の特徴付け、がでてくる。
それが、

---
次のものを満すような、m(>=1)と、状態の列
p1,...,pmが存在する

(p=p1)^(p'=pm)^(I,pm /|= C) ^
(すべてのi(<m)について次のことが成り立つ ((I,pi |= C ^ ExecI(P,pi,pi+1))))
---

これ。
- これ、よく見ると、さっきwhileのラベル付きプログ
ラムの意味(論)でプログラムの実行を遷移で追いま
したが、それを論理式で書いただけですね。

- 閑話休題。

*** 5.2.1 健全性 (つづき)
- さて、while文がわかったので、つづき。

任意の状態p,p'について、

I,p |= A => Exec[I'](while C do P od,p,p') => I,p' |= {¬C ^ A}

が真である

ということが示すべきことであり、数学的帰納法を
やっているので、

I |= {C^A}P{A}

は真としてよいということであった。

- 整理すると、前提として、

I |= {C^A}P{A}
I,p |= A
Exec[I'](while C do P od,p,p')

が成立するときに、

I,p' |= {¬C ^ A}

が成立することを示せばよいことになる。

- Execの詳細に着目しよう。

次のものを満すような、m(>=1)と、状態の列
p1,...,pmが存在する

(p=p1)^(p'=pm)^(I,pm /|= C) ^
(すべてのi(<m)について次のことが成り立つ ((I,pi |= C ^ ExecI(P,pi,pi+1))))

であり、p=p1とp'=pmは覚えておくことにすると、

(I,pm /|= C) ^
(すべてのi(<m)について次のことが成り立つ ((I,pi |= C ^ ExecI(P,pi,pi+1))))

となる。

(I,pm /|= C)

の部分は、pm=p'だから、成立することを証明したい、

I,p' |= {¬C ^ A}

の¬Cのところそのままだ。だからこの部分は示せた。
なので、あとは、

I,pm |= A.

を示せばよい。さて、p1(=p),...,pm(=p')という状
態の列の関係は、

(すべてのi(<m)について次のことが成り立つ ((I,pi |= C ^ ExecI(P,pi,pi+1))))

であり、

I |= {C^A}P{A}

を表明付きプログラムの意味論で解釈すると、

I,p |= A

である。もちろんここのpはp1である。
前提に再度たちかえって、

I |= {C^A}P{A}

ということは、任意の状態pa,pbについて、

I,pa |= C^A => pa,pbがPの実行関係 => I,pb |= A

ということであったから、

I,p |= A
(すべてのi(<m)について次のことが成り立つ ((I,pi |= C ^ ExecI(P,pi,pi+1))))

の2つをiについて展開すると、

- i = 1
(I,p1 |= A) ^ (I,p1 |= C ^ ExecI(P,p1,p2))
(I,p1 |= A^C) ^ (ExecI(P,p1,p2)) ; 同値変形
であり、これはI |= {C^A}P{A}の{C^A}Pそのもの
なので、
(I,p2 |= A)
であることが成立している。
- i = 2
(I,p2 |= A) ^ (I,p2 |= C ^ ExecI(P,p2,p3))
...
(I,p3 |= A)
であることが成立している。
- ...
- i = m - 1
...
(I,pm |= A)
であることが成立している。

となる。正式な証明としてはiに関する数学的帰納法
を使う。

というわけで、

(I,pm |= A)

が成立していることが示せた。

- この証明によって、次のことが言えた。

「PHL(PV,AV,S)の形式的証明について、n>1として
n-1番目の行までが健全であるならば、n番目の行が
while文であるとき、n番目の行も健全である。」

- whileについてやったのと同様の方法にて、帰結規
則以外の推論規則についてもこのことを示すことが
できる。(割愛)

- ポイントは、これら帰結規則以外の証明においては、
「Sの任意の表明Aに対してI |= Aとなる」という本
体証明の前件を一切使っていないこと。なんのこっ
ちゃない、それが必要になるのは帰結規則だけであ
り、その他の推論規則についてはそれが無くともも
ともと健全だったということだ。

- では、帰結規則がn番目の行だったらどうなのか。

- まず帰結規則を再掲する。

PHL(PV,AV,S)の帰結規則は、

{B}P{C}
-------
{A}P{D}

ただし、

PHL(PV,AV,S) |- (A => B)
PHL(PV,AV,S) |- (C => D)

である

- 示すべきは、これが(n行目までが)形式的に証明でき
ており、n-1 行目まではくわえて健全性まで持って
いるときに、このn行目も健全と言えるかどうか、
だ。

- さて、付帯条件、

PHL(PV,AV,S) |- (A => B)
PHL(PV,AV,S) |- (C => D)

がn-1行目に属していると考えれば(こう考えていい
かどうかはもやもやしている)、これは、健全でも
あるので、

I |= (A => B)
I |= (C => D)

となる。

- すると、

I |= {B}P{C}

これを、表明付きプログラムの意味論で読み替える
て、

任意のp,p'について

I,p |= B => Exec(P,p,p') => I,p' |= C

が成立する

ということと、先の伴意をつなげば、

I,p |= A => I,p |= B => Exec(P,p,p') => I,p' |= C => I,p' |= D

となり、これは、

{A}P{D}

の意味論に他ならない。

- あれ、

「Sの任意の表明Aに対してI |= Aとなる」

をまた使ってないじゃん。。。

- やはり、

---
付帯条件、

PHL(PV,AV,S) |- (A => B)
PHL(PV,AV,S) |- (C => D)

がn-1行目に属していると考えれば
---

がまずいのだろう。

- 考える。。。

- まずくないかも。P89に

(S |- A => B) {B}P{C} (S |- C => D)
-----------------------------------
{A}P{D}

というのもあるから。

- 考える。。。

- これはやはりまずいのだろう。形式的な証明だけを
考えているときはまずくないのだが、健全性を考え
るときには、{B}P{C}がある行にいたる行の健全性か
ら、この行の健全性を証明するわけだが、その段階
では(S |- A => B) (S |- C => D)の健全性を示す
ことは不要だからだ。
- すると、

PHL(PV,AV,S) |- (A => B)
PHL(PV,AV,S) |- (C => D)

というときに、

I |= (A => B)
I |= (C => D)

が、

「Sの任意の表明Aに対してI |= Aとなる」

から言えるかどうか。。。

- ああ、言えるな。

- PVとAVはあくまで一階述語論理の範囲であるから、
一階述語論理は非論理的公理が健全ならば健全なの
で、それがそのまま適用されるということだ。

- これでホーア論理PHLの健全性については掴めた。

- なお、

「Sの任意の表明Aに対してI |= Aとなる」

は、PHL(PV,AV,I)についてはその定義から自動的に
満たされるので、

「PHL(PV,AV,I)は、解釈Iに対して健全である」

が成立する。


こつこつ。

0 件のコメント: