体系の性質

核となるシステム

以下の定理が扱うのは核となるシステム、すなわち図 3.1 の規則に第 13 章の宇宙を加え、第 II 部の定数を除いたものである。これは Barendregt の意味での純粋型システム（Pure Type System）であり、Calculus of Constructions [Coquand 1988] の非述語的な $\Sort{0}$ の上に述語的な宇宙の階層を載せたもので、Luo の Extended Calculus of Constructions [Luo 1990] に近い。最初の三つの性質は、関数的な純粋型システムすべてで成り立つ [Barendregt 1992] が、強正規化は非述語性があるとはるかに難しくなり、Girard の可約性候補（reducibility candidates）の方法を必要とする [Girard 1972; Coquand 1988; Luo 1990]。帰納型を加えると何が変わるかは章末で述べる。

四つの性質

項の型は、変換を除いて一つに定まる。$\Infer$ はこれに依存しており、計算すべき答えが一つしかないからこそ、$\Check$ は、別の導出なら変換不可能な別の型を与えていたのではないかと心配せずに、その答えと比較できる。

正しく型付けされた項の型は、それ自身が型である（あるいは宇宙である。宇宙は T-Sort により型を持つが、型として書き下す必要はない）ので、$\Infer$ の結果はつねに $\InferSort$ に渡し直せるし、アルゴリズムが構築する文脈は整形式のままである。

計算は型を保存する。これが T-Conv を正当化し、正規化によって等しさを決定するという戦略全体を正当化する。項を簡約してもその型から外れることはないので、正規形どうしの比較は、比較すべきものを正しく比較している。

正しく型付けされた項は、どの順序で簡約しても正規形に到達する。これが最も深い定理である。$\Whnf$ と $\Normalize$、したがって $\IsDefEq$ と $\Infer$ が正しく型付けされた入力に対して停止するのはこの定理のおかげであり、次節で見るように整合性もこの定理に支えられている。

四つの性質が二つの保証を支える構図は決まっており、下図に描いた。矢印は「〜に必要である」と読む。

これらを合わせると、カーネルに求める二つの保証が得られる。

• 決定可能性。 アルゴリズム 5.1 はどんな入力に対しても停止するので、証明が正しいかどうかはつねに判定できる。
• 整合性。 False を証明する閉じた項は存在しない。

整合性

論証は二つの半分からなり、細部を見なくてもその形はわかる。

正規形に帰着する。 強正規化により、そのような項 $t$ は正規形 $n$ を持ち、型保存性により $n$ は同じ型を持つ。したがって、型 $\tPi{P}{\Sort{0}}{P}$ を持つ正規な閉じた項が存在しないことを示せば十分である。定理 14.4 を使うので、難しさはすべてこのステップにある。

正規形を解析する。 正規な項は、宇宙、$\Pi$、$\lambda$、または変数にいくつかの引数を適用したもの（中立項（neutral term））のいずれかである。スコープ内に変数がないので中立項ではありえず、宇宙と $\Pi$ 型の型は宇宙であって $\Pi$ ではないので、型が $\Pi$ であるような閉じた正規項は $\lambda$ でなければならない。よって $n = \tLam{P}{\Sort{0}}{s}$ であり、$P : \Sort{0} \vdash s : P$ かつ $s$ は正規である。では $s$ は何でありうるか。宇宙、$\Pi$、$\lambda$ であれば、その型は宇宙か $\Pi$ であって、変数 $P$ ではない。中立項であればスコープ内の変数から始まらなければならないが、そのような変数は $P$ 自身しかなく、その型は $\Sort{0}$ であり、これは $P$ ではないので $s$ は $P$ ではありえず、関数型でもないので $P$ に何かを適用することもできない。どの場合も不可能である。

付録 D はこれを、場合分けが暗黙に使っている、型付けと変換についての標準的な事実（生成（generation）、合流性、代入）も含めて丁寧に実行する。

帰納型がある場合

第 II 部の ι 規則は互いに重ならず、β とも重ならないので、簡約は合流的なままである。型保存性、強正規化、整合性は Calculus of Inductive Constructions について知られており [Werner 1994]、帰納型を加えた我々のシステムはその小さな断片である。上で述べた短い整合性の論証は、正規形に、$n$ が変数であるような $\NatRec{0}\;M\;z\;s\;n$ といった行き詰まった再帰子の適用が含まれるようになるので、それだけではもう十分ではない。整合性は、中立項が定数を頭部に持つ場合も含めた、より注意深い正規形の解析によって、強正規化から導かれる。

第 8 章の受理条件は、それぞれこの解析が破綻しうる一つの経路に対応する。正値性がなければ ι 簡約がループしうるので、強正規化が失われる。宇宙条件がなければ、型が自分自身の宇宙を含みうるので、第 13 章のパラドックスが戻ってくる。命題に対する消去の制限がなければ、証明無関係性（proof irrelevance。Lean が仮定するもの）が反証されてしまう。

Lean の完全な理論は、定義的な証明無関係性、宇宙多相、商型、一般の入れ子帰納型と相互帰納型を備えており、そのメタ理論はより微妙で、参照先は Carneiro の学位論文 [Carneiro 2019] である。それでも中心となる構造、すなわち強正規化と正規形の解析の組み合わせは同じである。

演習