学校の授業でHaskellとPrologを学んでいたんですが、Prologというか論理プログラミングが面白いなあと思ったのでメモすることにしました。
Prologなどの論理型プログラミングは宣言型プログラミングの一種で、記述された知識の集合(knowledge base)をもとにインタプリタへクエリを発行することで解を得るスタイルで利用します。
オンラインのProlog実行環境はSWISHが存在するのでこれを使っていました。
Prologの記法とクエリ
knowledge baseは知識の集合ですが、AならばBというロジックはPrologではB :- A.の形で表現されます。
また、常に成立する事実はAが真になったものと考えて省略し、B.と記述できます。
例えば、knowledge baseが以下のように定義されているとき、
human(bob). % bobはヒトである(常に真)
human(alice).
mammal(X) :- human(X). % ヒトは哺乳類であるクエリhuman(bob)., mammal(alice).はともにtrueとなりますが、human(peter).はマッチするルールが存在しないのでfalseとなります。
ここで、bob, aliceは定数(Atom)の項として扱われていますが、大文字から始まる項(human(X)のX)は変数として扱われます。論理プログラミングにおいて、クエリを成り立たせるような値を変数に束縛することを単一化(unification)といい、特に変数を定数として解決することをインスタンス化するといいます。
先ほどのknowledge baseに対し、クエリとしてhuman(X).を投げてみると、まずX = bobとしてインスタンス化されます。続いてNextをクリックするとX = aliceとしてインスタンス化されます。mammal(X).についても同様にして処理が行われます。
計算をさせる
自然数を定義して演算する
自然数の定義の一つにペアノの公理が存在しますが、Prologでこれを表現することができます。
ペアノの公理を必要最小限で表すと以下のような感じです。
- 0は自然数である。
xが自然数であるとき、s(x)は自然数である。
s() は次の自然数を返す後者関数(successor)です。
自然数であるときに成り立つ述語NatNumberに対して、3に相当する表記s(s(s(0)))は以下のようにして成立することが確かめられます。
\begin{aligned}
NatNumber(s(s(s(0)))) &\Leftarrow NatNumber(s(s(0)))\\
NatNumber(s(s(0))) &\Leftarrow NatNumber(s(0)) \\
NatNumber(s(0)) &\Leftarrow NatNumber(0) \\
NatNumber(0) &\Leftarrow True
\end{aligned}Prologでも、以下のように再帰を使った形で記述することができます。
natnum(0).
natnum(s(X)) :- natnum(X).再帰的にpredicateを定義する場合は、評価の終着点となるルールを記述しないとループしてしまうので気をつけます(数学的帰納法と同じですね)。
ここで定義した自然数と再帰を用いて加算を定義してみます。
形としてはplus(X, Y, Z)として、X + Y = Zが成立するときにTrueとなるように記述すると、以下のようになります。
plus(0, X, X).
plus(s(X), Y, s(Z)) :- plus(X, Y, Z).まず0に何を足しても0なので、0 + X = X、すなわち第1項が0で、第2, 3項が一致していれば成立して良さそうです。
続いてplus(X, Y, Z)が成立している条件下(0 + X = Xを含む)においてXを1増やした場合、加算の結果であるZも1増えます。これを使って加算を再帰的に定義できることとなります。右辺に対してsuccesorを使って左辺の部分の数を増やしているところがミソですね。
一瞬本当に成り立つのか疑問に思ってしまいますが、ある加算に対して第1項を減らしていくと必ず0にはたどり着くのでplus(0, X, X).まで持っていくことができます。ここまでくれば第3項がYの値でインスタンス化され、加算の結果を得ることができます。
実際に1 + 2 = 3を表すクエリを流すと以下のような結果が得られます。
plus(s(0), s(s(0)), s(s(s(0)))). % true
plus(X, s(s(0)), s(s(s(0)))). % X = s(0)
plus(s(0), Y, s(s(s(0)))). % Y = s(s(0))
plus(s(0), s(s(0)), Z). % Z = s(s(s(0)))加算を定義しただけなのに、変数を記述する場所を変えることで足される数も求められる点は結構面白いとおもいます。
これを利用すれば、2数の差を求めるpredicateは次のように書けますね。
diff(X, Y, Z) :- plus(X, Z, Y), !.
diff(X, Y, Z) :- plus(Y, Z, X), !.!はこれよりも前の文がtrueであるときに評価を打ち切る表記です。
X, Yの大小関係によって片方のみではfalseを返してしまう場合があるため2通り書きましたが、これらのパターンは排他的なのでどちらかが成り立てば他方の評価はfailになる(X = Yの場合を除く)ので途中で打ち切っても問題ありません。
この感じで次は乗算を定義してみます。
まずベースとなるルールですが、加算のときは0に何を足しても変わらない性質を使ったのと同様に、0に何をかけても0なのでtimes(0, X, 0).を定義します。
続いてtimes(X, Y, Z).が成立しているとき、Xを1増やすとZはYだけ増えます。先ほどと違いYだけ増やすというロジックが必要になりましたが、これは既に定義したplusを使えばすぐに解決します。
というわけで、乗算の定義はこんな感じになります。
times(0, X, 0).
times(s(X), Y, Z) :- times(X, Y, Z1), plus(Z1, Y, Z).カンマは「かつ」、すなわちANDを示す演算子です。左辺をtimes(s(X), Y, Z)と記述している一方で、Xの値を増やす前のZの値をtimes(X, Y, Z1)としてZ1にインスタンス化しています。このZ1の値とYの和が、今求めたいZとなっていれば乗算として正しいものと定義しています。
早速2 * 3 = 6を表すクエリを流してみます。
times(s(s(0)), s(s(s(0))), s(s(s(s(s(s(0))))))). % true
times(s(s(0)), s(s(s(0))), Z). % Z = s(s(s(s(s(s(0))))))
times(X, s(s(s(0))), s(s(s(s(s(s(0))))))). % X = s(s(0))乗算が普段の感覚と同じように演算できている様子がわかります。
定義した加算を使って、フィボナッチ数列のN番目の値Fを表すpredicatefibo(N, F)を定義してみたいと思います。
フィボナッチ数列は以下のようにして定められます。
\begin{aligned}
F_0 &= 0 \\
F_1 &= 1 \\
F_n &= F_{n-2} + F_{n-1}
\end{aligned}ベースとなるケースは明らかにF_0, F_1の2つです。
fibo(0, 0).
fibo(s(0), s(0)).続いて再帰的な定義になりますが、これまでと同様に2つ手前までの数を用意し、それぞれ同じpredicateを呼び出して対応する値をインスタンス化します。これらの和が現在のFと一致するように組み立てればOKなので、以下のようになります。
fibo(0, 0).
fibo(s(0), s(0)).
fibo(s(s(N)), F) :- fibo(s(N), F1), fibo(N, F2), plus(F1, F2, F).1つ手前のフィボナッチ数をF1, 2つ手前のフィボナッチ数をF2にインスタンス化しています。
動作を確認するとこんな感じになります。
fibo(s(s(0)), F). % F = s(0)
fibo(s(s(s(s(0)))), F). % F = s(s(s(0)))フィボナッチ数1に対応するのは1, 2番目ですが、fibo(N, s(0)).はどのようにunificationされるでしょうか。実際に実行すると、以下のように両方出力されるのでもれなく列挙されることがわかります。
fibo(N, s(0)).
N = s(0)
N = s(s(0))まとめ
論理プログラミングで計算ってどうやるの？から始まりunificationの賢さを実感しつつ、なかなか普段しない頭の使い方をしたので大変なところもありました。
普通の手続き型プログラミングでは逆の演算は別個で書かないといけないのに対して、ベースとなるルールに基づく論理プログラミングではロジックを考える必要なしに実行できる点がとても新鮮に感じました。