プログラミング言語が以下のように分類されていることがあります。

命令型
- 手続き型
- オブジェクト指向
宣言型
- 関数型
- 論理型

論理型について馴染みがないので、論理型プログラミング言語 Prolog に入門してみました。

今回は難しい部分には触れません（触れられませんでした）

Prolog とは

1972 年に登場
論理型プログラミング言語に分類される
Erlang という言語に影響を与えた

インストール

Prolog 言語の実装はいくつか存在する。今回は SWI Prolog を使用する。

Mac の場合

brew install swi-prolog

例. Hello World

以下のような内容で hello_world.pl を作成する。

hi :- write('Hello World!').

ファイルを読み込んで実行する。

$ swipl hello_world.pl

?- hi.
Hello World!
true.

Prolog の概要

Prolog のプログラムは論理式の集まり

プログラムを実行する ≒ 述語が定義された環境で定理の証明をおこなう
- 述語論理について勉強すればこの言語の基礎的な構造を理解できるらしい

一階述語論理

Wikipedia より:

一階述語論理（first-order predicate logic）とは、個体の量化のみを許す述語論理 (predicate logic) である。

すべての人間は死ぬ。
ソクラテスは人間である。
したがってソクラテスは死ぬ。

のような文は、それぞれ全称量化記号 (universal quantifier) $\forall$ を使って以下のように記号化できる。

$\forall x (Px \to Qx)$
$Pa$
$Qa$

ホーン節

以下のいずれかで表される節はホーン節と呼ばれる。

否定を含まないリテラルが一つの節（例. $L_1 \vee \neg L_2 \vee \cdots \vee \neg L_n$） ... 確定節と呼ばれる
否定を含むリテラルのみからなる節（例. $\neg L_1 \vee \neg L_2 \vee \cdots \vee \neg L_n$） ... ゴール節と呼ばれる

$\neg P \vee Q$ は $P \to Q$ で置き換えることができるので、以下のような形で表せる。

確定節: $C \leftarrow L_1 \wedge L_2 \wedge \cdots \wedge L_n$
ゴール節: $\leftarrow L_1 \wedge L_2 \wedge \cdots \wedge L_n$

これは Prolog の規則 C :- L1, L2, ..., Ln と対応する。

Prolog の規則の例

grandchild(X, Z) :- child(X, Y), child(Y, Z). /* 確定節 */

?- grandchild(iemitu, ieyasu). /* ゴール節（質問） */

Prolog の記法

節は「頭部」と「本体」で構成される。

<頭部> :- <本体>.

「本体」の true は省略できる

<頭部>.               /* これは以下と同じ */
<頭部> :- true.

述語定義は複数の節からなる。

述語名(引数1, 引数2,..., 引数n) :- <副目標1>, <副目標2>, ..., <副目標m>.

副目標のすべてが真になったときに節の宣言が真になる。

例. grandchild

Prolog では事実の集まりはデータベース (database）と呼ばれる。

質問に適合する事実があれば true を返し、そうでないときは false を返す（「知らない」という意味）。

grandchild(X, Z) :- child(X, Y), child(Y, Z).

child(nobuyasu, ieyasu).
child(hideyasu, ieyasu).
child(hidetada, ieyasu).
child(tadateru, ieyasu).
child(yoshinao, ieyasu).
child(yorinobu, ieyasu).
child(yorihusa, ieyasu).

child(iemitsu, hidetada).
child(tadanaga, hidetada).
child(masako, hidetada).
child(masayuki, hidetada).
child(mitsusada, yorinobu).

$ swipl grandchild.pl

?- grandchild(iemitsu, ieyasu).
true.

?- grandchild(hidetada, ieyasu).
false.

?- child(hideyasu, ieyasu).
true.

?- child(nobutada, nobunaga). /* 事実かもしれないがそのことを Prolog は知らないので false を返す */
false.

単一化

頭部のパターンが一致するかを調べて節の選択を可能にする操作。

知りたい事実を変数（大文字で始まる名前）にして与えると探索してくれる。

例. grandchild（先ほどの続き）

$ swipl grandchild.pl

?- grandchild(X, ieyasu). /* 解の候補を順番に出してくれる */
X = iemitsu ;
X = tadanaga ;
X = masako ;
X = masayuki ;
X = mitsusada.

データ型

Prolog には項と呼ばれるデータ型が存在する。項はいくつかに分類できる。

変数
アトム
数
- 整数
- 浮動小数点数
複合項

例. 2 乗を計算する

square.pl

square(X, Y) :- Y is X * X.

$ swipl square.pl

?- square(2, 3).
false.

?- square(2, 4).
true.

?- square(X, 4).          /* X は求めることができない */
ERROR: Arguments are not sufficiently instantiate
ERROR: In:
ERROR:   [11] 4 is _17012*_17014
ERROR:    [9] <user>
ERROR:
ERROR: Note: some frames are missing due to last-call optimization.
ERROR: Re-run your program in debug mode (:- debug.) to get more detail.

?- square(3, Y).
Y = 9.

再帰

例. 階乗を求める

fact(0, 1).                   /* 0 の階乗は 1 */
fact(N, F) :-
    N > 0,                    /* N > 0 をチェック */
    N1 is N - 1,              /* N - 1 を N1 に求める */
    fact(N1, F1),             /* N1! を F1 に割り当てる */
    F is N * F1.              /* N * F1 を F に求める */

参考 : http://bach.istc.kobe-u.ac.jp/prolog/intro/rec.html

$ swipl fact.pl

?- fact(0, X).
X = 1 .

?- fact(4, X).
X = 24 .

実行過程をトレースする

$ swipl fact.pl

?- trace.
true.

[trace]  ?- fact(4, X).
   Call: (10) fact(4, _8278) ? creep
   Call: (11) 4>0 ? creep
   Exit: (11) 4>0 ? creep
   Call: (11) _8812 is 4+ -1 ? creep
   Exit: (11) 3 is 4+ -1 ? creep
   Call: (11) fact(3, _8902) ? creep
   Call: (12) 3>0 ? creep
   Exit: (12) 3>0 ? creep
   Call: (12) _9038 is 3+ -1 ? creep
   Exit: (12) 2 is 3+ -1 ? creep
   Call: (12) fact(2, _9128) ? creep
   Call: (13) 2>0 ? creep
   Exit: (13) 2>0 ? creep
   Call: (13) _9264 is 2+ -1 ? creep
   Exit: (13) 1 is 2+ -1 ? creep
   Call: (13) fact(1, _9354) ? creep
   Call: (14) 1>0 ? creep
   Exit: (14) 1>0 ? creep
   Call: (14) _9490 is 1+ -1 ? creep
   Exit: (14) 0 is 1+ -1 ? creep
   Call: (14) fact(0, _9580) ? creep
   Exit: (14) fact(0, 1) ? creep
   Call: (14) _9672 is 1*1 ? creep
   Exit: (14) 1 is 1*1 ? creep
   Exit: (13) fact(1, 1) ? creep
   Call: (13) _9810 is 2*1 ? creep
   Exit: (13) 2 is 2*1 ? creep
   Exit: (12) fact(2, 2) ? creep
   Call: (12) _9948 is 3*2 ? creep
   Exit: (12) 6 is 3*2 ? creep
   Exit: (11) fact(3, 6) ? creep
   Call: (11) _8278 is 4*6 ? creep
   Exit: (11) 24 is 4*6 ? creep
   Exit: (10) fact(4, 24) ? creep
X = 24 .