型付け規則

文脈と判断

$f\;p$ のような項は単独では検査できず、その型は $f$ と $p$ が何であるかに依存する。文脈（context）$\Gamma$ がその情報を記録する。文脈は仮定の順序付きリスト

であり、スコープ内の各変数の型を与える。$\dom(\Gamma)$ は名前の集合 $\{x_1, \ldots, x_n\}$ を表し、空の文脈は $\cdot$ と書く。

順序は重要であり、$P : \Sort{0},\; h : P$ のように、後の型が前の変数に言及してよい。仮定 $h : P$ は、$P$ が命題だとわかってはじめて意味を持つ。文脈の中の名前は互いに異なることを要求するので、文脈は名前から型への辞書のように使えるが、その項目が順に互いへ依存する辞書である。

二つの判断を同時に定義する。

• $\ctxok{\Gamma}$ は文脈 $\Gamma$ が整形式（well formed）であること、すなわち仮定された各型がその手前の文脈において型であることを意味する。
• $\Gamma \vdash t : A$ は、$\Gamma$ の仮定のもとで項 $t$ が型 $A$ を持つことを意味する。

Curry-Howard の目で見れば、$\Gamma \vdash t : A$ は、$t$ が仮定 $\Gamma$ からの $A$ の証明であると言っている。

規則

図 3.1 にすべての規則を挙げる。各規則は線の上に前提、下に結論を持ち、前提がすべて成り立てば結論が成り立つ。右側の規則名は本書全体で使う。

規則のうち二つは項に対する操作を使っているが、続く数章ではそれをブラックボックスとして扱う。

代入。 T-App は、$B$ の中の $x$ の自由な出現をすべて $a$ で置き換えた結果を $\subst{B}{x}{a}$ と書く。たとえば $\subst{(P \to P)}{P}{Q} = Q \to Q$ である。束縛子の内側で名前を置き換えるには注意が要り、それは第 11 章で説明するが、それまでは直観的な意味で十分である。

定義的等価。 T-Conv は、$A$ と $B$ がカーネルに機械的に判定できる意味で「同じ型」であるとき、$A \conv B$ と書く。二種類の違いが無視される。

• 束縛変数の名前。$\tPi{P}{\Sort{0}}{P \to P}$ と $\tPi{Q}{\Sort{0}}{Q \to Q}$ は同じ命題を述べている。この点だけが異なる項を α 同値と呼び、$A \alphaeq B$ と書く。
• 計算。$\mathit{Id} = \tLam{X}{\Sort{0}}{X}$ とすると、$\mathit{Id}\;P$ は $X$ に $P$ を代入して $P$ に計算されるので、$\mathit{Id}\;P$ の証明は $P$ の証明として数えられるべきである。計算の一歩 $(\tLam{x}{A}{t})\;s \betared \subst{t}{x}{s}$ を β 簡約（beta-reduction）と呼ぶ。

カーネルは $A \conv B$ を、両辺を可能な限り計算してから結果が α 同値かどうかを調べることで判定する。第 12 章でこれを正確に定義する。

規則の読み方

規則は下から上へ、結論を立てるには前提を立てよという手順として読むのがよい。

C-Empty と C-Ext。 文脈は仮定を一つずつ加えて作り、新しい仮定の型はそれ自体が型でなければならない。側条件 $x \notin \dom(\Gamma)$ は同じ名前の仮定が二つあることを禁じるが、束縛変数の名前は重要でないので、これは何も制限していない。衝突しそうな束縛子は、先に名前を付け替えればよい。この条件を省いたカーネルで何が起きるかは第 11 章で示す。

T-Sort。 どの宇宙も次の宇宙に住み、$\Sort{0} : \Sort{1}$、$\Sort{1} : \Sort{2}$、以下同様である。宇宙が自分自身の型にはなれない理由は第 13 章で説明する。

T-Var。 変数は文脈が割り当てる型を持ち、論理的には仮定を使うことにあたる。

T-Pi。 $A$ が型で、$x : A$ を仮定したうえで $B$ が型なら、$\tPi{x}{A}{B}$ は型である。結果の宇宙は $\imax(u, v)$ で、$v = 0$ なら $0$、そうでなければ $\max(u, v)$ である。言葉にすると、$\Pi$ 型は本体が命題でありさえすれば何の上で量化していようと命題であり、そうでなければ二つの宇宙の大きい方に住む。論理的には、この規則は $A \to B$ と $\forall x{:}A.\,B$ がいつ整形式の主張であるかを言っている。

T-Lam。 $A$ から $B$ への関数を作るには、$x : A$ を仮定して型 $B$ の項 $t$ を作る。本体の型 $B$ は $x$ に言及してよく、結果の $\Pi$ 型にそのまま残る。依存性が入り込むのはここである。論理的には、これは含意と全称量化子の導入規則であり、$A \to B$ を証明するには $A$ を仮定して $B$ を証明する。

T-App。 $f$ が各 $x : A$ を $B$ の要素に写し、$a : A$ なら、$f\;a$ は $B$ の $x$ を $a$ で置き換えた型を持つ。$B$ が $x$ に言及しないなら、これは $A \to B$ と $A$ から $B$ を結論するモーダスポネンスであり、言及するなら全称命題の具体化である。たとえば $f : \tPi{n}{\Nat}{n + 0 = n}$ なら $f\;3 : 3 + 0 = 3$ である（自然数は第 7 章で登場する）。

T-Conv。 計算を除いて等しい型は交換可能であり、$h : \mathit{Id}\;P$ から $h : P$ を結論してよい。前提 $\Gamma \vdash B : \Sort{u}$ は、新しい型がそれ自体型であることを保証する。これは、使うかどうかが $t$ の形から決まらない唯一の規則であり、この事実は第 5 章のアルゴリズムで効いてくる。

適用が重要な理由

何かを組み立てる T-Lam や T-Pi のほうが重要に見えるかもしれないが、T-App がなければ、証明は仮定を返せても使うことはできない。おおまかに言えば、証明できるのは $P \to Q \to P$ のように、結論が仮定の一つそのものである命題だけになる。合成

の証明は $\tLam{f}{P \to Q}{\tLam{g}{Q \to R}{\tLam{p}{P}{g\,(f\,p)}}}$ で、$f$ を適用してから $g$ を適用する。仮定を言い直す以上のことをする証明はすべて T-App を通る。そして依存型理論では、T-App は代入が起きる場所でもあり、したがって微妙な点の大半が潜む場所でもある。

はじめての導出

導出とは、規則の実例からなる木で、その根が立証したい判断であるものをいう。$\tLam{P}{\Sort{0}}{\tLam{h}{P}{h}}$ が $\tPi{P}{\Sort{0}}{P \to P}$ を証明する導出を示す。$\Gamma_1 = P : \Sort{0}$、$\Gamma_2 = \Gamma_1, h : P$ と書き、整形式性の前提 $\ctxok{\Gamma}$ は定型なので省く。

カーネルが組み立てるのはこの木であり、下の表示では各節点が規則の一回の適用で、それが立証する判断を伴う。呼び出しビューに切り替えると、この木を生み出す再帰として上から下へ読める。項を自分のものに置き換えて、どの規則が発火するか見てみてほしい。

二つ観察しておく。第一に、木の形は項の形に従い、根に $\lambda$、その下に $\lambda$、葉に変数である。第二に、根の型は $\tPi{P}{\Sort{0}}{\tPi{h}{P}{P}}$ だが、述べた命題は $\tPi{P}{\Sort{0}}{P \to P}$ だった。両者は束縛変数の名前（$h$ か、矢印の無名の _ か）だけが異なるので α 同値であり、T-Conv がその隙間を埋める。第 6 章でこの例をアルゴリズムで再訪する。

演習