h5i

第 4 章

論理としての型付け規則

第 3 章では、8 つの型付け規則を論理の規則として紹介した。本章ではその意味を明確にするため、具体的な論理を一つ選んで論理式を型へ翻訳し、その論理におけるすべての証明がカーネルの受理する項になることを示す。さらに、カーネルを信頼するには整合性も必要であることを説明する。

比較対象となる論理

この論理の論理式は、命題変数 P,Q,…P, Q, \ldots から含意と命題の上の量化によって作られる。

φ,ψ  ::=  P  ∣  φ→ψ  ∣  ∀P. φ\varphi, \psi \;::=\; P \;\mid\; \varphi \to \psi \;\mid\; \forall P.\,\varphi

これは二階命題論理（second-order propositional logic）であり、「二階」というのは ∀\forall が個体ではなく命題の上を動くからである。小さいが決して自明ではなく、連言、選言、否定、矛盾はすべてこの中で定義できる。たとえば ⊥=∀P. P\bot = \forall P.\,P や φ∧ψ=∀R. (φ→ψ→R)→R\varphi \wedge \psi = \forall R.\,(\varphi \to \psi \to R) \to R である。

この論理の証明は、判断 Δ⊢φ\Delta \vdash \varphi の自然演繹による導出であり、ここで Δ\Delta は仮定のリストである。規則は下の図 4.1 の左列にあるもの、すなわち仮定を使う、含意の導入と除去、量化子の導入と除去である。

論理式を型へ翻訳する

各論理式は型へ翻訳され、それを φ∗\varphi^\ast と書く。

P∗=P,(φ→ψ)∗=φ∗→ψ∗,(∀P. φ)∗=Π(P:Sort 0). φ∗.P^\ast = P, \qquad (\varphi \to \psi)^\ast = \varphi^\ast \to \psi^\ast, \qquad (\forall P.\,\varphi)^\ast = \tPi{P}{\Sort{0}}{\varphi^\ast}.

命題変数は型変数に、含意は関数型に、命題の上の量化は Sort 0\Sort{0} の上の Π\Pi 型になる。

仮定のリストは文脈へ翻訳されるが、仮定ごとの仮定 hi:φi∗h_i : \varphi_i^\ast に加えて、文脈は判断のどこかに現れる命題変数を宣言しなければならない。

(φ1,…,φn)∗  =  P1:Sort 0,…,Pk:Sort 0,  h1:φ1∗,…,hn:φn∗,(\varphi_1, \ldots, \varphi_n)^\ast \;=\; P_1 : \Sort{0}, \ldots, P_k : \Sort{0},\; h_1 : \varphi_1^\ast, \ldots, h_n : \varphi_n^\ast,

ここで P1,…,PkP_1, \ldots, P_k は、翻訳する判断 Δ⊢φ\Delta \vdash \varphi の Δ\Delta または結論 φ\varphi に自由に現れる命題変数であり、h1,…,hnh_1, \ldots, h_n は新鮮な名前である。結論を含めなければならないのは、⋅⊢P→P\cdot \vdash P \to P における PP のように、変数が結論だけに現れることがあるからである。

図 4.1 では、各論理規則の隣に、それを実装する型付け規則を並べるが、型が整形式であることを確かめるだけの前提は省いてある。

図 4.1. 自然演繹（中央列）とそれを実装する型付け規則（右列）。各行で Δ∗\Delta^\ast は結論に対する文脈である。

Hypothesisφi∈ΔΔ⊢φi(hi:φi∗)∈Δ∗Δ∗⊢hi:φi∗;(T-Var)→-introΔ,φ⊢ψΔ⊢φ→ψΔ∗,h:φ∗⊢t:ψ∗Δ∗⊢λ(h:φ∗). t:φ∗→ψ∗;(T-Lam)→-elimΔ⊢φ→ψΔ⊢φΔ⊢ψΔ∗⊢f:φ∗→ψ∗Δ∗⊢a:φ∗Δ∗⊢f  a:ψ∗;(T-App)∀-introΔ⊢φP∉FV(Δ)Δ⊢∀P. φΔ∗,P:Sort 0⊢t:φ∗Δ∗⊢λ(P:Sort 0). t:Π(P:Sort 0). φ∗;(T-Lam)∀-elimΔ⊢∀P. φΔ⊢φ[P↦ψ]Δ∗⊢f:Π(P:Sort 0). φ∗Δ∗⊢ψ∗:Sort 0Δ∗⊢f  ψ∗:φ∗[P↦ψ∗];(T-App)\begin{array}{lcc} \text{Hypothesis} & \dfrac{\varphi_i \in \Delta}{\Delta \vdash \varphi_i} & \dfrac{(h_i : \varphi_i^\ast) \in \Delta^\ast}{\Delta^\ast \vdash h_i : \varphi_i^\ast}\rulename{T-Var} \\[18pt] \to\text{-intro} & \dfrac{\Delta, \varphi \vdash \psi}{\Delta \vdash \varphi \to \psi} & \dfrac{\Delta^\ast, h : \varphi^\ast \vdash t : \psi^\ast}{\Delta^\ast \vdash \tLam{h}{\varphi^\ast}{t} : \varphi^\ast \to \psi^\ast}\rulename{T-Lam} \\[18pt] \to\text{-elim} & \dfrac{\Delta \vdash \varphi \to \psi \qquad \Delta \vdash \varphi}{\Delta \vdash \psi} & \dfrac{\Delta^\ast \vdash f : \varphi^\ast \to \psi^\ast \qquad \Delta^\ast \vdash a : \varphi^\ast}{\Delta^\ast \vdash f\;a : \psi^\ast}\rulename{T-App} \\[18pt] \forall\text{-intro} & \dfrac{\Delta \vdash \varphi \qquad P \notin \FV(\Delta)}{\Delta \vdash \forall P.\,\varphi} & \dfrac{\Delta^\ast, P : \Sort{0} \vdash t : \varphi^\ast}{\Delta^\ast \vdash \tLam{P}{\Sort{0}}{t} : \tPi{P}{\Sort{0}}{\varphi^\ast}}\rulename{T-Lam} \\[18pt] \forall\text{-elim} & \dfrac{\Delta \vdash \forall P.\,\varphi}{\Delta \vdash \subst{\varphi}{P}{\psi}} & \dfrac{\Delta^\ast \vdash f : \tPi{P}{\Sort{0}}{\varphi^\ast} \qquad \Delta^\ast \vdash \psi^\ast : \Sort{0}}{\Delta^\ast \vdash f\;\psi^\ast : \subst{\varphi^\ast}{P}{\psi^\ast}}\rulename{T-App} \end{array}

右列から項を消すと、ちょうど中央列になる。二つの細部に注釈が要る。

∀\forall-intro の行では、論理側の側条件 P∉FV(Δ)P \notin \FV(\Delta) が、どの仮定も PP に言及しないことを保証するので、型付け規則は、文脈の依存順序を壊すことなく、仮定の後に P:Sort 0P : \Sort{0} を加えてよい。

∀\forall-elim の行では、T-Pi が翻訳されたどの論理式も Sort 0\Sort{0} に置くので、前提 ψ∗:Sort 0\psi^\ast : \Sort{0} は、∀\forall を含むものも含めてすべての論理式 ψ\psi について成り立つ。（T-Pi の imax\imax がその理由であり、Π(P:Sort 0). φ∗\tPi{P}{\Sort{0}}{\varphi^\ast} は Sort imax(1,0)=Sort 0\Sort{\imax(1, 0)} = \Sort{0} に落ち着く。）したがって全称命題は、論理の場合と同じく任意の論理式で具体化できる。この点は非述語性（impredicativity）と呼ばれ、第 13 章で再び取り上げる。

証明は項である

定理 4.1（証明は項である）。 Δ⊢φ\Delta \vdash \varphi が論理で証明可能なら、ある項 tt について Δ∗⊢t:φ∗\Delta^\ast \vdash t : \varphi^\ast が成り立つ。

図 4.1 は論理の証明の各ステップを型付け導出のステップに変えるので、証明に関する帰納法により、すべての証明が項になる。付録 Aでは命題変数のスコープを明示した形で定理を述べ、完全な証明を与える。

この定理は型検査器が論理のすべての証明を検査できると言っているが、カーネルが信頼に値するためには逆向きの保証も要り、論理が反駁する命題に対する項を受理してはならない。

整合性

⊥=∀P. P\bot = \forall P.\,P、「すべてが成り立つ」と定義する。論理には ⊥\bot の証明が存在しない。各命題変数を真か偽と読むと、どの読み方のもとでもすべての規則は真を保つが、∀P. P\forall P.\,P はある PP を偽にする読み方のもとで偽になるからである。

型理論もこれに合致すべきで、次の型を持つ閉じた項があってはならない。

⊥∗  =  Π(P:Sort 0). P.\bot^\ast \;=\; \tPi{P}{\Sort{0}}{P}.

この型の閉じた項 tt があれば大惨事で、すべての命題 C:Sort 0C : \Sort{0} について適用 t  Ct\;C が型 CC を持つことになり、あらゆる命題が証明可能になって、カーネルは無価値になる。

定義 4.2（整合性）。 型システムが整合的（consistent）であるとは、型 Π(P:Sort 0). P\tPi{P}{\Sort{0}}{P} を持つ閉じた項が存在しないことをいう。

整合性は、本書のあらゆる設計判断が保たなければならない性質である。とくに宇宙の設計は、システムが整合的であり続ける場合にのみ受け入れられる。第 13 章ではこの試験に落ちる、一見自然な設計を示し、第 14 章では本書のシステムの整合性を定理 14.5 として述べる。

演習

論理式 ∀P. ∀Q. (P→Q)→P→Q\forall P.\,\forall Q.\,(P \to Q) \to P \to Q を型へ翻訳し、自然演繹の証明「P→QP \to Q と PP を仮定し、前者を後者に適用する」に対して図 4.1 が生む証明項を書け。

解答

型は Π(P:Sort 0). Π(Q:Sort 0). (P→Q)→P→Q\tPi{P}{\Sort{0}}{\tPi{Q}{\Sort{0}}{(P \to Q) \to P \to Q}} である。二回の ∀\forall-intro が Sort 0\Sort{0} 上の外側の λ\lambda を二つ、二回の →\to-intro が λ(f:P→Q)\lambda(f : P \to Q) と λ(p:P)\lambda(p : P) を与え、→\to-elim が本体 f  pf\;p を与える。 λ(P:Sort 0). λ(Q:Sort 0). λ(f:P→Q). λ(p:P). f  p\tLam{P}{\Sort{0}}{\tLam{Q}{\Sort{0}}{\tLam{f}{P \to Q}{\tLam{p}{P}{f\;p}}}}。

t:Π(P:Sort 0). Pt : \tPi{P}{\Sort{0}}{P} から、型 Π(P:Sort 0). Π(Q:Sort 0). P→Q\tPi{P}{\Sort{0}}{\tPi{Q}{\Sort{0}}{P \to Q}}、「すべての命題は他のすべての命題を含意する」の項を組み立てられることを示せ。

解答

λ(P:Sort 0). λ(Q:Sort 0). λ(p:P). t  Q\tLam{P}{\Sort{0}}{\tLam{Q}{\Sort{0}}{\tLam{p}{P}{t\;Q}}} である。仮定 pp は無視され、T-App により t  Q:Qt\;Q : Q である。⊥∗\bot^\ast の証明があらゆるものを証明するというのは、この意味においてである。

覚えておくこと

  • 二階命題論理は型理論へ翻訳される。→\to は関数型に、∀P\forall P は Π(P:Sort 0)\Pi(P : \Sort{0}) に、仮定は文脈の項目になる。
  • 定理 4.1: 論理のすべての証明は、型の付く項になる。翻訳は規則ごとに対応する（図 4.1）。
  • カーネルが信頼に値するのは整合的である場合、つまり型 Π(P:Sort 0). P\tPi{P}{\Sort{0}}{P} の閉じた項が存在しない場合だけである。
  • 全称命題を任意の論理式で、それ自身によってさえ、具体化できるのは imax\imax による非述語性のおかげである。
前の章型付け規則次の章型検査アルゴリズム