ガード付き表示的意味論によるスタックマシンへのコンパイル

1. はじめに

今年は、表示的意味論がゆる言語ラジオで取り上げられていたので、表示的意味論の操作的意味を考え直してそれなりの処理系を作ってみたりしておりました。要するに表示的意味論とはコンパイラを作ることで意味を示す事と言って良いと思った訳です。ということは例えば数式からスタックマシンへのコンパイラも表示的意味論で作れるはずと思って作ろうとしてみました。しかしながら、以前作った表示的意味論にはガードがないため、タグレスな整数を判定することができないので困りました。そこで以前作った表示的意味論の操作的意味を拡張して条件を付与できるようにガードを記述できる表示的意味論の操作的意味を考えてみました。

2. そもそも表示的意味論って何？

例えば、加算と乗算がある言語Tを言語Eに変換する規則を示して表示的意味を示すことを考えます。

T ::= int(I) | add(T,T) | mul(T,T)
E ::= I | T+T | T*T

ここで、Iは整数を示します。Tは変換元の言語でありint(I)は数式内の整数、add(T,T)は数式内の加算、mul(T,T)は数式内の掛け算を示す抽象構文木を表します。
Eは変換後の数式を表しint(I)は数式内の整数でありE+Eが加算を示し、E*Eが掛け算を示します。

表示的意味論の規則を以下に示します:

  {int(I)} = {I}
  {add(T1,T2)} = {T1} + {T2}
  {mul(T1,T2)} = {T1} * {T2}

1. int(I)はIに変換します。
2. add(T1,T2)は(T1を変換したもの)+(T2を変換したもの)に変換します。
3. mul(T1,T2)は(T1を変換したもの)*(T2を変換したもの)に変換します。

この３つの規則によって表示的な意味を示すことができます。

3. ガード付き表示的意味論

それでは逆変換を考えてみましょう。

  {I}        = int(I) 
  {T1 + T2}  = add({T1},{T2})
  {T1 * T2}  = mul({T1},{T2})

1. Iはint(I)に変換します。
2. T1+T2はadd(T1を変換したもの,T2を変換したもの)に変換します。
3. T1*T2はmul(T1を変換したもの,T2を変換したもの)に変換します。

この３つの式で変換できると嬉しいのですが、Iが整数であることを単なる一階述語論理で考えると何でもマッチしてしまう問題が生じます。Iの型が判定できるのであればいいのですが判定できない処理系では処理ができません。

そこで以下のように記述できるように拡張したガード付きの表示的意味論を使うことにします:

  {I}       | integer(I) = int(I)
  {T1 + T2}              = add({T1},{T2})
  {T1 * T2}              = mul({T1},{T2})

|の後ろに条件を記述することでIの型が整数ならばint(I)に変換されるように書くことができるようにします。

4. 実装

4.1. 表示的意味論の操作的意味論

prologで実装すると以下のように書けます:

ds(_,A,A):-atom(A),!.
ds(G,A,E):-member(V,G),copy_term(V,A=A1),!,ds(G,A1,E),!.
ds(G,A,E):-A=..[O|As],maplist(ds(G),As,Es),E=..[O|Es].

ds(A,E):-ds([
  {int(I)} = I,
  {add(E1,E2)} = {E1}+{E2},
  {mul(E1,E2)} = {E1}*{E2}
],A,E).

:- ds({add(mul(int(1),int(2)),mul(int(3),int(4)))},E),writeln(E),E=1*2+3*4.
:- halt.

4.2. ガード付き表示的意味論の操作的意味論

prologで実装すると以下のように書けます:

cp(V,A=A1):- copy_term(V,A|P=A1),call(P),!.
cp(V,A=A1):- copy_term(V,A=A1).
ds(_,A,A):-atom(A),!.
ds(G,A,E):-member(V,G),cp(V,A=A1),!,ds(G,A1,E),!.
ds(G,A,E):-A=..[O|As],maplist(ds(G),As,Es),E=..[O|Es].
ds(A,E):-findall(DS,ds(DS),DSS),ds(DSS,A,E).

ds({I}    | integer(I) = int(I)).
ds({E1+E2}             = add({E1},{E2})).
ds({E1*E2}             = mul({E1},{E2})).

:- ds({1*2+3*4},T),
   writeln(T),
   T=add(mul(int(1),int(2)),mul(int(3),int(4))).
:- halt.

cp/2 述語を追加してcopy_termにガード機能をつけ:

cp(V,A=A1):- copy_term(V,A|P=A1),call(P),!.
cp(V,A=A1):- copy_term(V,A=A1).

copy_term/2をcp/2に置き換えました:

ds(G,A,E):-member(V,G),cp(V,A=A1),!,ds(G,A1,E),!.

変換規則は述語定義してfindallで取得するようにしてみました。

4.3. スタックマシンのコンパイラを表示的意味論で書く

comp({I}     = [I] where integer(I)).
comp({E1+E2} = [{E1},{E2},+]).
comp({E1*E2} = [{E1},{E2},*]).

こんな規則を考えました。実装は以下のようになります:

cp(V,A=A1):- copy_term(V,A|P=A1),call(P),!.
cp(V,A=A1):- copy_term(V,A=A1).
ds(_,A,A):-atom(A),!.
ds(G,A,E):-member(V,G),cp(V,A=A1),!,ds(G,A1,E),!.
ds(G,A,E):-A=..[O|As],maplist(ds(G),As,Es),E=..[O|Es].
ds(A,E):-findall(DS,ds(DS),DSS),ds(DSS,A,E).

comp({I}    | integer(I) = [I]).
comp({E1+E2}             = [{E1},{E2},+]).
comp({E1*E2}             = [{E1},{E2},*]).
comp(A,E):-findall(DS,comp(DS),DSS),ds(DSS,A,E).

:- comp({1*2+3*4},E),writeln(E),E=[[[1],[2],*],[[3],[4],*],+].
:- halt.

結果のリストがネストしてしまっているのが気になるところです。

4.4. スタックマシンのコンパイラを表示的意味論で書く(2)

ds/3で変数ならばそのまま返却するようにしました。
また、where演算子を追加しdsw/2述語でwhereがあれば述語を呼び出すようにしました:

:- op(600,xfx,where).
cp(V,A=A1):- copy_term(V,A|P=A1),call(P),!.
cp(V,A=A1):- copy_term(V,A=A1).
dsw(E where P,E):- call(P),!.
dsw(E,E).
ds(_,A,A):-var(A),!.
ds(_,A,A):-atom(A),!.
ds(G,A,E):-member(V,G),cp(V,A=A1),!,ds(G,A1,E1),dsw(E1,E),!.
ds(G,A,E):-A=..[O|As],maplist(ds(G),As,Es),E=..[O|Es].

comp({I}    | integer(I) = [I]).
comp({E1+E2}             = E where append([{E1},{E2},[+]],E)).
comp({E1*E2}             = E where append([{E1},{E2},[*]],E)).
comp(A,E):-findall(DS,comp(DS),DSS),ds(DSS,A,E).

:- comp({1*2+3*4},E),writeln(E),E=[1,2,*,3,4,*,+].
:- halt.

結果のネストが消えました。

4.5 表示的意味論でインタプリタ

ガードとwhereを使うとインタプリタが作れそうなので作ってみました:

:- op(600,xfx,where).
cp(V,A=A1):- copy_term(V,A|P=A1),call(P),!.
cp(V,A=A1):- copy_term(V,A=A1).
dsw(E where P,E):- call(P),!.
dsw(E,E).
ds(_,A,A):-var(A),!.
ds(_,A,A):-atom(A),!.
ds(G,A,E):-member(V,G),cp(V,A=A1),!,ds(G,A1,E1),dsw(E1,E),!.
ds(G,A,E):-A=..[O|As],maplist(ds(G),As,Es),E=..[O|Es].

comp({I}    | integer(I) = I).
comp({E1+E2}             = I where (I is {E1}+{E2})).
comp({E1*E2}             = I where (I is {E1}*{E2})).
comp(A,E):-findall(DS,comp(DS),DSS),ds(DSS,A,E).

:- comp({1*2+3*4},I),writeln(I),I=14.
:- halt.

表示的意味論でインタプリタが作れてしまいました。

6. まとめ

簡単な表示的意味の説明を行い、表示的意味の操作的意味論を考え、Prologで実装してみました。型情報がない環境では条件をつけられると便利なのでガード機能を表示的意味の操作的意味に加えました。ガード付きの表示的意味論によるスタックマシンのコンパイラを書いてみました。ネストが気になるので結果に対する述語呼び出しも可能にすることで、結果のネストをなくすことができました。さらにwhereを使って述語を動かすことで表示的意味論でインタプリタを作ることができました。
表示的意味論ではコンパイラしか作ることができないと思っていましたが、機能を拡張することでインタプリタも構成できるようになります。<ほんとか？

専門家ではないので詳しいことはよく分かりませんが、これは表示的意味論と言っていいのでしょうか？
詳しい方がいらしましたらコメント欄などで教えてください。