【検証論】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に対して健全である」

    が成立する。

こつこつ。