Prologによる、System Fの型付プログラム
2014/05/10 @suharahiromichi
2014/05/23 @suharahiromichi
2014/05/23 @suharahiromichi 「call/ccによる古典論理の証明」を見直す。
TAPL 第25章 System Fの型付けのプログラムをPrologで実装してみた。（ただし、存在型は未実装である。）
この文章のソースコードは以下にあります。
https://github.com/suharahiromichi/prolog/blob/master/tapl/tapl_systemf_qiita.swi
使い方の例：
% swipl.
?- ['tapl_systemf_qiita.swi'].
?- go2.
Prolog処理系はSWI-Prolog (Ver.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) 変数の参照
True tm_true 定数
False tm_false 定数
λX.y tm_tabs(T, y) 型のλ抽象
y [Bool] tm_tapp(y, ty_bool) 型の適用
∀x.y ty_all(x, y) 全称型
∃x.y ty_some(x, y) 存在型
T1→T2 t1->t2 関数型 (ty_arrの中置記法)
X ty_var(x) 型変数
Bool ty_bool 型定数
変換の例
一般的な記法
以下に全称型を含む一般的な記法を示す。
(1) (λX. λf:X→X. λa:X. f (f a))
(2) ∀X. (X→X)→X→X ((1)の型)
(3) double [Bool→Bool]
ここで使う記法
ここで使う記法では、(1)(2)(3)は次のようになる。
(1)
tm_tabs(x,
tm_abs(f : ty_var(x) -> ty_var(x),
tm_abs(a : ty_var(x),
tm_app(f, tm_app(tm_var(f), tm_var(a))))))
(2)
ty_all(x, (ty_var(x)->ty_var(x))->ty_var(x)->ty_var(x))
(3)
tm_tapp(double, ty_bool -> ty_bool).
ここで使う de Bruijn Index
内部的には、de Bruijn Index を使用する。その記法を以下に示す。
(1)
tm_tabs(
tm_abs(ty_var(0)->ty_var(0),
tm_abs(ty_var(1),
tm_app(tm_var(1),
tm_app(tm_var(1), tm_var(0))))))
(2)
ty_all((ty_var(0) -> ty_var(0)) -> ty_var(0) -> ty_var(0 )))))
(3)
tm_tapp(double, ty_bool -> ty_bool).
型の注釈で使う「:」と、そのなかでの関数型を示す「->」は、「,」より優先度が高いものとする。また、「->」は右結合で、「:」より優先度が高いものとする。
:- op(600, xfx, :). % 例、x : T
:- op(500, xfy, ->). % 例、Tx->Ty
型検査のプログラム
typeof
typeof/2述語の引数の意味を以下に示す。式はde Bruijn Indexで与える。引数の前の「+」は入力、「-」は出力、「?」はそのどちらにもなることを示す。
つまり、第2引数の「型」は、入力でも出力でもよく、入力なら型検査、出力なら型付けの意味になる。
typeof(+式, ?型)
typeof(E, T) :-
typeof([], E, T).
typeof/3述語の引数の意味を以下に示す。
typeof(+文脈, +式, ?型)
型検査をおこなうtypeof/3は、TAPL(参考文献1.)の 25.5節 型付けを移して、すこし修正したものである。なお、エラー時の処理はおこなわず、実行が「失敗」するようにしている。
typeof(CTX, tm_var(I), T) :-
getTypeFromContext(CTX, I, T).
typeof(CTX, ty_var(I), T) :- % 複雑な型を型適用するとき、必要になる。
getTypeFromContext(CTX, I, T).
typeof(CTX, tm_abs(TyT1, Tm2), TyT1 -> TyT22) :- % 型注釈のある場合
typeof([varbind(TyT1)|CTX], Tm2, TyT2),
typeShift(-1, TyT2, TyT22).
typeof(CTX, tm_abs(Tm2), TyT1 -> TyT2) :- % 型注釈のない場合
typeof([varbind(TyT1)|CTX], Tm2, TyT2).
typeof(CTX, tm_app(Tm1, Tm2), Ty12) :-
typeof(CTX, Tm1, Ty11 -> Ty12),
typeof(CTX, Tm2, Ty11).
typeof(CTX, tm_tabs(T2), ty_all(TyT2)) :-
typeof([tyvarbind|CTX], T2, TyT2).
typeof(CTX, tm_tapp(T1, TyT2), TyT22) :-
typeof(CTX, T1, ty_all(TyT12)),
typeSubstTop(TyT2, TyT12, TyT22).
typeof(_, tm_true, ty_bool).
typeof(_, tm_false, ty_bool).
typeof(CTX, tm_if(T1, T2, T3), TyT12) :-
typeof(CTX, T1, ty_bool),
typeof(CTX, T2, TyT12),
typeof(CTX, T3, TyT12).
getTypeFromContext
getTypeFromContextは、変数の型を文脈(context)から取り出すことをおこなう。de Bruijn Indexの場合は、Indexの値によって一意に決まるため、nth0述語で取り出すことができる(注1)。なお、Occurs Checkが必要になる理由につてては、(参考文献3.)を参照のこと。
getTypeFromContext(CTX, I, T) :-
nth0(I, CTX, varbind(TB)), % 項の変数で、型はTB。
unify_with_occurs_check(TA, TB), % Occurs Check のもとで、TA=TBを実行する。
I1 is I + 1,
typeShift(I1, TA, T). % TAPL Web fullpoly/syntax.ml を参照のこと。
getTypeFromContext(CTX, I, tyvarbind) :-
nth0(I, CTX, tyvarbind). % 型変数である。
typeShift
typeShift(D, T, T2) :- % ↑D,0,T = T2
typeShiftAbove(D, 0, T, T2).
typeShiftAbove(D, C, T, T2) :- % ↑D,C,T = T2
tymap(typeShiftAbove_onmap(D), C, T, T2).
typeShiftAbove_onmap(D, C, X, ty_var(X2)) :-
X >= C, !,
X2 is X + D.
typeShiftAbove_onmap(_, _, X, ty_var(X)).
gosh :-
T = ty_all(ty_var(3), ty_var(3) -> ty_var(0 )),
writeln(T),
typeShiftAbove(10, 1, T, T2), % indexの2以上にたいして10シフトする。
writeln(T2).
typeSubst
typeSubstTop(TS, TT, T2) :-
typeShift(1, TS, TS1),
typeSubst(TS1, 0, TT, T1),
typeShift(-1, T1, T2).
typeSubst(TS, J, TT, T2) :- % [J→TS]TT
tymap(typeSubst_onmap(TS), J, TT, T2).
typeSubst_onmap(TS, J, X, T2) :-
X == J, !,
typeShift(J, TS, T2).
typeSubst_onmap(_, _, X, ty_var(X)).
gosu :-
TT = ty_all(ty_var(3) -> ty_var(0 )),
writeln(TT),
typeSubst(ty_bool, 2, TT, T2), % indexの2をty_boolにする。
writeln(T2).
typeShift と typeSubst の共通述語
tymap(ONVAR, C, T1->T2, T12->T22) :- !, % ty_arr
tymap(ONVAR, C, T1, T12),
tymap(ONVAR, C, T2, T22).
tymap(ONVAR, C, ty_var(X), T2) :- !,
call(ONVAR, C, X, T2).
tymap(ONVAR, C, ty_all(T2), ty_all(T22)) :- !,
C1 is C + 1,
tymap(ONVAR, C1, T2, T22).
tymap(ONVAR, C, ty_some(T2), ty_some(T22)) :- !,
C1 is C + 1,
tymap(ONVAR, C1, T2, T22).
tymap(_, _, T, T). % 型定数
テスト
test(Tm, Ty) :-
var(Ty), !, % 型付け
write(Tm), nl,
dbi(Tm, Dm), write(Dm), nl,
% rbi(Dm, Tm2), write(Tm2), nl, !,
typeof(Dm, Dy),
write(Dy), nl,
rbi(Dy, Ty),
write(Ty), nl.
test(Tm, Ty) :- % 型チェック
write(Tm), nl,
write(Ty), nl,
dbi(Tm, Dm), write(Dm), nl,
dbi(Ty, Dy), write(Dy), nl,
typeof(Dm, Dy).
実行例
簡単な例
go0 :- % λX.λx:X.x : ∀X.X->X
% λ λ0 0 0 : ∀0->0
% spy(typeof),
T = tm_tabs(tm_abs(ty_var(0 ), tm_var(0 ))),
typeof(T, Ty),
write(Ty), nl.
ちょっとした例
go1 :- % λX.λf:X-X.λx:X.f x : ∀X.(X->X)->X->X
% λ λ0->0 λ1 1 0 : ∀(0->0 )->0->0
% spy(typeof),
test(tm_tabs(x,
tm_abs(f : ty_var(x) -> ty_var(x),
tm_abs(a : ty_var(x),
tm_app(tm_var(f), tm_var(a))))),
_).
double、型は上と同じ
go2 :- % λX.λf:X-X.λx:X.f f x : ∀X.(X->X)->X->X
% λ λ0->0 λ1 1 1 0 : ∀(0->0 )->0->0
test(tm_tabs(x,
tm_abs(f : ty_var(x) -> ty_var(x),
tm_abs(a : ty_var(x),
tm_app(tm_var(f),
tm_app(tm_var(f), tm_var(a)))))),
_).
double に型の適用をする
go3 :- % (λX.λf:X-X.λx:X.f f x) [Bool] : (Bool->Bool)->Bool->Bool
test(tm_tapp(
tm_tabs(x,
tm_abs(f : ty_var(x) -> ty_var(x),
tm_abs(a : ty_var(x),
tm_app(tm_var(f),
tm_app(tm_var(f), tm_var(a)))))),
ty_bool),
_).
BoolのChurch表現 (TAPL)
go4 :-
Tru = tm_tabs(x, tm_abs(t : ty_var(x), tm_abs(f : ty_var(x), tm_var(t)))),
Fls = tm_tabs(x, tm_abs(t : ty_var(x), tm_abs(f : ty_var(x), tm_var(f)))),
CBool = ty_all(x, ty_var(x)->ty_var(x)->ty_var(x)),
test(Tru, CBool), nl,
test(Fls, CBool).
Church数 (TAPL)
go5 :-
C0 = tm_tabs(x, tm_abs(s : ty_var(x)->ty_var(x),
tm_abs(z : ty_var(x), tm_var(z)))),
C1 = tm_tabs(x, tm_abs(s : ty_var(x)->ty_var(x),
tm_abs(z : ty_var(x),
tm_app(tm_var(s), tm_var(z))))),
C2 = tm_tabs(x, tm_abs(s : ty_var(x)->ty_var(x),
tm_abs(z : ty_var(x),
tm_app(tm_var(s),
tm_app(tm_var(s), tm_var(z)))))),
CNat = ty_all(x, (ty_var(x)->ty_var(x))->ty_var(x)->ty_var(x)),
CSUCC = tm_abs(n : CNat,
tm_tabs(x,
tm_abs(s : ty_var(x)->ty_var(x),
tm_abs(z : ty_var(x),
tm_app(tm_var(s),
tm_app(tm_app(tm_tapp(tm_var(n),
ty_var(x)),
tm_var(s)),
tm_var(z))))))),
CPLUS = tm_abs(m : CNat,
tm_abs(n : CNat,
tm_app(tm_app(tm_tapp(tm_var(m), CNat),
CSUCC),
ty_var(n)))),
test(C0, CNat), nl,
test(C1, CNat), nl,
test(C2, CNat), nl,
test(CSUCC, CNat->CNat), nl,
test(CPLUS, CNat->CNat->CNat), nl,
CPairNat = ty_all(x, (CNat -> CNat -> ty_var(x)) -> ty_var(x)), % 型
PairNat = tm_abs(n1 : CNat, % コンストラクタ
tm_abs(n2 : CNat,
tm_tabs(x,
tm_abs(f : CNat -> CNat -> ty_var(x),
tm_app(tm_app(tm_var(f), tm_var(n1)),
tm_var(n2)))))),
FstNat = tm_abs(p : CPairNat,
tm_app(tm_tapp(tm_var(p), CNat),
(tm_abs(n1 : CNat, tm_abs(n2 : CNat, tm_var(n1)))))),
SndNat = tm_abs(p : CPairNat,
tm_app(tm_tapp(tm_var(p), CNat),
(tm_abs(n1 : CNat, tm_abs(n2 : CNat, tm_var(n2)))))),
test(PairNat, CNat -> CNat -> CPairNat), nl,
test(FstNat, CPairNat -> CNat), nl,
test(SndNat, CPairNat -> CNat), nl.
List (TAPL)
go6 :-
CList_x =
ty_all(r, % CList X
(ty_var(x) -> ty_var(r) -> ty_var(r)) -> ty_var(r) -> ty_var(r)),
Nil =
tm_tabs(x,
tm_tabs(r,
tm_abs(c : ty_var(x) -> ty_var(r) -> ty_var(r),
tm_abs(n : ty_var(r),
ty_var(n))))),
Cons =
tm_tabs(x,
tm_abs(hd : ty_var(x),
tm_abs(tl : CList_x, % CList X
tm_tabs(r,
tm_abs(c : ty_var(x) -> ty_var(r) -> ty_var(r),
tm_abs(n : ty_var(r),
tm_app(tm_app(tm_var(c),
tm_var(hd)),
tm_app(tm_app(tm_tapp(tm_var(tl),
ty_var(r)),
tm_var(c)),
tm_var(n))))))))),
IsNil =
tm_tabs(x,
tm_abs(l : CList_x, % CList X
tm_app(tm_app(tm_tapp(tm_var(l), ty_bool),
tm_abs(hd : ty_var(x),
tm_abs(tl : ty_bool,
tm_false))),
tm_true))),
test(Nil, ty_all(x, CList_x)), nl,
test(Cons, ty_all(x, ty_var(x) -> CList_x -> CList_x)), nl,
test(IsNil, ty_all(x, CList_x -> ty_bool)).
call/cc による古典論理の証明
「call/ccを使って」二重否定除去の定理：∀P. ~ ~ P → P を証明する。
二重否定除去の定理は古典論理の範疇に属するので、直観論理に対応する型付きラムダ計算の範囲では証明できない。そこで、call/cc : ∀P. ((P → False) → P) → P を公理として追加することで、実際に証明できることを示す。
~P は P→False のことであるから、∀P. ((P → False) → False) → P を証明する。
まず、Falseに当たるデータ型を定義する。False型は要素を持たない型である。この文章では、ty_falseと表記するが、bool型の要素のtm_falseとは別のものである。
False型についての推論（帰納法）を実施するためには、False型をもらって（Falseとは別の）型を返す式が必要になる。これは、Coq(Gallina)では、match f return P with endと書く。withとendの間にあるべき条件節が空なので、fの型は「要素の無い型」であればよい（なければならない）。ここでは、False型に限定するものとする。
typeof(CTX, return(Tm1, T2), T2) :-
typeof(CTX, Tm1, ty_false).
returnを使うと、Falseの型の定義にあたる、Fales_indは次のように定義でき、∀P.False → P の型を持つ。これは「ex falso quodlibet」の定理でもある（文献4.）。False_indは何度も使うので、定義を保存しておく。
false_ind(tm_tabs(p,
tm_abs(f : ty_false,
return(tm_var(f), ty_var(p))))).
go70 :-
false_ind(False_ind),
test(False_ind, ty_all(p, ty_false -> ty_var(p))).
ついで、call/cc の型を typeof に追加する。call/ccの型は型付きラムダ式の範囲で書くことができるが、定義の中身を書くことはできない。そのため、型だけをtypeofの中に定義する。
typeof(_, callcc, T) :-
dbi(ty_all(p, ((ty_var(p) -> ty_false) -> ty_var(p)) -> ty_var(p)), T).
次の go7 は成功する。その Qは、∀P. ((P → False) → False) → P の型を持ったラムダ式であり、その値は、定理 ∀P. ~ ~ P → P が成立する「証拠」であると考えられる。
go7 :-
false_ind(False_ind),
Q = tm_tabs(p,
tm_abs(h : (ty_var(p) -> ty_false) -> ty_false,
tm_app(tm_tapp(callcc, ty_var(p)),
tm_abs(h1 : ty_var(p) -> ty_false,
tm_app(tm_tapp(False_ind, ty_var(p)),
tm_app(tm_var(h), tm_var(h1))))))),
test(Q,
ty_all(p, ((ty_var(p) -> ty_false) -> ty_false) -> ty_var(p))).
もうすこし平たくいうと、「call/ccがあると古典論理が証明できる」というのは、
∀P. (((P→False)→P)→P) → ((P→False)→False)→Pの型を持つ項が定義できる、すなわち、直観論理で∀P. ((~P→P)→P) → (~ ~P→P)が証明できる、ということと同じなのであろう。
go72 :-
false_ind(False_ind),
Q = tm_tabs(p,
tm_abs(c : ((ty_var(p) -> ty_false) -> ty_var(p)) -> ty_var(p),
tm_abs(h : (ty_var(p) -> ty_false) -> ty_false,
tm_app(tm_var(c),
tm_abs(h1 : ty_var(p) -> ty_false,
tm_app(tm_tapp(False_ind, ty_var(p)),
tm_app(tm_var(h), tm_var(h1)))))))),
test(Q, ty_all(p,
(((ty_var(p) -> ty_false) -> ty_var(p)) -> ty_var(p)) ->
((ty_var(p) -> ty_false) -> ty_false) -> ty_var(p))).
de Bruijn Index 変換
以下では、通常のラムダ式からde Bruijn Indexに変換する処理、および、逆変換する処理について説明する。
正変換
dbi(Exp, Dbi) :-
empty_assoc(Env),
dbi(Exp, Env, 0, _, Dbi).
dbi/4述語の引数の意味は以下のとおり。
dbi(+ラムダ式, +環境, +自由変数のインデックス，
-自由変数の更新されたインデクス， -変換後の式)
dbi(tm_abs(X:T, M), Env, F, F3, tm_abs(T2, D)) :-
dbi(T, Env, F, F2, T2),
dbi_abs(X, M, Env, F2, F3, D).
dbi(tm_abs(X, M), Env, F, F2, tm_abs(D)) :- !,
dbi_abs(X, M, Env, F, F2, D).
dbi(tm_tabs(X, M), Env, F, F2, tm_tabs(D)) :- !,
dbi_abs(X, M, Env, F, F2, D).
dbi(ty_all(X, M), Env, F, F2, ty_all(D)) :- !,
dbi_abs(X, M, Env, F, F2, D).
dbi(tm_var(X), Env, F, F, tm_var(N)) :-
atom(X),
get_assoc(X, Env, N), !.
dbi(ty_var(X), Env, F, F, ty_var(N)) :-
atom(X),
get_assoc(X, Env, N), !.
%% 本当の自由変数は、出現の順番にindexを更新する。
%% ただし、同じ変数名が出現しても対応できない。
dbi(tm_var(_), _, F, F1, tm_var(F1)) :- !,
F1 is F + 1.
dbi(ty_var(_), _, F, F1, ty_var(F1)) :- !,
F1 is F + 1.
%% tm_app, tm_tapp, tm_var その他の定数
dbi(Tm, Env, F, F2, Tm2) :-
Tm =.. [Func|Tms], !,
dbi_list(Tms, Env, F, F2, Tm2s),
Tm2 =.. [Func|Tm2s].
dbi_abs(X, M, Env, _, F2, D) :- % tm_absとtm_tabsの共通述語
atom(X), !,
map_assoc(inc, Env, Env1),
put_assoc(X, Env1, 0, Env2),
assoc_to_values(Env2, L),
max_list(L, F1),
dbi(M, Env2, F1, F2, D).
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(Dbi, Exp) :-
rbi(Dbi, 0, Exp).
rbi(tm_abs(T, M), I, tm_abs(X:T2, M2)) :- !,
rbi(T, I, T2),
rbi_abs(M, I, X, M2).
rbi(tm_abs(M), I, tm_abs(X, M2)) :- !,
rbi_abs(M, I, X, M2).
rbi(tm_tabs(M), I, tm_tabs(X, M2)) :- !,
rbi_abs(M, I, X, M2).
rbi(ty_all(M), I, ty_all(X, M2)) :- !,
rbi_abs(M, I, X, M2).
rbi(tm_var(N), I, tm_var(X)) :-
integer(N),
N =< I, !, % bound
N1 is I - N,
atom_concat(x, N1, X).
rbi(ty_var(N), I, ty_var(X)) :-
integer(N),
N =< I, !, % bound
N1 is I - N,
atom_concat(x, N1, X).
rbi(tm_var(N), _, tm_var(X)) :- !,
atom_concat(x, N, X). % free
rbi(ty_var(N), _, ty_var(X)) :- !,
atom_concat(x, N, X). % free
rbi(Tm, I, Tm2) :-
Tm =.. [Func|Tms], !,
rbi_list(Tms, I, Tm2s),
Tm2 =.. [Func|Tm2s].
rbi_abs(M, I, X, M2) :-
I1 is I + 1,
atom_concat(x, I1, X),
rbi(M, I1, M2).
rbi_list([Tm|Tms], I, [Tm2|Tm2s]) :-
rbi(Tm, I, Tm2),
rbi_list(Tms, I, Tm2s).
rbi_list([], _, []).
テスト
t1 :- % (1)
X0 = tm_tabs(x,
tm_abs(f : ty_var(x) -> ty_var(x),
tm_abs(a : ty_var(x),
tm_app(tm_var(f),
tm_app(tm_var(f), tm_var(a)))))),
writeln(X0),
dbi(X0, X), writeln(X),
rbi(X, X1), writeln(X1).
t2 :- % (2)
X0 = ty_all(x, (ty_var(x)->ty_var(x))->ty_var(x)->ty_var(x)),
writeln(X0),
dbi(X0, X), writeln(X),
rbi(X, X1), writeln(X1).
補足説明
注1
本資料では de Bruijn Index を0から使用する。
1からにする場合は、(参考文献 3.) の補足説明を参照のこと。
参考文献
- Benjamin C. Pierce、住井 監訳「型システム入門 プログラミング言語と型の理論」オーム社
- SWI-Prolog、http://www.swi-prolog.org/
- Prologによる、単純型付きラムダ式の型検査と型推論について、
http://qiita.com/suharahiromichi/items/6d944725636c6cac7400 - Pierce他、梅村他訳「ソフトウエアの基礎」、Coqにおける論理
http://proofcafe.org/sf/Logic_J.html