実例で追う

定理 $T$ の証明 $t$ を検証するために、カーネルは $\Check(\cdot, t, T)$ を呼び、これが $\Infer(\cdot, t)$ を呼んでその結果を $T$ と比較する。トレースには、$\Infer$ が行う再帰呼び出しと、各呼び出しが対応する型付け規則を示す。ノードを開いたり閉じたりして、再帰を追ってほしい。

恒等証明

$\Gamma_1 = P : \Sort{0}$、$\Gamma_2 = \Gamma_1, h : P$ とおく。第 1 章 の冒頭の例の導出は、整形式性の前提を省くと次のようになる。

アルゴリズムは、同じ導出を下から上へ組み立てる。呼び出し $\Infer(\cdot, \tLam{P}{\Sort{0}}{\tLam{h}{P}{h}})$ は次のように進む。

• $\Infer(\cdot,\; \tLam{P}{\Sort{0}}{\tLam{h}{P}{h}})$ T-Lam
  • $\InferSort(\cdot,\; \Sort{0})$: $\Infer$ が $\Sort{1}$ を返すので、注釈は型である T-Sort
  • 文脈が空なので、$\Freshen$ は $P$ をそのままにする
  • $\Infer(\Gamma_1,\; \tLam{h}{P}{h})$ T-Lam
    • $\InferSort(\Gamma_1,\; P)$: $\Infer$ が $P$ を引いて $\Sort{0}$ を返す T-Var
    • $\Freshen$ は $h$ をそのままにする
    • $\Infer(\Gamma_2,\; h)$ は $h$ を引いて $P$ を返す T-Var
    • $\tPi{h}{P}{P}$ を返す
  • $\tPi{P}{\Sort{0}}{\tPi{h}{P}{P}}$ を返す

型を返す各呼び出しは、導出木の一つのノードに対応し、計算を使う呼び出しは一つもない。最後に $\Check$ が、結果を宣言された型 $\tPi{P}{\Sort{0}}{P \to P}$ と比較する。$P \to P$ は $\tPi{\_}{P}{P}$ の略記であり、$h$ も $\_$ も本体には現れないので、両者の違いは束縛変数一つの名前だけである。したがって $\IsDefEq$ は成功し、証明は受理される。

同じ実行を、カーネル自身に記録させたものが次であり、呼び出しビューは上のリストと、証明木ビューは導出と一致する。

# 同じ証明を、完全な項として与える。カーネルはその型を推論し、
# ゴールと比較する。
goal forall (P : Sort 0), P -> P
exact fun (P : Sort 0) => fun (h : P) => h
qed

誤った証明

利用者が、$t = \tLam{P}{\Sort{0}}{\tLam{h}{P}{P}}$ は $\tPi{P}{\Sort{0}}{P \to P}$ を証明すると主張したとしよう。本体は証明 $h$ ではなく命題 $P$ を返している。カーネルは $\Check(\cdot, t, \tPi{P}{\Sort{0}}{P \to P})$ を呼び、まず $\Infer$ が走る。呼び出しは上と同じだが、最後の $\Infer(\Gamma_2, P)$ だけが $\Sort{0}$ を返す。つまり $\Infer$ は成功し、結果は

となる。項 $t$ は正しく型付けされるが、主張された命題の証明にはなっていない。$\Check$ が二つの型を比較しても、どちらもこれ以上計算できず、いちばん内側の本体が片方では $\Sort{0}$、もう片方では $P$ なので、束縛変数を改名しても一致しない。そのため $\IsDefEq$ は失敗し、$\Check$ は型の不一致を報告する。（第 11 章 では、$\IsDefEq$ が使うアルゴリズムでこの比較を一歩ずつ再現する。）

この誤りが見つかったのは、利用者が証明すべき命題を宣言したからにほかならない。$\Infer$ だけを走らせるカーネルなら、$t$ を受理し、黙って別の型を割り当てていただろう。どのスクリプトでも goal が先頭に来るのはこのためであり、qed がそれと照合するのもこのためである。

goal forall (P : Sort 0), P -> P
exact fun (P : Sort 0) => fun (h : P) => P
qed

仮定を使う: モーダス・ポネンス

ここまでの例では関数を一度も適用していないので、次の検査を考えよう。

この型は「$P$ ならば $Q$ であり、$P$ が成り立つなら、$Q$ が成り立つ」と述べている。四つの $\lambda$ が、これまでと同じように文脈を $\Gamma = P : \Sort{0},\; Q : \Sort{0},\; f : P \to Q,\; p : P$ まで拡張し、本体 $f\;p$ は $\Infer$ の適用のケースに達する。

• $\Infer(\Gamma,\; f\;p)$ T-App
  • $\Infer(\Gamma,\; f)$ は $P \to Q$、すなわち $\tPi{\_}{P}{Q}$ を返す。$\Whnf$ はこれを変えず、これは $\Pi$ である T-Var
  • $\Check(\Gamma,\; p,\; P)$ は成功する。$p : P$ が $\Gamma$ にあるからである T-Var, T-Conv
  • $\subst{Q}{\_}{p} = Q$ を返す。名前 $\_$ は $Q$ に現れないので、代入は何もしない

利用者が代わりに $f\;f$ と書いていたら、二つ目のステップで $\Check(\Gamma, f, P)$ が呼ばれ、$P \to Q$ は $P$ ではないので失敗する。ここでは関数を自分自身に食わせることはできない。下で f p を f f に変えて試してほしい。

goal forall (P : Sort 0), forall (Q : Sort 0), (P -> Q) -> P -> Q
exact fun (P : Sort 0) => fun (Q : Sort 0) => fun (f : P -> Q) => fun (p : P) => f p
qed

全称命題の具体化

依存的な適用では、T-App の代入が実質的な仕事をする。最初の例の証明を $\mathit{id} = \tLam{P}{\Sort{0}}{\tLam{h}{P}{h}}$ とし、$\Gamma = Q : \Sort{0}$ とする。このとき $\Infer(\Gamma, \mathit{id}\;Q)$ は次のようになる。

• $\Infer(\Gamma,\; \mathit{id}\;Q)$ T-App
  • $\Infer(\Gamma,\; \mathit{id})$ は $\tPi{P}{\Sort{0}}{\tPi{h}{P}{P}}$ を返す。すでに $\Pi$ である T-Lam
  • $\Check(\Gamma,\; Q,\; \Sort{0})$ は成功する T-Var
  • $\subst{(\tPi{h}{P}{P})}{P}{Q} = \tPi{h}{Q}{Q}$、すなわち $Q \to Q$ を返す

論理的には、これは $\forall$ 除去であり、「どの命題も自分自身を含意する」から「$Q$ は $Q$ を含意する」を得ている。結果の型は引数 $Q$ の値に依存し、依存 $\Pi$ 型が表しているのはまさにこのことで、T-App が代入を行う理由でもある。エクスプローラでは、$\mathit{id}$ は定義された定数で、$Q$ は文脈から来る。T-App ノードの注記に代入が記録される。

def id : forall (P : Sort 0), P -> P := fun (P : Sort 0) => fun (h : P) => h

変換

第 3 章 の $\mathit{Id} = \tLam{X}{\Sort{0}}{X}$ を思い出そう。核となる体系には定義がないので、$\mathit{Id}\;P$ は項 $(\tLam{X}{\Sort{0}}{X})\;P$ の略記である。次の検査を考える。

$\Infer$ はまず、注釈 $\mathit{Id}\;P$ が型であることを確かめ、$\InferSort(\Gamma_1, \mathit{Id}\;P)$ は $\Infer$ の適用のケースに達する。関数 $\tLam{X}{\Sort{0}}{X}$ の型は $\tPi{X}{\Sort{0}}{\Sort{0}}$ で、引数 $P$ は $\Check(\Gamma_1, P, \Sort{0})$ を通り、結果は $\subst{\Sort{0}}{X}{P} = \Sort{0}$ である。したがって $\mathit{Id}\;P$ は型であり、しかも命題である。本体 $h$ の型は $\mathit{Id}\;P$ なので、

となる。束縛変数を改名するだけでは、これは $\tPi{P}{\Sort{0}}{P \to P}$ にならないが、$\IsDefEq$ は比較の前に両辺を計算する。$\mathit{Id}\;P \betared P$ なので、推論された型は $\tPi{P}{\Sort{0}}{\tPi{h}{P}{P}}$ になり、最初の例と同じく比較は成功する。型付け規則で言えば、このステップは導出の根における T-Conv の一回の使用である。

アルゴリズムは、T-Conv をどこで適用するかを決して決めない。第 5 章 で述べたとおり、変換は $\IsDefEq$ の呼び出しの中に隠れており、二つの型が比較される場所でしか走らない。

ライブの導出を見ると、計算がどこで起きるかが分かる。注釈 $\mathit{Id}\;P$ は T-App で検査され、推論された型には、$\Check$ がゴールと比較するまで $\mathit{Id}\;P$ が残ったままである。

# h の注釈は (fun (X : Sort 0) => X) P であり、P に計算される。
goal forall (P : Sort 0), P -> P
exact fun (P : Sort 0) => fun (h : (fun (X : Sort 0) => X) P) => h
qed

演習

上の例のように $\Infer$ を手で走らせてみると、アルゴリズムの理解を確かめるよい練習になり、どれもプレイグラウンドで試せる。

goal forall (P : Sort 0), forall (Q : Sort 0), forall (R : Sort 0), (P -> Q) -> (Q -> R) -> P -> R
exact fun (P : Sort 0) => fun (Q : Sort 0) => fun (R : Sort 0) => fun (f : P -> Q) => fun (g : Q -> R) => fun (p : P) => g (f p)
qed