この記事は定理証明アドベントカレンダー2013のたぶん?日目の記事です

誰でも定理証明器を作れるようになろうという趣旨です。ここではCoqのパクリみたいなサブセットを48時間で作ります。

前回 http://qiita.com/kikx/items/10d143edc090bdfec477 の続きです。

型検査

型検査は文脈と2つの項が正しく型付けされた組であるかを検査します。この正しく型付けされた組であるというのを、

Γ ⊢ A : t

と書きます。Γは文脈で、Aとtが項です。しかし、この記事では表で書くことにこだわっているので、

インデックス	値と型
5 (A)	Type
4 (a)	0 (A)
3 (b)	1 (A)
2 (c)	2 (A)
1 (H)	2 = 1 (a = b)
0 (H0)	2 = 1 (b = c)
===	===
⊢	4 : 5 (a : A)

のように見やすく書くことにします。上の表はインデックス4の型はインデックス0であることが文脈に入っていて、前回と同じように文脈をそろえてやると、インデックス5が型であることがわかるので正しい表になります。

型検査の問題は勝手な表

インデックス	値と型
Γ	Γ
===	===
⊢	A : t

が与えられたときに、正しい表であるかどうかを計算することになります。これは上に書いた場合を一般の場合に行えばよいことがわかります。

項Aの型を文脈Γを使って計算する
計算した型が与えられた項tと一致するかどうかを確かめる

よって、型検査の実装は単に次のようになります

typeCheck :: Local -> Term -> Term -> Bool
typeCheck e a t =
  case typeof e a of
    Just s -> termEq t s
    None -> False

termEqは前回実装した項の比較です。残りは型を計算する関数 typeof を実装すればよいわけです。

変数の型は簡単に計算できます。ただし、これは失敗することがあるので Maybe Term を返すことにします。ちゃんとエラーハンドリングしたい場合は他のモナドを使ってください。

typeof :: Local -> Term -> Maybe Term
typeof e (Var i) =
  Just $ termShift 0 (i + 1) $ case e!!i of
    Decl ty  -> ty
    Def ty t -> ty

型検査の規則

残りの項の型を計算するのは大変です。まず型検査の規則を知らなければいけません。この規則は色々な文献にいろんな形で書いてあります。例えば

http://coq.inria.fr/distrib/current/refman/Reference-Manual006.html#sec167 Coqのリファレンスマニュアル
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.88.9497 Variants of the Basic Calculus of Constructions

しかし、この規則を読んで typeof 関数を実装するのは大変です。TaPLを読んでおけば、一言で構文主導になっていないからと説明できます。

構文主導になっているものとして、以下の論文の付録なんかがあります。

http://matita.cs.unibo.it/PAPERS/sadhana.pdf A compact kernel for the calculus of inductive constructions

というわけで、この構文主導になっているバージョンを参考にしながら実装していきます。

型の型

項 Univ i は型の型でした。そして、型の型の型は Univ (i + 1) にすることになっていたので、この場合は簡単です。

typeof _ (Univ i) = Just $ Univ (i + 1)

関数の型

ラムダ式 Lam ty body の型は関数型です。bodyの型をTとするとtyを受け取ってTを返す関数型になるはずです。しかし、依存型の型システムではTはtyの値にも依存します。このような関数型を Prod ty T で表します。よってアンチョクに書くと

-- だめな例
typeof e (Lam ty body) = do
  tbody <- typeof (Decl ty : e) body
  return $ Prod ty tbody

でよいように見えます。何が悪いのかというと、ty が型であることを検査していません。型は項ですが、一般の項が全て型であるわけではありません。型でないといけない場所に書いてある項は型であることを確かめなければいけません。

項 ty が型であるというのは、ty の型が型の型であることをいいます。これを行う操作を追加すると

typeof e (Lam ty body) = do
  assertType e ty
  tbody <- typeof (Decl ty : e) body
  return $ Prod ty tbody

のようになります。assertType は型ではなかったときに失敗することにします。この場合は Nothing を返します。この実装は後回しにしましょう。

関数型の型

今度は Prod ty body の型を計算します。これは関数型で、すでに型であるので、その型は型の型になるはずです。よって、適当な自然数 i を決めて、Univ i を返します。

さらに、引数の型 ty と結果の型 body もすでに型です。なので、assertType を呼び出さないといけないのですが、ここでは結果の型 Univ uty と Univ ubody も必要です。そこで、assertType の別バージョンで、結果を返すものを使います。

typeof e (Prod ty body) = do
  uty <- typeofType e ty
  ubody <- typeofType (Decl ty : e) body
  return $ Univ (max uty ubody)

typeofType は型 ty の型が Univ uty だった場合は uty を返します。ty が型でなかった場合は assertType と同様に失敗します。

結果は2つの整数の大きいほうとしています。これは一番保守的なやり方です。もっと結果を小さくするとCoqのPropみたいになって便利になりますが、注意して決めないと矛盾ができてしまいます。

関数適用の型

最後に関数適用 App f a の型を計算します。これが一番難しいので最後に残っているわけですね。

まず、f の型は関数型 Prod ty body でなければなりません。次に引数 a の型は ty と一致していないといけません。結果の型は、普通の型システムの場合はbodyでいいのですが、依存型の場合は引数に渡した値に依存する結果の型を持ってもいいので、body の中で引数の値を参照しているところに、実際の値 a を代入してあげる必要があります。

typeof e (App f a) = do
  fty <- typeof e f
  case fty of
    Prod ty body | typeCheck e a ty ->
      return $ termShift 0 (-1) $ reduceFull (Def ty a:e) body
    _ -> Nothing

代入する代わりに reduceFull と -1 シフトを使っています。subst を実装した場合はそちらを使ったほうがいいでしょう。ここでは全く効率を考えていないためこの実装を使います。

残りの関数

関数 typeofType は項の型を計算して、Univ i になっていることを確認し、i を返します。

typeofType :: Local -> Term -> Maybe Int
typeofType e t = do
  ty <- typeof e t
  case reduceFull e ty of
    Univ i -> return i
    _ -> Nothing

ここで注意しないといけないのは、ちゃんと計算しないといけないことです。

関数 assertType は上と同様の確認を行って、結果を返さない関数です。

assertType :: Local -> Term -> Maybe ()
assertType e t = void $ typeofType e t

暗黙の仮定

これらの関数は相互に再帰呼び出ししています。これがちゃんと停止するためには引数に仮定が必要です。例えば、型検査されていない項を計算しようとすると無限ループになることがあります。

最初に、どの関数にも渡さないといけない文脈は正しく作られていなければなりません。すなわち、中身が正しく型検査されている必要があります。すなわち、

空リストは正しく作られている
e が正しく作られていて、ty が assertType e ty を満たすときには、Decl ty : e も正しく作られている
e が正しく作られていて、ty が assertType e ty を満たし、t が typeCheck e t ty を満たすときに、Def ty t : e も正しく作られている。

この方法で正しい文脈を作って渡さないといけません。

次に、reduceFull e t に渡す項 t は正しく型検査されていなければなりません。ここでは、typeof e t が失敗しないことをいいます。このことから、termEq e t1 t2 の引数も同様の条件が必要であり、typeCheck e a t の t も同様であることがわかります。

これらを守っていれば、各関数は停止します。さらに、

typeof e t の結果が ty のときは、t の部分項と ty と ty の部分項は型検査する必要はない。

実際に、reduceFull や typeof の中で再帰呼び出しするときにこのことを使っています。しかし、これらの事実を証明するのは大変です。

次回は型を増やします

Write Yourself a Theorem Prover in 48 Hours (その2)

型検査