** 5.2 ホーア論理の健全性と完全性
自分なりの言葉で書く。
- まず、ホーア論理の「形式的理論と意味論を定義で
きたので」とあるのですが、いろいろ定義してきた
が、この2つのものの境目がどこだっけ？と考えると、
思い出せない。。。歳を取るとは恐しいことだ。し
かしめげずに整理しなおすことにする。ホーア論理
の形式的理論と意味論の境目を明確にしよう。
- 形式的理論の定義：形式的理論とは形式化された理
論のことであり、次の2つから成る。
- 形式的理論の言語
- 語彙
- 変数
- 定数
- 関数記号
- 述語記号
- 項の定義
- 語彙をどのように組み合わせて項を成すかのルー
ル。
- 論理式の定義
- 論理記号の定義
- 項と論理記号をどのように組み合わせて論理式
を成すかのルール。
- 証明の形式化
- 後述。
- ふむ。形式的理論というのは統語論+証明と考えてい
いのかも。
- 形式的理論の意味論：形式的理論の意味論とは、形
式的理論の解釈である。解釈とは次のものどもであ
る。
- 語彙の解釈
数学の何かに対応させる。対応させかたは次のと
おり。
- 領域Dをきめる。
- Dの要素を定数に割り当てる。
- 関数記号に、D上の関数を割り当てる。
- {Truth,False}という真理値集合を導入する。
- D上の述語はD上の要素達から真理値集合への関
数であるとして定義する。
- 述語記号に、D上の述語を割り当てる。
- 項の解釈
- まず、変数の解釈のために、環境というものを
導入する。環境は、変数記号から定数記号(よっ
てDの要素)への関数である。
- 項(t)の解釈(Ip[t]) (再帰的定義)
- tが定数のとき、I[t]。すなわち語彙の解釈ど
おり。
- tが変数のとき、p(t)。すなわち環境(関数) ど
おり。
- tがまずは関数記号のとき、
I[f](Ip[t1],...Ip[tn])
というように、関数記号は語彙の解釈として、
引数については再帰的に解釈する。
- 論理式の解釈
論理式の解釈とは、それぞれの論理式に真偽値を
どう割り当てるかということである。
- まず、論理記号に対応する真理値関数を定義す
る。真理値関数はD上の関数ではなく、真理値集
合上の関数である。
- 論理積/2
- 論理和/2
- 含意/2
- 否定/1
- ただし、限量子については、真理値の集合(真理
値集合だけではない)から真理値の関数となる。
- 限量子(すべての)
- 限量子(ある)
- 続いて論理式の解釈を定める。
- 論理式の解釈は、項の解釈を前提として、論
理記号に論理関数を割り当てる形で再帰的に
真理値を計算するものとする。
- 形式的理論の証明
- 形式的理論の証明は次の2つを基礎とする。
- 公理と呼ぶ論理式(の指定)
- 公理は、論理的公理と非論理的公理に大別さ
れる。
- 推論規則(の指定)
- 形式的証明：形式的証明は、証明の記法を明確に
定めたものである。例えばヒルベルト型の形式的
証明などがある。(説明は割愛)
- なんかこれ、3回はブログに書いた気がする。。。
- めげずに形式的なホーア論理って何だったけ？をも
う一度やってみよう。
- とあるホーア論理構築 (なるべく簡潔に)
- 統語論
- プログラムの語彙(PV)を決める。
- PVの項の構文を決める。
- プログラムの構文をPVの項を基礎に決める。
- 表明の語彙(AV)を決める。(PVの拡張とする。)
- 表明の項の構文を決める。
- 表明の論理式の構文を、項を基礎に決める。
- 表明付きプログラムの構文を決める。
- 解釈
- PVの解釈を決める。
- 表明の論理式の解釈(Iとする)を決める。(これと
PVとの間にはいろいろ決めるが割愛。)
- 公理
- 論理的公理を決める。
- 非論理的公理は、解釈Iにて正しい論理式全てと
する。
- 推論規則
- 表明の推論規則を決める。
- 表明付きプログラムの推論規則を決める。
- 意味論
- ここまでで意味論が定義されているのは次のとお
り。
- PV
- AV
- 表明の項
- 表明の論理式
- ここまでで意味論が定義されていないのは次のと
おり。
- プログラム
- 表明付きプログラム
- プログラムの意味論を定義する。
- プログラムカウンタ
- 状況
- 状況の遷移。遷移関係
- 状態
- 状態の列
- 実行
- 実行関係
- 表明付きプログラムの意味論を定義する。
- {A}P{B}について、表明の部分は表明の意味論
として、Pの部分は実行関係を意味として、意
味論を決定。
- ふむ。一応、本を見なくても自分で組み立てられる
ようにはなった。
こつこつ。
0 件のコメント:
コメントを投稿