**** 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に対して健全である」
が成立する。
こつこつ。
