Prologによる、単純型付きラムダ式の型検査と型推論について


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オペレータ入れる。

## 課題

1. 総称型(generics)への拡張：copy_termを使う？
2. System F への拡張：


# 参考文献

1. Benjamin C. Pierce、住井 監訳「型システム入門 プログラミング言語と型の理論」オーム社
2. Benjamin C. Pierce他、梅村他訳「ソフトウエアの基礎」、http://proofcafe.org/sf/
3. SWI-Prolog、http://www.swi-prolog.org/
4. GNU Prolog、http://www.gprolog.org/


```