【検証論】5 ホーア論理の数学 （その7）

*** 5.2.4 相対完全性定理
**** 再度自分なりに「十分な記述能力を持つ」を確認する
 - どうもしっくりこない。この最弱前条件と十分な記
   述能力を持つということが。そこで、再度自分なり
   に確認する。
 - まず、最弱前条件と呼ばれる、状態の集合の定義。

   pwpI(P,B) = {p|∀p'.(ExecI'(P,p,p') => I’,p' |= B}

 - これはわかる。
 - 次に、表明Aが状態集合Sを表現する、ということの定
   義。

   S = {p| I,p |= A}
   
   であるとき、表明Aは状態集合Sを表現する、と言う。

 - 注意点。Sを表現するAはたくさんある。あるAが表現
   しているとして、Aと同値な表明はすべて表現してい
   ると言える。
 - 注意点。∀p.(I,p |= A' => I,p |= A)となるA'があ
   るなら、次が成り立つ。

   ∀p.(I,p |= A' => p ∈ S}

   違う言葉でいうと、前者をみたす状態の集合は、後
   者を満たす状態の集合の部分集合である。
 - さて、任意のプログラムPと表明Bについて、
   pwpI'(P,B)を表現する表明が存在するとき、
   PHL(PV,AV,I)は十分な記述能力を持つという。
 - このこと自体はそんなに理解は難しくない。
 - このことを形式的に書いてみよう。
   ∀P∀B∃A∀.(I,p |= A => p∈pwpI(P,B) )
 - ところで、とある{A}P{B}について

   PHL(PV,AV,I) |= {A}P{B}

   が成立する、ということの定義は、

   ∀p∀p'.(I',p |= A => (ExecI'(P,p,p') => I',p' |= B))

   であった。ここでI'は解釈Iのうち表明に関する部分。
   以降、Iは解釈の対象の部分に文脈によって限るものとする。
 - これは、十分な記述能力を持つことの定義に似てい
   る。どのくらい似ているか調べてみる。
 - 十分な記述能力をもつことの形式的記述を展開してみる、
   
   ∀P∀B∃A∀p.(I,p |= A => p∈pwpI(P,B) )

   は

   ∀P∀B∃A∀p.(I,p |= A => p∈{p''|∀p'.(ExecI(P,p'',p') => I,p' |= B} )

   である。さて、pが集合に属するということは、その
   内包表記の条件を満たすのでこの後の部分は集合表
   記を外すことができる。

   ∀P∀B∃A∀p.(I,p |=   A => ∀p'.(ExecI(P,p,p') => I,p' |= B} )

   前半はp'を含まないので、p'の限量子は前に出すこ
   とができる。

   ∀P∀B∃A∀p∀p'.(I,p |=   A=> (ExecI(P,p,p') => I,p' |= B} )

   これは完全であることの言明とほぼ同値である。違う
   のは、PとBを先に固定したときに、それに対応するA
   が必ず存在するという情報が入っていることだ。

   これが重要なポイントだ。
   

 - では、ここでこまごまやってきたことはどういう価
   値があるのか、まとめてみる。
 - まず、新しく「状態集合を表現する言明」という概念
   を導入した。それをつかって、伴意の後半を満たす
   状態集合を最弱前条件として定義した。さらに、最
   弱前条件を表現するAをホーア論理が持つとき(十分
   な記述能力があるとき)、伴意するということは、

   ∀P∀B∃A∀p.(I,p |= A => p∈pwpI(P,B) )

   と同値であることがわかった。
 - これによって、完全性を示すということは、

   伴意 => 形式的に証明可能

   を示すということであったが、それをホーア論理が
   十分な記述力を持つときは、

   ∀P∀B∃A∀p.(I,p |= A => p∈pwpI(P,B) )
   => 形式的に証明可能

   を示せばよいということになることがわかった。
 - だいたいわかった。だけど本に記載されている次の論
   理式は理解できない。

   I |= {A}P{B} <=> I |= A => pwp(P,B)   (5.8)

 - とりあえず、これは無視する。上のように自分なり
   に理解した形で相対完全性定理の証明をこころみる。
   (5.8)を理解しないと証明できないとわかったら、理
   解を試みる。
**** 閑話休題
 - 相対完全性定理の証明を読み、自分でも書きつつ考
   える。
 - おおすじは理解できた。
 - しかし代入性や項書換えのところがスキルが足りなく
   ておいつかない。
 - これをちゃんとやるには、項書換えについてそこそ
   こ訓練しないと駄目な気がする。形式的言語の取り
   回しスキルが全般的に足りていない。
 - 相対完全性定理をちゃんとやるのは将来の課題として
   先に進む。

のろのろ。