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

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

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

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 \}}

書くのきちぃ〜

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

制約付きの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 p.148

T-Abs

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章~