誰でも動かせるPrologで操作的意味論を書こうぜ

はじめに

言語を作る場合には BNF があり操作的意味や型付け規則を定義してあると説得力が増します。シークエント計算の推論規則は長方形に収めることが出来るので、２次元的に図として書くにはとても便利な記述方法です。しかし、読み書きするには、よく知られている処理系がないのでなかなか覚えることが出来ない人も多いのではないでしょうか？

\begin{array}{lr}
  評価 &
  \bbox[3px,border:1px solid black]{\;t \longrightarrow t}
  \\[-30px]
  \hspace{250px}
  \\[-30px]
\end{array}
\\
\begin{array}{cr}
  \dfrac{
    t_1 \longrightarrow t_1' }{
    t_1\;t_2 \longrightarrow t_1'\;t_2 }
  & \text{(E-App1)}
  \\
  \dfrac{
    t_2 \longrightarrow t_2' }{
    v_1\;t_2 \longrightarrow v_1'\;t_2}
  & \text{(E-App2)}
  \\
  (\lambda x.t_{12})\;v_2 \longrightarrow
  [x \rightarrow t_1]\;t_{12}
  & \text{(E-AppAbs)}
\end{array}

そこで、ここでは、Prolog を用いてシークエント計算に似せた記述をする手法を提案します。論理型言語の処理系でよく知られている言語といえば Prolog です。残念ながらPrologは書く順番が異なるためシークエント計算ではありませんが工夫をすることで似せることが可能です。

まず軽くPrologのインストールやHelloworldとフィボナッチの計算を紹介します。次に、関数型言語で扱うような構文木を評価する大ステップ評価器を作成し、シークエント計算に似た表記に書き換えます。また、ifを使った方法を紹介し、小ステップ評価器と評価文脈を紹介します。その後、単相型推論、多相型推論等を紹介します。最後に、部分型付けにおけるPrologの限界とアルゴリズミックな部分型付けによる解決方法を述べます。
これらの紹介した手法でPrologを使って様々な言語の処理系を作れば、形式的な言語を読み書きする素養が身につくことでしょう。

インストール

Prologの処理系は様々ありますが、SWI-PrologはUTF-8も使えるのでおすすめです。

brew install swi-prolog
apt-get install swi-prolog

Windows版のSWI-Prologも存在ますが、BOMの追加が必要となるためVM上で用いることをおすすめします。

Hello World

hello.pl

:- write('hello world'),nl.
:- halt.

Prologでは述語を,で区切って複数記述することによりプログラムを記述します。
:-から.までをすぐに実行することができます。writeは標準出力に出力する述語で、nlは改行を出力する述語です。haltはプログラムを終了する述語です。
拡張子はPerlとかぶりますがplを使います。

$ swipl hello.pl
hello world

実行するには、swipl hello.pl とコマンドを実行します。
プログラムにバグがあった場合などでreplが表示されることがあります。
そういった場合も、あわてず、?- halt.と入力してください。

足し算をする述語

Prologには関数がないのですが、代わりに述語を使います。
述語で値を返すには変数に値を束縛することで返却します。
足し算をする述語を定義して使うには以下のようにします。

add.pl

add(X,Y,R) :- R is X + Y.
:- add(1,2,R),writeln(R),halt.

C言語のvoidな関数でポインタを用いて値を返すイメージに似ています。

フィボナッチ

fib.pl

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.

残念ながら、関数をネストして記述できないのでフィボナッチのような計算は記述量が増えます。
これをみてダメだなと思ってPrologをやめる人は多いでしょう。

Prologで書く大ステップ評価器

ここからが、Prologの本領発揮です。
ラムダ計算はPrologではわずか数行で記述可能です。

HOAS的に書くと以下のようにかけます。

lambda.pl

:-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の変数を直接用いているからです。
この方法では、(X->X)$(X->X)といった式を書いた場合にラムダ抽象の変数が共有されてしまう問題があるので注意が必要です。

置換操作をより詳細に行うには例えば以下のように記述します。

lambda.pl

:-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,E2_),subst(X,Y,E,E3),eval(E3,R).

subst(X,X,E,E).
subst(X,Y,I,I) :- integer(I).
subst(X,Y,E1+E2, E1_+E2_) :- 
  subst(X,Y,E1,E1_),subst(X,Y,E2,E2_).
subst(X,Y,X->E1,X->E1).
subst(X,Y,Y->E1,Y_->E2):- term_to_atom(_,Y_),subst(Y,Y_,E1,E1_),subst(X,Y,E1_,E2).
subst(X,Y,X1->E1,X2->E1_) :- subst(X,Y,E1,E1_).
:- eval((y->x->x+Yx$(1+1)$(3),R),writeln(R).
:- eval((f->x->y->(f$x)+(f$y))$(z->z+1)$3$4,R),writeln(R).
:- halt.

本質的な箇所のみを端的に表すことも可能ですし、より詳細に記述することもPrologを用いて可能なのです。

シークエント計算に似せた大ステップ評価器

ラムダ計算をシークエント計算の図で表すと以下のように表すことができます。

構文

\begin{array}{llr}
e ::= & & 項: \\
      & i & 整数\\
      & e + e & 加算 \\
      & e \;\text{->}\; e & ラムダ抽象 \\
      & e \;$\; e & 関数適用 \\
\end{array}

評価規則

\begin{array}{cr}
i \Downarrow i & \text{(E-Int)}\\
\dfrac{e_1 \Downarrow i_1 \quad e_1 \Downarrow i_2 \quad 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\quad e_1 \Downarrow v_2\quad [x\;\text{->}\;e_1]e \Downarrow v}
{e_1\;$\;e_2 \Downarrow v} & \text{(E-App)} \\
\end{array}

この記述にPrologのプログラムを似せてみましょう。
述語term_expansion/2は読み込み時に述語定義を書き換え可能な述語です。
term_expansion(A--B,B:-A).と書くと読み込み時に前後の順番を反転できるので、論文によく用いられるシーケント計算の推論規則に似せることができます。

sequent.pl

:-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)のように線を好きな長さにできます。
日本語と英語は語順が違うので英語の習得が難しいように、同じプログラムでも前後が変わるだけで印象ががらりと変わります。カンマ区切りはPrologの文法上どうしようもありませんが、語順を合わせることで推論規則により親しみを持つことができるでしょう。

ifを用いた記述

Scalaの基礎となるDOTの論文などで用いられているような、以下のように記述する手法もあります。

\begin{array}{rcl}
i & \Downarrow& i\\
e_1 + e_2 & \Downarrow & r \quad if\;e_1 \Downarrow r_1,e_2 \Downarrow r_2, r\;is\;r_1 + r_2 \\
x \rightarrow e & \Downarrow & x \rightarrow e\\
e_1\;e_2 & \Downarrow & r \quad  if\;e_1 \Downarrow x \rightarrow e,e_2 \Downarrow y, [x := y]e \Downarrow r\\
\end{array}

このような記述は、ifをPrologの:-と読み替えましょう。

lambda_if.pl

:-op(1200,xfx,if).
:-op(801,xfx,⇓).
:-op(799,xfy,->).
:-op(500,yfx,$).
term_expansion(A if B, A :- B).

    I ⇓ I     if integer(I).
E1+E2 ⇓ R     if E1 ⇓ R1, E2 ⇓ R2, R is R1 + R2.
 X->E ⇓ X->E.
E1$E2 ⇓ R     if E1 ⇓ (X->E), E2 ⇓ Y, copy_term((X->E),(Y->E3)), E3 ⇓  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.

小ステップ評価器

i \longrightarrow i\;\text{(E-Int)}\\

\dfrac{t_1 \longrightarrow t_1'}
{t_1 + t_2 \longrightarrow t_1' + t_2}\text{(E-Add1)} \;
\dfrac{t_2 \longrightarrow t_2'}
{v_1 + t_2 \longrightarrow v_1 + t_2'}\text{(E-Add2)} \;
\dfrac{v_3\;is\; v_1 + v_2}
{v_1 + v_2 \longrightarrow v_3} \text{(E-Add3)} \\

\dfrac{t_1 \longrightarrow t_1'}
{t_1 - t_2 \longrightarrow t_1' - t_2} \text{(E-Sub1)} \;
\dfrac{t_2 \longrightarrow t_2'}
{v_1 - t_2 \longrightarrow v_1 - t_2'} \text{(E-Sub2)} \;
\dfrac{v_3\;is\; v_1 - v_2}
{v_1 - v_2 \longrightarrow v_3}\text{(E-Sub3)} \\

\dfrac{t_1 \longrightarrow t_1'}
{t_1 * t_2 \longrightarrow t_1' * t_2} \text{(E-Mul1)} \;
\dfrac{t_2 \longrightarrow t_2'}
{v_1 * t_2 \longrightarrow v_1 * t_2'} \text{(E-Mul2)} \;
\dfrac{v_3\;is\; v_1 * v_2}
{v_1 * v_2 \longrightarrow v_3} \text{(E-Mul3)} \\

\dfrac{t_1 \longrightarrow t_1'}
{t_1 / t_2 \longrightarrow t_1' / t_2} \text{(E-Div1)} \;
\dfrac{t_2 \longrightarrow t_2'}
{v_1 / t_2 \longrightarrow v_1 / t_2'} \text{(E-Div2)} \;
\dfrac{v_3\;is\; v_1 / v_2}
{v_1 / v_2 \longrightarrow v_3} \text{(E-Div3)} \\

lambda_smallstep.pl

:- op(920, xfx, [ --->,-->> ]).
:- op(1200, xfx, [ -- ]).
term_expansion(A -- B, B :- A).

\+integer(A), A ---> A_
--%------------------------------------ (E-Add1)
A + B ---> A_ + B.

integer(V), \+integer(B), B ---> B_
--%------------------------------------ (E-Add2)
V + B ---> V + B_.

integer(V1), integer(V2), V is V1 + V2
--%------------------------------------ (E-Add3)
V1 + V2 ---> V.

\+integer(A), A ---> A_
--%------------------------------------ (E-Sub1)
A - B ---> A_ - B.

integer(V), \+integer(B), B ---> B_
--%------------------------------------ (E-Sub2)
V - B ---> V - B_.

integer(V1), integer(V2), V is V1 - V2
--%------------------------------------ (E-Sub3)
V1 - V2 ---> V.

\+integer(A), A ---> A_
--%------------------------------------ (E-Mul1)
A * B ---> A_ * B.

integer(V), \+integer(B), B ---> B_
--%------------------------------------ (E-Mul2)
V * B ---> V * B_.

integer(V1), integer(V2), V is V1 * V2
--%------------------------------------ (E-Mul3)
V1 * V2 ---> V.

\+integer(A), A ---> A_
--%------------------------------------ (E-Div1)
A / B ---> A_ / B.

integer(V), \+integer(B), B ---> B_
--%------------------------------------ (E-Div2)
V / B ---> V / B_.

integer(V1), integer(V2), V is V1 div V2
--%------------------------------------ (E-Div3)
V1 / V2 ---> V.

A ---> A :- integer(A).               % (E-Int)

A -->> A_ :- \+v(A), A ---> B, !, B -->> A_.
A -->> A.

:- 10 ---> R, writeln(R).
:- 10 + 20 ---> R1, writeln(R1).
:- 10 - 20 ---> R2, writeln(R2).
:- 10 * 20 ---> R3, writeln(R3).
:- 1*2+3/4 -->> R4, writeln(R4).
:- halt.

小ステップ評価器は、１度に１つの変換のみを行います。大ステップ評価器では途中経過を見ることが出来ませんが、少ステップ評価器は途中の状態を見ることができる特徴があります。

評価文脈

シークエント計算はかなり圧縮して記述できるのですが、同じような変換規則は助長です。評価文脈を用いると、より推論規則を短く記述できます。

\begin{array}{l}
構文\\
t ::= i \;|\; t + t \;|\; t - t \;|\; t * t \;|\; t / t \\
v ::= i \\
評価文脈\\
e ::= e + t\;|\;v + e \;|\; e - t \;|\; v - e \;|\; e * t \;|\; v * e \;|\; e / t \;|\; v / e \;|\; []\\
評価規則\\
\end{array}\\
\dfrac{v_3\;is\; v_1 + v_2}
{v_1 + v_2 \longrightarrow v_3} \text{(E-Add3)} \;

\dfrac{v_3\;is\; v_1 - v_2}
{v_1 - v_2 \longrightarrow v_3}\text{(E-Sub3)} \\

\dfrac{v_3\;is\; v_1 * v_2}
{v_1 * v_2 \longrightarrow v_3} \text{(E-Mul3)} \;

\dfrac{v_3\;is\; v_1 / v_2}
{v_1 / v_2 \longrightarrow v_3} \text{(E-Div3)} \\

i \longrightarrow i\;\text{(E-Int)}\;

\dfrac{t_2 \longrightarrow t_2'}
{[t_2]e_1 \longrightarrow [t_2']e_1} \text{(E-EvalContext)} \\

または

\begin{array}{l}
構文\\
t ::= i \;|\; t + t \;|\; t - t \;|\; t * t \;|\; t / t \\
v ::= i \\

評価規則\\
v_1 + v_2 \longrightarrow v_3 \;if\; v_3\;is\; v_1 + v_2\\
v_1 - v_2 \longrightarrow v_3 \;if\; v_3\;is\; v_1 - v_2\\
v_1 * v_2 \longrightarrow v_3 \;if\; v_3\;is\; v_1 * v_2\\
v_1 / v_2 \longrightarrow v_3 \;if\; v_3\;is\; v_1 / v_2\\
i \longrightarrow i \\
[t_2]e_1 \longrightarrow [t_2']e_1 \;if\; t_2 \longrightarrow t_2'\\
\quad where\;e ::= e + t\;|\;v + e \;|\; e - t \;|\; v - e \;|\; e * t \;|\; v * e \;|\; e / t \;|\; v / e \;|\; []\\

\end{array}\\

評価文脈は[]をhole(穴)と呼び、次に評価すべき箇所を穴として表します。
t=e[t']と表すことが出来て、評価文脈eの穴に項t'を埋めると項tになります。
項から評価文脈を探す述語e/4は、項、評価文脈、穴にマッチした項、穴を表す変数の４つの変数を受け取り、評価文脈に穴を埋めた項を取得するには、穴となる変数と項を単一化することで行います。
評価文脈を使った変換規則はPrologで書くと以下のようになります。

lambda_evaluation_context.pl

:- op(920, xfx, [ ---> , -->> ]).
:- op(1200, xfx, [ -- ]).
term_expansion(A -- B, B :- A).

v(A) :- integer(A).
e(S+T, E+T, P, H) :- \+v(S), e(S,E,P,H).
e(V+T, V+E, P, H) :- v(V), \+v(T), e(T,E,P,H).
e(S-T, E-T, P, H) :- \+v(S), e(S,E,P,H).
e(V-T, V-E, P, H) :- v(V), \+v(T), e(T,E,P,H).
e(S*T, E*T, P, H) :- \+v(S), e(S,E,P,H).
e(V*T, V*E, P, H) :- v(V), \+v(T), e(T,E,P,H).
e(S/T, E/T, P, H) :- \+v(S), e(S,E,P,H).
e(V/T, V/E, P, H) :- v(V), \+v(T), e(T,E,P,H).
e(T, H, T, H).

e(T1, T1_, T2, T2_), T1\=T2, T2 ---> T2_
--%------------------------------------ (E-EvalContext)
T1 ---> T1_.

integer(V1), integer(V2), V is V1 + V2
--%------------------------------------ (E-Plus3)
V1 + V2 ---> V.

integer(V1), integer(V2), V is V1 - V2
--%------------------------------------ (E-Minus3)
V1 - V2 ---> V.

integer(V1), integer(V2), V is V1 * V2
--%------------------------------------ (E-Times3)
V1 * V2 ---> V.

integer(V1), integer(V2), V is V1 div V2
--%------------------------------------ (E-Div3)
V1 / V2 ---> V.

A ---> A :- integer(A).               % (E-Int)

A -->> A_ :- \+v(A), A ---> B, !, B -->> A_.
A -->> A.

:- 10 ---> R, writeln(R).
:- 10 + 20 ---> R1, writeln(R1).
:- 10 - 20 ---> R2, writeln(R2).
:- 10 * 20 ---> R3, writeln(R3).
:- 1*2+3/4 -->> R4, writeln(R4).
:- halt.

Prologでも評価文脈を用いたほうが短く記述できました。
処理は遅くなりますが[]を穴として記述すれば、理解しやすいかもしれません:

e(S+T, E+T, P) :- \+v(S), e(S, E, P).
e(V+T, V+E, P) :- v(V), \+v(T), e(T, E, P).
e(S-T, E-T, P) :- \+v(S), e(S, E, P).
e(V-T, V-E, P) :- v(V), \+v(T), e(T, E, P).
e(S*T, E*T, P) :- \+v(S), e(S, E, P).
e(V*T, V*E, P) :- v(V), \+v(T), e(T, E, P).
e(S/T, E/T, P) :- \+v(S), e(S, E, P).
e(V/T, V/E, P) :- v(V), \+v(T), e(T, E, P).
e(T, [], T).

e(S, E, T), S\=T, T ---> T_, subst([], T_, E, S_)
--%------------------------------------ (E-EvalContext)
S ---> S_.

e/3は項、評価文脈、評価文脈の穴にマッチした項を変数として受け取る述語です。穴は[]と表すため、穴を表す変数は返却しません。
穴を項で埋めるにはsubstを使って置き換えます。[]を他に用いることになった場合に対処できなくなる問題はあるでしょう。

単相型推論

typeof.pl

:- 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.

具体化する際にコンテキストと型を合わせた中で変数は別なものに書き換えることで具体化が可能になります。type_ofではなくtypeと書いてあったり、表記の乱れがありますが、様々な論文でも同様の表記の違いがあるのでどう書いても動くということを理解すると、幅が広がるのではないかと思います。

部分型付けとアルゴリズミックな部分型付け

部分型付けの規則は構文主導の規則ではなく、深さ優先探索を評価戦略として用いるPrologで実行すると無限ループに陥ります。Prologで動作させるにはアルゴリズミックな規則に書き換える必要があります。カインドを求める場合は更に事情が悪くなり、簡単な規則だけでは対処できなくなるようです。構文主導ではない推論規則を用いて証明を行うことは可能なので、アルゴリズミックではない規則にも意味はあるのです。

rcdsub.pl

:- op(910, xfx, [ ⊢ ]).
:- op(901, xfx, [∈]).
%:- op(900, xfx, [ : ]).
:- op(501, xfx, <:).
:- op(500, yfx, $).
:- op(11, yfx, .>).
:- op(1200, xfx, [ -- ]).
term_expansion(A -- B, B :- A).

maptpl(F,(A,B)) :- call(F,A), maptpl(F,B).
maptpl(F,A) :- call(F,A).
maprcd(F,{T}) :- maptpl(F,T).
maptpl(F,(A,B),(A_,B_)) :- call(F,A,A_), maptpl(F,B,B_).
maptpl(F,A,A_) :- call(F,A,A_).
maprcd(F,{T},{T_}) :- maptpl(F,T,T_).
membertpl(X,(X,_)).
membertpl(X,(_,B)) :- membertpl(X,B).
membertpl(X,X).
memberrcd(X,{T}) :- membertpl(X,T).

isVal(_ -> _).
isVal(V) :- isRcdVal(V).
isRcdVal(T) :- maprcd(isRcdVal1, T).
isRcdVal1(L=T) :- atom(L), isVal(T).

T <: T.
_ <: top.
bot <: _.
(S1->S2) <: (T1->T2) :- S1 <: T1, S2 <: T2.
S <: T :- maprcd(subtypercd1(S), T).
subtypercd1(S, (Li:Ti)) :- memberrcd(Li:Si,S), Si <: Ti.

X ∈ (_,X).
X ∈ (Γ,_) :- X ∈ Γ.

X : T ∈ Γ
--%-------------------------------------- (TA-Var)
Γ ⊢ (X : T).

(Γ, X : T1) ⊢ E2 : T2
--%-------------------------------------- (TA-Abs)
Γ ⊢ ((X : T1) -> E2) : (T1 -> T2).

Γ ⊢ E1 : bot, Γ ⊢ E2 : _
--%-------------------------------------- (TA-AppBot)
Γ ⊢ E1 $ E2 : bot.

Γ ⊢ E1 : (T11 -> T12),
Γ ⊢ E2 : T2, T2 <: T11
--%-------------------------------------- (TA-App)
Γ ⊢ E1 $ E2 : T12.

Γ ⊢ E1 : R1, memberrcd(Li:Ti,R1)
--%-------------------------------------- (TA-Proj)
Γ ⊢ E1.>Li : Ti.

maprcd(taRcd1(Γ),E1,T1)
--%-------------------------------------- (TA-Rcd)
Γ ⊢ E1 : T1.

taRcd1(Γ,Li=Ei,Li:Ti) :- Γ ⊢ Ei : Ti.
typeof(E1:T1) :- [] ⊢ E1 : T1.
% test sub
:- {a:bot,b:top,c:top} <: {b:top,a:bot}.
:- {a:bot,b:top} <: {b:top,a:bot}.
:- \+ ({a:bot} <: {b:top,a:bot}).
:- \+ ({a:bot,b:top} <: {b:top,a:bot,c:top}).

% test mapRcd
:- V=((x:top)-> x), maprcd(writeln,{a=V,b=V,c=V}).

% test isValRcd
:- \+ isRcdVal({}).
:- \+ isRcdVal(1).
:- V=((x:top)-> x),isRcdVal({a=V,b=V}).
:- V=((x:top)-> x),isRcdVal({a=V,b=V,c=V}).

% test typeof
:- typeof(((x:top)-> x):T),writeln(T),!,T=(top->top).
:- typeof(((x:top)-> x)$((x:top)-> x):T2),writeln(T2).
:- typeof(((x:(top->top))-> x) $ ((x:top)-> x):T3),writeln(T3).
:- typeof((((r:{x:(top->top)})-> r.>x $ r.>x)):T4a),writeln(T4a).
:- typeof({x=((z:top)->z)}:TT),writeln(TT).
:- typeof((((r:{x:(top->top)})-> (r.>x $ r.>x)) $ {x=((z:top)->z), y=((z:top)->z)}):T4),writeln(T4).
:- typeof(((x:bot)-> x):T5),writeln(T5),!,T5=(bot->bot).
:- typeof(((x:bot)-> (x $ x)):T6),writeln(T6),!,T6=(bot->bot).

:- halt.

まとめ

様々な例で、推論規則をPrologに書き換えてみました。
すべてのシークエント計算の推論規則をPrologにすぐに書き換えることは出来るわけではありません。しかしながら、多くの場合に素直にPrologに書き換えることが可能です。Prologに書き換え出来ないような場合は構文主導の規則ではないのでアルゴリズミックな規則に書き換える必要があります。
Prologで素直に書くことができる推論規則であれば、論理型言語より低級な言語に書き換え高速化することも容易となるでしょう。Prologは論理型言語の段階で実装上の問題を解決することが出来ます。是非皆さんも挑戦してみてください。

参考文献

TIPER Type Inference Prototyping Engines from Relational Specifications of type systems http://kyagrd.github.io/tiper/

CoPL

TAPL

The Essence of Dependent Object Types

COMFRK vol.1 Prolog で Scheme の操作的意味論を実装 zick
http://comfrk.info/arch/vol1.pdf