PAIPrologをつくろうの会

参考文献

PAIP Prologを商用で使いやすくしたもの: Allegro Prolog (ホビー用途なら無料)

PAIP PrologをAllegro Prolog に寄せたもの: Allegretto Proolog

実装

Prologおもしろ話

yarnの依存関係解決は独自実装されたprologで解決されていた

/icons/hr.icon

第n回 xxxx/xx/xx 担当: tani

(:start *** :end ***)

2nd シーズン開始!

/icons/hr.icon

第7回 2025/02/25 担当: conao3

(:start "11.3 Idea 3: Automatic Backtracking" :end "11章の終わりまで")

読書回。

お困り相談と進捗

ゼブラパズルが動かない。。CommonLisp版をコピペしても動かない

prolog in prologの例も動かない。解が出力されてないだけ?

次回こそ12章に入ってprologコンパイラだ!

11.3 automatic backtracking

prolog実装には2つの実装方法がある。

prolog1.lispのようなアプローチをbatch approach

これから実装するのがincremental approach

バッチアプローチの特徴

前のセクションで実装したもの。すべての可能な解のリストを返却することで問題を解決する

これを「バッチアプローチ」と呼ぶ。なぜなら答えが一連の処理のバッチとして取得されるから

場合によってはこれがまさに求めているものであるが、他の場合では単一の解で十分なこともある

インクリメンタルアプローチの特徴

実際のPrologのように動作し、解は見つかった順に一つずつ表示される

各解が表示された後、ユーザーは次の解を見つけるか、停止するかを選択できる

これを「インクリメンタルアプローチ」と呼ぶ

インクリメンタルアプローチの利点

複数の解のうち、多数の解のうち最初の方にある場合、インクリメンタルアプローチはより高速に動作する

解が無限にある場合でも機能する

深さ優先探索で実装することができ、任意の時点で必要な記憶領域がバッチアプローチより少ない。

インクリメンタルアプローチの実装

listではなく、pipeを利用するようにする

pipeを利用することで必要ない計算は遅延され、無限個のリストは有限の時間と空間になる

pipeにするのは簡単で、mapcanをmappend-pipeにするだけで済む

この実装方法は Winston and Horn (1988) and by Abelson and Sussman (1985) で利用されている

我々は違う方法で実装する

proveとprove-allが全ての解ではなく、一つの解を返却するようにする

これはchapter4のgpsのacheveとacheve-allの関係に似ている

proveの動作

gpsと違うのは再帰的なサブゴールやclobbered sibling goalはチェックしないこと

これはproveに継続を渡すことと同等

これによりproveが成功した場合、トップレベルのゴール全体が成功したことになる

失敗した場合、バックトラッキングを行い、違う選択肢を試す

proveはnilがfailだという事実に依存していることに注意

proveが成功した場合

proveが成功した場合、解が見つかったことを意味する

さらに多くの解が必要な場合、プロセスを失敗させればよい

そうするとバックトラッキングが行なわれ、もう一度試すことになる

一つの方法として、全てのクエリを拡張し、変数を出力してユーザーに計算を続行するかどうかを尋ねるゴールを追加することができる

ユーザーがyesと答えた場合、ゴールは「失敗」し、バックトラッキングが行なわれる

ユーザーがnoと答えた場合、ゴールは成功し、それが最終ゴールだった場合、そこで計算は終了する

プリミティブ

これにはデータベースに対してマッチングさせるのではなく、何らかの手続きを実行する新しいタイプのゴールが必要

Prologでは「プリミティブ」と呼ばれている

なぜなら言語組込みでありユーザーが新しいものを定義することはできないから

ユーザーはプリミティブを呼び出す非プリミティブな手続きを定義することはできる

私たちの実装ではプリミティブはlisp関数として実装される

述語はこれまで通り節のリストとして表現されるか、または単一のプリミティブとして表現される

すべてのプリミティブは3つの引数を受け取る関数でなければならない

プリミティブ関係への引数のリスト(ここでは表示する変数のリスト)

これらの引数のバインディングリスト

保留中のゴールのリスト

プリミティブの登録

(setf (get 'show-prolog-vars 'clauses) 'show-prolog-vars)

動作例

このバージョンは有限の問題に対して前のバージョンと同様に動作する。

唯一の違いはセミコロンを入力するのがシステムではなく、ユーザーであること

利点は無限の問題にもシステムを利用することができること

code:lisp

(?- (member 2 ?list))

?LIST = (2 . ?REST3302);

?LIST = (?X3303 2 . ?REST3307);

?LIST = (?X3303 ?X3308 2 . ?REST3312);

?LIST = (?X3303 ?X3308 ?X3313 2 . ?REST3317).

No.

この結果は2が先頭に含まれるリスト、2番目の要素が2であるリスト、3番目の要素が2であるリストなどであることを意味する

ユーザーがセミコロンではなくピリオドを入力した時点で無限の計算が停止する

「No」はこれ以上表示する解がないことを意味する

これは以下の状態である

解が全くない場合

ユーザーがピリオドを入力した場合

全ての解を出力した場合

より抽象的なクエリの例

より抽象的なクエリも聞くことができる

code:lisp

(?- (member ?item ?list))

?ITEM = ?ITEM3318

?LIST = (?ITEM3318 . ?REST3319);

?ITEM = ?ITEM3323

?LIST = (?X3320 ?ITEM3323 . ?REST3324);

?ITEM = ?ITEM3328

?LIST = (?X3320 ?X3325 ?ITEM3328 . ?REST3329);

?ITEM = ?ITEM3333

?LIST = (?X3320 ?X3325 ?X3330 ?ITEM3333 . ?REST3334).

No.

lengthの例

このようにlengthを定義する

code:lisp

(<- (length () 0))

(<- (length (?x . ?y) (1 + ?n)) (length ?y ?n))

このような動作例が得られる

code:lisp

(?- (length (a b c d) ?n))

?N = (1 + (1 + (1 + (1 + 0))));

No.

code:lisp

(?- (length ?list (1 + (1 + 0))))

?LIST = (?X3869 ?X3872);

No.

code:lisp

(?- (length ?list ?n))

?LIST = NIL

?N = 0;

?LIST = (?X3918)

?N = (1 + 0);

?LIST = (?X3918 ?X3921)

?N = (1 + (1 + 0)).

No.

無限ループになってしまう例

code:lisp

(?- (length ?l (1 + (1 + 0))) (member a ?l))

?L = (A ?X4057);

?L = (?Y4061 A);

No.

code:lisp

(?- (member a ?l) (length ?l (1 + (1 + 0))))

?L = (A ?X4081);

ただし、これら2つの解を生成した後の動作は極めて異なる

最初のクエリ

2番目のクエリ

そのため、ユーザーが中断するまで動作は停止しない

Prologの制約

この例はPrologが純粋な論理プログラミング言語として持つ制約を明らかにしている

ユーザーは問題の論理だけではなく、制御の流れにも注意を払う必要がある

Prologは探索空間が小さい場合にはバックトラックを行い、すべての解を見つけることができる

しかし、探索空間が無限(もしくは非常に大きい)場合、プログラマーは制御の流れを導く責任がある

Prologの位置付け

自動的な制御の流れをより多くサポートする言語を設計することは可能である

しかしPrologは手続き型言語と純粋な論理プログラミングの中間として、便利で効率的な基盤を提供する

バックトラッキングへのアプローチ

問題設定

既存のプログラムに「小さな」変更を加えることを求められていることする

プログラマーの選択肢は以下の5つである

推測

1つの可能性を選び、他の可能性を破棄する

正しい推測を行う手段、または間違った推測から回復する手段が必要

知る

追加の情報を提供することで、正しい選択肢を決定する

呼び出し元の関数を変更し、追加の情報を得る必要がある

リストを返却する

複数の返り値をリストとして返却する

呼び出し元の関数を変更し、リスト形式の返り値を期待するようにする必要がある

パイプを返す

呼び出し元の関数を変更し、パイプ形式の返り値を期待するようにする必要がある

推測して保存

1つの可能性を選んで返すが、他の可能性を後で計算できるよう十分な情報を記録する

現在の計算状態と、残りの可能性に関する情報を保存する必要がある

最適な選択肢

最後の「推測して保存」が最も望ましい

効率的: 使用されない答えを計算する必要がない

非侵襲的: 呼び出し元の関数を変更する必要がない

ただし大きな課題がある

現在の計算状態をパッケージ化して保存し、最初の選択肢がうまくいかない場合に戻れるようにする必要がある

Prologインタープリタの場合

現在の状態は、ゴールのリストとして簡潔に表現される

他の問題では、計算状態全体を簡単に要約することはできない

Schemeの機能

この関数は現在の計算状態を関数としてパッケージ化し、保存して後で呼び出すことができる

残念ながらCommonLispにこれに相当する機能はない

11.4 ゼブラパズル

Prologの得意とする例

ここではPrologの非常に得意とする論理パズルの例を示す

このパズルには15の事実が含まれている

パズルの制約

5つの家が一列に並んでおり、それぞれに所有者、ペット、煙草、飲み物、色がある

イギリス人は赤い家に住んでいる

スペイン人は犬を飼っている

コーヒーは緑の家で飲まれる

ウクライナ人はお茶を飲む

緑の家は象牙色の家のすぐ右隣にある

ウィンストンを吸う人はカタツムリを飼っている

クールズは黄色い家で吸われる

ミルクは真ん中の家で飲まれる

ノルウェー人は左端の家に住んでいる

チェスターフィールドを吸う人はキツネを飼っている人の隣に住んでいる

クールズを吸う人は馬を飼っている家の隣に住んでいる

ラッキーストライクを吸う人はオレンジジュースを飲む

日本人はパーラメントを吸う

ノルウェー人は青い家の隣に住んでいる

回答すべき質問

水を飲むのは誰か

ゼブラを飼っているのは誰か

パズルを解くための準備

code:lisp

(<- (member ?item (?item . ?rest)))

(<- (member ?item (?x . ? rest)) (member ?item ?rest))

(<- (nextto ?x ?y ?list) (iright ?x ?y ?list))

(<- (nextto ?x ?y ?list) (iright ?y ?x ?list))

(<- (iright ?left ?right (?left ?right . ?rest)))

(<- (iright ?left ?right (?x . ?rest))

(iright ?left ?right ?rest))

(<- (= ?x ?x))

恒等関係の定義

恒等関係を定義する

ゼブラパズルの定義

ゼブラパズルを1つの節で定義する準備が整った

パズルの制約の表現

ただし制約9と10は最初の制約に組み合わされている

例えば、制約2「イギリス人は赤い家に住んでいる」は「国籍がイギリス人で色が赤い家が家のリストに含まれている」と解釈する

他の制約も同様に表現していく

実行時間とパフォーマンス

これは46LIPS (Logical inferences per second) に相当する

優れたPrologシステムは10,000から100,000LIPS以上の性能を持つため、このシステムは非常に低速である

問題の小さな変更が検索時間に与える影響

問題に対する小さな変更が、検索時間に大きな影響を与えることがある

これらの節の順序は任意であり、どちらの順序でリストしても違いがないように思えるかもしれない

しかし、実際にはこれら2つの節の順序を逆にすると、実行時間がほぼ半分に短縮される

考察

この結果はPrologのバックトラッキングアルゴリズムが節の順序に敏感であることを示している

効率的なプログラムを作成するためには、節の順序や制約の記述方法に注意を払う必要がある

11.5 The Synergy of Backtracking and Unification

バックトラッキングを用いた後向き推論

Prologのバックトラッキングを伴なう後向き推論は、問題の可能な解を生成するための強力な方法である

この手法により、可能な解を1つずつ検討し、候補が棄却された場合に次の候補を提案する「生成-テスト(generate-and-test)」戦略を簡単に実装できる

ただし、生成-テスト戦略は、可能な解の空間が小さい場合にのみ実用的である

ゼブラパズルの解空間

ゼブラパズルでは、5うの家それぞれに5つの属性がある

したがって解候補の総数は5!^5(約240億)通りであり、1つずつテストするには多すぎる

単一化(およびそれに対応する論理変数の概念)が、このパズルにおいて生成-テスト戦略を実用的にする鍵である

部分的な候補の指定

完全な候補解を列挙する代わりに、単一化を使用して部分的な候補を指定する

例えばノルウェー人が左端に住んでおり、ミルクを飲む人が真ん中の家に住んでいるという2つの制約から始める

これらの制約を満たす完全な候補をすべて生成するのではなく、残りの情報を匿名の論理変数として曖昧にしておく

制約の適用と単一化

次の制約はイギリス人が赤い家に住んでいることを指定する

しかしイギリス人とノルウェー人は単一化できないため、この配置は棄却され、次の可能性が検討される

イギリス人は2番目の家に配置されるが、2番目の家の他の属性(色、飲み物など)は指定されない

これにより、不要な推測を避けることができる

効率的な探索

探索は必要な情報だけを生めながら進み、単一化が失敗した場合にはバックトラッキングする

このアプローチにより、計算が行なわれる前にバックトラッキングが発生した場合でも時間を節約できる

一方で、後で値を生めることも可能である

単一化の拡張

単一化を拡張することで、より多くの作業を単一化に任せ、バックトラッキングの作業量を減らすことができる

code:lisp

(?- (length ?l 4)

(member d ?l) (member a ?l) (member c ?l) (member b ?l)

(= ?l (a b c d)))

このプロセスの大部分はバックトラッキングによって行なわれる

単一化の拡張

別のアプローチとして単一化を拡張して定数や変数だけではなく、リストも扱えるようにする

11.6 Destructive Unification

バインディングリストの課題

セクション11.2で見たように変数のバインディングリストを管理するのは少し複雑である

またバインディングリストが大きくなると非効率になりやすい

なぜなら、リストを線形探索する必要があり、バインディングリストを保持するためのメモリを確保する必要があるからである

破壊的単一化のアプローチ

このアプローチではバインディングリストは存在しない

代わりに、各変数はそのバインディングを保持するフィールドを含む構造体として表現される

変数が他の式と単一化されると、変数のバインディングフィールドがその式を指すように変更される

code:lisp

(defconstant unbound "Unbound")

(defstruct var name (binding unbound))

(defun bound-p (var) (not (eq (var-binding var) unbound)))

変数が未束縛であるか、非変数式である場合はその引数を返す

変数が別の変数に束縛されている場合、その変数もさらに束縛されている可能性があるため、ループが含まれている

なぜなら、インライン関数として実装できるからである

code:lisp

(defmacro deref (exp)

"Follow pointers for bound variables."

'(progn (loop while (and (var-p ,exp) (bound-p ,exp))

do (setf ,exp (var-binding ,exp)))

,exp))

11.7 Prolog in Prolog

Lisp処理系でLisp処理系を簡単に書くことができるように、Prolog処理系でPrologを書くこともまた簡単である

code:lisp

(<- (prove ?goal) (prove-all (?goal)))

(<- (prove-all nil))

(<- (prove-all (?goal . ?goals))

(clause (<- ?goal . ?body))

(concat ?body ?goals ?new-goals)

(prove-all ?new-goals))

(<- (clause (<- (mem ?x (?x . ?y)))))

(<- (clause (<- (mem ?x (? . ?z)) (mem ?x ?z))))

code:lisp

(?- (prove (mem ?x (1 2 3))))

?X = 1;

?X = 2;

?X = 3;

No.

11.8 Prolog Compared to Lisp

PrologがAI(および一般的なプログラム開発)で成功している理由

PrologとLispの共通点

PrologがAIやプログラム開発に成功している多くの特徴はLispの特徴と共通している

従来の言語とLispを区別する特徴を再考し、Prologが提供するものを確認する

以下のポイントが存在する

リスト(および他のデータ型)の組込みサポート

新しいデータ型はリストや構造体を使用して簡単に作成できる

読み取り、印刷、及びコンポーネントへのアクセスのサポートが自動的に提供される

数値、シンボル、文字もサポートされている

ただし、論理変数は変更できないため、特定のデータ構造や操作は提供されない

例えばPrologではベクトルの要素を更新する方法はない

自動ストレージ管理

プログラマーは新しいオブジェクトを割り当てる際に、その回収を心配する必要はない

ほとんどのデータはヒープではなくスタックに割り当てられるため、Prologでの回収は通常Lispよりも高速である

動的型付け

宣言は必要ない

実際、型宣言を行う標準的な方法はないが、一部の実装では型宣言が可能である

一部のPrologシステムは固定長整数のみを提供するため、多くの宣言が不要になる

第一級関数

バックトラッキングの選択ポイントは第一級オブジェクトではないが、Lispの継続と非常に似た文法で利用できる

統一された構文

Lispと同様に、Prologはプログラムとデータの両方に対して統一された構文を持つ

これにより、Prologでインタプリタやコンパイラを直接書くことができる

Lispの前置演算子リスト表記はより統一されているが、Prologは中置及び後置演算子を許可するため、一部のアプリケーションではより自然である

対話型環境

式を即座に評価できる

高品質のPrologシステムは、コンパイラとインタプリタの両方を提供し、多くのデバッグツールを備えている

拡張性

Prologの構文は拡張可能である

プログラムとデータが同じ形式を共有しているため、Prologでマクロに相当するものを書いたり、組込み言語を定義したりすることが可能である

ただし、結果のコードが効率的にコンパイルされることを保証するのは難しい場合がある

Prologのコンパイルの詳細は実装に依存する

11.9 History and References

略

11.10 Exercises

略

/icons/hr.icon

第6回 2025/02/03 担当: conao3

休憩回。デバッグ重すぎて進捗悪かったです。:big-sorry:

お困り案件

名前空間ってどうやって認識させたらいいんだろう? とりあえず1ファイル完結にすると動いたからそれでやってた。

なんか勝手にターミナル幅に合わせてpprintされるの止めたい。このせいで情報密度が下がってるので困ってる。

tips

まずCommonLisp実装を動かせるようにする。

CommonLisp処理系: sbcl

HomebrewなりNixなりでインストールすると良いです。

code:bash

sbcl

This is SBCL 2.4.10, an implementation of ANSI Common Lisp.

SBCL is free software, provided as is, with absolutely no warranty.

It is mostly in the public domain; some portions are provided under

BSD-style licenses. See the CREDITS and COPYING files in the

distribution for more information.

*

プログラムの実行

つまりこう

code:lisp

cat sample.lisp

(format t "hello~&")

(format t "world~&")

sbcl --script sample.lisp

hello

world

code:lisp

sbcl --script dev/ref/prolog1.lisp

db: NIL

db: (MEMBER)

db.member: (((MEMBER ?ITEM (?ITEM . ?REST))))

db: (MEMBER)

db.member: (((MEMBER ?ITEM (?ITEM . ?REST)))

((MEMBER ?ITEM (?X . ?REST)) (MEMBER ?ITEM ?REST)))

goals=((MEMBER 2 (1 2 3))) bindings=((T . T))

goals=NIL bindings=NIL

res=NIL

goals=((MEMBER ?ITEM102 ?REST103)) bindings=((?REST103 2 3) (?X101 . 1)

(?ITEM102 . 2))

goals=NIL bindings=((?REST105 3) (?ITEM104 . 2) (?REST103 2 3) (?X101 . 1)

(?ITEM102 . 2))

res=(((?REST105 3) (?ITEM104 . 2) (?REST103 2 3) (?X101 . 1) (?ITEM102 . 2)))

goals=((MEMBER ?ITEM107 ?REST108)) bindings=((?REST108 3) (?X106 . 2)

(?ITEM107 . 2) (?REST103 2 3)

(?X101 . 1) (?ITEM102 . 2))

goals=NIL bindings=NIL

res=NIL

goals=((MEMBER ?ITEM112 ?REST113)) bindings=((?REST113) (?X111 . 3)

(?ITEM112 . 2) (?REST108 3)

(?X106 . 2) (?ITEM107 . 2)

(?REST103 2 3) (?X101 . 1)

(?ITEM102 . 2))

goals=NIL bindings=NIL

res=NIL

goals=((MEMBER ?ITEM117 ?REST118)) bindings=NIL

res=NIL

res=NIL

res=NIL

goals=NIL bindings=((?REST105 3) (?ITEM104 . 2) (?REST103 2 3) (?X101 . 1)

(?ITEM102 . 2))

res=(((?REST105 3) (?ITEM104 . 2) (?REST103 2 3) (?X101 . 1) (?ITEM102 . 2)))

res=(((?REST105 3) (?ITEM104 . 2) (?REST103 2 3) (?X101 . 1) (?ITEM102 . 2)))

goals=NIL bindings=((?REST105 3) (?ITEM104 . 2) (?REST103 2 3) (?X101 . 1)

(?ITEM102 . 2))

res=(((?REST105 3) (?ITEM104 . 2) (?REST103 2 3) (?X101 . 1) (?ITEM102 . 2)))

res=(((?REST105 3) (?ITEM104 . 2) (?REST103 2 3) (?X101 . 1) (?ITEM102 . 2)))

Yes;

Clojure実装におけるtips

CommonLispとの一般的な違いは公式ドキュメントを参照。

特に以下の点は注意

動的に変更したい場合は専用のデータ構造を使う。Atomとか。

optional引数はない。オーバーロードにより引数が少ない関数を定義して、明示的に呼ぶことで表現する。Javaと同じ。

code:clojure

(defn my-inc "n に1足す関数"

(+ n 1))

;; FIXME: こういう宣言はできない

(defn my-inc "n に step(default=1) 足す関数"

(+ n step))

;; こうやって宣言する。docstringが引数の前にあるのはこういう文法の拡張があるため。

(defn my-inc

"n に step(default=1) 足す関数"

(my-inc n 1))

(+ n step)))

code:clojure

;;=> (true false false false false false false)

ドット対はない。そのため、以下の対応になる。

code:clojure

(map rest

;;=> ((2 3) (3) ())

(map next

;;=> ((2 3) (3) nil)

code:clojure

(cons 1 2)

;;=> 1. Unhandled java.lang.IllegalArgumentException

;; Don't know how to create ISeq from: java.lang.Long

(cons 1 '(2))

;;=> (1 2)

(cons '(1 2 3) '(4 5 6))

;;=> ((1 2 3) 4 5 6)

code:clojure

(defn unify

(unify x y {}))

;; care about notation of cons-cell.

(and (seq? %) (= '. (first %)))

(when (not= 2 (count a))

(throw (ex-info "exact 1 element after `.'" {})))

(second a))))

x (peal-cdr-fn x_)

y (peal-cdr-fn y_)]

(cond

(nil? bindings) nil

(= x y) bindings

(variable? x) (unify-variable x y bindings)

(variable? y) (unify-variable y x bindings)

(and (sequential? x) (sequential? y))

(unify (next x) (next y)

(unify (first x) (first y) bindings))))))

code:clojure

(= 1 1)

;;=> true

(= '(1 2 3) '(1 2 3))

;;=> true

;;=> true

;;=> true

基本コンテナ(シーケンス)は以下

code:clojure

(range 5)

;;=> (0 1 2 3 4)

(class (range 5))

;;=> clojure.lang.LongRange

(class '(0 1 2 3 4))

;;=> clojure.lang.PersistentList

property listはない。素直に別のデータ構造で表現しよう。マップとか。

とはいえ「メタデータ」というのはある。これでできるかも。

code:clojure

(def s (with-meta 'a {:a 1}))

(meta s)

;;=> {:a 1}

末尾再帰最適化はあるが、再帰ポイントを自分で明示的に指定する必要がある。そのため、何も対策しない場合は普通の関数呼び出しになるため、当然、スタックオーバーフローの危険がある。

code:clojure

(if (= 0 step)

n

(my-inc (+ n 1) (- step 1))))

(my-inc 5 5)

;;=> 10

(my-inc 5 5000000)

;;=> 1. Unhandled java.lang.StackOverflowError

;; (No message)

(if (= 0 step)

n

(recur (+ n 1) (- step 1)))) ; loopのないrecurは、暗黙のloopが関数のbodyにあるため、それが採用される

(my-inc' 5 5000000)

;;=> 5000005 ; これならループに変換されるため、スタックオーバーフローにならない

/icons/hr.icon

第5回 2025/01/30 担当: tani

Programming with Prolog 箇所から

code:prolog

(<- (member ?item (?item . ?rest)))

(<- (member ?item (?x . ?rest)) (member ?item ?rest))

以下と同じ

code:prolog

(<- (member ?item ?list)

(= ?list (?item . ?rest)))

(<- (member ?item ?list) ; ?list = nil

(= ?list (?x . ?rest))

(member ?item ?rest))

このような定義もできる

↑ 全体を句と呼ぶ。 A を先頭、B C D を ボディと呼ぶ。

code:prolog

(<- (member ?item ?list)

(= ?list (?first . ?rest));

(or (= ?item ?first)

(member ?item ?rest)))

定義の読み方

code:prolog

(defun prove-all (goals bindings)

"Find a solution to the conjunction of goals."

(cond ((eq bindings fail) fail) ; 1

((null goals) bindings) ; 2

(t (prove (first goals) bindings (rest goals))))) ; 3

1. 前のステップで既に束縛が失敗していたら、この証明探索自体も失敗にする

2. もう証明するべきものがないなら、 束縛変数の状態を返す

code:prolog

(defun prove (goal bindings other-goals)

"Return a list of possible solutions to goal."

(let ((new-clause (rename-variables clause)))

(prove-all

(append (clause-body new-clause) other-goals)

(unify goal (clause-head new-clause) bindings))))

(get-clauses (predicate goal))))

そして、シンボル自体に登録された句情報を取りだす

(((MEMBER ?ITEM (?ITEM . ?REST)))((MEMBER ?ITEM (?X . ?REST)) (MEMBER ?ITEM ?REST)))

a, b をもとにすべて証明する!

code:prolog

(defun prove (goal bindings other-goals)

"Return a list of possible solutions to goal."

(let ((clauses (get-clauses (predicate goal))))

(if (listp clauses)

(some

(let ((new-clause (rename-variables clause)))

(prove-all

(append (clause-body new-clause) other-goals)

(unify goal (clause-head new-clause) bindings))))

clauses)

;; The predicate's "clauses" can be an atom:

;; a primitive function to call

(funcall clauses (rest goal) bindings

other-goals))))

/icons/hr.icon

第4回 2025/01/23 担当: Sirasagi62

自己紹介

Sirasagi62 初心者Lisper

Lispは今回が初めてです

普段はTypescript,Golang,Pythonなどの手続き系が多いです

コードの読解

マッチング

パターンマッチングユーティリティ

unfiy関数

文献1,2のアルゴリズムのStep2に相当

一致しているから終了

Step3に相当

unify-variable関数

最初の2つの分岐は同じ処理の順序を逆にしているだけ

デフォルト= bindingが見つからない場合は追加する

unifier関数

代入リストの中身を実際に代入していく

コードの読解

PrologのDB

概説

基本はKVS

Lispのシンボルを使うので(手続き型を使う自分にとっては)ややトリッキー

データ構造の違い

clause-*関数

Prologの節

Prologの節をheadとbodyに分解する

get-clauses関数

KVSのKeyに対応するValueを取り出す操作だが...

シンボル自体に節を格納していることに注意

情報そのものは述語シンボルが持つ

hashmap,a-listで実装しても問題ないと思う

predicate

各relationの述語を取得する

(like Alice Bob) -> like

add-clause関数

ゴール節の後件の述語をキーにしている

prove関数とprove-all関数

読解のポイント:unifyによってbindingを生成するので、証明に失敗するとbindingがnilとなる

それを引数としているprove-allも失敗してくれる

成功した場合にはその前提の証明を一通り試みる

動作を順を追って確認してみる

1. 最初の目標と代入の処理

code: (lisp)

---prove-all---

goals: ((IS-A FUJI APPLE))

bindings: ((T . T))

---prove---

goal: (IS-A FUJI APPLE)

bindings: ((T . T))

clauses: (((IS-A FUJI FRUIT))

((IS-A ?OBJECT APPLE) (IS-A ?OBJECT FRUIT) (COLOR ?OBJECT RED)))

2. 最初のルールの適用(最初の目標：(IS-A FUJI APPLE))

code: (lisp)

each clause: ((IS-A FUJI FRUIT))

---prove-all---

goals: NIL

bindings: NIL

よって、bindingsがfail(nil)となる

このルールは棄却

3. 次のルールの適用(最初の目標：(IS-A FUJI APPLE))

code: (lisp)

each clause: ((IS-A ?OBJECT APPLE) (IS-A ?OBJECT FRUIT) (COLOR ?OBJECT RED))

---prove-all---

goals: ((IS-A ?OBJECT2421 FRUIT) (COLOR ?OBJECT2421 RED))

bindings: ((?OBJECT2421 . FUJI))

新しい目標として次の2つが追加：

4. 次の目標　(IS-A ?OBJECT2421 FRUIT)の処理

code: (lisp)

---prove---

goal: (IS-A ?OBJECT2421 FRUIT)

bindings: ((?OBJECT2421 . FUJI))

clauses: (((IS-A FUJI FRUIT))

((IS-A ?OBJECT APPLE) (IS-A ?OBJECT FRUIT) (COLOR ?OBJECT RED)))

each clause: ((IS-A FUJI FRUIT))

---prove-all---

goals: NIL

bindings: ((?OBJECT2421 . FUJI))

代入はそのまま維持

これ以上、示す目標はないので代入を維持して、戻る

5. 次の目標 (COLOR ?OBJECT2421 RED)の処理

code: (lisp)

---prove---

goal: (COLOR ?OBJECT2421 RED)

bindings: ((?OBJECT2421 . FUJI))

clauses: (((COLOR FUJI RED)))

each clause: ((COLOR FUJI RED))

---prove-all---

goals: NIL

bindings: ((?OBJECT2421 . FUJI))

代入は引き続き維持

これ以上、示す目標はないので代入を維持して、戻る

6. 結果のまとめ

最終的な代入：

code: (lisp)

bindings: ((?OBJECT2421 . FUJI))

目標をすべて示せたので終了

クエリが正しいことが示された

変数関連

rename-varibales

gensymで変数名を置き換えている

異なる節で同一の変数名が登場したときに対応する

variable-in

証明するgoalに含まれる一意な変数を抽出している

証明が完了したあとに、bindingと照らし合わせながらいい感じに出力するために使う

漸進的アプローチ

1つ証明を見つけるたびに中断する

中断後、続けるかどうかをユーザーに尋ねる

noの場合は成功したことにして探索を終了

余談

なぜ最汎単一化代入(most general unifier,mgu)となることを保証できるのか

Robinsonによって単一化定理(Unification Theorem)として示されている(1965,文献1)

日本語での証明は有川,原口の「述語論理と論理プログラミング」(1988,文献2)のp89に掲載されている(p84あたりから用語の定義があるのでそっちから読んだほうが分かりやすい)

証明の概略（以下は文献2の定理3・10に基づいてる）

用語:

集合であることに注意。2つ以上与えられても各項目が一致したら1つになる

PAIPの実装だと最大でも2

文献1,文献2でもドット積のような記法で表している

code:typescript

function composition (theta: set, lambda: set) {

// theta={x->f(a),y->b} lambda={a->g(b),b->y,x->a}

// lambdaの代入をすべてthetaに適用する

// theta1={x->f(g(b)),y->y}

const theta1 = theta.substituteBy(lambda)

// (y.y)みたいになっている要素を削除する

// theta2={x->f(g(b))} // y:yが削除

const theta2 = theta1.deleteSelfReference()

// theta2とlambdaのどちらにもある同じkeyが存在する場合、lambda側を削除する

// lambda1={a->g(b),b->y} // x:aが削除

const lambda1 = lambda.deleteDuplicatedKeys(theta2)

// 集合の和

return sum(theta1,lambda1)

// 返り値:{x->f(g(b)), a->g(b), b->y}

}

証明の流れ

Aが単一化不能であることを発見した場合

のどちらかであり、単一化可能な例を発見して停止した場合はループ不変条件によりMGUとなる

つまり？

単一化可能な場合は最初に単一化できた時点で終了する

単一化できるまで代入をどんどん追加していく

MGUは単一化代入の中で最小の場合

=>初めて単一化できたタイミング=代入がMGU

厳密な証明（特に条件式がループ不変条件になる理由）は文献2を参照されたし

関東圏だと東京、埼玉、千葉あたりは県立図書館に所蔵あり

これ以外に導出原理自体の完全性、停止性や否定の導出などにも言及あり

その他

高速化について

PAIPで用いられているコンパイルとは別にWarren Abstract Machine(WAM)というアプローチもある（言及あり）

以下の本で詳述されているらしい

T. Dobry, A high performance architecture for PROLOG. Kluwer Academic Publishers, 1990.

並行処理化

ICOTによる第五世代コンピュータプロジェクトで試みられた

GHCという並行推論言語を実装したらしい

パイプライン化に近い雰囲気（文献3）

GPGPUによる並列処理化はできるかもしれないが難しそう

その他のアイディア

SAT solverなどではGNNを使うアプローチもあるらしい

現実世界での応用例について

Prologの文法と応用についてまとめられたサイト

IBMのWatsonも部分的に用いているらしい

近年ではLLMと組み合わせる研究もある

GraphRAGという手法はPrologにかなり近いことをやっている

Prologの代わりにNeo4jなどのグラフDBと組み合わせている

Prologの方ができることの幅は広いので、Prologにも波及するかも

ELIZA

2024/12/21にオリジナルのELIZA(SLIP版)の起動に成功したらしい(文献4)

GitHubのレポ

余談の余談：Jagger

参考文献

code:references

/icons/hr.icon

第3回 2025/01/16 担当: lambdair

11.2 unification(Programming with Prologの直前)まで

自己紹介

lambdair 職業Lisper

トヨクモでClojure書いてます

会社入ってからちゃんと使い始めたのでLispの経験としては2年目ぐらい

プライベートではisabelle/holやlean4などの定理証明系で遊んでいます

本編

単一化（unification）について学ぶ

単一化とは？

ざっくりいうと、パターンマッチを双方向に拡張したもの

以下のようなものが動く

code:scheme

(unify '(?x + 1) '(2 + ?y))

;; => ((?Y . 1) (?X . 2))

また，変数同士をマッチさせられるのも特徴

code:scheme

(unify '(f ?x) '(f ?y))

;; => ((?X . ?Y))

ただし，パターンマッチにできて単一化にできないこともある

単一化は構文的に変数が他の項に一致するか探すだけで，評価したり，等式以外の制約を与えたりはできない

e.g.

code:scheme

(unifier '(?a + ?a = 2) '(?x + ?y = ?y))

;; => (2 + 2 = 2)

余談：単一化のちゃんとした定義

代入はここではbindingsのこと

code:scheme

((?X . 1) (?Y . f))

単一化の結果得られたものを単一化子（unifier）と呼ぶ

unifierは一つとは限らない

e.g.

最汎単一化子（most general unifier; mgu）を求めるアルゴリズムが存在する

今回実装するのはこれ

最汎ってどういうこと？

e.g.

most generalを保証しているのは無理やりdecomposeとかせずに，decomposeが失敗したらすぐdeleteしているのが効いている？

mguを求めるアルゴリズム

内容は以下の規則に分けられる

1. decompose

関数記号が同じ項同士の等式を、その部分項同士の等式に分解する規則

$ \frac{E_1, f(s_1,\ldots,s_n) \approx f(t_1, \ldots, t_n), E_2}{E_1, s_1 \approx t_1, \ldots, s_n \approx t_n, E_2}

2. delete

解かれた変数を問題から除去する規則

$ \frac{E_1, x \approx t, E_2}{(E_1, E_2)\sigma} \quad\text{and} \quad \frac{E_1, t \approx x, E_2}{(E_1, E_2)\sigma}

e.g.

paipによるとこのような問題は稀で，計算量も増えるのでほとんどの実装ではやっていないらしい？

そのため不健全な答えを生成することがある

e.g.

code:scheme

;; occurs check あり

(unify '?x '(f ?x))

;; => ((?x f ?x))

;; occurs check なし

(unify '?x '(f ?x))

3. eliminate

同じ項同士の等式を削除する規則

$ \frac{E_1, x \approx x, E_2}{E_1, E_2}

以下のような流れでmguを求める

解くべき等式が無くなったら見つかったということ

$ \begin{aligned} x + (\mathsf{0} + y) \approx \mathsf{s}(z) + (\mathsf{0} + x) \quad &\Longrightarrow_{\mathsf{decompose}} && x \approx \mathsf{s}(z), \mathsf{0} + y \approx \mathsf{0} + x\\ &\Longrightarrow_{\mathsf{decompose}} && x \approx \mathsf{s}(z), \mathsf{0} \approx \mathsf{0}, y \approx x\\ &\Longrightarrow_{\mathsf{eliminate}, \{y \mapsto x\}} && x \approx \mathsf{s}(z), \mathsf{0} \approx \mathsf{0}\\ &\Longrightarrow_{\mathsf{delete}} && x \approx \mathsf{s}(z)\\ &\Longrightarrow_{\mathsf{eliminate}, \{x \mapsto \mathsf{s}(z)\}} && \square \end{aligned}

実装

common lispとの差分

基本的に関数や関数定義のマクロをそのまま翻訳したのであんまりないはず

nilの代わりに#fを使っているぐらい？

unifierの名前が衝突しているのでapply-unifierに変更した

参考文献

/icons/hr.icon

第2回 2025/01/08 担当: conao3

chapter6.3「A Rule-Based Translator Tool」まで。

自己紹介

conao3 職業Lisper, Clojurian

トヨクモのClojurian

全てのソフトウェアはLanguageServerで提供されるべき

リンガフランカとしてのS式

Lispが好きだけど、任意の言語において「Lisp性」を見出すことができれば妥協できる

Lisp性は未定義

第1級オブジェクトとしての関数

マクロ

などなど

本編

Chapter5, 6でパターンマッチが取り扱われているので、この章を読む。

パターンマッチが実装できる

結果としてELIZAが実装できる

ELIZAとは

こんな感じの応答をするプログラム。

code:quote

Men are all alike.

IN WHAT WAY

They're always bugging us about something or another.

CAN YOU BE MORE SPECIFIC

Well, my boyfriend made me come here.

YOUR BOYFRIEND MADE YOU COME HERE

He says I'm depressed much of the time.

I AM SORRY TO HEAR YOU ARE DEPRESSED

It's true. I am unhappy.

DO YOU THINK COMING HERE WILL HELP YOU NOT TO BE UNHAPPY

I need some help, that much seems certain.

WHAT WOULD IT MEAN TO YOU IF YOU GOT SOME HELP

Perhaps I could learn to get along with my mother.

TELL ME MORE ABOUT YOUR FAMILY

構成要素は以下の通り

1. 入力を読み取る

2. 入力にマッチするパターンを見つける

3. 入力を応答に変換する

4. 応答を表示する

当然ながら2と3が肝になっている。

パターンマッチとは

このような入出力例を考える。

code: quote

Pattern: (i need a X)

Response: (what would it mean to you if you got a X ?)

Input: (i need a vacation)

Transformation: (what would it mean to you if you got a vacation ?)

この場合、X = vacationとして、Responseに埋め込むと目標を達成できる。

インターフェース

パターン変数

マッチ結果

バインディングをalistで返却する。つまりこんな感じ。

code:commonlisp

;; マッチ失敗の場合

nil

;; ?X -> vacationのとき

'((?X . vacation))

;; ?X -> vacation, ?Y -> youのとき

'((?X . vacation) (?Y . you))

;; バインディングなしの場合 (マッチ失敗の nil と区別する必要があるためこの形式を採用する)

'((t . t))

変換

code:commonlisp

(sublis '((?X . vacation))

'(what would it mean to you if you got a ?X ?))

(WHAT WOULD IT MEAN TO YOU IF YOU GOT A VACATION ?)

追加の形式

下記の形式で使えるようにする。

code:commonlisp

(pat-match '((?* ?p) need (?* ?x))

'(Mr Hulot and I need a vacation))

((?P MR HULOT AND I) (?X A VACATION))

(pat-match '((?* ?x) is a (?* ?y)) '(what he is is a fool))

((?X WHAT HE IS) (?Y FOOL))

なお、

code:commonlisp

(pat-match '(?x (?or < = >) ?y) '(3 < 4)) => ((?Y . 4) (?X . 3))

(pat-match '(x = (?and (?is ?n numberp) (?is ?n oddp))) '(x = 3)) => ((?N . 3))

(pat-match '(?x /= (?not ?x)) '(3 /= 4)) => ((?X . 3))

マクロ

Lisperが導入したくなるのがマクロ。

もっと簡便に入力できるようにしたいとき、実装に手を入れるのではなく、簡便な入力から本来入力すべきものに変換して渡すことができないか考える -> マクロ

つまりこう

ここでは簡単に字句マクロ (とはいえシンボル単位だけど) が導入されている。

code:commonlisp

(pat-match-abbrev '?x* '(?* ?x)) => (?* ?X)

(pat-match-abbrev '?y* '(?* ?y)) => (?* ?Y)

(setf axyd (expand-pat-match-abbrev '(a ?x* ?y* d))) => (A (?* ?X) (?* ?Y) D)

(pat-match axyd '(a b c d)) => ((?Y B C) (?X))

ELIZAの実装

パターンマッチを得ることができたら、後はELIZAのパターンを定義するだけ。

code:quote

(defparameter *eliza-rules*

'((((?* ?x) hello (?* ?y))

(How do you do. Please state your problem.))

(((?* ?x) I want (?* ?y))

(What would it mean if you got ?y)

(Why do you want ?y) (Suppose you got ?y soon))

(((?* ?x) if (?* ?y))

(Do you really think its likely that ?y) (Do you wish that ?y)

(What do you think about ?y) (Really-- if ?y))

(((?* ?x) no (?* ?y))

(Why not?) (You are being a bit negative)

(Are you saying "NO" just to be negative?))

(((?* ?x) I was (?* ?y))

(Were you really?) (Perhaps I already knew you were ?y)

(Why do you tell me you were ?y now?))

(((?* ?x) I feel (?* ?y))

(Do you often feel ?y ?))

(((?* ?x) I felt (?* ?y))

(What other feelings do you have?))))

この定義により、以下の入出力例を得ることができる

code:quote

(eliza)

ELIZA> (hello there)

(HOW DO YOU DO. PLEASE STATE YOUR PROBLEM.)

ELIZA> (i want to test this program)

(WHAT WOULD IT MEAN IF YOU GOT TO TEST THIS PROGRAM)

ELIZA> (i could see if it works)

(DO YOU REALLY THINK ITS LIKELY THAT IT WORKS)

ELIZA> (no not really)

(ARE YOU SAYING "NO" JUST TO BE NEGATIVE?)

ELIZA> (no)

(ARE YOU SAYING "NO" JUST TO BE NEGATIVE?)

ELIZA> (forget it-- i was wondering how general the program is)

(WHY DO YOU TELL ME YOU WERE WONDERING HOW GENERAL THE PROGRAM IS NOW?)

ELIZA> (i felt like it)

(WHAT OTHER FEELINGS DO YOU HAVE?)

ELIZA> (i feel this is enough)

(DO YOU OFTEN FEEL THIS IS ENOUGH ?)

小噺

ELIZAはWeizenbaum 1966により発表された。

似たようなシステムとしてKenneth Colby (1975)のPARRYもある。

このプログラムは何人かの専門心理学者を欺くのに十分なほど、被害妄想的な人物の会話をシミュレートできた

実装

Clojureで実装した。

CommonLisp版との差分

Clojureはalistではなく、Mapを使う文化。

ここでいうMapはいわゆるmapとは違い、他言語では辞書とか連想配列とか言われる構造。

初回バインディングのときにこのプレースホルダを削除するような処理が必要。

readされたシンボルは大文字に変換されない。つまりこう。

code:clojure

(= 'clojure 'Clojure)

;;=> false

(= 'clojure 'clojure)

;;=> true

そのためパターンのルールと全く同じ大文字小文字で入力しないと上手くマッチングできない。

実装上のポイント

副作用がないのでTDDが強力なツールになる。

この順でやるとよい

おもしろい例

code:clojure

;; マッチしそうだけどマッチしない。

(sut/pat-match '(((?* ?x) (?* ?y)) ?x ?y) '((a b c d) (a b) (c d)))

;; => nil

(sut/pat-match '(((?* ?x) (?* ?y))) '((a b c d)))

;;=> {:x (), :y (a b c d)}

次回

unification!

https://scrapbox.io/files/677e554b2935237c73020a67.png

code:clojure

(sut/pat-match '(((?* ?x) ?x)) '((a a a a)))

;;=> nil

;; 自作pat-matchでも同じ問題を再現できる

あれ?

code:clojure

(sut/pat-match '((?* ?x) (?* ?x)) '(a a a a))

;;=> {:x (a a)}

/icons/hr.icon

第1回 2024/12/19 担当: tani

概要

キックオフ

11.0 Prolog について

11.1 PAIProlog で遊ぶ

PAIProlog のインストール・使い方

はじめに

すすめ方について

毎回ページをアナウンスするのが面倒なので、基本的にこのページを更新する

スクロールするのが面倒なので、ページ最下部 (初回) ページ最上部(最新回) になるようスタックしていく

自然消滅防止のため、進捗なしでも定例開催したい

ソースコードについて

PAIP Prolog に用いたコードは各自管理。実装言語は自由。

継承するのが無難。改造しまくって、自身のコードがオリジナルのコードよりも大きくなった場合は、

別ライセンスのコードに MITライセンスのコードが埋め込まれているという体もとりやすい。

参加者について

途中参加歓迎。輪読成果発表中の質問歓迎。vim-jp 外での宣伝はほどほどに。

自己紹介

LISP歴 10年くらい (2013 (2014?) ~)

Prolog 歴 5年くらい

S式Prolog 歴 2 年くらい

好き: SBCL, SWI Prolog

本編

The idea behind logic programming is that the programmer should state the relationships that describe a problem and its solution.

プログラマーは、2つについて書くだけでよいという姿勢

逆にプログラマーが頑張らなくてよいとされるもの

問題を解くアルゴリズム (手続き) の詳細

深さ優先探索

アルゴリズムはすべて 論理プログラミングのシステムに委託できるという思想

Prolog の 3つの世界観

1. 単一の大きなデータベースが支配する

不正確な言い方になるが基本的に局所変数という概念はない。

巨大なデータベースを読み書きするだけ

In Prolog we would represent a fact like "the population of San Francisco is 750,000" as a relation. In Lisp, we would be inclined to write a function, population, which takes a city as input and returns a number.

普通はサンフランシスコの人口は75万人という情報は関数のような形で表されるが Prolog は サンフランシスコの人口と 75万のあいだに関係がある

code: mermaid

graph LR

SanFransisco --function--> 750000

code:mermaid

graph LR

Sanfransisco <--relation--> 750000

よく双方向性と呼ばれたりしている概念。入力と出力に区別がない。

基本的に Immutable プログラミングである

例

データベース

アリスとボブは友達

ボブとクリスは友達

ボブはトムと友達

計算

アリスは X と友達であり、

X は Y と友達であり、

Y とはクリスのことである

X はだれ?

上記の例では、計算の途中で X は 不変である。

X を ??? だと仮定して計算 (探索) を進めているはずなので、とちゅうで X の値が破壊的に変更されてしまうと前提が崩れてしまう。

なので一度束縛された値は不変である。

次に登場するバックトラッキングのときに再束縛するのはアリ

3. Prolog は基本動作がバックトラッキングである。

失敗したら巻き戻して再実行する。

ループや探索アルゴリズムを書かなくても、自動バックトラッキングでループや探索が勝手に実現される。便利。

他方、よく無限ループしたりスタック溢れが発生する

複数ある場合は、一度に 1 つとみなされます。 「人口が 500,000 人を超え、州都である都市はどこですか?」など、クエリに複数のリレーションが含まれる場合、Prolog は人口リレーションを調べて、人口が 500,000 人を超える都市を検索します。見つかった都市ごとに資本関係をチェックして、その都市が首都であるかどうかを確認します。そうであれば、Prolog は都市を出力します。そうでない場合は、後戻りして、人口関係にある別の都市を見つけようとします。

code:mermaid

graph TD

new_york((New York))

los_angeles((Los Angeles))

chicago((Chicago))

phoenix((Phoenix))

austin((Austin))

dallas((Dallas))

boston((Boston))

sacramento((Sacramento))

denver((Denver))

ny_pop((8,467,513))

la_pop((4,000,000))

chi_pop((2,716,000))

phx_pop((1,680,992))

aus_pop((964,254))

dal_pop((1,343,573))

bos_pop((675,647))

sac_pop((524,943))

den_pop((715,522))

new_york <-->|population| ny_pop

los_angeles <-->|population| la_pop

chicago <-->|population| chi_pop

phoenix <-->|population| phx_pop

austin <-->|population| aus_pop

dallas <-->|population| dal_pop

boston <-->|population| bos_pop

sacramento <-->|population| sac_pop

denver <-->|population| den_pop

phoenix <-->|capital of| arizona

austin <-->|capital of| texas

boston <-->|capital of| massachusetts

sacramento <-->|capital of| california

denver <-->|capital of| colorado

11章の目的

Prolog をつかった問題の解き方

Lisp で Prolog が実装できることを示す

WAM: Prolog 専用のバイトコードインタプリタ

In Prolog the assertions are called clauses, and they can be divided into two types: facts, which state a relationship that holds between some objects, and rules, which are used to state contingent facts. Here are representations of two facts about the population of San Francisco and the capital of California. The relations are population and capital, and the objects that participate in these relations are SF, 750000, Sacramento, and CA:

大事な概念

事実の例

code:lisp

(population SF 750000)

(capital Sacramento)

code:lisp

(likes Kim Robin)

(likes Sandy Lee)

(likes Sandy Kim)

(likes Robin cats)

事実をデータベースに登録する方法

code:lisp

(<- (likes Kim Robin))

(<- (likes Sandy Lee))

(<- (likes Sandy Kim))

(<- (likes Robin cats))

注意 (再掲):

LISPは関数で、Prolog は関係である

LISPで上記の関係を定義する場合二つの関数を定義する必要がある

code:lisp

(defun likes (x)

(defun likers-of (x)

Xが好きな人を列挙する関数と X を好きな人を列挙する関数

Prolog は 好き という関係がモノ同士に成立するかどうかしか気にしなので1つで良くなっている。

句の種類:ルールを登録してみる。

code:lisp

(<- (likes Sandy ?x) (likes ?x cats))

注意: 右から読む

宣言的解釈 ↓ (情報を取得するだけ)

後方連鎖解釈 (手続き的解釈)

100点をとったら、寿司屋につれってくれる。

これは普通の推論とは逆方向の推論であり、これが論理プログラミングの根幹となるアイディア ・アルゴリズム

他の章との関係

通常の推論システム (注:古い人工知能) は、「?x がネコがすきなら サンディは ?x が好き」と結論するような思考の流れを持ちます。これを前方連鎖解釈といいます。

tani の解説:

推論をするには、簡単な事実から難しい事実を導く行為です。

手持ちの知識から新しい知識を作るのが推論であり、前方連鎖解釈といいます。

先に知りたい新しい知識を提示して、より簡単な知識に分解していって、分解していった先が手持ちの知識のみになれば成功。という立場をとります。

先頭 (head) は難しい事実

残り (body) は難しい事実を簡単な事実に分解する方法

これ以上分解できない (= 手持ちの知識) として宣言する場合は body が無い句 つまり 事実として登録されます。

注意: body にあるもの全てが成功しないと、head が成功したと見做されません。

code:lisp

(<- (likes Kim ?x) (likes ?x Lee) (likes ?x Kim))

実際につかってみよう

インストール方法

簡単な方法:

Allegro Common Lisp のおためし版をダンロードする

> (require :prolog)

> (in-package :prolog)

PAIP Prolog を使う方法

code:flake.nix

{

description = "A flake for paiprolog";

inputs = {

nixpkgs.url = "github:nixos/nixpkgs/nixpkgs-unstable";

flake-parts.url = "github:hercules-ci/flake-parts";

};

outputs = inputs@{ nixpkgs, flake-parts, ... }:

flake-parts.lib.mkFlake { inherit inputs; } {

systems = nixpkgs.lib.platforms.all;

perSystem = { config, pkgs, lib, system, ... }:

{

devShells.default = pkgs.mkShell {

packages = with pkgs; [

rlwrap

];

};

};

};

}

実行例

(asdf:load-system :paiprolog)

(in-package :paiprolog)

code:sh

rlwrap sbcl

This is SBCL 2.4.10, an implementation of ANSI Common Lisp.

SBCL is free software, provided as is, with absolutely no warranty.

It is mostly in the public domain; some portions are provided under

BSD-style licenses. See the CREDITS and COPYING files in the

distribution for more information.

* (require :asdf)

("ASDF" "asdf" "UIOP" "uiop")

* (asdf:load-system :paiprolog)

WARNING: redefining PAIPROLOG.AUXFNS:VARIABLE-P in DEFUN

WARNING: redefining PAIPROLOG.AUXFNS:PAT-MATCH in DEFUN

WARNING: redefining PAIPROLOG::ARGS in DEFUN

WARNING: redefining PAIPROLOG:<- in DEFMACRO

WARNING: redefining PAIPROLOG::ADD-CLAUSE in DEFUN

WARNING: redefining PAIPROLOG::TOP-LEVEL-PROVE in DEFUN

T

* (in-package :paiprolog)

* (<-- (id ?x ?x))

ID

* (?- (id 1 ?x))

?X = 1;

No.

*

練習問題:

code:lisp

(<-- (append () ?x ?x))

(<- (append (?x . ?xs) ?ys (?x . ?zs))

(append ?xs ?ys ?zs))

(?- (append (1 2 3) (4 5 6) ?xs))

?xs = (1 2 3 4 5 6)

(?- (append ?x (4 5 6) (1 2 3 4 5 6)))

?x = (1 2 3)

(?- (append (1 2 3) ?y (1 2 3 4 5 6)))

?y = (4 5 6)

(?- (append ?x ?y (1 2 3 4 5 6)))

?x = (1 2 3)

?y = (4 5 6)

(?- (append (1 2 ?x) (?y 5 6) (?z 2 3 4 5 6)))

code:prolog

append([], X, X).

append(XS, YS, ZS).

trace(append/3).