とりあえず、Prologの初心者にも優しくインストールから教えていきますのでどなたでも安心してお読みいただけます。ただし、aptやbrewなどが使えるUnixな環境でお楽しみください。
気がつけば、QiitaのPrologの投稿数が現在ちょうど400件になった今日この頃、みなさんいかがお過ごしでしょうか？
私は、円が安くて物価が高いので家の庭で野菜の栽培を始めてみたところ、トマトがガンガン成長するので
というわけで、表示的意味論のゆる言語ラジオを見てて、理解ができてそうでできてないなぁ。俺もPrologでやった覚えはあるが忘れた。と思いまして、再考してみた次第です。
1. 超速 Prolog 入門
1.1. インストール
早速、SWI-Prologをインストールしていきましょう。
$ brew install swi-prolog
あるいは
$ apt install swi-prolog
などでインストールできます。アンインストールは
$ brew uninstall swi-prolog
$ apt uninstall swi-prolog
$ brew remove swi-prolog
$ apt remove swi-prolog
みたいな感じで大体消せるはず。
vi hello.pl
お好きなエディタでhello.plを作り以下のように書きます。
% hello.pl Prologの行コメントです。この行はなくても動きます。
:- writeln('hello world').
:- halt.
swi-prologにおいては、:- から始まる項は、読み込み時に実行されます。
これは標準的なPrologの仕様ではありませんが、便利なのでこう書きました。
writeln/1 は改行付きの文字列出力述語です。Prologは小文字で始まるか''で括られた識別子をatomといってインターンされた識別子です。LispやRubyのシンボルのような役割を果たします。文字列もありますが同じ文字列でも =/2 で比較してアドレスが違うと等価ではない
halt/0 はプロセスを停止する述語です。swiplは対話的な環境なのでhaltしないと入力プロンプトが出てきてしまいます。そんな時は、'halt/0' を使って止めます。
実行するには以下のように、swipl が SWI-Prolog のコマンドで引数に Prolog のファイルを指定します。
$ swipl hello.pl
hello world
$
初めての方はめんどくさいからいいや、と思うかも知れませんが簡単なのでやってみてください。
Prolog? やったことあるよ。インストールしただけだけど、、、。と言えるようになります。
インストールしないと、記事は読んだと言えますけどね。
1.2. 続きはWebで
Prologは色々と訳わかんない機能とかあると思いますが、興味があればWebで色々記事をあたってみてください。
2. Prolog で操作的意味論
CoPL や TAPL などの入門書を読みますとまず出てくるのが操作的意味論の評価規則です。
ここでは簡単な四則演算のインタプリタをPrologで実装します。
(数学的な)BNFで以下のような四則演算ができる言語を作ります:
構文
e ::= 式
i 整数
| e+e 加算
| e-e 減算
| e*e 乗算
| e/e 割算
操作的意味論では評価規則を一階述語論理の述語として書きます。一階述語論理といっても全称記号や存在記号がない簡単な記法を用います。書いてある順番通りに辿る構文主導であるとかアルゴリズミックであると言われる規則の評価戦略は深さ優先探索でありPrologで実行することができます。
% eval.pl
% 評価規則 eval/2 eval(入力,出力)
eval(I,I):- integer(I).
eval(E1+E2,I):- eval(E1,I1),eval(E2,I2), I is I1+I2.
eval(E1-E2,I):- eval(E1,I1),eval(E2,I2), I is I1-I2.
eval(E1/E2,I):- eval(E1,I1),eval(E2,I2), I is I1*I2.
eval(E1*E2,I):- eval(E1,I1),eval(E2,I2), I is I1 div I2.
% この評価規則は以下のように実行できます。
:- eval(1*2+3*4,14). % これは正しいことの証明が行われて問題がなければ何も出力されません。
:- eval(1*2+3*4,I),writeln(I). % 結果を出力します。
:- halt.
このプログラムはswiplコマンドを用いて実行できます。
$ swipl eval.pl
14
ここではCoPLで詳しく説明されている大ステップ評価器を実装してみました。
Prologなら言語を作ってTwitterで呟けるほど簡潔に言語が実装できます。
短く実装できるということはプログラミング言語の性質を俯瞰してみることができるということです。
高速さを追い求めれば、もっと長い記述をしたほうが速くなりますが、俯瞰してみて実際に動かしてみれる点がProlog上のインタプリタ実装の素晴らしいところです。
この利点は最新の関数型言語の研究論文などでも活かされています。
見た目は理論のものと違うじゃないかと批判する方もおられると思いますが、論理プログラミングと同じ考え方で理論が形成されている点を考慮してみてください。定義さえしっかりしていれば多少の見た目の違いはどうでもいいことなのです。
操作的意味論の理論はここからさらに、数学的な性質を検証していくことになります。例えばこの言語は必ず有限時間内に計算が終わる性質である停止性についての証明などをする訳ですが、そのようなことはPrologで簡単にはできませんので定理証明支援系のシステムを用いると良いでしょう。
3. Prolog で型理論
操作的意味論と同様にPrologを使うと型理論でよく用いられる型付け規則を述語で実装し実際に動かして実験してみることができます。
% t.pl
% 型付け規則
:- t(I,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).
:- t(E1/E2,int):- t(E1,int),t(E2,int).
% 型検査
:- t(1*2+3*4,int).
% 型推論(型再構築)
:- t(1*2+3*4,T),writeln(T).
:- halt.
実行するには:
$ swipl t.pl
int
4. Prolog で表示的意味論
さて操作的意味論はインタプリタの実装、型理論は型付け規則の述語であり、場合によっては型推論(型再構築)が行える述語で定義でき実行できました。では、表示的意味論はPrologで実装するとどういったプログラムになるのでしょうか？答えは簡単です。コンパイラを作ることになります。
ここでは構文 a ::= int(i) | add(a,a) | sub(a,a) | mul(a,a) | div(a,a) なる言語の表示的意味を示すPrologの述語を作ります。
しかしここでは、その前に、表示的意味論の処理系である言語を作ります。
単なる変換プログラムを書いても表示的意味は示せますが、[[]]を使ったテクニックが表示的意味論では一般的に用いられます。これは操作的意味論でいうところの評価文脈のようなものでありまして、特殊な処理をしなければなりません。特殊な処理とは一体何かと申しますと、表示的意味論のインタプリタを実装してその上で検証することになります。表示的意味論のインタプリタを作るということは表示的意味論の操作的意味を示すことになります。
4.1. 例となる表示的意味の変換関数
[[int(i)]] = i
[[add(a1,a2)]] = [[a1]]+[[a2]]
[[sub(a1,a2)]] = [[a1]]-[[a2]]
[[mul(a1,a2)]] = [[a1]]*[[a2]]
[[div(a1,a2)]] = [[a1]]/[[a2]]
4.2. 表示的意味論の意味を書いた変換述語
trans(int(I),I).
trans(add(A1,A2),E1+E2):- trans(A1,E1),trans(A2,E2).
trans(sub(A1,A2),E1-E2):- trans(A1,E1),trans(A2,E2).
trans(mul(A1,A2),E1*E2):- trans(A1,E1),trans(A2,E2).
trans(div(A1,A2),E1/E2):- trans(A1,E1),trans(A2,E2).
4.1. 表示的意味論の操作的意味論（表示的意味論のインタプリタのProlog実装）
e(G,A,E):-member(V,G),copy_term(V,A=A1),!,e(G,A1,E),!.
e(_,A,A):-atom(A),!.
e(G,A,E):-A=..[O|As],maplist(e(G),As,Es),E=..[O|Es].
表示的意味論の関数定義はGの中に含みます。問題は関数を実行した際に単一化されてしまうと何度も使えない事なので、copy_termを用いた事です。copy_term/2は自明とは言い難い述語なのでもう少し考える必要があるかも。
4.2. 表示的意味論の実装と実行
e(A,E):-e([
[[int(I)]]=I,
[[add(E1,E2)]]=[[E1]]+[[E2]],
[[sub(E1,E2)]]=[[E1]]-[[E2]],
[[mul(E1,E2)]]=[[E1]]*[[E2]],
[[div(E1,E2)]]=[[E1]]/[[E2]]
],A,E).
e/2 関数環境に変換関数の定義を含めてe/3を呼び出すようにしておきます。
:- e([[add(mul(int(1),int(2)),mul(int(3),int(4)))]],E),writeln(E),E=1*2+3*4.
:- halt.
変換前のプログラムをに渡すと、変換結果が得られます。
5. まとめ
Prologを用いてさまざまな意味論を実装し最後に表示的意味論の実装を作ってみました。
操作的意味論はインタプリタを実装する事で意味を表します。
表示的意味論はコンパイラを実装する事で意味を表すとも考えられます。
表示的意味論のコンパイラを関数型言語で実装すると普通は計算結果を出してしまいますし、論理型言語の術後も形が違います。
表示的意味論の記法は特殊ですから、Prologでそのまま実装はできないし、関数型言語でも難しい。
そこでPrologで表示的意味論のインタプリタを実装しその上で表示的意味論の例を実装し実行してみました。
表示的意味論の大ステップ評価器は表示的意味論の操作的意味を示すものと言えます。
ですから、表示的意味論の操作的意味を示したのち、四則演算をする言語の表示的意味論を示しました。
このようにPrologを用いると表示的意味論も実装しながら学べるため実装は簡単です。
しかしどの意味論についてもPrologでできることは実装して実験するところまでです。数学的な諸性質を詳しく調べる話になるとPrologだけでは役不足です。そうなると定理証明支援系のソフトウェアを用いると照明を実装して確かめることができるため便利でより確実に検証できるでしょう。