Prolog入門の感想

prolog-intro-report.md

Introduction to Prolog (in Japanese) を一通り読んだ感想:

• 便利だなぁ "変数を含んだ質問では，複数の答えが存在する場合がある． たとえば， saburo の子供は naoyuki と shinji の 2 人がいるから ?- father(saburo, C). の答えは 2 種類存在するはずである． Prolog ではこのような場合，プログラム中での記述の順序にしたがって 答えが表示される．"
• えーと。これは定義の順に辿って最初に見つかった1つの例が選択されるってことなんです？ "質問 ?- father(G, F), father(F, hyogo). の場合も左から順に処理される． まず father(G, F) の最初の答え G=naoyuki, F=hyogo が求められる．"
• これでも、、、バックトラックを手作業で制御するとなると、、、記述量が増えませんか？
• あーspyは便利ですね。
• でも、、、それってシンボリック実行の方がより強力だと感じます
• うーん、これCollatzを実装したとしても任意の自然数で停止する証左にならないのでは。。。
• これ結局実行しているから、バックトラックで枝切りした範囲でしか健全性が主張できないのでは
• 数式微分の例なんですが、、、これ本当に数学の微分の公理系と一致していますか？高校数学を忘却してしまったために知覚できません。。。
• 命題論理は、、、まぁどこにでもあるのでは。。。
• ボトムに落ちてはダメなのでは。。。 "実行して見ると， v1 から v4 などについてはちゃんと yes と表示されますが v1 から v5 は答が出ません． これは， v1 → v2 → v3 → v4 → v1 → … となり， プログラムが無限ループしているためです． 無限ループを止めるには C-c (コントロールC) を入力してから a を入れます．"
• ただ、バックトラックを許すならばもっと大規模な問題を検査できるという点については同意できると思います。容易にボトムに落ちる可能性がいつも残されますが。
• Prologの世界では基本的に #停止性 については議論できないということなのでしょうか。。。
• あー、なんかパーサは書きやすいそうな雰囲気が。。。
• #割り算の定義 ゼロ除算はどうするんですか？
• "nat(N), prime(N)." はすごい自然な表記ですね。 #Prologは国語だ というのが少しわかった気がします。
• ただ、、、その中身はガード条件を実際に実行して素数を低い値から順番に求めているだけなのでは。。。
• 今の雰囲気だとPrologは既存の命令型言語と同等の力と停止性の不足があるが、より簡潔に記述できる。ただしバックトラックという例外は起きる可能性は何時でもあって、当該バックトラックは手動で制御する必要がある。なんかSmalltalkのカオリが。。。

ATS3へのフィードバックは:

• Prologの変数に相当するものがあると便利
• spyに相当するものがあると便利
• シンボリック実行が欲しい
• "nat(N), prime(N)." のような簡潔な記述をしたい

追加:

• Notationの記法拡張機能

こんな文面でメールする:

I slightly learn Prolog for the design of ATS3.
My opinion is following:

Variable is useful

$ cat family.pl
father(naoyuki, hyogo).
father(saburo, naoyuki).
father(saburo, shinji).
father(yoshihisa, hisako).
mother(hisako, hyogo).
mother(yoko, naoyuki).
mother(yoko, shinji).
mother(nobuko, hisako).
$ swipl
?- [family].
true.

?- father(F, hyogo), father(G, F).
F = naoyuki,
G = saburo.

Already does ATS2 have such variable to prove something?

spy is useful

$ cat fact.pl
fact(0, 1).
fact(N, F) :-
    N > 0,
    N1 is N-1,
    fact(N1, F1),
    F is N*F1.
$ swipl
?- [fact].
true.

?- spy(fact).
% Spy point on fact/2
true.

[debug]  ?- fact(10,F).
 * Call: (8) fact(10, _828) ? creep
   Call: (9) 10>0 ? creep
   Exit: (9) 10>0 ? creep
   Call: (9) _1052 is 10+ -1 ? creep
   Exit: (9) 9 is 10+ -1 ? creep
 * Call: (9) fact(9, _1054) ? creep
   Call: (10) 9>0 ? creep
   Exit: (10) 9>0 ? creep
   Call: (10) _1058 is 9+ -1 ? creep
   Exit: (10) 8 is 9+ -1 ? creep
 * Call: (10) fact(8, _1060) ? creep
   Call: (11) 8>0 ? creep
   Exit: (11) 8>0 ? creep
   Call: (11) _1064 is 8+ -1 ? creep
   Exit: (11) 7 is 8+ -1 ? EOF: exit

There will be some debugger for proof things of ATS3?

Compressed description of specification

$ cat nat.pl
nat(0).
nat(s(X)) :- nat(X).

plus(0, Y, Y).
plus(s(X), Y, s(Z)) :- plus(X, Y, Z).

le(X, Y) :- plus(X, _, Y).

lt(X, Y) :- le(s(X), Y).

quot(X, Y, 0, X) :- lt(X, Y).
quot(X, Y, s(Q), R) :- plus(Y, X1, X), quot(X1, Y, Q, R).

dnd(M, N) :- quot(N, M, _, s(_)).

df(s(0), _).
df(s(s(M)), N) :- dnd(s(s(M)), N), df(s(M), N).

prime(s(X)) :- df(X, s(X)).
$ swipl
?- [nat].
true.

?- nat(N), prime(N).
N = s(s(0))

nat(N), prime(N). is very smart description of specification.

Regards,