ET Seminar 2008 (1)

等価変換理論集中セミナー2008
かねて切望されていた集中セミナーが開かれる運びとなった。取りまとめをされたshinh氏、講師を勤められるalohakun氏、会場を提供して頂いたサイボウズに感謝の意を示すと共に、微力ながら事前知識の整理をお手伝いしようかと思う。事前知識というのは、計算論における述語論理のチューリング完全性と等価変換という魅惑のパラダイス(？)、この両者の間に横たわっている「名状しがたきもの」の事である。

まずPrologの理論的背景と実際のプログラムの接点から始めよう。Robert Kowalskiが見出したSLD導出の話である。プログラムと証明の対応から確認する。

+----+----------------------+----------------------------------+
|    |プログラム            |証明                              |
+----+----------------------+----------------------------------+
|前提|is_human(socrates).   |is_human(socrates)は真            |
|    |die(X) :- is_human(X).|die(X)は真 または !is_human(X)は真|
+----+----------------------+----------------------------------+
|命題|?- die(X).            |die(X)は真 となるXは何か?         |
+----+----------------------+----------------------------------+
|過程|die(X)                |!die(X)と仮定                     |
|    |  is_human(X)         |ならば !is_human(X)は真           |
|    |  is_human(socrates)  |しかし !is_human(socrates)は矛盾  |
|    |X = socrates.         |X = socrates ならば die(X)は真    |
+----+----------------------+----------------------------------+

プログラムの各述語と証明の各命題に対応が見てとれる。ここでプログラムの各述語の形式をホーン節と呼び、述語論理における正リテラルが高々一つの論理式を指す。細かな対応を補足すると次のようになる。

   is_human(socrates).     % ファクト
≡ ⇒ is_human(socrates)
≡ is_human(socrates)      % ホーン節

   die(X) :- is_human(X).  % ルール
≡ is_human(X) ⇒ die(X)
≡ die(X) ∨ !is_human(X)  % ホーン節

   ?- die(X).              % クエリ
≡ die(X) ⇒
≡ !die(X)                 % ホーン節

Prologの挙動を証明と対応付けるアルゴリズムはSLD導出(Selective Linear Definite Resolutin)という名で与えられている。これはプログラムに対応するホーン節集合を考え、二重否定によって真となる部分集合を検索するアルゴリズムである。

集合: (die(X) ∨ !is_human(X)), is_human(socrates)
入力: !die(X)
step-0 入力を選択節とする
  選択節: !die(X)
step-1 集合より選択節を簡約化可能なホーン節を選択節に加える
  選択節: !die(X) ∧ (die(X) ∨ !is_human(X))
step-2 簡約化
  選択節: !is_human(X)
step-3 集合より選択節を簡約化可能なホーン節を選択節に加える
  選択節: !is_human(X) ∧ is_human(socrates)
step-4 簡約化
  選択節: NIL
step-5 選択節が空なので入力は真
  出力: NIL ≡ !!die(socrates)

このように(二重否定による肯定を許可)して述語論理とPrologの実行解釈が結びつく。さて実はここからが本題で、論理式とプログラムの対応が具体的に定まるのなら、膨れ上がっていく状態の制御(how)は論理(what)を使うことで相当に抑制できるのではないか、という提案が浮上して来る。特にSLD導出で現れる"選択"と"簡約"の処理を上手く作り込む事で、制御の負担が減るのではないかと期待したのである。この"選択"と"簡約"をバックトラックとユニフィケーションによって実現することは言うまでもない。
(続く)