Prolog
TaPL
SWI-Prolog

PrologによるSystem Fの型付プログラム

More than 3 years have passed since last update.

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_qitta.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) :-                 % [JTS]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 を公理として追加することで、実際に証明できることを示す。

~PP→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.) の補足説明を参照のこと。

参考文献

  1. Benjamin C. Pierce、住井 監訳「型システム入門 プログラミング言語と型の理論」オーム社
  2. SWI-Prolog、http://www.swi-prolog.org/
  3. Prologによる、単純型付きラムダ式の型検査と型推論について、 http://qiita.com/suharahiromichi/items/6d944725636c6cac7400
  4. Pierce他、梅村他訳「ソフトウエアの基礎」、Coqにおける論理 http://proofcafe.org/sf/Logic_J.html