Simply Typed Lambda Calculus

単純型理論 ${\lambda }_{\to }$

• λ計算 に型をつけたもの
  • 型代入の話は HM型推論をJuliaで実装する の理論につながる

${\lambda }_{\to }$ の型

• 型変数 $A$ は型
• $A,B$ が型なら $(A\to B)$ は型

$A_1\to A_2\to \cdots A_n\to A\equiv (A_1\to (A_2\to \cdots ))$

${\lambda }_{\to }$ の項

• 項は $\lambda$ 式

${\lambda }_{\to }$ の判定

def. ${\lambda }_{\to }$ の判定

$x_1:A_1,\cdots x_n:A_n⊢t:A$ を 判定
$x_1:A_1,\cdots x_n:A_n$ を 文脈 という

ex.

$x:\alpha \to \beta \to \gamma ,y:\alpha \to \beta ,z:\alpha$ のとき
$xz(yz)⊢\gamma$

${\lambda }_{\to }$ の推論規則

def. ${\lambda }_{\to }$ の推論規則

• $\Gamma$: 文脈
• $x$: 変数
• $f,a,t$: 項
• $A,B$: 型
• $(x:A)\in \Gamma$: $\Gamma$ に $x:A$ が現れる

1. (Assumption) $\frac{}{\Gamma ⊢x:A}(x:A\in \Gamma )$
2. ($\to$-I; Implication Introduction) $\frac{\Gamma ,x:A⊢t:B}{\Gamma ⊢\lambda x.t:A\to B}$
3. ($\to$-E) $\frac{\Gamma ⊢f:A\to B\Gamma ⊢a:A}{\Gamma ⊢fa:B}$

Subjection Reduction

$\beta$ 簡約しても型は変わらない

th. SR

$\Gamma ⊢t:A,t{\twoheadrightarrow }_{\beta }u\Rightarrow \Gamma ⊢u:A$

プログラムのデータ型が実行で変わらない事を保証

prop

$\Gamma ,x:A⊢t:B,\Gamma ⊢a:A\Rightarrow \Gamma ⊢t[x:=a]:B$

型代入

def. 型代入

型代入 $\sigma :\mathrm{TypeVars}\to \mathrm{Types}$
${\alpha }^{\sigma }:=\sigma (\alpha )$

• $\sigma \le \rho$: $\sigma \circ \exists {\rho }_1=\rho$ ($\sigma$ の方が単純*)
• $\sigma$ が $A,B$ の unifier とは $A^{\sigma }=B^{\sigma }$

ex.

A = (a_1 -> a_2) -> a_3, B = b_1 -> (b_2 -> b_3) のとき
型代入
b_1 => a_1 -> a_2
a_3 => b_2 -> b_3
_ => x
は unifier

主型(principal type)

$\lambda x.x$ の型について,
$⊢\lambda x.x:\alpha \to \alpha$
$⊢\lambda x.x:(\alpha \to \beta )\to (\alpha \to \beta )$

参考文献

• http://web.sfc.keio.ac.jp/~hagino/logic18/14.pdf
• https://takuto-h.hatenadiary.org/entry/20110401/unify
• web.yl.is.s.u-tokyo.ac.jp/~kohei/rinkou/types/resume/9.pdf