単純階型理論
SImple Theory of Types
定義
型を以下のように定義する
型変数は型である
$ A,Bが型なら、$ A\to Bは型である
「$ \to」は右結合
$ x_1:A_1,\cdots,x_n:A_n\vdash t:A
$ x,tは項
「$ \vdash」の左辺全体を「文脈」と呼ぶ
至って単純mrsekut.icon
分岐もないのでずっと上に伸びていくだけ
ASS
$ \frac{}{\Gamma \vdash x: A}(\mathrm{ASS}) \quad(x: A \in \Gamma)
Assumption
$ x: A \in \Gammaは$ (x: A) \in \Gamma
$ x: A \in \Gammaな状況下で$ \Gamma\vdash x:Aだと言っている
複数の場合も表しており、$ x_1,\cdots,x_nがそれぞれ$ A_1,\cdots,A_nを型にもつなら、$ x_i:A_i
(→I)
$ \frac{\Gamma, x: A \vdash t: B}{\Gamma \vdash \lambda x, t: A \rightarrow B}(\rightarrow I)
Implication Introduction
→の導入
関数定義時の関数の型を導いている
(→E)
$ \frac{\Gamma \vdash f: A \rightarrow B \quad \Gamma \vdash a: A}{\Gamma \vdash f a: B}(\rightarrow E)
Implication Elimination
→の除去
関数適用時の結果の型を導いている
補足
$ f,a,bは項
$ \Gammaは文脈
定理
$ \vdash t:Aかつ$ t\xrightarrow{\ast}_{\beta\eta}sならば、$ \vdash s:A
$ \vdash t:Aならば、$ tは強正規化可能 $ \vdash t:Aかつ$ \vdash s:Bなら、$ t=_{\beta\eta}sか否かの判定は決定可能 参考