【検証論】5 ホーア論理の数学

* 5 ホーア論理の数学
自分なりのポイントを、自分なりの言葉で書く。
 - ホーア論理は4章で定義したような、形式的理論であ
   る。
 - 4章で定義したのは、主に統語論(Syntax)である。
 - ただし、一階述語論理のフレームワークを採用して
   いる部分や、解釈に因っている部分もあるので、一
   部、意味論(Semantics)に入っている。
 - 形式的理論なので、理論の健全性や完全性という概
   念がある。
 - 復習としてここで形式的理論の健全性と完全性を振
   り返ると、、、
    - 論理式Aは解釈Iと環境pに対して正しい、ということ
      を、

      I,p |= A

      と書く。

    - 論理式Aは解釈Iと任意の環境に対して正しい(伴意)
      ということを、

      I |= A

      と書く。

    - トートロジー。任意の解釈Iに対して I |= A が成立
      するとき、Aをトートロジーと呼ぶ。

    - 形式的に証明可能
      - 形式的理論Tにおいて、形式的証明によって論理式
        を証明できたとき、

        T |- その論理式

        と書く。

    - 形式的理論Tが解釈Iにおいて完全性と持つというこ
      とは、

      任意の論理式Fに対して、I |= F ならば、T |- F と
      なる

      ということである。すなわち意味論としての正しさ
      があるものは、統語論としての正しさも証明できる
      ということ。

    - 形式的理論Tが解釈Iに対して健全であるとは、

      任意の論理式Fに対して、T |- F ならば、I |= F
      となる

      ということである。すなわち統語論をベースに証明
      されたものは、意味論としても正しい、ということ。

 - さて、このようなお話のもと、ゲーデルの不完全性
   定理とは、
    - ゲーデルの不完全性定理
      形式的理論が次のふたつを満すならば、それが健全
      かつ完全となるような解釈は存在しない。
      - 自然数の理論を含む。
      - 論理式が非論理的公理であるかどうかを決定可能
        (turing decidable)である。
 - ここで、PHL(PV,AV,S)が集合Sの決め方が任意なので、
   結果として、ホーア論理はゲーデルの不完全性定理
   を免れる、という。これはなんだかもやもやして理
   解できていない。が、先に進もう。
** 5.1 ホーア論理の意味論
 - あたりまえだが、完全性を議論するには、統語論と
   意味論の両方が必要。
 - ホーア論理については、表明の意味論は一階述語論
   理に準ずるとして、プログラムの意味論と、表明付
   きプログラムの意味論はまだ未定義である。
 - それを定義していく。
*** 5.1.1 プログラムの意味論
 - 「プログラムの意味論とは、プログラムの実行方法
   を数学的に定義することである。」
 - ここでは操作的意味論でやる。
 - 操作的意味論は、抽象的なインタプリタを定義する
   ようなものらしい。
 - プログラムの操作的意味論の構成要素
   - 1. ラベル付きプログラム (BNFで定義)
   - 2. プログラムカウンタ
   - 3. 状態 (変数の値を指定する)
   - 4. 遷移関係 (実行の1ステップを記述する)
   - 5. PVの解釈IP (式の意味を決める)
 - 操作的意味論の語彙
   - 状態(situation)とは、変数の値の状態であり、変
     数から領域への関数によって表現されるものである。
     これは表明の意味論における環境と同じものである。
     よって、状態と環境を同義語とする。
   - 状況(configuration)とは、状態とプログラムカウ
     ンタの組<ρ,l>である。
   - 遷移関係とは、プログラムの1ステップによって、
     状況1から状況2に変わるときの状況1から状況2へ
     の写像のことである。
   - 実行とは、状況の列であり、その列の頭の状況のプ
     ログラムカウンタは、プログラムの最初のラベルで
     あり、それを起点遷移関係にて遷移する状況を並べ
     たものである。頭の状況を初期状況と呼び、初期状
     況を成す状態のことを、初期状態と呼ぶ。
   - 次の状況とは、着目している状況から遷移関係に
     て移りえる状況のことである。並列計算可能な言
     語では、次の状況が複数になることがあるが、逐
     次実行型言語では次の状況が2個以上となることは
     ない。(2個になるのは条件分岐)。
 - 遷移関係をプログラム言語の各文に対して定義する
   のが、どうやら操作的意味論の要のようだ。
 - Min言語の遷移関係を定義。
*** 5.1.2 Min言語の合成性
 - まず原文まま引用。
---

Min言語の合成性

プログラム(文)の働きは部品の働きによって完全に決定
される。

---
 - 働きというところが感覚的な記述になっているよう
   な気がする。働きの語彙の定義が見当たらないので。
 - おそらく、意味論(Semantics)のことではないか。
 - ちょっと噛み砕きつつ、自分なりに正確にしたい。
 - 部品は、証明の木の葉のことであった。
 - プログラムの意味論(Semantics)の要は、遷移関係で
   あった。
 - それらを組み入れると、
---

Min言語の合成性

プログラム(文)の遷移関係は、そのプログラム(文)の部
品(証明木の葉)の遷移関係達によって完全に決定される。

---
 - なんか、あまり嬉しくないな。こう書いてみても。

*** 5.1.3 実行関係による合成性の表現
 - 「働き」ってもしかして副作用のことなのか？
 - 語彙
   - 実行関係：初期状態ρにてプログラムPを実行した
     ときに、状態ρ'にて停止することを、Exec(P,ρ,
     ρ')と書く。
     - Min言語の各文について、実行関係にて初期状態
       と終状態の関係を調べてみる。すると、Min言語
       の合成性が実行関係としてもみてとれる。
 - プログラムカウンタの合成性
   原文まま引用。
---

プログラムカウンタの合成性

Min言語ではプログラムカウンタは、部分プログラムの
最初のラベルから入り、最後のラベルから出ていく。

---
 - 構造化プログラミングとは、gotoやjumpを使わないこ
   とによって、プログラムカウンタの合成性を極力維持
   するようにするプログラミングスタイルである。(プ
   ログラミング言語は問わない)
 - 構造化プログラミングにてプログラムを書くことを目
   的とするプログラミング言語は、構造化プログラミン
   グ言語であるとみなされる。代表的なものに、C言語
   やPascalがある。
   
*** 5.1.4 表明付きプログラムの意味論
 - 語彙の「ホーア論理の解釈」とは、表明の語
   彙の解釈のことである。その解釈をIと呼ぶ。
 - 語彙の表明付きプログラム{A}P{B}の、解釈I
   に対する部分正当性は、
---

   ∀ρ.∀ρ'.(I,ρ|= A => Exec[I'](P,ρ,ρ')  =>   I,ρ'|= B)

   ただしI'はIの語彙をPVに制限したものである。

---
   と定義する。なお、これは原文からの引用ではない。
   (誤字や脱字が多いため)

こつこつ。