コンテンツへスキップ
Topos Uranos
日本語

標準形のアルゴリズムとその応用

要約

標準形の課では、すべての論理式が選言標準形とも連言標準形とも同値であることを証明した。この課では、それらを真理値表なしで計算する方法と、それらの使い方を学ぶ。計算は三つの段階からなる書き換えのアルゴリズムである。まず双条件、排他的選言、否定論理和、含意を消去する。次にド・モルガンの法則と二重否定によって否定を変数まで押し下げる。そして分配を行う。選言標準形のためには連言を選言に対して、連言標準形のためには選言を連言に対して分配する。アルゴリズムの正しさ（意味論的置換の帰結である）と停止性（各段階の各ステップで減少する数値的な尺度による）を証明し、さらにその限界も証明する。すなわち、二変数の連言 nn 個の選言の連言標準形は、必ず 2n2^n 個の節をもつ。続いて、内部の見えない装置の真理値表から標準形を求め、隣接する行の併合によって簡単にし、直列と並列のスイッチ回路に変換する。四つのスイッチをもつ装置の問題は、表、二つの標準形、回路とともに完全に解かれ、五つのスイッチの問題は挑戦問題として残される。

学習目標

  1. 書き換えのアルゴリズムを適用して論理式の選言標準形と連言標準形を求め、双条件の現れる位置に応じて適した消去の仕方を選ぶ。
  2. アルゴリズムが正しいことを意味論的置換によって、停止することを各ステップで減少する尺度によって証明し、連言標準形がもとの論理式より指数的に長くなりうる理由を説明する。
  3. ブラックボックスの標準形をその真理値表から構成し、隣接する行の併合によって簡単にする。
  4. 直列と並列のスイッチ回路を論理式で表し、自然言語で与えられた仕様を満たす回路を設計し、簡単にする。

標準形の課では、その存在について二つの証明を与えた。第一の証明は真理値表を経由する。その表は 2n2^n 行（変数が nn 個のとき）をもつ。第二の証明は、論理式をその唯一の形成規則に従って変数からたどる。どちらも、含意、双条件、入れ子になった否定で書かれた論理式を前にしてどう進めばよいかは述べていない。しかし論理式はふつうそのような形で現れる。そうであるならば、表記そのものの上で働き、考えずに実行でき、停止することと同値な論理式を与えることが確かな手続きが欠けている。それがアルゴリズムであり、その研究がこの課の第一の対象である。第二の対象は、それを使って行うこと、すなわち装置のふるまいを論理式で記述し、それを再現する回路を構成することである。

表記と置換

このコースの論理式は白丸と黒丸の記号列であり、¬\neg、∨\vee、∧\wedge、→\rightarrow、↔\leftrightarrow、⊻\veebar は否定論理和から定義された略記であったことを思い出そう（命題論理の言語の課）。((p∨q)→(¬q∧p))((p \vee q) \rightarrow (\neg q \wedge p)) と書くとき、私たちは記号列を書いているのではなく、その表記を書いている。表記とは木であり、その葉は変数、節点は結合子 ¬\neg、∧\wedge、∨\vee、→\rightarrow、↔\leftrightarrow、⊻\veebar、↓\downarrow で、各節点はその成分をもつ。どの表記もただ一つの論理式、すなわちその略記を展開して得られる論理式を指す。そして同じ論理式がいくつもの表記をもちうる。標準形の課では、¬¬φ\neg\neg\varphi と (φ∨φ)(\varphi \vee \varphi) が同じ記号列であることを指摘した。アルゴリズムが読むのは表記であって記号列ではない。そのため両者を区別しておくのがよい。この区別が重要なのは各ステップがどこに作用するかを知るためだけなので、文字 φ\varphi、ψ\psi、χ\chi を表記にも、それが指す論理式にも用い、指される論理式が意味論的に同値であるとき φ≡ψ\varphi \eqsem \psi と書く。表記の部分表記とは、その節点の一つを根とする部分木である。

アルゴリズムの一つのステップは、ある部分表記を別の部分表記に置き換える。この置き換えが意味を変えないことを保証する道具は、意味論的帰結と同値の課の意味論的置換定理である。しかしあの定理は記号列の中の一つの出現を置き換えるものであり、一つの部分表記は記号列の中のいくつもの出現に対応しうる。各略記はその成分を複製するからである。(φ∨ψ)=((φ↓ψ)↓(φ↓ψ))(\varphi \vee \psi) = ((\varphi \downarrow \psi) \downarrow (\varphi \downarrow \psi)) では、成分 φ\varphi が二回現れる。次の補題は置換を表記に適合させる。

補題表記における置換

χ\chi を表記とし、θ\theta をその部分表記の一つ、θ′\theta' を θ≡θ′\theta \eqsem \theta' を満たす表記とする。χ′\chi' が χ\chi のその部分表記を θ′\theta' に置き換えて得られるならば、χ≡χ′\chi \eqsem \chi' である。

証明

  1. χ′=θ′≡θ=χ\chi' = \theta' \eqsem \theta = \chi

    θ\theta が根をもつ節点の深さ、すなわちその節点より上にある χ\chi の結合子の個数に関する帰納法による。深さが 00 ならば、部分表記は表記全体である。

  2. χ=c(χ1,χ2),χ′=c(χ1′,χ2),χ1′≡χ1\dato{hi}{\chi = c(\chi_1, \chi_2), \qquad \chi' = c(\resaltar{\chi_1'}, \chi_2), \qquad \chi_1' \eqsem \chi_1}

    深さが 00 より大きければ、χ\chi の根は結合子 cc で、その成分は χ1\chi_1（および χ2\chi_2、ただし cc が二項の場合）であり、θ\theta はそのうちの一つ、たとえば χ1\chi_1 の中の節点を根とし、深さはより小さい。帰納法の仮定により、χ1\chi_1 の内部での変更は同値な表記を与える。

  3. v(χ′)=Fc(v(χ1′),v(χ2))=Fc(v(χ1),v(χ2))=v(χ)v(\chi') = F_c\left( v(\chi_1'), v(\chi_2) \right) = F_c\left( v(\chi_1), v(\chi_2) \right) = v(\chi)

    派生結合子の値の定理（命題論理の意味論の課）と否定論理和の条項により、付値における c(χ1,χ2)c(\chi_1, \chi_2) の値は χ1\chi_1 と χ2\chi_2 の値の関数であり、これらの値は変わらない。したがって χ\chi と χ′\chi' はどの付値においても同じ値をもつ。

ここで FcF_c は結合子の真理関数である。F¬(a)=1−aF_\neg(a) = 1 - a、F∧(a,b)=abF_\wedge(a, b) = ab であり、ほかの結合子についても同様である。同じ結果は、意味論的置換定理を記号列の中の θ\theta の各コピーに一回ずつ適用し、同値を推移性によってつなぐことでも得られる。表記による証明のほうが短いのは、コピーではなく書かれた結合子を数えるからである。