prologでラムダ計算
まずは自然数を定義
%num(X):-Xは自然数。0,1,2,... = 0,s(0),s(s(0)),... num(0). num(s(X)):-num(X).
実行してみると正しいことがわかる。
?- num(0). true. ?- num(s(0)). true. ?- num(s(s(0))). true.
足し算の定義
%num(X):-Xは自然数。0,1,2,... = 0,s(0),s(s(0)),... num(0). num(s(X)):-num(X). %nPlus(X,Y,Z):-X+Y->Z nPlus(s(X),Y,s(Z)):-nPlus(X,Y,Z). nPlus(0,X,X):-num(X).
s^n(0)のまま表現するんだ！すげえはじめてprologで感動した。
?- nPlus(0,0,X). X = 0. ?- nPlus(0,s(0),X). X = s(0). ?- nPlus(s(s(0)),s(0),X). X = s(s(s(0))). ?- nPlus(s(s(0)),s(s(0)),X). X = s(s(s(s(0)))).
s(X),{X=0} って 関数の状態で答えになってるのがな不思議
schemeなら (s 0) ってことだけど、ここじゃ止められないはず。
おそらくsって関数がないといって止まるはず。
s^n(0)をコード化する
数字に変換しようとおもって、述語writeを作った
%num(X):-Xは自然数。0,1,2,... = 0,s(0),s(s(0)),... num(0). num(s(X)):-num(X). %nWrite(X):-Xの値を数字としてコード化する。 nWrite(X):-nWrite(X,0). nWrite(s(X),Y):-plus(Y,1,Z),nWrite(X,Z). nWrite(0,X):-writeln(X).
実行してみた
?- nWrite(0). 0 true. ?- nWrite(s(s(0))). 2 true.
sにホントはインクリメントの意味を持たせて展開しようとしたが無理だった。
かけ算
%num(X):-Xは自然数。0,1,2,... = 0,s(0),s(s(0)),... num(0). num(s(X)):-num(X). %nPlus(X,Y,Z):-X+Y->Z nPlus(s(X),Y,s(Z)):-nPlus(X,Y,Z). nPlus(0,X,X):-num(X). %nTimes(X,Y,Z):-X*Y->Z nTimes(s(X),Y,Z):-nTimes(X,Y,W),nPlus(W,Y,Z). nTimes(0,X,0).
?- nTimes(s(s(0)),s(s(s(0))),X). X = s(s(s(s(s(s(0)))))).
うおっ、わけわからん。traceする。
?- trace. Unknown message: query(yes) [trace] ?- nTimes(s(s(0)),s(s(s(0))),X). Call: (7) nTimes(s(s(0)), s(s(s(0))), _G347) ? creep Call: (8) nTimes(s(0), s(s(s(0))), _L199) ? creep Call: (9) nTimes(0, s(s(s(0))), _L219) ? creep Exit: (9) nTimes(0, s(s(s(0))), 0) ? creep Call: (9) nPlus(0, s(s(s(0))), _L199) ? creep Call: (10) num(s(s(s(0)))) ? creep Call: (11) num(s(s(0))) ? creep Call: (12) num(s(0)) ? creep Call: (13) num(0) ? creep Exit: (13) num(0) ? creep Exit: (12) num(s(0)) ? creep Exit: (11) num(s(s(0))) ? creep Exit: (10) num(s(s(s(0)))) ? creep Exit: (9) nPlus(0, s(s(s(0))), s(s(s(0)))) ? creep Exit: (8) nTimes(s(0), s(s(s(0))), s(s(s(0)))) ? creep Call: (8) nPlus(s(s(s(0))), s(s(s(0))), _G347) ? creep Call: (9) nPlus(s(s(0)), s(s(s(0))), _G425) ? creep Call: (10) nPlus(s(0), s(s(s(0))), _G427) ? creep Call: (11) nPlus(0, s(s(s(0))), _G429) ? creep Call: (12) num(s(s(s(0)))) ? creep Call: (13) num(s(s(0))) ? creep Call: (14) num(s(0)) ? creep Call: (15) num(0) ? creep Exit: (15) num(0) ? creep Exit: (14) num(s(0)) ? creep Exit: (13) num(s(s(0))) ? creep Exit: (12) num(s(s(s(0)))) ? creep Exit: (11) nPlus(0, s(s(s(0))), s(s(s(0)))) ? creep Exit: (10) nPlus(s(0), s(s(s(0))), s(s(s(s(0))))) ? creep Exit: (9) nPlus(s(s(0)), s(s(s(0))), s(s(s(s(s(0)))))) ? creep Exit: (8) nPlus(s(s(s(0))), s(s(s(0))), s(s(s(s(s(s(0))))))) ? creep Exit: (7) nTimes(s(s(0)), s(s(s(0))), s(s(s(s(s(s(0))))))) ? creep X = s(s(s(s(s(s(0)))))).
あ、わかった。body部の 述語それぞれは前から確定することに依存してプログラム組むのかー
今回で言えば nTimesが確定してから ,nPlusやるってこと。
andが含まれるとき 後ろの述語が前のものに依存してる。
遅延評価と無縁になるな。
あー、でもあれか。 変数のまま計算するアプローチがあるのかな？
でも、後段のほうが無限に発散しそうな気がしないでもない。
