このエントリは型 Advent Calendar 2019 - Qiita 3日目に遡って投稿しているエントリです。 担当に遅刻した訳ではなくて空いてたので前から詰めて投稿しただけです。
h_sakuraiです。世の中に型推論アルゴリズムは色々知られていると思いますが、Prologを使えば単一化とバックトラックがあるので型推論を素直に書けるよというネタ記事です。
swiprolog のインストール
$ apt install swi-prolog
$ brew install swi-prolog
等で、インストールできます。
ハローワールド
hello.pl
:- write(hello),write(' '),write(world),nl.
:- writeln(飛べない + 豚 = ただの豚).
:- H='hello world',format('~w\n',[H]).
:- halt.
SWI-PrologはLispのシンボル的なAtomを文字列代わりによく使います。短くて済むので便利です。
writelnを使うと改行が使えます。
:- から始まる行はプログラム読み込み中に実行されます。
実行方法:
$ swipl hello.pl
hello world
飛べない+豚=ただの豚
hello world
OK 表示できました。
述語内の式はただの式だ。飛べない + 豚 = ただの豚 はただの式だ。
型推論
t.pl
t(I,int):- integer(I). % T-Int
t(E1+E2,int):- t(E1,int),t(E2,int). % T-Add
t(E1-E2,int):- t(E1,int),t(E2,int). % T-Sub
t(E1*E2,int):- t(E1,int),t(E2,int). % T-Mul
t(E1/E2,int):- t(E1,int),t(E2,int). % T-Div
:- t(1+2*3+4/5,int).
:- t(1+2*3+4/5,T),writeln(T).
:- t(hoge,int).
:- halt.
実行方法
$ swipl t.pl
int
Warning: /tmp/t.pl:8:
Goal (directive) failed: user:t(hoge,int)
推論結果intが表示されました。
t(hoge,int) は失敗するので警告が表示されます。
% 以降はコメントです。
ユニットテストとか
現代的 Prolog にはユニットテストがついておりますので使ってみましょう:
t2.pl
t(I,int):- integer(I).
t(E1+E2,int):- t(E1,int),t(E2,int).
t(E1-E2,int):- t(E1,int),t(E2,int).
t(E1*E2,int):- t(E1,int),t(E2,int).
t(E1/E2,int):- t(E1,int),t(E2,int).
:- begin_tests(t2).
test(int):- t(1,int).
test(e):- not(t(hoge,int)).
test(e):- t(1+2*3+4/5,int).
:- end_tests(t2).
:- run_tests.
:- halt.
実行方法:
$ swipl t2.pl
% PL-Unit: t2 ... done
% All 3 tests passed
テストしたので実行感があります。
Norminalな部分型システム
みんな嫌いな?磯野家の家系図の話は部分型システムの理解に有用だった話
sub.pl
sub(_<namihe). % Namihe
sub(T<T). % Jibun
sub(T1<T3):- sub(T1<T2),sub(T2<T3). % Trans
sub(T1<T2):- class(T1<T2). % Class
class(sazae<namihe).
class(tarao<sazae).
:- sub(tarao<namihe>).
:- halt.
これ実行すると死ぬので、ctrl+c からの e します。
$ swipl sub.pl
^C^C^C^C
WARNING: By typing Control-C twice, you have forced an asynchronous
WARNING: interrupt. Your only SAFE operations are: c(ontinue), p(id),
WARNING: s(stack) and e(xit). Notably a(abort) often works, but
WARNING: leaves the system in an UNSTABLE state
Action (h for help) ? exit
$
Prolog は完全性を捨て、チューリング完全となったのだ。
左再帰がいけないのだ。消すが良い。
sub2.pl
sub(_<namihe). % Namihe
sub(T<T). % Jibun
sub(T1<T3):- class(T1<T2),sub(T2<T3). % Class-Trans
class(sazae<namihe).
class(tarao<sazae).
:- sub(tarao<namihe).
:- halt.
$ swipl sub2.pl
そうか、カツオ。何の音沙汰もないということは元気な証拠だ。
わかったぞ！ナカジマ。推移則があったら、左再帰の箇所を具体的な定義に変えればいいんだね。
まとめ
Prolog 使うと推論規則を簡単に実装できて楽だよ。