Prolog

Prologの簡単なプログラムを実行することができます。




使い方

Prologのプログラムを上の領域に書き込んで[run]ボタンを押してください。 [ex1]…[ex8]を押すと、上の領域に例が書き込まれます。 たとえば、[ex1]を押すと次の例が書き込まれます。 
    append([], X, X).
    append([E|X], Y, [E|Z]) :- append(X, Y, Z).
    ?- append([a, b], [c, d], X).

[trace]を押すと、プログラムが実行される様子を見ることができます。

(文献[3]を参照してみてください。)

[proof]を押すと、証明の図(HTMLのTABLE)を出力させることができます (例)。 たとえば次のような図が下の領域に書き込まれます。 (これをHTMLファイルにしてブラウザで開いくと次のようになります)
p(a)
(1) p(a) :- q(a), r(a).
q(a), r(a)
(2) q(a).
(3) r(a).

  1. p(X) :- q(X), r(X).
  2. q(a).
  3. r(a).
  4. ?- p(X).
これは次のような意味になります。
証明する項
(節の番号) 節の内容: この規則で下の項の列から上の項が導かれる。
項1, 項2, …
項1の証明の図
項2の証明の図
…

Prologのプログラム

Prologのプログラムは次の形のものから構成されています。
  1. P :- Q1, … , Qn.
  2. P.
  3. ?- Q1, … , Qn.
3 の形のものは1個だけです。 ここで、P, Q1, … , Qn は項です。 これは次のような意味になります。
  1. ∀X1…∀Xm(P ← Q1 ∧ … ∧ Qn)
  2. ∀X1…∀Xm(P ← true)
  3. ∀X1…∀Xm(false ← Q1 ∧ … ∧ Qn)
X1, …, Xm は P, Q1, … , Qn に出てくる変数です。 (Prologのプログラムでは変数は大文字から始まる名前です。) true, false は値が常に true, false となる述語を表します。 Prologのプログラムは、1, 2 を仮定したとき 3 の否定 ∃X1…∃Xm(Q1 ∧ … ∧ Qn) を証明する(1, 2, 3 から false を証明する)ように動作しますが、 以下の例のように実行する順序が決まっているため、 証明できるものが必ずprologで証明できるとは限りません。

[], [x|y], [x1, … , xn] という記法は、 次のような項を表します。 (上のプログラムは という意味になります。)

Prologのプログラムは

  1. ∀X(append([], X, X))
  2. ∀E∀X∀Y∀Z(append([E|X], Y, [E|Z])←append(X, Y, Z))
から ∃X(append([a, b], [c, d], X)) を以下のような手順で証明するように動作します。 まず、 append([], X, X) と 1, 2 の左側(append([], X, X))とappend([E|X], Y, [E|Z]) が単一化可能かどうかをこの順で調べます。 1 は単一化可能ではありません。2 は、変数を新しい変数で置き換えて
append([E1|X1], Y1, [E1|Z1]) ←append(X1, Y1, Z1)
とすると
E1→a, X1→[b], Y1→[c, d], X→[a|Z1]
という代入により単一化可能です。 この代入は最も一般的な単一化代入となります。 この代入により、右側は
append([b], [c,d], Z1)
となります。 もし ∃Z1(append([b], [c,d], Z1)) が証明できたとすると、 2 から ∀E1(append([E1|[b]], [c, d], [E1|Z1]) が証明できて、上の代入によって ∃Z1(append([a,b], [c,d], [a|Z1])) が証明できるということになります。

次に、この項(複数あるときは左から順に)について、上と同じ手順で調べていきます。 1 は単一化可能ではありません。2 は、変数を新しい変数で置き換えて

append([E2|X2], Y2, [E2|Z2]) ←append(X2, Y2, Z2)
とすると
E2→b, X2→[], Y2→[c, d], Z1→[b|Z2], X→[a|[b|Z2]]
という単一化代入により単一化可能です。 この代入により、右側は
append([], [c,d], Z2)
となります。 今度は ∃Z2(append([], [c,d], Z2)) が証明できたとすると、 ∃Z1(append([a,b], [c,d], [a|[b|Z2]])) が証明できるということになります。

次に、この項について、上と同じ手順で調べていきます。 1 は、変数を新しい変数で置き換えて

append([], X3, X3)
とすると
X3→[c, d], Z2→[c, d], Z1→[b|[c, d]], X→[a|[b|[c, d]]]
という単一化代入により単一化可能です。 ここには右側がないので、 X=[a|[b|[c, d]]]=[a, b, c, d] となって append([a, b], [c, d], [a, b, c, d]) が証明できるということになります。

単一化

二つの項の変数を項で置き換えて、二つの項が項として等しくなるようにする ことができるとき単一化可能であるといいます。 このときの代入を単一化代入といいます。 (ある項の変数を項で置き換えることを代入といいます。) ある単一化代入σが、任意の単一化代入θに対してσ=μ・θとなる代入μが存在するとき、 σを最も一般的な単一化代入といいます。 (μ・θは代入の合成を表します。代入θで置き換えた項に対して代入μで置き換えることを 表します。) たとえば、 append([a, b], [c, d], X) と append([E1|X1], Y1, [E1|Z1]) は単一化可能で、
  1. E1→a, X1→[b], Y1→[c, d], X→[a|Z1] とすると、 両方とも append([a, b], [c, d], [a|Z1]) となる。
  2. E1→a, X1→[b], Y1→[c, d], X→[a|e] とすると、 両方とも append([a, b], [c, d], [a|e]) となる。
は単一化代入になります。 1 は最も一般的な単一化代入で、 たとえば、Z1→eとすると 2 になります。

プログラムの実行順序

    p(a).
    p(b).
    q(b, c).
    q(b, d).
    r(X) :- p(Y), q(Y, X).
    ?- r(X).
というプログラムを実行すると次のようになります。 r(X)が節の左側と単一化可能なものを上から順に見ていくと、 最初に上から5個めのr(X) :- p(Y), q(Y, X).という節と単一化可能となるので、 その右側を左から順に調べていきます。 p(Y)について調べてみると、最初に一番上の節p(a)と単一化可能となり、 p(Y)の実行は成功します。 次にq(Y, X)について見ていくと、単一化可能なものはないので、失敗します。 失敗したときはその前のp(Y)が単一化可能な次の節を探します。 するとp(b)と単一化可能となり、p(Y)は成功し、このときは、q(Y, X)はq(b, c)と 単一化可能となるのでq(Y, X)は成功し、最初のr(X)も成功します。 このように1個の項の実行が失敗したときは、その前に実行していた項の まだ調べていない節を調べにいきます。 また、q(Y, X)はq(b, d)とも単一化可能ですが、最初の解に続けて (最初の方が失敗したとして)こちらの方も探すことができます。

このように 単一化可能な節を上から探していく、 左から順に実行していく、 という順序なので、 次のようなプログラムでは最初の解を見つけるときに止まらなくなります。 

    p(X) :- p(f(X)).
    p(f(a)).
    ?- p(X).

    p(X) :- p(f(X)), q(X).
    p(f(a)).
    q(f(a)).
    ?- p(X).

参考文献

  1. 黒川利明: Prologのソフトウェア作法, 岩波書店, 1985.
  2. 後藤滋樹: PROLOG入門 知識情報処理の序曲, サイエンス社, 1984.
  3. 柴山悦哉, 桜川貴司, 萩野達也: Prolog-KABA入門, 岩波書店, 1986.
  4. 中島秀之: Prolog, 産業図書, 1983.
  5. W.F.Clocksin, C.S.Mellish: Prologプログラミング，日本コンピュータ協会, 1983．
  6. 舟本奨: はじめてのProlog，ナツメ社, 1987．
  7. R.Kowalski: 論理による問題の解法, 培風館.
  8. 道具としてのProlog入門編，archive, No.9, CQ出版社．
  9. 道具としてのProlog応用&仕組み編，archive, No.10, CQ出版社．