アドベントカレンダーの一覧を見ていたところPrologのアドベントカレンダーがないので作ってみました。
この記事はProlog Advent Calendar 2016の１日目の記事です。
言語処理系の論文等で使われている形式的な言語は論理型言語です。言語を習得するには処理系があると便利で、論理型言語であるPrologの処理系は無料で手に入ります。Prologがネイティブと言えるほど使い込めば、形式的な言語を理解し読み書きする素養が身につきます。
もちろん、Prologの魅力は言語処理系だけではありません。様々な応用例を書いてもらえるとウレシイところです。
インストール
brew install swi-prolog
apt-get install swi-prolog
windowsもありますが、bash上で使うかVMがよいと思います。
SWI-PrologはUTF-8も使えるのでおすすめです。
Hello World
:- write('hello world'),nl,halt.
Prologのプログラムは述語を使って行います。
Prologは:-から.までを即実行します。writeは標準出力に出力する述語で、nlは改行を出力する述語です。haltはプログラムを終了する述語です。
拡張子はproとかswiとかがいいのかもしれないのですけど、plを使ってます。
足し算をする述語
Prologには関数がないのですが、関数の代わりに述語というものがあります。
足し算をする述語を定義して使うには以下のようにします。
add(X,Y,R) :- R is X + Y.
:- add(1,2,R),writeln(R),halt.
eval(X+Y,R):-R is X+Y.
:- eval(1+2,R),writeln(R),halt.
HOAS的なラムダ計算
ラムダ計算はHOAS的に書くと以下のようにかけます。
:-op(1000,yfx,$).
eval(I,I) :- integer(I).
eval(E1+E2,R) :- eval(E1,R1),eval(E2,R2), R is R1 + R2.
eval(X->E,X->E).
eval(E1$E2,R) :- eval(E1,X->E),eval(E2,Y),copy_term(X->E,Y->E3),eval(E3,R).
:- eval((Y->X->X+Y)$(1+1)$(3),R),writeln(R).
:- eval((F->X->Y->(F$X)+(F$Y))$(Z->Z+1)$3$4,R),writeln(R).
:- halt.
HOAS的というのは、変数名にPrologの変数を直接用いているからです。
単相の型推論
:- op(1000,yfx,$).
type_of(_,I,int) :- integer(I).
type_of(C,X,T) :- var(X), member(Y:T,C),X==Y.
type_of(C,E1+E2,int) :- type_of(C,E1,int),type_of(C,E2,int).
type_of(C,X->E,T->T2) :- type_of([X:T|C],E,T2).
type_of(C,E1 $ E2, T) :- type_of(C,E1,T2->T),type_of(C,E2,T2).
:- type_of([], 1+1,T),writeln(T).
:- type_of([], (X->(X+1)),T),writeln(T).
:- type_of([], Y->(X->(X+Y)),T),writeln(T).
:- type_of([], (X->(X+1))$(1+1),T),writeln(T).
:- halt.
と書けます。Prologは動的型付けの言語と言えると思いますが、なにもない世界に静的型を作る場合には型がない言語で書くほうがわかりやすい場合もあるように思います。
多相の型推論
多相の型推論も以下のように簡単に書けます。
:- set_prolog_flag(occurs_check,true).
:- op(500,xfy,$).
type(_, I, int) :- integer(I).
type(Γ, E1+E2, int) :- type(Γ, E1, int), type(Γ, E2, int).
type(Γ, X, T1) :- atom(X), member(X:T, Γ), instantiate(T, T1).
type(Γ, X -> E, T1 -> T2) :- type([X:mono(T1)|Γ], E, T2).
type(Γ, X $ Y, B) :- type(Γ,X,A -> B), type(Γ,Y,A).
type(Γ, let(X = E0, E1), T) :- type(Γ, E0, A), type([X:poly(Γ,A) | Γ], E1, T).
instantiate(poly(Γ,T),T1) :- copy_term((Γ,T),(Γ,T1)).
instantiate(mono(T),T).
run(Γ,E) :- type(Γ,E,T), writeln(E : T).
:-run([],x->x).
:-run([],x->x+1).
:-run([],x->y->(y$x)).
:-run([],let(id=(x->x),id$id)).
:-run([],let(id=(x->x),(id$(x->x+1))$(id $ 10))).
:- halt.
copy_termは項をコピーし、その時変数は別の変数を割り当てる述語です。
具体化する際にコンテキストと型を合わせた中で変数は別なものに書き換えることで具体化が可能になります。
シーケント計算に似せた記述
ラムダ計算を図に表すと以下のように表すことができます。
構文
\begin{array}{lclr}
e & ::= & & 項: \\
& | & i & 整数\\
& | & e + e & 加算 \\
& | & e \;\text{->}\; e & ラムダ抽象 \\
& | & e \;$\; e & 関数適用 \\
\end{array}
評価規則
\begin{array}{crcr}
i \Downarrow i
& \text{(E-Int)}
\\
\dfrac{e_1 \Downarrow i_1\;\;\;e_1 \Downarrow i_2\;\;\;i\;is\;i_1+i_2 }{
e_1+e_2 \Downarrow i
} & \text{(E-Add)}
\\
e_1\;\text{->}\;e_2 \Downarrow e_1\;\text{->}\;e_2
& \text{(E-Abs)}
\\
\dfrac{e_1 \Downarrow x\;\text{->}\;e\;\;\;
e_1 \Downarrow v_2\;\;\;
[x\;\text{->}\;e_1]e \Downarrow v}{
e_1\;$\;e_2 \Downarrow v
} & \text{(E-App)}
\\
\end{array}
Prologのマクロ的な機能であるterm_expansionを使えば、
論文によく用いられるシーケント計算の推論規則に似せて記述することもできます。
term_expansion(A--B,B:-A).と書くことで前後の順番を反転することが可能なのです。
:-op(1200,xfx,--).
:-op(801,xfx,⇓).
:-op(799,xfy,->).
:-op(500,yfx,$).
term_expansion(A--B,B:-A).
integer(I)
-- % (E-Int)
I ⇓ I.
E1 ⇓ R1, E2 ⇓ R2, R is R1 + R2
-- %-------------- (E-Add)
E1+E2 ⇓ R.
!
-- %----------------------------- (E-Abs)
X->E ⇓ X->E.
E1 ⇓ X->E, E2 ⇓ Y,
copy_term(X->E,Y->E3), E3 ⇓ R
--%------------------------------ (E-App)
E1 $ E2 ⇓ R.
:- (Y->X->X+Y)$(1+1)$(3) ⇓ R,writeln(R).
:- (F->X->Y->(F$X)+(F$Y))$(Z->Z+1)$3$4 ⇓ R,writeln(R).
:- halt.
Prologの%は一行コメントですので、%----- (E-App)のように線を書くとシーケント計算に似せることができます。
演算子もただの複合項にすぎませんので、eval(A,B)はA⇓Bと書くこともできます。
フィボナッチ
fib(0,0).
fib(1,1).
fib(X,R):-X1 is X-1, X2 is X-2, fib(X1, R1), fib(X2, R2), R is R1 + R2.
:- fib(10,R), writeln(R),halt.
残念ながら、関数が使えないのでFibのようなものは長く書く必要が有ります。
しかしながら、Prologの素晴らしいところは関数を使えない代わりに、クォートすることなく式を表すことができます。クォートすることなく式を表せるようにするか、ネストした関数を使えるようにするかのどちらかを選択するかというところで、Prolog(正確にはエジンバラ形式のProlog)は主にクォートすることなく式を書けることを選んだのです。
この性質故に、Prologはプログラミング言語のプロトタイプを作成するのに向いている言語なのです。
参考文献
TIPER Type Inference Prototyping Engines from Relational Specifications of type systems http://kyagrd.github.io/tiper/