型付け規則 - mrsekut-p

型付け規則

typing rule

型理論の文脈では推論規則と呼ぶ

ゲンツェンの自然演繹(NK)と同様に証明したいものを一番下に書き、そこから規則に従って上向きに葉を伸ばしてい

:を結合力の強い演算子と見ておくとうまく読める

:>,>$ \vdash

型付け導出の表記

T-True

$ \mathrm{true}: \mathrm{Bool}

T-False

$ \mathrm{false}: \mathrm{Bool}

T-If

$ \frac{t_1:\mathrm{Bool}\quad t2:T \quad t3:T}{\mathrm{if}\quad t_1\quad\mathrm{then}\quad t_2\quad\mathrm{else} \quad t_3:T}

CT-If

$ \frac{\Gamma \vdash t_1:\mathrm{T_1}|C_1 \quad \Gamma\vdash t2:T_2|C_2 \quad \Gamma\vdash t3:T_3|C_3} {\Gamma\vdash\mathrm{if}\quad t_1\quad\mathrm{then}\quad t_2\quad\mathrm{else} \quad t_3:T_2 \quad| C_1\cup C_2\cup C_3\cup \{ T_1=\mathrm{Bool},T_2=T_3 \}}

書くのきちぃ〜mrsekut.icon

しかも単純にこの記法見づらくない？mrsekut.icon

制約付きのif

傍線上では、$ T_1,T_2,T_3は特定の型を要請していないが、

傍線下の制約の箇所に$ T_1=\mathrm{Bool}, T_2=T_3が加わる

T-Zero

$ 0: \mathrm{Nat}

T-Succ

$ \frac{t_1:\mathrm{Nat}}{\mathrm{succ}\;t_1:\mathrm{Nat}}

T-Pred

$ \frac{t_1:\mathrm{Nat}}{\mathrm{pred}\;t_1:\mathrm{Nat}}

T-IsZero

$ \frac{t_1:\mathrm{Nat}}{\mathrm{iszero}\;t_1:\mathrm{Bool}}

T-Var

$ \frac{(\Gamma(t)=\sigma\quad(\sigma\succeq T)}{\Gamma\vdash t:T}

$ \sigmaは型スキーム

$ \succeqは型スキームのinstance

ref CoPL.icon p.148

T-Abs

ラムダ抽象の型付け規則T-Abs

T-App

関数適用の規則T-App

T-Nil

$ \frac{}{\Gamma \vdash []:[T]}

[]は空配列

[T]はT型の配列の型

T-Cons

$ \frac{\Gamma\vdash t_1:T \quad \Gamma\vdash t_2:[T]}{\Gamma\vdash t_1::t_2:[T]}

::は配列の結合

参考

CoPL 8章~