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

*** 5.2.3 記述能力の十分条件
 - 語彙の記述能力を議論するために、最弱前条件とい
   う概念を導入する。
 - 定義だが、誤字があるので原文ままではない。
---

Pがプログラム、Bが表明であるとき、最弱前条件とは、
次のように定義される集合pwpI(P,B)のことである。

pwpI(P,B)={p|すべてのp'について、(ExecI(P,p,p') => I,p' |= B)}が成立する。}

---
 - pwpI(P,B)は状態の集合だが、固定された解釈Iにお
   いては、状態の集合は表明を制約する。なぜか？ 考
   えてみる。
 - 解釈Iと表明Aがあるとする。すると、表明Aの解釈I
   における意味は、どのような環境(=状態)で表明Aが
   真となるか、である。
 - よって、状態の集合は、それらにて、そしてそれら
   のみで真となる表明の指定と同一視してよい。ただ
   し、この表明は単一とは限らない。そこで、「制約
   する」としてみた。

 - さて、pwpI(P,B)に対応する表明が語彙で表現可能か
   どうかは語彙次第である。
 - 任意のプログラムPと表明BについてpwpI(P,B)を表現
   する表明が存在するとき、PHL(PV,AV,I)は「十分な
   記述能力を持つ」という。
 - さて、
   
   I |= {A}P{B}

   は、

   すべての状態p,p'について、
   I,p |= A => ExecI(P,p,p') => I,p' |= B
   が真である。

   ということであった。これは、

   すべての状態pについて、
   I,p |= A =>
    (すべての状態p'について、ExecI(P,p,p') => I,p' |= B)
   が真である。

   と変形できる。さらに最弱前条件の定義から、

   すべての状態pについて、
   I,p |= A => (pがpwpI(P,B)に属する)
   が真である。

   と書き換えられる。

   よって、

   (I |= {A}P{B})
   <=>
   (すべての状態pについて、
   I,p |= A => (pがpwpI(P,B)に属する)
   が真である。)

   という同値が成立する。

 - さて、これは十分な記述力を持つことを仮定しては
   いなかった。十分な記述力を持たない場合は、

   (すべての状態pについて、
   I,p |= A => (pがpwpI(P,B)に属する)
   が真である。)

   におけるI,p |= Aについて、pがpwpI(P,B)に属してい
   ても偽になることがあるケースがあるということ。

   十分な記述力を持つということは、そういうケース
   が存在しないということ。すなわち、
   
   (すべての状態pについて、
   I,p |= A <= (pがpwpI(P,B)に属する)
   が真である。)

   が真である、ということ。
 - うーん。ここで何故pwpI(P,B)が最弱といえるのなの
   かがわからない。それは次回確認しよう。

よろよろ。