融合原理の健全性と完全性
真偽値の変数 , およびその否定 をリテラルという。リテラル, およびリテラルを論理和 で繋げた論理式を節という。さらに, 節, および節を論理積 で繋げた論理式を節形式という。例えば,
- , はリテラル,
- , , は節,
- , , , は節形式。
変数 からなる節形式 があるとき, 写像 を の割当という。どんな割当についても真となる節形式 は恒真であるという。また, が真となるような割当が存在するとき, 節形式 は充足可能であるという。例えば,
- 節形式 は恒真である。
- 節形式 は充足可能である。実際, , , という割当は を充足する。
- しかし, 節形式 は充足可能でない。後ろの二つのリテラルをいずれも真にするためには, , とする他ないが, すると が となってしまう故。このように充足可能でない, すなわち充足不可能な節形式が存在する。
ある節形式が充足可能かどうかを判定する問題を, 節形式の充足可能性問題 という。これは理論と実用の両面から重要な問題として広く知られている。融合原理は, この問題を解くための論拠の一つとして知られる。
融合とは, 二つの節 と から, 節 を作ることをいう。次の命題は明らか。
[命題1]節形式 の二つの節 , を融合して を作ったとき, 同じ割当 で と を充足できる。すなわち,
. が を充足する が を充足する.
いま, 節形式 が与えられたとして, 次の手続き RES を繰り返す:
(1)節形式 から と を選んで( でもよい), これらを融合し を作る。なお, 融合後の節 に重複するリテラルがあればひとつだけ残す。また,
- , もしくは
- あるリテラル について と のどちらも に含まれている
ならば融合失敗として, 融合を選び直す。どのように融合を選んでも失敗するなら文字列 "SAT" を出力して停止する。うまく融合を選べたら(2)へ。
(2)もし, 節 が空節 ならば, 文字列 "UNSAT" を出力して停止する。そうでなければ, 節 を に加えた節を, 改めて と更新して(1)へ。
なお, この手続き RES は必ず停止する。なぜなら, この手続きは に となる新しい節 を加えていくが, この新しい節の種類は高々有限個しか存在しないからである。実際, 節形式 がもともと 種類の変数でできているなら, 節の種類はぜんぶで 個となって有限である。
この記事では, この手続き RES が を決定すること, すなわち, 節形式 を入力とした RES の出力について,
- (健全性) RES が "UNSAT" を出力するならば, は充足不可能であり,
- (完全性) が充足不可能ならば, RES は "UNSAT" を出力する,
ことを証明する。
(証明)先の[命題1]から, RES における の更新前と更新後で充足同値が保たれる。すなわち, 更新前の が充足可能であることと, 更新後の が充足可能であることは同値である。したがって, RES が停止する直前の について主張を証明すれば, 入力の についても同じ主張がしたがう。
健全性のほうがたやすい。 RES が "UNSAT" を出力するということは, 空節 が導かれたということになり, この空節を導いた節形式 の二つの節 が存在する。あるリテラル について , としてよい。すると とかけるが, と のどちらか一方は必ず偽だから, この は充足不可能である。
完全性については対偶を示す。すなわち, 次の主張:
RES が "SAT" を出力するならば, は充足可能である
を, に含まれる変数の種類 に関する帰納法で示す。
まず として, この変数を とかけば, 論理的に は ① , ② , ③ の三通りに限られる。①なら , ②なら とすれば を充足できる。そして③は起こり得ない;この からは空節を導けるので, RES が "SAT" を出力するという仮定に反するからである。よって, は充足可能である。
次に, RES が "SAT" を出力する直前の について, が からなる節形式ならば, の節の形は次の三通りに分けられる( RES の定義から, の任意の節 について, と の両方が同じ節 に現れる場合は除かれることに注意):
- ,
- ,
- .
以下, を充足する割当 を構成する。すなわち:
- 2の形が現れない場合。まず, 3の形の節 のみによる節形式 を入力として RES を走らせると, 仮定からこの出力も "SAT" になるので(why?), 帰納法の仮定によってある割当 が存在してこの を充足する。したがって, , すなわち , とすれば, は を充足する。
- 1の形が現れない場合。上と同様にして示せる。
- 1と2の形がどちらも現れる場合。このとき, やはり上と同様に, 3の形の節のみからなる節形式 を充足する割当 をとれば, この割当のもとで ① または ② が成立つ;背理法によって示す。ある がとれて かつ だったとすれば, と の融合である も となる. しかるに の作り方から, この融合による節 が に現れないことがわかる。ゆえに残る可能性はあるリテラル について と がともに に含まれる場合, すなわち恒真である場合しかないが, これは が となったことに反する。よって, ① ならば , ② ならば とすれば, は を充足する。
Setsのcoequalizer (Awodey, 3.5.11)
Reference. Awodey, S. (2010) Category Theory, Oxford: Oxford University Press, 2nd ed. 2011.
概要
集合 から生成する最小の同値関係を とかく. のcoequalizerが, とするとき であることを示せ.
を包む最小の同値関係
問にはさらに, この を
と定めよ, とある. これは確かに, を包む 上の同値関係であって, かつそのなかで最小の集合である. このことを示しておく.
同値関係であること.
反射律. 任意に をとる. いま任意に, を包む 上の同値関係 をとると, の反射律から となるから .
対称律. をとれば, 任意の について となって, の対称律から となる. は任意だったから .
推移律. 対称律と同様.
を包むこと. とすれば, 任意の について より . は任意だったから .
最小であること. 任意に をとれば, の定義から .
よって示せた. しかしこの定義は今回の問で使いにくいと思うので, より構造の分かりやすいやり方でこの「最小の同値関係」を定めるのがよいだろう. すなわち, , かつ
として とする.
同値関係であること.
反射律. 任意に をとれば .
対称律. をとれば, ある があって となるので, より.
推移律. 対称律と同様.
を包むこと. 故.
最小であること. いま任意に を包む 上の同値関係 をとるとき, 任意の について
となることを示せば十分. 帰納法で示す. なら明らか. をとるとき,
が の由来なら で, の対称律から .
が由来としても同様.
よって示せた. なお, と は同じ集合となる(最小性から, は よりも小さいので , 逆も同様). 以下, を とかく.
(ところで,
として としてもよい. Why?)
Quine
A = " B = 'A = %s;' % (chr(34) + A + chr(34)) + A; print(B)"; B = 'A = %s;' % (chr(34) + A + chr(34)) + A; print(B)
Principles of Model Checking: Lemma 3.27
Reference: Baier, Christel, and Joost-Pieter Katoen. Principles of Model Checking, MIT Press, 2008.
Lemma 3.27の証明は, もう少し見通しよくできると思う。
Def. . 直感的には は を prefix にもつword 全体の集合である. この記法から, LT property が safety property であるという定義は,
とかける. また, 定義より
.
Lemma. .
証明 (左辺) (右辺). 終
を と略記する. なお, ここに .
Lemma 3.27. is a safety property .
証明 は成立つから, 右辺は と同値である. いま, を とかくことにすれば,
is safety
.
が従う. 最右辺は と同値. 終
the epis among posets are the surjections (Awodey, 2.8.9)
Reference. Awodey, S. (2010) Category Theory, Oxford: Oxford University Press, 2nd ed. 2011.
解答にsurjection ⇒ epi の証明しかなかったので, epi ⇒ surjection 側のメモをしておく(解答はおそらくepi ⇒ surjection を not epi ⇒ not surjection で取り違えている;つまり、解答はsurjection ⇒ epiの証明を二度与えていた)。この問題は、epi ⇒ surjection が本質的なので残念だった。
問題:objectがposetで, arrowがmonotone function(二つのposet に関する集合間の写像 であって, ならば を満たすもの;単調関数)であるようなcategory 上で, arrow がepicならばsurjective (on elements)か?
この問題の意義のために, 考えているcategoryが の場合の epi ⇒ surjective の証明を書くと次のようになる:
(証明)arrow つまり function がnot surjectiveとすると . いま へのarrows として, つまり および ( だけ をとって, なら )とすれば だから であるが, なら だから となって, はnot epic. 終
対偶をとり, not surjectiveと仮定して得られる を元手に反例を構成していく流れで, を を入力したときだけ値が異なるように作ることでうまくいく。このように なら反例が作りやすいのだが, では上の証明の をmonotoneであるように取る必要があるため, 少し工夫を凝らす。
(証明)arrow がnot surjectiveとすると . いま (なお )へのarrows を以下のように定める(ここからがこの問題の意義):
とすると . このもとで および とおく( 以下/未満なら へ, そうでなければ へ飛ぶようにしてある;そう考えればこれはmonotoneにみえる). 実際にこれらはmonotoneか?
なる をとる. とすると かつ ゆえ だが だから となって で不合理. したがって .
とすると かつ つまり かつ ゆえ と から より だから であるしかない. これを代入して かつ ゆえ が得られるが, これは に不合理. したがって .
作り方から ゆえ . いま とする. なら ゆえ仮定を併せて だから . なら だから で . よって ゆえ . よって はnot epic. 終
ブール代数
Def. Boolean algebra とは, poset と, その二つの要素 の組である. また, 上の二項演算 join: , meet: , および単項演算 complementation: が定義されており, これらは以下の要請を満たす:
とするとき,
①
②
③ and
④ and
⑤
⑥ .
Remark. poset とは, 集合 と, 上の半順序 の組である. 上の半順序 とは, 上の二項関係, つまり直積の部分集合 であって, として, 以下の要請:
(反射律)
(推移律) and
(反対称律) and
を満たすものである.
ブール代数と聞くと集合 , もしくは 上の演算を思い浮かべてしまうのだが, 順序を含めて拡張してもこれだけの公理でうまく定義できているので驚いた。ここから諸定理を示すのはそこまで難しくないが, ファインマンの三角関数よろしく, 一通りまとめてみようと思う。
Lem. (, の基本公式) , および , .
proof. の反射律から だから, ③より and . 後者は④から従う. 終
Lem. (, の可換則) および .
proof. 基本公式より and が成り立つので, ③から . 同様にして( を入れ替えると考えてもよい), . の反対称律から . 後者は④から従う. 終
Lem. ( と の関係) .
proof. ⑤⑥から . の可換則からこれらは と同値で, ⑤から と同値. 終
Lem. (De Morganの法則) および .
proof. 基本公式から より, 両辺で をとり . を入れ替え, 可換則から . ④から .
一方, 基本公式から で, 両辺で をとり⑥から . 同様に . ③から . 再び両辺で をとって . よって の反対称律から結論の前者が従う. 後者は, 前者の が任意であることから, を に, を に置き換え が得られるので, 両辺で をとって⑥により(「二重否定」を除去することで)従う. 終
proof. ⑤で とすると, ⑥から は の反射律から成立つので, . De Morganの法則と の可換則, および⑥から . 終
ex1. として . おなじみの二値集合である.
ここで の指定がないのは, もろもろの条件によって自然に定まるからである. すなわち, この集合がboolean algebraとなり得るように 上の半順序 を定義する場合, が半順序であることから, 反射律より . また公理の要請①②から . ここで とすると かつ と反対称律から となって仮定に反するので でなければならない. したがって, と一意に定まり, 逆にこの は半順序である.
また, 実は かつ であるしかない:⑤と の可換則から だから, もし なる が存在すれば, 任意の について となり, を で置き換え⑥を使えば ゆえ, 任意の について が従う. しかるに, これにより先の同値は とかけるので, 反対称律から任意の につき となり, これは に反する. 従って, 任意の につき でなければならない.
つまり「 として 」という言明だけで, 他の言及がなくとも, 半順序と単項演算 は自然に定まっているのである. 特に, 以上の流れから分かるように, という点が本質的である.
いわゆる「真理値表」を作ってみよう. は先に見たとおり.
については⑤より , . また より, ④から . 逆に②から ゆえ .
についてはDe Morganの法則から, それぞれ , , が従う.
ex2. 集合 の冪集合 . , , , , , とすれば, はboolean algebraとなる. 特に, は (一元集合)の冪集合とみなせる:.
Reference. Awodey, S. (2010) Category Theory, Oxford: Oxford University Press, 2nd ed. 2011.