最近インターンのハッサン君に UCLA の教材をもらって論理の勉強をしている。最近やってる Alloy にはバックエンドとして SAT という物が使われていて、その仕組みを知りたいと言ったら教材をくれた。昔 Prolog も作った http://d.hatena.ne.jp/propella/20090502/p1 事だし楽勝じゃ！と思ってたんだけどなかなか難しく、一週間経っても終わらない。忘れると困るので覚えた事をここに書く。
目的はブール演算を使って推論をする事。
プログラマにとってはブール演算はとても身近な物だ。使う値は true と false だけ、演算子は and or not の三つで、これをどうやっても難しくなりようが無いと思いきや、なかなか面白い問題を孕んでいる。ブール演算の話が難しくなるのは、メタな話題が不用意に混じるからだと思う。例えば
- true ∧ false = false (真 and 偽 は 偽)
という式。この式自体もブール値を持っているので
- (true ∧ false = false) = true
のようにして、等式の性質もまたブール式だというややこしい事になる。さらにブール式を集合と思う事も出来るのでさらにややこしくて、同じ事を言うのに
- A ∧ ~A = false (この式は A がどんな時でも false)
- A ∧ ~A は inconsistent (この式が true になる A の集合と考えると解は無い)
のように二つの言い方がある。こっちの問題はむしろ記法の問題で、プログラミング言語みたいに厳密に型を意識して書くと良いと思うんだけど、数学的な記法というのは素人目からすると厳密さに欠ける気がする。と、このまま続けると愚痴だらけになるので、メモに移る。
ブール演算の定義
ブール演算で使う主な記号は次の通り
- true : 真を表す
- false : 偽を表す
- ∧ : and 演算子。true ∧ true = true その他の場合は false
- ∨ : or 演算子。false ∨ false = false その他の場合は true
- ~ : not 演算子(ほんとはフみたいな字だけど化けたので ~ にした)。~true = false, ~false = true
∧ の両辺はブール値だけど、何気なく「束縛」に使われる事もあるので注意。例えば A ∧ B と言うと単に A と B の and を取った値じゃなくて、「A = true かつ B = true の場合」という風に変数名に意味がある時がある。特に | の後ろ。
あと重要な記号 ⇒ と ⊧ と | について、a ⇒ b は a implies b と読むブール演算子。a の時 b という意味に使うが a = false の時の振る舞いが普通の言語と違う。
| a | b | a ⇒ b |
| false | false | true |
| false | true | true |
| true | false | false |
| true | true | true |
a ⊧ b は a satisfies b と呼ぶ。これは ⇒ と似ているが両辺はブール値ではなく、論理式の集合の時に使うらしい。まだあやふやなんだけど、Haskell 風に書くとだいたい ⊧ :: ([Bool] -> Bool) -> ([Bool] -> Bool) -> Bool と思うと意味が繋がる。両辺がブール値の集合ではなく、関数(ブール値を代入すると値が定まる式)な事に注意。
a | b の読み方は分からないけど、Haskell 風には where。つまり、b が成り立つ時の a の値を表す。例えば
- A ∧ B | A = true ∧ B = B
となる。この場合、| の右辺の A は、A の値じゃ無くて、A = true という束縛を表すので注意。演算の結果変数 A が消える。A = false を代入するには
- A ∧ B | ~A
と書く。どのくらい一般的なのか知らないけど、たいへんいけてない文法だと思う。
複数のブール値の性質
複数のブール値の性質を言うのに特別な述語がある。
- valid : 全部が true
- invalid : false の物がある
- consistent : true の物がある
- inconsistent : 全部が false
例えば二つのブール値があった時
| valid? | consistent? | ||
| false | false | invalid | inconsistent |
| false | true | invalid | consistent |
| true | false | invalid | consistent |
| true | true | valid | consistent |
となる。特に valid と inconsistent が良く出てくる。
量化子
量化子というのは、「全てのなんとか」、「なんとかが存在する」というやつ。ブール論理ではわりと単純な定義になっている。
- ∃PΔ ≝ Δ|P ∨ Δ| ~P (Δ が成り立つ P が存在する)
- ∀PΔ ≝ Δ|P ∧ Δ| ~P (P がどんなであっても Δ が成り立つ)
この定義は簡単で良い。しばらく出てこないので省略。
Conjunctive Normal Form (CNF)
∨ とか ∧ とか入力が大変なので別の方法を考える事にする。全てのブール式は
- (a1 ∨ a2 ∨ a3 ∨ ...) ∧ (b1 ∨ b2 ∨ b3 ∨ ...) ∧ ...
という形に書き換えられる事が知られている。そこで、これを「集合の集合」という風に書くと扱いが楽だ。つまり次のようになる。
- {{a1, a2, a3, ...}, {b1, b2, b3, ...} , ... }
外側の集合は and、内側の集合は or の意味になる。例えばこんな感じに計算出来る。
- {{false, false}, {true, false}}
- = {false, true} -- 内側の or を計算
- = false -- 外側の and を計算
なお、型を変えないで
- {{}} = true
- {} = false
とした方が美しい。
推論
つづきます。。。
