単純型理論とか\lambda_\toとも言う

単純型付きラムダ計算の基礎になったもの

ラムダ抽象に型を付ける

主要型を持つ

強正規化できる

定義

単純階型理論における項は、ラムダ抽象

ラムダ抽象の定義を引き継ぐ

型を以下のように定義する

型変数は型である

A,Bが型なら、A\to Bは型である

「\to」は右結合

x_1:A_1,\cdots,x_n:A_n\vdash t:A

x,tは項

「\vdash」の左辺全体を「文脈」と呼ぶ

至って単純

分岐もないのでずっと上に伸びていくだけ

ASS

\frac{}{\Gamma \vdash x: A}(\mathrm{ASS}) \quad(x: A \in \Gamma)

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)

→ の導入

関数定義時の関数の型を導いている

(→E)

\frac{\Gamma \vdash f: A \rightarrow B \quad \Gamma \vdash a: A}{\Gamma \vdash f a: B}(\rightarrow E)

→ の除去

関数適用時の結果の型を導いている

補足

f,a,bは項

\Gammaは文脈

定理

\vdash t:Aかつt\xrightarrow{\ast}_{\beta\eta}sならば、\vdash s:A

\vdash t:Aならば、tは強正規化可能

つまり、tのβη簡約は必ず停止する

\vdash t:Aかつ\vdash s:Bなら、t=_{\beta\eta}sか否かの判定は決定可能

単純型付きラムダ計算との関連

参考