*** 5.2.1 健全性
- 定義なので原文ママ引用。
---
ホーア論理の健全性 (soundness)
PHL(PV,AV,S)が、解釈Iに対して健全であるとは、
PHL(PV,AV,S) |- {A}P{B}であるときには、必ず
I |= {A}P{B} となることをいう。
---
- これはあくまで健全性とはどういうことかという定
義。ホーア論理が健全性をもっているかどうかをこ
れから調べる。
- さて、それにあたって次の補題をまず示すのがよい
ようだ。
---
PHL(PV,AV,S)が解釈Iに対して健全である必要十分条件
は、Sの任意の表明Aに対して I |= A となることである。
---
- えっと、「必要十分条件」って何だっけ？
- 岩波数学入門辞典によると、P => Q, Q => P のとき、
PはQの、QはPの必要十分条件というようだ。
- なので、この補題が成立することを確認するには、
「PHL(PV,AV,S)が解釈Iに対して健全である」
=>
「Sの任意の表明Aに対して I |= A となる」
と
「Sの任意の表明Aに対して I |= A となる」
=>
「PHL(PV,AV,S)が解釈Iに対して健全である」
を調べればよいようだ。
- 本に載っているこの証明がなんだかよく分からない。
そこで自分なりに考えてみる。
- まず第一の方向。
「PHL(PV,AV,S)が解釈Iに対して健全である」
=>
「Sの任意の表明Aに対して I |= A となる」
これを示せばよい。
- まず、
「PHL(PV,AV,S)が解釈Iに対して健全である」
ということは健全性の定義により、
「PHL(PV,AV,S) |- {A}P{B}であるときには、必ずI |= {A}P{B} となる」
ということであった。
- なので、この後半の I |= {A}P{B} をうまくとると、
「Sの任意の表明Aに対して I |= A となる」
が言えるのではないかな。
- さて、ここではAはSに属しているので、表明単体と
してみると公理として正しさは確保できている。
- すると推論規則の方の公理でスキップ文の公理があ
るので、
PHL(PV,AV,S) |- {A}skip{A}
は成り立つ。
- ところで、帰結規則をここで使うと
{A}skip{A}
---------------------
{<恒真論理式>}skip{A}
と推論できる。というのは、<恒真論理式> => A は、
AがSに含まれていることからTrue => Trueであり、ト
リビアルに成立するからだ
ここで、<恒真論理式>をTrueと書くことにすると、
健全性から、
I |= {True}skip{A}
が成り立つということになる。
- では、
I |= {True}skip{A}
が成り立つということはどういうことであろうか。
- これは、表明付きプログラムの意味論から、
全ての状態pおよび全ての状態p'について、
I,p |= True => Exec[I'](skip,p,p') => I,p' |= A
が成立するということ。
- さて、
Exec[I'](skip,p,p') <=> 'p = p
なので、これは、
I,p |= True => p = p' => I,p' |= A
が全てのpとp'で成立する、ということ。
- さて、Trueは恒真論理式なので、解釈によらず常に
正しいから最左は成立し、結果、任意のp'について、
I,p' |= A
となる。これは
I |= A
の正式表記であった。■
- さて、次は逆の条件、
「Sの任意の表明Aに対して I |= A となる」
=>
「PHL(PV,AV,S)が解釈Iに対して健全である」
を確認しよう。
- ここでも健全性の定義を使って詳細化すると、
「Sの任意の表明Aに対して I |= A となる」
=>
「PHL(PV,AV,S) |- {A}P{B}であるときには、必ずI |= {A}P{B} となる」
ということだ。
- あれ？ これ、よく考えるとおかしくないか？
「Sの任意の表明Aに対して I |= A となる」
解釈Iは、表明付きプログラムに対する解釈だから、
表明付きプログラムではない単なる表明であるAが伴
意されることはないのでは？
たぶん、気持的には解釈Iの中の表明に関する部分に
よって、Aが伴意される、ということじゃないか。
ということで、その気持で行こう。
- さて、これは任意のPについて成立することを示さな
ければいけないからPはいろいろあるので大変である。
そこでPの行数に関する帰納法で確認することにしよ
う。
- ではまず、Pが1行のみのプログラムの場合はどうか。
- 「形式的証明」で一行のみで成立するプログラムとい
うのは、公理だけである。よって、代入文の公理と
スキップ文の公理を確認すればよい。
- 代入文の公理は、
{A[t/x]} x := t {A}
である。これが形式的に証明されているときに、
I |= {A[t/x]} x := t {A}
と言えるかどうか、だが、形式的に証明されている、
ということはこれが公理であることと同義なので、
そのこと自体はここでの確認において無価値かな。
- そこで、伴意の文を詳細化してみると、
任意の状態pとp'について、
I,p |= {A[t/x]} => Exec[I'](x := t,p,p') => I,p' |= {A}
が成立することを示せばよいことになる。
- ここで、
Exec[I'](x := t,p,p') <=> p' = p[Ip[t]/x]
なので、
任意の状態pとp'について、
I,p |= {A[t/x]} => p' = p[Ip[t]/x] => I,p' |= {A}
が成立する、
となる。この言明が真かどうか確認してみよう。
- まず、I,p |= {A[t/x]}が真でなければ、それ以降は
何であっても全体は真になる。なので、I,p |=
{A[t/x]}が真であるような状態pについて考えればよ
い。p' = p[Ip[t]/x]は、ちょっと奇妙だがp'を設定
しているだけなので、常に真と考える。すると、そ
んなp'において、I,p' |= {A} が成立すればOKとな
る。
- pは状態であり、これは環境と同義であった。
ということは、p[Ip[t]/x]は、pという環境において、
変数xについてはもともとpで割り付けていた値では
なく、Ip[t]を割り付ける、ということだ。
- これは項の代入性そのものであり、自明だろう。
- 次。スキップ文の公理
- スキップ文の公理は、
{A} skip {A}
である。これが形式的に証明されているときに、
I |= {A} skip {A}
と言えるかどうか、だが、形式的に証明されている、
ということはこれが公理であることと同義なので、
そのこと自体はここでの確認において無価値であろ
う。
- そこで、伴意の文を詳細化してみると、
任意の状態pとp'について、
I,p |= {A} => Exec[I'](skip,p,p') => I,p' |= {A}
が成立することを示せばよいことになる。
- ここで、
Exec[I'](skip,p,p') <=> p' = p
なので、
任意の状態pとp'について、
I,p |= {A} p' = p => I,p' |= {A}
が成立する、
となる。これは{A}が伴意されるなら{A}は伴意され
る、という言明なので、自明だろう。
- ゆえに、一行のみの形式的証明について成立するこ
とが確認できた。
- 次に、n>1として、n行から構成される形式的証明を
考えよう。数学的帰納法を用いるので、n-1行までは
正しい(伴意する)ことが確認できているとする。
- n行目が、公理(代入文 or スキップ文)であれば、一
行のみと同様に自明である。なので、n行目が推論規
則である場合を確認すればよい。すると、次のもの
について確認することになる。
- while文
- if文
- begin文
- 帰結規則
- まずwhile文からやろう。
- 今、n行の形式的証明があり、n-1行目までは健全で
あるとする。そして、n行目が、
{A} while C do P od {¬C ^ A}
であるとする。
- n行目がこうであるということは、n-1行目までのど
こかに、
{C^A}P{A}
がある、ということである。これは健全であるから、
I |= {C^A}P{A}
が成立しているということになる。これを情報とし
て、示すべきは、
I |= {A} while C do P od {¬C ^ A}
である。この伴意を詳細化すると、
任意の状態p,p'について、
I,p |= A => Exec[I'](while C do P od,p,p') => I,p' |= {¬C ^ A}
が真である
ということだ。
- さて、上記のwhile文のExecは次のものと同値である。
次のものを満すような、m(>=1)と、状態の列
p1,...,pmが存在する
(p=p1)^(p'=pm)^(I,pm /|= C) ^
(すべてのi(<m)について次のことが成り立つ ((I,pi |= C ^ ExecI(P,pi,pi+1))))
- どわーーー。while文がやっぱりわからん。
- ということで、とりあえずここまでとして、次回は、
while文について自分なりに整理しなおすことにする。
こつこつ。
0 件のコメント:
コメントを投稿