Prologによる、単純型付きラムダ式の型検査と型推論について
本ページの内容は、加筆訂正する予定です。
以下も参照してください。単純型付きラムダ式に全称型を追加したSystem FのPrologによる型検査について説明しています、
http://qiita.com/suharahiromichi/items/9adc16a40ecb1bc36825
2014/05/02 @suharahiromichi
単純型付きラムダ式の型検査のプログラムをPrologで実装してみた。そのうえで、同じプログラムが「Prologの双方向性」によって、型推論もできることを示す。
この文章のソースコードは以下にあります。
https://github.com/suharahiromichi/prolog/blob/master/tapl/tapl_stlc_qiita.swi
使い方の例：
% swipl.
?- ['tapl_stlc_qiita.swi'].
?- go24.
Prolog処理系はSWI-Prolog (5.10.4)で動作を確認している。GNU Prologでは未確認である。
省略時解釈（ディフォルト）のとおり Occurs Check のオプションは off のままとする。ただし、途中の1箇所において、unify_with_occurs_check述語で、Occurs Check 付きの一致判定「=」をおこなう。このことは後述する。
ここで使う記法について
型検査にはde Bruijn Index (注1) を使用するが、わかりやすさから、一般的なラムダ式をde Bruijn Indexに変換して使う。
また、どちらの場合も、Prologで扱える前置記法 f(x,g(y,z)) の形式を使用する。
de Bruijn Index に変換するコードは後半に示す。
記法の一覧
λx.y tm_abs(x, y) 型注釈のないλ抽象
λx:T.y tm_abs(x:T, y) 型注釈のあるλ抽象 (「:」は中置記法)
f x tm_app(f, x) 適用
x tm_var(x) 変数の参照
t1->t2 t1->t2 関数型 (中置記法)
Bool ty_bool 型定数
True tm_true 定数
False tm_false 定数
変換の例
一般的な記法
λa:Bool. λ:b:Bool->Bool. b (b a)
ここで使う記法
tm_abs(a:ty_Bool,
tm_abs(b:ty_Bool->ty_Bool,
tm_app(tm_var(b),
tm_app(tm_var(b), tm_var(a)))))
ここで使う記法(de Bruijn Index)
tm_abs(ty_Bool,
tm_abs(ty_Bool->ty_Bool,
tm_app(tm_var(0),
tm_app(tm_var(0), tm_var(1)))))
型の注釈で使う「:」と、そのなかでの関数型を示す「->」は、「,」より優先度が高いものとする。
:- op(600, xfx, :). % 例、x : T
:- op(500, xfy, ->). % 例、Tx->Ty
型検査のプログラム
typeof
typeof/2述語の引数の意味を以下に示す。式はde Bruijn Indexで与える。引数の前の「+」は入力、「-」は出力、「?」はそのどちらにもなることを示す。
つまり、第2引数の「型」は、入力でも出力でもよく、入力なら型検査、出力なら型推論の意味になる。「Prologの双方向性」が利用できる例である。
typeof(+式, ?型)
typeof(E, T) :-
typeof([], E, T).
第2引数の「型」は、入力でも出力でもよい。たとえば正しい型を指定して実行すると、結果は「成功」になる（型検査）。間違った型を指定したら結果は「失敗」になる。第1引数に与えられた式がもともと型付けできなければ、このときも、結果は「失敗」になる。
?- typeof(tm_true, ty_Bool).
また、変数を指定して実行すると、その変数に正しい型が設定される（型推論）。
?- typeof(tm_true, T).
T = ty_Bool.
第1引数に与えられた式が型付けできなければ、結果は「失敗」になる。
typeof/3述語の引数の意味を以下に示す。
typeof(+文脈, +式, ?型)
型検査をおこなうtypeof/3は、TAPL(参考文献1.)の10.3節 型検査 をそのまま移しただけである。ただし、tm_absに型注釈（型修飾）のない場合も許している。このとき、ラムダ変数の型を新しい（未束縛の）Prologの変数で表し文脈に追加している。 この変数はtypeofの実行にともなって、束縛される（型が決まる）ことが期待される。もし、型が決まらないなら、未束縛のProlog変数のまま出力される。
この方法によれば、全称型の型変数をPrologの変数で表すことで、System Fの型検査や型推論に拡張することができる。
また、もとのプログラムにあるエラー時の処理はおこなわず、結果として実行が「失敗」するようにしている。
typeof(CTX, tm_var(I), T) :-
getTypeFromContext(CTX, I, T).
typeof(CTX, tm_abs(TyT1, Tm2), TyT1 -> TyT2) :- % 型注釈のある場合
typeof([TyT1|CTX], Tm2, TyT2).
typeof(CTX, tm_abs(Tm2), TyT1 -> TyT2) :- % 型注釈のない場合
typeof([TyT1|CTX], Tm2, TyT2).
typeof(CTX, tm_app(Tm1, Tm2), Ty12) :-
typeof(CTX, Tm1, Ty11 -> Ty12),
typeof(CTX, Tm2, Ty11).
typeof(CTX, tm_true, ty_Bool).
typeof(CTX, tm_false, ty_Bool).
typeof(CTX, tm_if(T1, T2, T3), TyT2) :-
typeof(CTX, T1, ty_Bool),
typeof(CTX, T2, TyT12),
typeof(CTX, T3, TyT12).
getTypeFromContext
getTypeFromContextは、変数の型を文脈(context)から取り出すことをおこなう。
de Bruijn Indexの場合は、Indexの値によって一意に決まるため、（なにも考えずに）nth0述語を使用することができる。
nth0(I, CTX, TB)は、リストCTXのI番め（0から数える）をTBに返すもので、決定的に動作する（注2)。
Occurs Checkが必要になる理由につてては、「λx.x x」の実行例を参照のこと。
getTypeFromContext(CTX, I, TA) :-
nth0(I, CTX, TB), % (*1)
unify_with_occurs_check(TA, TB). % Occurs Check のもとで、TA=TBを実行する。
テスト
test(Tm, Ty) :-
dbi(Tm, Dm), write(Dm), nl,
rbi(Dm, Tm2), write(Tm2), nl, !,
typeof(Dm, Ty),
write(Ty).
実行例
型付けできない例
型付けできないことで有名な例、「λx.x x」 である。
go23 :-
test(tm_abs(x,
tm_app(tm_var(x), tm_var(x))),
_).
型付けできないのが正しいので、これは「失敗」で終了する。
しかし、getTypeFromContextのOccurs Checkを外す(unify_with_occurs_check(TA, TB)を TA = TBに書き換える)と間違った型を返す。これは以下の理由による。
λx.x x の本体 (x x) の全体の型をT1、二番目のxの型をTxとする。すると、一番目のxの型はTx->T1になるが、これもTxであるはずだから、Tx = Tx->T1 になる。つまり、xの型は Tx かつ Tx->T1 になってしまい、これは型としておかしい。
しかしながら、Prologで（実行速度を優先して、省略時解釈のまま）Occurs Checkを行わ ない と、これを「おかしい」と判断されないため、このおかしいまま、λx.x x の型として以下の奇妙な結果を返す。
(Tx->T1)->T1、ただし Tx=Tx->T1
Occurs Check をおこなうと、Tx = Tx->T1 は「おかしい」と判断され「失敗」になる。結果としてtypeof全体が「失敗」になる。
ソフトウェアの基礎（文献2.) のサンプル
これは型付けできる例である。
go24 :-
Tm = tm_abs(a : ty_Bool,
tm_abs(b : ty_Bool -> ty_Bool,
tm_app(tm_var(b),
tm_app(tm_var(b), tm_var(a))))),
Ty = ty_Bool -> (ty_Bool -> ty_Bool) -> ty_Bool,
test(Tm, Ty). % 型検査
go24(Ty) :-
Tm = tm_abs(a : ty_Bool,
tm_abs(b : ty_Bool -> ty_Bool,
tm_app(tm_var(b),
tm_app(tm_var(b), tm_var(a))))),
test(Tm, Ty). % 型推論
前の例で、型注釈がない場合。式は直接de Bruijn Index で与えている。
go241 :-
Tm = tm_abs(ty_Bool, tm_abs(tm_app(tm_var(0 ),
tm_app(tm_var(0 ),
tm_var(1))))),
Ty = ty_Bool -> (ty_Bool -> ty_Bool) -> ty_Bool,
typeof(Tm, Ty). % 型検査
go241(Ty) :-
Tm = tm_abs(ty_Bool, tm_abs(tm_app(tm_var(0 ),
tm_app(tm_var(0 ),
tm_var(1))))),
typeof(Tm, Ty). % 型推論
de Bruijn Index 変換
以下では、通常のラムダ式からde Bruijn Indexに変換する処理、および、逆変換する処理について説明する。
正変換
dbi(Exp, Dbi) :-
empty_assoc(Env),
dbi(Exp, Env, 0, _, Dbi). % (*1)
dbi/4述語の引数の意味は以下のとおり。
dbi(+ラムダ式, +環境, +自由変数のインデックス，
-自由変数の更新されたインデクス， -変換後の式)
dbi(tm_abs(X:T, M), Env, F, F2, tm_abs(T, D)) :-
atom(X), !,
map_assoc(inc, Env, Env1),
put_assoc(X, Env1, 0, Env2), % (*1)
assoc_to_values(Env2, L),
max_list(L, F1),
dbi(M, Env2, F1, F2, D).
dbi(tm_abs(X, M), Env, F, F2, tm_abs(D)) :- !,
dbi(tm_abs(X:T, M), Env, F, F2, tm_abs(T, D)).
dbi(tm_var(X), Env, F, F, tm_var(N)) :-
atom(X),
get_assoc(X, Env, N), !.
%% 本当の自由変数は、出現の順番にindexを更新する。
%% ただし、同じ変数名が出現しても対応できない。
dbi(tm_var(_), _, F, F1, tm_var(F1)) :- !,
F1 is F + 1.
dbi(Tm, Env, F, F2, Tm2) :-
Tm =.. [Func|Tms], !,
dbi_list(Tms, Env, F, F2, Tm2s),
Tm2 =.. [Func|Tm2s].
dbi_list([Tm|Tms], Env, F, F2, [Tm2|Tm2s]) :-
dbi(Tm, Env, F, F1, Tm2),
dbi_list(Tms, Env, F1, F2, Tm2s).
dbi_list([], _, F, F, []).
inc(N, N1) :-
N1 is N + 1.
逆変換
rbi(Exp, Dbi) :-
rbi(Exp, 0, Dbi). % (*1)
rbi(tm_abs(T, M), I, tm_abs(X:T, M2)) :- !,
I1 is I + 1,
atom_concat(x, I1, X),
rbi(M, I1, M2).
rbi(tm_abs(M), I, tm_abs(X, M2)) :- !,
rbi(tm_abs(_, M), I, tm_abs(X, M2)).
rbi(tm_var(N), I, tm_var(X)) :-
integer(N),
N =< I, !, % bound
N1 is I - N + 1,
atom_concat(x, N1, X).
rbi(tm_var(N), I, tm_var(X)) :- !,
atom_concat(x, N, X). % free
rbi(Tm, I, Tm2) :-
Tm =.. [Func|Tms], !,
rbi_list(Tms, I, Tm2s),
Tm2 =.. [Func|Tm2s].
rbi_list([Tm|Tms], I, [Tm2|Tm2s]) :-
rbi(Tm, I, Tm2),
rbi_list(Tms, I, Tm2s).
rbi_list([], _, []).
テスト
test2(Tm) :-
write(Tm), nl,
dbi(Tm, Dm), write(Dm), nl,
rbi(Dm, Tm2), write(Tm2).
sample コード
TAPL 演習6.1.1
go11 :- % C0
test2(tm_abs(s:_, tm_abs(z:_, tm_var(z)))).
go12 :- % C2
test2(tm_abs(s:_, tm_abs(z:_,
tm_app(tm_var(s), tm_app(tm_var(s), tm_var(z)))))).
go13 :- % plus
test2(tm_abs(m,
tm_abs(n,
tm_abs(s,
tm_abs(z,
tm_app(tm_var(m),
tm_app(tm_var(s),
tm_app(tm_app(tm_var(n), tm_var(s)),
tm_var(z))))))))).
型注釈のある場合
go14 :-
Tm = tm_abs(a : ty_Bool,
tm_abs(b : ty_Bool -> ty_Bool,
tm_app(tm_var(b),
tm_app(tm_var(b), tm_var(a))))),
test2(Tm).
自由変数のある場合
go15 :-
test2(tm_app(tm_abs(s:_, tm_abs(z:_, tm_var(z))),
tm_var(x))).
補足説明
注1
本資料では de Bruijn Index を0から使用する。
1からにする場合は、「(*1)」の箇所の「0」を「1」に変更する。
注2
de Bruijn Indexではない一般のラムダ式の場合は、文脈を「変数名：型」のリストで保持している場合、変数Xの型TBをmember述語を使ってで見つけることになる。member(X:TB, CTX)。一般のラムダ式の場合は、同じ名前の変数が存在しスコープによっての意味が異なる。このとき、memberは複数解を求めてしまう。しかし、その場合でも必ず一番外側の、つまり最初に見つけたものを使わなければならない。
member述語の非決定性を殺すためにcutオペレータ入れる。
課題
- 総称型(generics)への拡張：copy_termを使う？
- System F への拡張：
参考文献
- Benjamin C. Pierce、住井 監訳「型システム入門 プログラミング言語と型の理論」オーム社
- Benjamin C. Pierce他、梅村他訳「ソフトウエアの基礎」、http://proofcafe.org/sf/
- SWI-Prolog、http://www.swi-prolog.org/
- GNU Prolog、http://www.gprolog.org/