# 単純型付きラムダ計算とカリー＝ハワード対応：証明はプログラムである

> 単純型付きラムダ計算の主部簡約定理と、テイトの還元可能性による強正規化定理を証明する。直観主義の自然演繹の証明と型付き λ 項が一対一に対応し、β 簡約が証明の回り道の除去になることを示し、BHK 解釈と Lean のコードで読み解く。
> https://rikai.mugen-giken.com/mathematics/logic-and-type-theory/simple-types-curry-howard

## 0. この記事の要点

プログラムの関数に「整数を受け取って整数を返す」といった型を付けると、型の合わない呼び出しは最初から排除されます。この記事は、そうした型の付いた関数だけからなる小さな計算体系を調べ、型の付いた関数の計算は必ず終わること、そして型の付いた関数が数学の証明とまったく同じ形をしていることを示します。読み終えると、Lean で定理を書くことがなぜプログラムを書くことなのかを説明できるようになります。

- **単純型付きラムダ計算**（STLC）は、[λ 項](/mathematics/logic-and-type-theory/lambda-calculus#def-lambda-term)に「型」$A\to B$ を付け、型の合う適用だけを許す体系です。型付けは簡約で保たれ（**主部簡約定理**、<Ref to="thm-subject-reduction" />）、型の付く項は**どの順に簡約しても必ず止まります**（**強正規化定理**、<Ref to="thm-strong-normalization" />）。後者はテイトの還元可能性の方法で証明します。
- **カリー＝ハワード対応**（<Ref to="thm-curry-howard" />）：型 $A\to B$ を命題「$A$ ならば $B$」と読むと、型 $A$ の項は直観主義の自然演繹（仮定から決まった規則で結論を導く形の証明体系）における $A$ の証明と一対一に対応し、[β 簡約](/mathematics/logic-and-type-theory/lambda-calculus#def-beta)は証明の「回り道の除去」に対応します。
- この対応から、強正規化定理は「すべての証明は回り道のない正規な証明に直せる」という定理になり、そこから論理の無矛盾性や、パースの法則 $((p\to q)\to p)\to p$ が直観主義論理で証明できないことが導けます。
- **BHK 解釈**は「$A\to B$ の証明とは、$A$ の証明を $B$ の証明に変える方法である」という証明の意味論で、カリー＝ハワード対応はその精密化です。排中律がここに含まれない理由もこの観点から説明できます。
- Lean で `theorem` を書くことは、この対応のもとでプログラムを書くことにほかなりません。記事中の Lean 4 のコードは、標準ライブラリだけで動作を確認したものです。

<Aside type="tip" title="この記事で使う事前知識">

- **λ 項**: 関数を $\lambda x.M$ の形で書き、$MN$ で適用する式。→ [λ 項](/mathematics/logic-and-type-theory/lambda-calculus#def-lambda-term)
- **β 簡約**: $(\lambda x.M)N$ を、$M$ の中の $x$ に $N$ を代入した式に書き換える計算の 1 ステップ。→ [β 簡約](/mathematics/logic-and-type-theory/lambda-calculus#def-beta)
- **置換**: 式の中の変数を別の式で置き換える操作 $M[x:=N]$。→ [置換](/mathematics/logic-and-type-theory/lambda-calculus#def-substitution)
- **数学的帰納法**: 自然数や、式の構成のような段階的に作られるものについて、一段ずつ性質を確かめて全体に広げる証明法。→ [証明の技術](/mathematics/foundations/proof-techniques)

</Aside>

## 1. 動機：証明とプログラムが同じものだったら

### 1.1. 二つの見慣れた作業

数学の証明を書くことと、プログラムを書くことは、ふつう別の作業だと考えられています。けれども、次の二つを並べてみてください。

- **命題**「$A$ ならば（$B$ ならば $A$）」の証明。「$A$ を仮定する。さらに $B$ を仮定する。最初の仮定から $A$。」
- **プログラム**「$a$ を受け取り、$b$ を受け取って、$a$ を返す関数」。λ 記法で $\lambda a.\lambda b.\,a$。

証明は「仮定を受け取って結論を作る手続き」になっていて、プログラムはまさにその手続きです。もう一つ、三段論法（モーダス・ポネンス）「$A\to B$ と $A$ から $B$」は、「関数 $f:A\to B$ に引数 $a:A$ を適用すると $f\,a:B$」とそっくりです。

この類似は偶然ではありません。**命題を型と読み、証明をその型のプログラムと読む**と、論理の規則と型付けの規則が完全に一致するのです。カリー (1934, 1958) が組合せ論理（変数を使わず、K や S といった少数の記号だけで関数を表す体系）で気づき、ハワード (1969) が自然演繹と λ 計算の対応として定式化しました。これが**カリー＝ハワード対応**で、この記事の主題です。

### 1.2. Lean では実際にそう書く

証明支援系 Lean は、この対応をそのまま実装しています。次の Lean 4 のコードはどれも、標準ライブラリだけでそのまま通ります。

```lean
theorem k_comb (A B : Prop) : A → B → A := fun a _ => a

theorem s_comb (A B C : Prop) : (A → B → C) → (A → B) → A → C :=
  fun f g a => f a (g a)

theorem k_tac (A B : Prop) : A → B → A := by
  intro a _
  exact a
#print k_tac   -- theorem k_tac : ∀ (A B : Prop), A → B → A := fun A B a a_1 => a
```

`theorem` の `:` の後ろが命題（型）、`:=` の後ろが証明（項）です。`fun a _ => a` は前章の λ 項 $\lambda a.\lambda b.\,a$ に型を付けたもので、`_` は使わない引数の名前です。3 つ目は同じ定理を **tactic**（`by` 以下の命令列）で証明したもので、`intro` は仮定を導入し、`exact` は結論そのものの項を与えます。`#print` で中身を表示すると、tactic が組み立てたのは結局 `fun A B a a_1 => a` という λ 項だと分かります。Lean のカーネルが確認しているのは、「この項がこの型をもつか」という型検査だけです。

### 1.3. なぜ型が要るのか

前章の型なしラムダ計算では、どんな項にも不動点がありました。論理として読むと、「$X$ は $X$ の否定に等しい」という文が作れてしまい、矛盾します（[型なしラムダ計算](/mathematics/logic-and-type-theory/lambda-calculus) の <Ref to="mathematics/logic-and-type-theory/lambda-calculus#rem-untyped-inconsistency" />）。型はこの自己適用 $xx$ を禁止します。その代償として計算能力は落ちますが、代わりに**すべての計算が止まる**という強い性質が得られます。論理として使うにはこの性質こそが必要で、それが無矛盾性の源になります。

## 2. 単純型付きラムダ計算

### 2.1. 型と型付け規則

<Definition id="def-stlc" title="単純型付きラムダ計算">
**型**を、基本型 $o_1,o_2,\ldots$ から $A\to B$ で作られるものとする（$\to$ は右結合）。**項**は型なしの λ 項と同じだが、抽象に束縛変数の型を書いて $\lambda x{:}A.M$ とする。**文脈** $\Gamma$ は変数と型の組 $x_1{:}A_1,\ldots,x_n{:}A_n$ の有限列（変数は相異なる）で、**型付け判断** $\Gamma\vdash M:A$ を次の 3 規則で帰納的に定める。

$$
\frac{(x{:}A)\in\Gamma}{\Gamma\vdash x:A}\ (\mathrm{var})\qquad
\frac{\Gamma,x{:}A\vdash M:B}{\Gamma\vdash\lambda x{:}A.M:A\to B}\ (\mathrm{abs})\qquad
\frac{\Gamma\vdash M:A\to B\quad\Gamma\vdash N:A}{\Gamma\vdash MN:B}\ (\mathrm{app})
$$

β 簡約 $(\lambda x{:}A.M)N\to_\beta M[x:=N]$ と置換は型なしの場合と同じに定める。
</Definition>

規則は項の形で決まります。変数なら (var)、抽象なら (abs)、適用なら (app) しか使えません。したがって次が成り立ちます。

<Lemma id="lem-generation" title="生成補題と型の一意性">
(1) $\Gamma\vdash x:A$ ならば $(x{:}A)\in\Gamma$。$\Gamma\vdash\lambda x{:}A.M:C$ ならば、ある $B$ について $C\equiv A\to B$ かつ $\Gamma,x{:}A\vdash M:B$。$\Gamma\vdash MN:B$ ならば、ある $A$ について $\Gamma\vdash M:A\to B$ かつ $\Gamma\vdash N:A$。

(2) $\Gamma\vdash M:A$ かつ $\Gamma\vdash M:A'$ ならば $A\equiv A'$。また、$\Gamma\vdash M:A$ の導出はただ一つである。
</Lemma>

<Proof of="lem-generation">
(1) 項の形ごとに、最後に使える規則が一つしかないことから従う。(2) $M$ の構成に関する帰納法。変数は $\Gamma$ の中の型が一つ。抽象 $\lambda x{:}A.M$ は (1) と帰納法の仮定で $A\to B$ が一意。適用 $MN$ は、帰納法の仮定により $M$ の型 $A\to B$ が一意なので $B$ も一意。導出の一意性も同じ帰納法で、各段の規則とその前提が項から決まることによる。
</Proof>

<Example id="ex-self-application" title="自己適用には型が付かない">
$x$ にどんな型 $A$ を与えても $xx$ には型が付きません。$\Gamma\vdash xx:B$ とすると、(1) から $x$ は $A\to B$ と $A$ の両方の型をもち、型の一意性から $A\equiv A\to B$。ところが右辺の型は左辺より真に長い記号列なので、これは不可能です。こうして $\omega\equiv\lambda x.xx$ や不動点結合子 $Y$ は締め出されます。
</Example>

### 2.2. 主部簡約定理

<Lemma id="lem-typing-subst" title="弱化と置換">
(1)（弱化）$\Gamma\vdash M:B$ で $y$ が $\Gamma$ に現れないなら、$\Gamma,y{:}A\vdash M:B$。

(2)（置換）$\Gamma,x{:}A\vdash M:B$ かつ $\Gamma\vdash N:A$ ならば $\Gamma\vdash M[x:=N]:B$。
</Lemma>

<Proof of="lem-typing-subst">
(1) 導出に関する帰納法。(abs) では束縛変数を $y$ と異なるように選ぶ（変数の規約）。

(2) $M$ に関する帰納法。$M\equiv x$ なら $B\equiv A$ で $M[x:=N]\equiv N$。$M\equiv y\ne x$ なら $(y{:}B)\in\Gamma$。$M\equiv PQ$ なら <Ref to="lem-generation" /> (1) で $P:C\to B$、$Q:C$ に分け、帰納法の仮定と (app)。$M\equiv\lambda y{:}C.P$ なら $B\equiv C\to D$、$\Gamma,x{:}A,y{:}C\vdash P:D$。文脈の順序を入れ替えても導出は変わらないので $\Gamma,y{:}C,x{:}A\vdash P:D$、(1) で $\Gamma,y{:}C\vdash N:A$、帰納法の仮定で $\Gamma,y{:}C\vdash P[x:=N]:D$、(abs) で結論を得る。
</Proof>

<Theorem id="thm-subject-reduction" title="主部簡約定理">
$\Gamma\vdash M:A$ かつ $M\to_\beta M'$ ならば $\Gamma\vdash M':A$。したがって $M\twoheadrightarrow_\beta M'$ でも同じ。
</Theorem>

<Proof of="thm-subject-reduction">
$M\to_\beta M'$ の定義（<Ref to="mathematics/logic-and-type-theory/lambda-calculus#def-beta" />）に関する帰納法。β 基の縮約 $(\lambda x{:}B.P)N\to_\beta P[x:=N]$ のとき、<Ref to="lem-generation" /> (1) を 2 回使うと $\Gamma,x{:}B\vdash P:A$、$\Gamma\vdash N:B$。<Ref to="lem-typing-subst" /> (2) で $\Gamma\vdash P[x:=N]:A$。部分項の中の簡約の場合は、生成補題で型付けを分解し、帰納法の仮定を当てはめて同じ規則で組み直す。
</Proof>

「型の付いたプログラムは、実行の途中でも型が付いたまま」という意味で、型安全性の半分にあたる定理です。逆向き（簡約先に型が付けば元にも付く）は成り立ちません（演習）。

## 3. 強正規化定理

項 $M$ が**強正規化可能** (SN) であるとは、$M$ から始まる β 簡約（[定義](/mathematics/logic-and-type-theory/lambda-calculus#def-beta)）の無限列が存在しないことをいいます。前章の $\Omega$ はもちろん SN ではなく、$KI\Omega$ は正規形をもつが SN ではありません。

<Theorem id="thm-strong-normalization" title="強正規化定理">
$\Gamma\vdash M:A$ ならば、$M$ は強正規化可能である。
</Theorem>

型の大きさや項の大きさに関する素朴な帰納法は失敗します。$(\lambda x{:}A.M)N\to M[x:=N]$ では $N$ が何か所にもコピーされ、項は大きくなりうるからです。テイト (1967) のアイデアは、型ごとに「十分によい項」の集合を定め、「よい」という性質のほうを型に沿って帰納的に定義することでした。

以下、SN な項についての帰納法を使います。SN な項全体の上で、関係 $M\to_\beta M'$ には無限下降列がありません。したがって、性質 $P$ について「$M$ のすべての 1 ステップ簡約先 $M'$ で $P(M')$ ならば $P(M)$」が SN な各 $M$ で成り立てば、すべての SN な $M$ で $P(M)$ が成り立ちます（$P$ を満たさない SN な項があれば、$P$ を満たさない 1 ステップ簡約先を次々にとって無限列が得られ、矛盾）。これを **SN 帰納法**と呼びます。また、抽象でない項を**中立**と呼びます。中立な項 $M$ と任意の $N$ について、$MN$ は β 基ではありません。

次の定義がなぜ型ごとに集合を作るのかを先に述べます。基本型 $o$ の項については「止まる（SN）」ことを求めれば十分ですが、$o\to o$ のような関数の型の項には、「よい引数を渡すとよい結果を返す」という性質を求めたい。そこで「よい項」の意味を、型が大きくなるにつれて一段ずつ定めていきます。

<Definition id="def-reducible" title="還元可能な項">
各型 $A$ に対し、項の集合 $\mathrm{Red}_A$ を型の構成に関する帰納法で定める。

- 基本型 $o$ について $\mathrm{Red}_o=\{M\mid M \text{ は SN}\}$。
- $\mathrm{Red}_{A\to B}=\{M\mid \text{すべての } N\in\mathrm{Red}_A \text{ について } MN\in\mathrm{Red}_B\}$。

</Definition>

次の補題は、この定義を使いやすくする 3 つの性質です。(CR1) は還元可能なら止まること、(CR2) は簡約しても還元可能のままであること、(CR3) は「簡約先がすべてよい中立な項は、それ自身もよい」ことを述べています。証明は型に関する帰納法で、矢印型の (CR3) では引数 $N$ の簡約についての SN 帰納法が内側に入ります（外側の帰納法は型、内側は $N$ の簡約です）。

<Lemma id="lem-cr-conditions" title="還元可能性の 3 条件">
すべての型 $A$ について次が成り立つ。

- (CR1) $M\in\mathrm{Red}_A$ ならば $M$ は SN。
- (CR2) $M\in\mathrm{Red}_A$ かつ $M\to_\beta M'$ ならば $M'\in\mathrm{Red}_A$。
- (CR3) $M$ が中立で、$M$ の 1 ステップ簡約先がすべて $\mathrm{Red}_A$ に属するならば、$M\in\mathrm{Red}_A$。

とくに (CR3) から、変数はすべての $\mathrm{Red}_A$ に属する（変数は中立で、簡約先をもたない）。
</Lemma>

<Proof of="lem-cr-conditions">
型 $A$ に関する帰納法で 3 条件を同時に示す。

**$A=o$ の場合。** (CR1) は定義そのもの。(CR2) SN な項の簡約先は SN（$M'$ からの無限列は $M$ からの無限列を与える）。(CR3) $M$ からの簡約列は必ず最初に 1 ステップ簡約先を通り、そこから先は SN なので有限で止まる。

**$A=B\to C$ の場合。** $B,C$ では 3 条件が成り立つとする。

(CR1) $M\in\mathrm{Red}_{B\to C}$ とする。変数 $x$ は $B$ の (CR3) により $\mathrm{Red}_B$ に属するから、$Mx\in\mathrm{Red}_C$ で、$C$ の (CR1) により $Mx$ は SN。$M$ からの無限列 $M\to M_1\to\cdots$ があれば $Mx\to M_1x\to\cdots$ も無限列になるので、$M$ は SN。

(CR2) $N\in\mathrm{Red}_B$ について $MN\in\mathrm{Red}_C$ で $MN\to_\beta M'N$。$C$ の (CR2) で $M'N\in\mathrm{Red}_C$。よって $M'\in\mathrm{Red}_{B\to C}$。

(CR3) $M$ を中立とし、その 1 ステップ簡約先はすべて $\mathrm{Red}_{B\to C}$ に属するとする。$N\in\mathrm{Red}_B$ について $MN\in\mathrm{Red}_C$ を示せばよい。$N$ は $B$ の (CR1) により SN なので、$N$ に関する SN 帰納法を使う。$M$ が中立だから $MN$ も中立で、$MN$ の 1 ステップ簡約先は (i) $M\to M'$ による $M'N$ と (ii) $N\to N'$ による $MN'$ しかない（$MN$ 自身は β 基でない）。(i) は仮定 $M'\in\mathrm{Red}_{B\to C}$ から $M'N\in\mathrm{Red}_C$。(ii) は $B$ の (CR2) で $N'\in\mathrm{Red}_B$、SN 帰納法の仮定で $MN'\in\mathrm{Red}_C$。$C$ の (CR3) により $MN\in\mathrm{Red}_C$。
</Proof>

次の補題は、関数 $\lambda x{:}A.M$ がよいかどうかを、中身 $M$ に還元可能な項を代入した結果がよいかどうかに帰着させます。$(\lambda x{:}A.M)N$ の 1 ステップ簡約先は、$M$ の中での簡約、$N$ の中での簡約、代入の 3 通りしかないので、$M$ と $N$ の両方を同時に追う必要があり、その組で SN 帰納法を回します。

<Lemma id="lem-red-abs" title="抽象の還元可能性">
すべての $N\in\mathrm{Red}_A$ について $M[x:=N]\in\mathrm{Red}_B$ ならば、$\lambda x{:}A.M\in\mathrm{Red}_{A\to B}$。
</Lemma>

<Proof of="lem-red-abs">
$N\in\mathrm{Red}_A$ について $(\lambda x{:}A.M)N\in\mathrm{Red}_B$ を示す。変数 $x\in\mathrm{Red}_A$ を代入すると $M\equiv M[x:=x]\in\mathrm{Red}_B$ なので、(CR1) より $M$ と $N$ はともに SN である。「$M$ と $N$ は SN で、すべての $N_0\in\mathrm{Red}_A$ について $M[x:=N_0]\in\mathrm{Red}_B$ かつ $N\in\mathrm{Red}_A$」という状況で、対 $(M,N)$ に関する SN 帰納法（$M$ か $N$ の一方を 1 ステップ簡約する関係にも無限下降列はない）で示す。

$(\lambda x{:}A.M)N$ は中立なので (CR3) を使う。1 ステップ簡約先は 3 種類しかない。

- $M[x:=N]$：仮定から $\mathrm{Red}_B$ に属する。
- $(\lambda x{:}A.M')N$（$M\to M'$）：各 $N_0$ について $M[x:=N_0]\twoheadrightarrow_\beta M'[x:=N_0]$ なので (CR2) により $M'[x:=N_0]\in\mathrm{Red}_B$。$M'$ も同じ状況にあるので帰納法の仮定が使える。
- $(\lambda x{:}A.M)N'$（$N\to N'$）：(CR2) で $N'\in\mathrm{Red}_A$、帰納法の仮定が使える。

(CR3) により $(\lambda x{:}A.M)N\in\mathrm{Red}_B$。
</Proof>

2 番目の場合で、$M\to M'$ ならば $M[x:=N_0]\twoheadrightarrow_\beta M'[x:=N_0]$ を使いました（β 基の縮約は置換と両立します。$M$ に関する帰納法で確かめられます）。$\twoheadrightarrow_\beta$ の各ステップに (CR2) を繰り返し使えば、還元可能性は保たれます。

次の基本補題が、強正規化定理の本体です。同時置換とは、複数の変数に対して一度に[置換](/mathematics/logic-and-type-theory/lambda-calculus#def-substitution)を行うことです。主張は、型の付く項の自由変数に還元可能な項を代入すれば、結果も還元可能になる、というものです。項の形ごとに、これまでの補題を一つずつ当てはめて示します。

<Lemma id="lem-adequacy" title="基本補題">
$x_1{:}A_1,\ldots,x_n{:}A_n\vdash M:B$ で、$N_i\in\mathrm{Red}_{A_i}$（$i=1,\ldots,n$）ならば、同時置換 $M[\vec x:=\vec N]\in\mathrm{Red}_B$。
</Lemma>

<Proof of="lem-adequacy">
型付けの導出に関する帰納法。(var) なら $M\equiv x_i$ で $M[\vec x:=\vec N]\equiv N_i\in\mathrm{Red}_{A_i}$。(app) なら $M\equiv PQ$、帰納法の仮定で $P[\vec x:=\vec N]\in\mathrm{Red}_{C\to B}$、$Q[\vec x:=\vec N]\in\mathrm{Red}_C$ なので、$\mathrm{Red}_{C\to B}$ の定義から積は $\mathrm{Red}_B$ に属する。(abs) なら $M\equiv\lambda y{:}C.P$、$B\equiv C\to D$ で、$\vec x,y$ の文脈で $P:D$。任意の $N\in\mathrm{Red}_C$ について帰納法の仮定から $P[\vec x:=\vec N][y:=N]\equiv P[\vec x:=\vec N,\,y:=N]\in\mathrm{Red}_D$（$y$ は $\vec N$ に自由に現れないように選ぶ）。<Ref to="lem-red-abs" /> により $\lambda y{:}C.P[\vec x:=\vec N]\equiv M[\vec x:=\vec N]\in\mathrm{Red}_{C\to D}$。
</Proof>

<Proof of="thm-strong-normalization">
$\Gamma=x_1{:}A_1,\ldots,x_n{:}A_n$ とし、<Ref to="lem-adequacy" /> で $N_i\equiv x_i$ とする。変数は還元可能（<Ref to="lem-cr-conditions" />）なので $M\in\mathrm{Red}_A$、(CR1) により $M$ は SN である。
</Proof>

<Remark id="rem-tait-strength" title="テイトの方法の要点">
還元可能性 $\mathrm{Red}_{A\to B}$ の定義は「よい引数に適用するとよい値を返す」という、BHK 解釈（§5）そのものの形をしています。SN という性質そのものは帰納法の仮定として弱すぎ（SN な $M,N$ の積 $MN$ が SN とは限らない。$\omega\omega$ が反例）、「適用で閉じた SN」に強めると帰納法が回るのです。この方法はジラールによって多相型の体系 F に拡張され、さらに依存型理論の正規化証明の基本的な道具になっています。
</Remark>

## 4. カリー＝ハワード対応

### 4.1. 直観主義の自然演繹

<Definition id="def-nj" title="含意の自然演繹">
命題変数 $p_1,p_2,\ldots$ から $\to$ で作られる論理式を考える。**仮定の集まり** $\Delta$ は論理式の有限集合で、判断 $\Delta\vdash A$ を次の規則で帰納的に定める。

$$
\frac{A\in\Delta}{\Delta\vdash A}\ (\mathrm{Ax})\qquad
\frac{\Delta\cup\{A\}\vdash B}{\Delta\vdash A\to B}\ ({\to}\mathrm{I})\qquad
\frac{\Delta\vdash A\to B\quad\Delta\vdash A}{\Delta\vdash B}\ ({\to}\mathrm{E})
$$

$({\to}\mathrm{I})$ は「$A$ を仮定して $B$ を示したら、仮定を**解消**して $A\to B$」、$({\to}\mathrm{E})$ はモーダス・ポネンスである。
</Definition>

型付けの文脈 $\Gamma$ は変数と型の列、ここでの仮定の集まり $\Delta$ は論理式の集合です。仮定に名前（変数）を付けて並べたものが文脈にあたり、仮定に重複がない場合は、どの論理式を仮定しているかという同じ情報を表します。次の定理で「$A_i$ には重複がない」と置くのはそのためです。

[一階述語論理と完全性定理](/mathematics/logic-and-type-theory/first-order-logic) で使ったヒルベルト流の体系は公理を多く置いて推論規則を減らしていました。自然演繹は逆に、各論理記号に「導入」と「除去」の規則を一組ずつ与え、人間が書く証明の形に近づけたものです（ゲンツェン 1935）。

型付け規則と見比べると、型付き項の型から項を消したものが自然演繹そのものです。逆に、自然演繹の証明の各仮定に名前（変数）を付けると項が復元できます。

<Theorem id="thm-curry-howard" title="カリー＝ハワード対応（含意の断片）">
型の基本型 $o_i$ を命題変数 $p_i$ と同一視する。

1. $x_1{:}A_1,\ldots,x_n{:}A_n\vdash M:B$ ならば $\{A_1,\ldots,A_n\}\vdash B$。
2. $\{A_1,\ldots,A_n\}\vdash B$ ならば、ある項 $M$ について $x_1{:}A_1,\ldots,x_n{:}A_n\vdash M:B$（$A_i$ には重複がないとする）。
3. さらに、仮定に名前を付けた自然演繹の導出と、型付けの導出（したがって、<Ref to="lem-generation" /> により型付き項）とは一対一に対応する。この対応のもとで、β 基 $(\lambda x{:}A.M)N$ は「$({\to}\mathrm{I})$ で $A\to B$ を導いた直後に $({\to}\mathrm{E})$ で使う」という回り道に対応し、その縮約 $M[x:=N]$ は「$A$ の仮定を使っていた箇所に $A$ の証明 $N$ を直接差し込む」ことに対応する。

</Theorem>

<Proof of="thm-curry-howard">
(1) 型付けの導出に関する帰納法。各規則から項を消すと、(var) は (Ax)、(abs) は $({\to}\mathrm{I})$、(app) は $({\to}\mathrm{E})$ になる。(abs) で文脈から $x{:}A$ が消えることが、$({\to}\mathrm{I})$ で仮定 $A$ が解消されることに対応する。

(2) 導出に関する帰納法。仮定の集まり $\Delta=\{A_1,\ldots,A_n\}$ に対し、各 $A_i$ に変数 $x_i$ を一つずつ割り当てた文脈を $\Gamma_\Delta$ とする。(Ax) なら $A=A_i$ について $\Gamma_\Delta\vdash x_i:A$。$({\to}\mathrm{E})$ なら帰納法の仮定の項 $M:A\to B$、$N:A$ から $MN:B$。$({\to}\mathrm{I})$ で $\Delta\cup\{A\}\vdash B$ から $\Delta\vdash A\to B$ を得るとき、$A\notin\Delta$ なら新しい変数 $x$ を $A$ に割り当てて帰納法の仮定の $\Gamma_\Delta,x{:}A\vdash M:B$ から $\lambda x{:}A.M$。$A\in\Delta$（たとえば $A=A_j$）なら $\Gamma_\Delta\vdash M:B$ が得られているので、新しい変数 $x$ について弱化（<Ref to="lem-typing-subst" /> (1)）で $\Gamma_\Delta,x{:}A\vdash M:B$ とし、$\lambda x{:}A.M$ をとる（$x$ は使われない仮定）。

(3) (1) と (2) の構成は、名前付きの仮定をもつ導出の上では互いに逆である（どちらも規則を一つずつ置き換えるだけ）。β 基 $(\lambda x{:}A.M)N$ の型付けの導出は、$M:B$ の導出の下に (abs)、その右に $N:A$ の導出、最後に (app) という形で、これが記述どおりの回り道である。縮約後の項 $M[x:=N]$ の導出は、<Ref to="lem-typing-subst" /> (2) の証明のとおり、$M$ の導出の (var) $x:A$ の葉を $N:A$ の導出で置き換えたものになっている。
</Proof>

<Figure caption="β 簡約は証明の回り道の除去である。左の証明は A→B を導入した直後に除去しているが、右では仮定 A の位置に A の証明を直接差し込む。">
<svg viewBox="0 0 640 190" width="100%" role="img" aria-label="自然演繹で含意を導入した直後に除去する回り道と、それを除いた証明を対比する図">
  <defs>
    <marker id="ch-arrow" markerWidth="8" markerHeight="8" refX="6" refY="3" orient="auto">
      <path d="M 0 0 L 6 3 L 0 6 z" fill="var(--sl-color-accent)" />
    </marker>
  </defs>
  <text x="90" y="30" text-anchor="middle" fill="currentColor" font-size="13">[x : A]</text>
  <text x="90" y="52" text-anchor="middle" fill="currentColor" font-size="13">⋮  M</text>
  <text x="90" y="74" text-anchor="middle" fill="currentColor" font-size="13">B</text>
  <line x1="40" y1="82" x2="140" y2="82" stroke="currentColor" stroke-width="1.2" />
  <text x="150" y="86" fill="currentColor" font-size="11">→I</text>
  <text x="90" y="102" text-anchor="middle" fill="currentColor" font-size="13">A → B</text>
  <text x="230" y="80" text-anchor="middle" fill="currentColor" font-size="13">⋮  N</text>
  <text x="230" y="102" text-anchor="middle" fill="currentColor" font-size="13">A</text>
  <line x1="40" y1="112" x2="260" y2="112" stroke="currentColor" stroke-width="1.2" />
  <text x="270" y="116" fill="currentColor" font-size="11">→E</text>
  <text x="150" y="134" text-anchor="middle" fill="currentColor" font-size="13">B</text>
  <text x="150" y="168" text-anchor="middle" fill="currentColor" font-size="12">項 (λx:A. M) N</text>
  <line x1="320" y1="90" x2="380" y2="90" stroke="var(--sl-color-accent)" stroke-width="2" marker-end="url(#ch-arrow)" />
  <text x="350" y="80" text-anchor="middle" fill="var(--sl-color-accent)" font-size="12">β</text>
  <text x="500" y="44" text-anchor="middle" fill="currentColor" font-size="13">⋮  N</text>
  <text x="500" y="66" text-anchor="middle" fill="var(--sl-color-accent)" font-size="13">A</text>
  <text x="500" y="90" text-anchor="middle" fill="currentColor" font-size="13">⋮  M</text>
  <text x="500" y="112" text-anchor="middle" fill="currentColor" font-size="13">B</text>
  <text x="500" y="168" text-anchor="middle" fill="currentColor" font-size="12">項 M[x := N]</text>
</svg>
</Figure>

### 4.2. 正規な証明とその帰結

強正規化定理をカリー＝ハワード対応で読み替えると、「どの証明も、回り道を一つずつ除いていけば有限回で回り道のない証明（**正規な証明**）になる」という定理になります。これはプラヴィッツ (1965) が自然演繹で直接示した**正規化定理**にあたります。正規な証明は形がきわめて制限されているので、そこから論理についての情報が引き出せます。

次の補題は、これ以上簡約できない項がどんな形をしているかを調べます。式 $(((yN_1)N_2)N_3)$ のように、適用を左へ左へとたどると、先頭にある $y$ に着きます。この先頭が変数であることが、下の無矛盾性の証明で使われます。

<Lemma id="lem-normal-shape" title="正規形の形">
β 正規形の項は $\lambda x_1{:}A_1.\cdots\lambda x_k{:}A_k.\,y\,N_1\cdots N_m$（$k,m\ge0$、$y$ は変数、各 $N_j$ は β 正規形）の形をしている。
</Lemma>

<Proof of="lem-normal-shape">
外側の $\lambda$ をすべて外すと、抽象でない項 $M$ が残る。$M$ を適用の左側へたどって $M\equiv H\,N_1\cdots N_m$（$H$ は適用でない）と書く。$H$ は変数か抽象である。$H$ が抽象なら、$M$ は抽象でないので $m\ge1$ で、$HN_1$ が β 基になり正規形であることに反する。よって $H$ は変数で、$N_j$ は正規形の部分項だから正規形である。
</Proof>

<Corollary id="cor-consistency" title="無矛盾性">
基本型 $o$ の閉項は存在しない。したがって、含意の自然演繹で命題変数 $p$ は仮定なしには証明できない。
</Corollary>

<Proof of="cor-consistency">
$\vdash M:o$ とする。<Ref to="thm-strong-normalization" /> により $M$ は正規形 $M'$ をもち、<Ref to="thm-subject-reduction" /> により $\vdash M':o$。$o$ は矢印型でないので、<Ref to="lem-normal-shape" /> の形で $k=0$、すなわち $M'\equiv yN_1\cdots N_m$。しかし文脈が空なので変数 $y$ には型が付かない。矛盾。後半は <Ref to="thm-curry-howard" /> (2) による。
</Proof>

「$p$ が証明できない」は小さな主張に見えますが、「どんな命題でも証明できるわけではない」、すなわち論理が**無矛盾**であることを、証明の構文だけを調べて示しています。同じ方法で、パースの法則 $((p\to q)\to p)\to p$ は直観主義論理では証明できないことが示せます（演習）。この法則は真理値表では恒真なので、直観主義論理は古典論理より真に弱いことが分かります。

### 4.3. 論理積・論理和・矛盾への拡張

対応は他の論理記号にも広がります。型に積 $A\times B$、直和 $A+B$、空の型 $\bot$ を加え、それぞれに導入と除去の項を用意します。

| 論理 | 型 | 導入（証明の作り方） | 除去（証明の使い方） |
|---|---|---|---|
| $A\to B$ | 関数型 $A\to B$ | $\lambda x{:}A.M$ | 適用 $MN$ |
| $A\wedge B$ | 積 $A\times B$ | 組 $\langle M,N\rangle$ | 射影 $\pi_1M$、$\pi_2M$ |
| $A\vee B$ | 直和 $A+B$ | $\mathrm{inl}\,M$、$\mathrm{inr}\,N$ | 場合分け $\mathrm{case}\,M\,(x.P)\,(y.Q)$ |
| $\bot$（矛盾） | 空の型 $\bot$ | なし | $\mathrm{abort}_C\,M$ |
| $\neg A$ | $A\to\bot$ | $\lambda x{:}A.M$ | 適用 |

簡約規則は「導入の直後の除去」を消すもの（$\pi_1\langle M,N\rangle\to M$、$\mathrm{case}\,(\mathrm{inl}\,M)\,(x.P)\,(y.Q)\to P[x:=M]$ など）で、主部簡約・強正規化・正規形の形の議論はそのまま拡張されます（Girard–Lafont–Taylor の第 6・10 章）。Lean 4 では次のように書けます。

```lean
theorem and_swap (A B : Prop) : A ∧ B → B ∧ A :=
  fun ⟨a, b⟩ => ⟨b, a⟩

theorem or_swap (A B : Prop) : A ∨ B → B ∨ A :=
  fun h => h.elim (fun a => Or.inr a) (fun b => Or.inl b)

theorem nn_em (A : Prop) : ¬¬(A ∨ ¬A) :=
  fun h => h (Or.inr (fun a => h (Or.inl a)))

#print axioms nn_em   -- 'nn_em' does not depend on any axioms
```

`⟨a, b⟩` が組、`Or.inl` / `Or.inr` が $\mathrm{inl}$ / $\mathrm{inr}$、`h.elim` が $\mathrm{case}$ です。Lean の `¬A` は定義により `A → False` です。`#print axioms` は、その証明が依存する公理を表示するコマンドで、`nn_em` は公理を一つも使わない純粋な λ 項だと分かります。

## 5. BHK 解釈：証明とは何か

カリー＝ハワード対応の背後には、ブラウワー、ハイティング、コルモゴロフにさかのぼる**証明の解釈**があります。

<Definition id="def-bhk" title="BHK 解釈">
論理式 $A$ の**証明**とは何かを、論理記号に沿って次のように説明する（形式的な定義ではなく、意味の説明である）。

- $A\wedge B$ の証明とは、$A$ の証明と $B$ の証明の組である。
- $A\vee B$ の証明とは、$A$ の証明か $B$ の証明のどちらかと、どちらであるかの印である。
- $A\to B$ の証明とは、$A$ の任意の証明を $B$ の証明に変換する方法（構成）である。
- $\bot$ の証明は存在しない。$\neg A$ の証明は、$A$ の証明を $\bot$ の証明に変える方法である。
- $\forall x\,A(x)$ の証明とは、各 $x$ に $A(x)$ の証明を対応させる方法、$\exists x\,A(x)$ の証明とは、具体的な $a$ と $A(a)$ の証明の組である。

</Definition>

この表を §4.3 の表と比べると、BHK の「方法」が λ 項、「組」が対、「印付きのどちらか」が直和に置き換わっているだけです。カリー＝ハワード対応は、BHK 解釈の「方法」を λ 計算という**特定の計算体系**で具体化し、それが論理の規則と正確に一致することを定理として示したもの、と読めます。

この解釈では、排中律 $A\vee\neg A$ の証明は「$A$ の証明か、$\neg A$ の証明のどちらかを実際に示すこと」になります。任意の $A$ についてそれを一様に行う方法はありません（たとえば $A$ が未解決の予想なら、どちらも手元にない）。だから排中律は BHK 解釈では正当化されず、直観主義論理の規則にも含まれません。一方で $\neg\neg(A\vee\neg A)$ には上の `nn_em` という具体的な証明があります。「排中律の否定は矛盾する」までは構成的に言えるが、そこから排中律そのものには進めない、ということです。[証明の技術](/mathematics/foundations/proof-techniques) で注意した、背理法のどこが古典論理に固有か（<Ref to="mathematics/foundations/proof-techniques#rem-intuitionism" />）という区別が、ここで正確になります。

<Remark id="rem-classical-in-lean" title="Lean での古典論理">
ふつうの数学は排中律を自由に使います。Lean では排中律 `Classical.em` は**公理から導かれる定理**として用意されています。`#print axioms Classical.em` を実行すると `propext`、`Classical.choice`、`Quot.sound` の三つの公理に依存していると表示されます。純粋な λ 項としての証明（カリー＝ハワード対応の内側）と、公理を使う証明（外側）の境界を、Lean は公理の依存関係として正確に記録しています。この三つの公理の意味と、そこから排中律が導かれる仕組み（ディアコネスクの定理）は、[依存型理論](/mathematics/logic-and-type-theory/dependent-type-theory) と [証明支援系 Lean の仕組み](/mathematics/logic-and-type-theory/lean-kernel) で扱います。
</Remark>

単純型だけでは、$\forall$ と $\exists$ を型として表せません。「各 $x$ に $A(x)$ の証明を対応させる関数」の型は、値 $x$ によって行き先の型 $A(x)$ が変わる関数の型、つまり**依存型**を必要とします。これが次章の主題です。

## 6. 演習

<Exercise id="exr-s-proof" difficulty="易">
項 $S\equiv\lambda f{:}A\to B\to C.\,\lambda g{:}A\to B.\,\lambda a{:}A.\,fa(ga)$ が型 $(A\to B\to C)\to(A\to B)\to A\to C$ をもつことを型付け規則で確かめ、対応する自然演繹の証明を言葉で述べよ。
<Solution>
$\Gamma=f{:}A\to B\to C,\ g{:}A\to B,\ a{:}A$ とする。(var) と (app) で $\Gamma\vdash fa:B\to C$、$\Gamma\vdash ga:B$、さらに (app) で $\Gamma\vdash fa(ga):C$。(abs) を 3 回使えば主張の型を得る。自然演繹では、「$A\to B\to C$、$A\to B$、$A$ を仮定する。モーダス・ポネンスで $B\to C$ と $B$ を得て、もう一度使って $C$。三つの仮定を順に解消して結論を得る」という証明になる。§1.2 の Lean の `s_comb` はこの項そのものです。
</Solution>
</Exercise>

<Exercise id="exr-subject-expansion" difficulty="標準">
主部簡約の逆（$M\to_\beta M'$ かつ $\Gamma\vdash M':A$ ならば $\Gamma\vdash M:A$）が成り立たないことを、例を挙げて示せ。
<Solution>
$z{:}o$ の文脈で $M\equiv(\lambda x{:}o.\lambda y{:}o.y)(zz)$ を考える。$M\to_\beta\lambda y{:}o.y$ で、これは型 $o\to o$ をもつ。一方 $M$ には型が付かない。生成補題（<Ref to="lem-generation" />）により、$M$ に型が付くなら引数 $zz$ に型が付くが、$z{:}o$ で $o$ は矢印型でないので $zz$ には型が付かない。縮約で捨てられる部分に型の付かない項を置けばよいわけです。
</Solution>
</Exercise>

<Exercise id="exr-peirce" difficulty="難">
$p,q$ を異なる命題変数とする。パースの法則 $((p\to q)\to p)\to p$ が含意の自然演繹で（仮定なしに）証明できないことを、<Ref to="lem-normal-shape" /> を使って示せ。
<Solution>
証明できるとすると、<Ref to="thm-curry-howard" />、<Ref to="thm-strong-normalization" />、<Ref to="thm-subject-reduction" /> により、その型の閉じた正規形 $M$ がある。$M$ は矢印型をもつので $k\ge1$ の形で、$M\equiv\lambda f{:}(p\to q)\to p.\,K$、$f{:}(p\to q)\to p\vdash K:p$、$K$ は正規形。$p$ は矢印型でないので $K\equiv yN_1\cdots N_m$ で、$y$ は文脈の変数 $f$ しかない。$f$ の型から $m=1$ で、$N_1$ は型 $p\to q$ の正規形である。<Ref to="lem-normal-shape" /> の形で $k=0$ なら $N_1\equiv y'N'_1\cdots N'_{m'}$（$y'=f$）となるが、$f$ に $m'\le1$ 個の引数を与えた項の型は $(p\to q)\to p$ か $p$ で、$p\to q$ にならない。よって $k\ge1$ で $N_1\equiv\lambda x{:}p.L$、$f{:}(p\to q)\to p,\ x{:}p\vdash L:q$。$q$ は矢印型でないので $L\equiv y'N'_1\cdots N'_{m'}$ で、$y'$ は $f$ か $x$。$y'=x$ なら $m'=0$ で $L$ の型は $p\ne q$。$y'=f$ なら $m'=1$ で $L$ の型は $p\ne q$（$m'=0$ なら矢印型）。どちらも $q$ にならず矛盾。パースの法則は古典論理では恒真なので、直観主義の含意論理は古典論理より真に弱いことが分かります。
</Solution>
</Exercise>

<Exercise id="exr-nn-em" difficulty="標準">
§4.3 の Lean の証明 `nn_em` を、λ 項として読み下せ。仮定 $h:\neg(A\vee\neg A)$ をどのように 2 回使っているかを説明せよ。
<Solution>
項は $\lambda h.\,h\,(\mathrm{inr}\,(\lambda a.\,h\,(\mathrm{inl}\,a)))$ である。目標は $\bot$ で、手元の道具は $h:(A\vee\neg A)\to\bot$ だけなので、$A\vee\neg A$ の証明を作って $h$ に渡すしかない。$A$ の証明はないので右側 $\neg A$ を選び、$\neg A=A\to\bot$ の証明として「$a:A$ を受け取ったら $\mathrm{inl}\,a:A\vee\neg A$ を作って $h$ に渡す」関数を作る。こうして $h$ は内側（$a$ を受け取った後）と外側で 2 回使われる。BHK の言葉では、「排中律の反証 $h$ があるなら、それ自身を使って反証の反証が作れる」という構成になっています。
</Solution>
</Exercise>

## 参考文献

- J.-Y. Girard, Y. Lafont and P. Taylor, *Proofs and Types*, Cambridge University Press, 1989 — 第 2〜4 章（自然演繹とカリー＝ハワード対応）、第 6 章（強正規化）。
- M. H. Sørensen and P. Urzyczyn, *Lectures on the Curry–Howard Isomorphism*, Elsevier, 2006 — 第 2〜4 章。
- W. W. Tait, "Intensional interpretations of functionals of finite type I", *The Journal of Symbolic Logic* 32 (1967), 198–212.
- W. A. Howard, "The formulae-as-types notion of construction", in J. P. Seldin and J. R. Hindley (eds.), *To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism*, Academic Press, 1980, 479–490.
- D. Prawitz, *Natural Deduction: A Proof-Theoretical Study*, Almqvist & Wiksell, 1965.
- A. S. Troelstra and D. van Dalen, *Constructivism in Mathematics*, Vol. 1, North-Holland, 1988 — 第 1 章（BHK 解釈）。