Martin-Löf型理論
概要
Martin-Löf型理論（Martin-Löf type theory）とは、型が項に依存することを許す依存型の理論で、依存積型 $\prod$、依存和型 $\sum$、恒等型 $a=_Ab$、宇宙などを形成・導入・除去・計算の規則で定めた体系である。型を命題、項を証明と読むと、$\prod$ と $\sum$ は全称と存在に、恒等型は等号にあたり、直観主義論理による数学を型と項だけで展開できる。恒等型の除去規則である道の帰納法から等号の対称性・推移性が従い、等号が決定可能な型では二つの等しさの証明が等しい（Hedberg の定理）。単一性公理と高次帰納的型を加えたものがホモトピー型理論である。
型理論の単純型付きラムダ計算では、型は項に依存しない。「長さ $n$ の列の型」や「$x$ と $y$ が等しいという命題の型」のように、型が項に依存することを許したのが 依存型 の理論であり、その代表が Martin-Löf による Martin-Löf 型理論（Martin-Löf type theory、直観主義型理論）である。この体系では、依存積型 $\prod$ と依存和型 $\sum$ が「すべての」「ある」に、恒等型 $a=_Ab$ が等号にあたり、命題をその証明の型と読む（命題としての型）。こうして直観主義論理による数学を、集合論を経ずに型と項だけで展開できる。
恒等型を「定義上の等しさ」と区別して扱う版を 内包的（intensional）、両者を同一視する版を 外延的（extensional）という。この記事では内包的な版を、UFP13 第 1 章の非形式的な書き方で述べる。そのうえで、等号の対称性・推移性と群の法則、型理論の「選択公理」、宇宙を使った $0_{\mathbf 2}\ne1_{\mathbf 2}$、Hedberg の定理（等号が決定可能な型では二つの等しさの証明は等しい）を証明する。内包的な版に単一性公理と高次帰納的型を加えたものがホモトピー型理論である。
判断と型の構成
Martin-Löf 型理論の基本の主張（判断）は次の 2 つである（UFP13 §1.1, pp. 17–19）。
- $a:A$：「項 $a$ は型 $A$ をもつ」。
- $a\equiv b:A$：「型 $A$ の項 $a,b$ は 定義上等しい（judgmental equality）」。
判断は仮定の列（文脈）$x_1:A_1,\dots,x_n:A_n$ のもとでなされる。ここで $A_i$ は前の $x_j$ に依存してよい。判断は命題ではなく、否定したり量化したりできない。
型は 宇宙 の項として扱う。宇宙の列 $\mathcal U_0:\mathcal U_1:\mathcal U_2:\cdots$ があり、$A:\mathcal U_i$ なら $A:\mathcal U_{i+1}$ でもある（UFP13 §1.3, pp. 24–25）。添字を気にしないときは $\mathcal U$ と書く。型 $A$ 上の 型の族 とは関数 $B\colon A\to\mathcal U$ のことである。
各型は、形成（型の作り方）、導入（項の作り方）、除去（その型の項を使って別の型の項を作る方法）、計算（除去を導入に当てたときの定義上の等しさ）の規則で与えられる。除去規則は帰納法の形をとる。
$A:\mathcal U$、$B\colon A\to\mathcal U$ とする（UFP13 §1.4–1.9, pp. 25–39）。
- 依存積型 $\prod_{x:A}B(x)$：項は $\lambda x.\,b$（$x:A$ のもとで $b:B(x)$）で、適用 $f(a):B(a)$ と計算規則 $(\lambda x.\,b)(a)\equiv b[a/x]$ をもつ。$B$ が $x$ によらないとき $A\to B$ と書く。
- 依存和型 $\sum_{x:A}B(x)$：項は対 $(a,b)$（$a:A$、$b:B(a)$）。除去規則：族 $C\colon\sum_{x:A}B(x)\to\mathcal U$ と $g:\prod_{a:A}\prod_{b:B(a)}C((a,b))$ から、$f((a,b))\equiv g(a)(b)$ を満たす $f:\prod_{w}C(w)$ が得られる。とくに射影 $\mathrm{pr}_1(w):A$、$\mathrm{pr}_2(w):B(\mathrm{pr}_1(w))$ が定まる。$B$ が $x$ によらないとき $A\times B$ と書く。
- 和型 $A+B$：項は $\mathrm{inl}(a)$、$\mathrm{inr}(b)$。族 $C$ と両方の場合の項から、場合分けで $\prod_{z:A+B}C(z)$ の項が得られる。
- 空型 $\mathbf 0$（導入規則がなく、任意の族 $C\colon\mathbf 0\to\mathcal U$ について $\prod_{z:\mathbf 0}C(z)$ の項がある）、単位型 $\mathbf 1$（項 $\star$）、真偽の型 $\mathbf 2$（項 $0_{\mathbf 2},1_{\mathbf 2}$ と場合分け）。
- 自然数の型 $\mathbb N$：項は $0$ と $\mathrm{succ}(n)$。族 $C\colon\mathbb N\to\mathcal U$、$c_0:C(0)$、$c_s:\prod_{n:\mathbb N}C(n)\to C(\mathrm{succ}(n))$ から、$f(0)\equiv c_0$、$f(\mathrm{succ}(n))\equiv c_s(n,f(n))$ を満たす $f:\prod_{n:\mathbb N}C(n)$ が得られる（帰納法）。
$A:\mathcal U$ と $a,b:A$ に対し、恒等型 $a=_Ab$（$\mathrm{Id}_A(a,b)$ とも書く）が型をなし、導入規則 $\mathrm{refl}_a:a=_Aa$ をもつ。除去規則は次の 道の帰納法（$J$ 規則）である（UFP13 §1.12.1, pp. 48–49）。族
$$
C\colon\prod_{x,y:A}(x=_Ay)\to\mathcal U
$$
と $c:\prod_{x:A}C(x,x,\mathrm{refl}_x)$ が与えられると、
$$
f:\prod_{x,y:A}\ \prod_{p:x=_Ay}C(x,y,p),\qquad f(x,x,\mathrm{refl}_x)\equiv c(x)
$$
となる $f$ が得られる。$x=_Ay$ の項を $x$ から $y$ への 道、または等しさの証明という。$\neg P:\equiv(P\to\mathbf 0)$、$x\ne y:\equiv\neg(x=y)$ とおく。
道の帰納法の要点は、両端点 $x,y$ が自由に動く族についてだけ、$\mathrm{refl}$ の場合に帰着できることである。端点を固定した族、たとえばループの族 $C(p)$（$p:a=_Aa$）には使えない（UFP13 §1.12, p. 51）。
$a\equiv b$ なら $\mathrm{refl}_a:a=b$ である。逆は内包的な版では成り立たない（ex-mltt-addition）。外延的な版は 反映規則「$p:a=b$ なら $a\equiv b$」を加える。反映規則のもとでは任意の $p:x=x$ について $p\equiv\mathrm{refl}_x$ となり、すべての型が下の意味で集合になる（UFP13 p. 102 と Exercise 2.14, p. 104）。プログラムを書く体系としては、Coq・Agda は内包的、NuPRL は外延的な版に基づく（UFP13 第 1 章の注, p. 54）。
命題としての型
型 $A$ を命題と読み、項 $a:A$ をその証明と読む。単純型の範囲では、これは 型理論 の定理「Curry–Howard対応」として含意の自然演繹と正確に対応する。依存型を使うと、量化子と等号も型になる（UFP13 §1.11, pp. 41–43、等号は §1.12, p. 47）。
| 論理 | 型 |
|---|---|
| 偽 $\bot$、真 $\top$ | $\mathbf 0$、$\mathbf 1$ |
| $P\wedge Q$、$P\vee Q$、$P\Rightarrow Q$ | $P\times Q$、$P+Q$、$P\to Q$ |
| $\neg P$ | $P\to\mathbf 0$ |
| $\forall x\in A.\,B(x)$ | $\prod_{x:A}B(x)$ |
| $\exists x\in A.\,B(x)$ | $\sum_{x:A}B(x)$ |
| $a=b$ | $a=_Ab$ |
存在を $\sum$ と読むと、存在の証明は「証拠となる項」とその性質の証明の対であり、そこから証拠を取り出せる。その帰結が次の定理である。
$X:\mathcal U$、$A\colon X\to\mathcal U$、$P\colon\prod_{x:X}A(x)\to\mathcal U$ とする。関数
$$
\Bigl(\prod_{x:X}\ \sum_{a:A(x)}P(x,a)\Bigr)\to\Bigl(\sum_{g:\prod_{x:X}A(x)}\ \prod_{x:X}P(x,g(x))\Bigr)
$$
と、逆向きの関数が存在する。
$F:\prod_{x:X}\sum_{a:A(x)}P(x,a)$ に対し、$g:\equiv\lambda x.\,\mathrm{pr}_1(F(x))$ とおくと $g:\prod_{x:X}A(x)$ である。$h:\equiv\lambda x.\,\mathrm{pr}_2(F(x))$ とおくと、$\mathrm{pr}_2(F(x)):P(x,\mathrm{pr}_1(F(x)))$ であり、計算規則により $g(x)\equiv\mathrm{pr}_1(F(x))$ なので、$h:\prod_{x:X}P(x,g(x))$ である。よって $F\mapsto(g,h)$ が求める関数である。逆向きは、$\sum$ の除去規則で対 $(g,h)$ の場合に帰着し、$(g,h)\mapsto\lambda x.\,(g(x),h(x))$ と定めればよい。$\square$
関数外延性（ホモトピー型理論）を仮定すると、この 2 つの関数は互いに逆の同値になる（UFP13 Theorem 2.15.7, p. 100）。この「選択公理」は、仮定の中ですでに値が指定されているので、集合論の選択公理とは意味が違う（UFP13 p. 100）。
恒等型の基本性質
道の帰納法から、等号が同値関係であることと、さらに群のような法則が従う（UFP13 Lemma 2.1.1, 2.1.2, 2.1.4, pp. 62–66。以下の定義の仕方は本記事で選んだもの）。
$A:\mathcal U$ とする。
- $p:x=y$ に対し 逆 $p^{-1}:y=x$ があり、$\mathrm{refl}_x^{-1}\equiv\mathrm{refl}_x$ である。
- $p:x=y$、$q:y=z$ に対し 合成 $p\cdot q:x=z$ があり、$\mathrm{refl}_x\cdot q\equiv q$ である。
- 次の型に項がある：$p\cdot\mathrm{refl}_y=p$、$p^{-1}\cdot p=\mathrm{refl}_y$、$p\cdot p^{-1}=\mathrm{refl}_x$、$(p\cdot q)\cdot r=p\cdot(q\cdot r)$（$r:z=w$）。
1：$C(x,y,p):\equiv(y=x)$、$c(x):\equiv\mathrm{refl}_x$ として道の帰納法を使う。
2：$C(x,y,p):\equiv\prod_{z:A}(y=z)\to(x=z)$、$c(x):\equiv\lambda z.\,\lambda q.\,q$ として道の帰納法を使い、得られた $f$ で $p\cdot q:\equiv f(x,y,p)(z)(q)$ とおく。$\mathrm{refl}_x\cdot q\equiv c(x)(z)(q)\equiv q$ である。
3：どれも $p$ についての道の帰納法による。$q,r$ を含む主張では、族を $C(x,y,p):\equiv\prod_{z,w:A}\prod_{q:y=z}\prod_{r:z=w}\bigl((p\cdot q)\cdot r=p\cdot(q\cdot r)\bigr)$ のように、残りの変数について $\prod$ をとって作る。こうすると両端点が自由な族になる。$p\equiv\mathrm{refl}_x$ の場合、1・2 の計算規則により
$$
\mathrm{refl}_x\cdot\mathrm{refl}_x\equiv\mathrm{refl}_x,\quad \mathrm{refl}_x^{-1}\cdot\mathrm{refl}_x\equiv\mathrm{refl}_x,\quad \mathrm{refl}_x\cdot\mathrm{refl}_x^{-1}\equiv\mathrm{refl}_x,\quad (\mathrm{refl}_x\cdot q)\cdot r\equiv q\cdot r\equiv\mathrm{refl}_x\cdot(q\cdot r)
$$
なので、それぞれ $\mathrm{refl}$ が求める項である。$\square$
同じように道の帰納法で、関数 $f\colon A\to B$ は道を道に送る：$\mathrm{ap}_f:(x=y)\to(f(x)=f(y))$、$\mathrm{ap}_f(\mathrm{refl}_x)\equiv\mathrm{refl}_{f(x)}$（UFP13 Lemma 2.2.1, p. 71）。また型の族 $P\colon A\to\mathcal U$ は道に沿って 輸送 される：$\mathrm{transport}^P(p,-)\colon P(x)\to P(y)$、$\mathrm{transport}^P(\mathrm{refl}_x,-)\equiv\mathrm{id}_{P(x)}$（UFP13 Lemma 2.3.1, p. 72）。後者は「等しいものは同じ性質をもつ」ことの型理論での形である。
宇宙 $\mathcal U$ があれば、$0_{\mathbf 2}\ne1_{\mathbf 2}$ の項がある。
$\mathbf 2$ の場合分けで、型の族 $P\colon\mathbf 2\to\mathcal U$ を $P(0_{\mathbf 2}):\equiv\mathbf 1$、$P(1_{\mathbf 2}):\equiv\mathbf 0$ と定める。$p:0_{\mathbf 2}=1_{\mathbf 2}$ に対し $\mathrm{transport}^P(p,\star):P(1_{\mathbf 2})\equiv\mathbf 0$ である。よって $\lambda p.\,\mathrm{transport}^P(p,\star):(0_{\mathbf 2}=1_{\mathbf 2})\to\mathbf 0$ である。$\square$
Hedberg の定理
型 $A$ が 集合 であるとは、$\prod_{x,y:A}\prod_{p,q:x=y}(p=q)$ に項があること、すなわち同じ端点をもつ二つの道がつねに等しいことをいう（UFP13 Definition 3.1.1, p. 107）。$A$ が 決定可能な等号 をもつとは、$\prod_{x,y:A}\bigl((x=y)+\neg(x=y)\bigr)$ に項があることをいう。
すべての型が集合であるという主張は UIP（uniqueness of identity proofs）と呼ばれる。UIP は道の帰納法からは証明できない（UFP13 §5.8, p. 171。この記事では証明しない）。道の帰納法が端点を固定したループに直接は使えないことは、その表れである。それでも、等号が決定可能な型は集合である。
決定可能な等号をもつ型は集合である（UFP13 Theorem 7.2.5, p. 224。Hedberg による。同書 p. 249）。
$d:\prod_{x,y:A}\bigl((x=y)+\neg(x=y)\bigr)$ をとる。
段 1（定数関数）。$x,y:A$ と $e:(x=y)+\neg(x=y)$ に対し、和型の場合分けで $g(e)\colon(x=y)\to(x=y)$ を、$g(\mathrm{inl}(r))(p):\equiv r$、$g(\mathrm{inr}(n))(p):\equiv$（$n(p):\mathbf 0$ から空型の除去で得る項）と定める。さらに $e$ についての場合分けで、$\prod_{p,q:x=y}\bigl(g(e)(p)=g(e)(q)\bigr)$ の項を作る：$e\equiv\mathrm{inl}(r)$ なら両辺は $r$ に定義上等しいので $\mathrm{refl}_r$、$e\equiv\mathrm{inr}(n)$ なら $n(p):\mathbf 0$ から空型の除去で得る。$f_{x,y}:\equiv g(d(x,y))$ とおくと、$f_{x,y}\colon(x=y)\to(x=y)$ と、すべての $p,q$ について $f_{x,y}(p)=f_{x,y}(q)$ の項 $k(p,q)$ を得る。
段 2（道を $f$ で書き直す）。族 $C(x,y,p):\equiv\bigl(p=f_{x,x}(\mathrm{refl}_x)^{-1}\cdot f_{x,y}(p)\bigr)$ に道の帰納法を使う。$p\equiv\mathrm{refl}_x$ の場合は、$s:\equiv f_{x,x}(\mathrm{refl}_x)$ について lem-mltt-groupoid の 3 により $s^{-1}\cdot s=\mathrm{refl}_x$ の項があり、その逆が求める項である。よって任意の $p:x=y$ について $p=f_{x,x}(\mathrm{refl}_x)^{-1}\cdot f_{x,y}(p)$ である。
段 3。$p,q:x=y$ とし、$t:\equiv f_{x,x}(\mathrm{refl}_x)^{-1}$ とおく。段 1 の $k(p,q)$ に関数 $r\mapsto t\cdot r$ の $\mathrm{ap}$ を当てると $t\cdot f_{x,y}(p)=t\cdot f_{x,y}(q)$ である。段 2 と合成して
$$
p=t\cdot f_{x,y}(p)=t\cdot f_{x,y}(q)=q
$$
を得る（道の合成と逆は lem-mltt-groupoid による）。$\square$
この証明は道の帰納法・和型・空型だけを使い、関数外延性も単一性公理も使わない。UFP13 の証明は関数外延性を使う別の道筋による。
$\mathbf 2$ の場合分けを 2 回使い、$d(0_{\mathbf 2},0_{\mathbf 2}):\equiv\mathrm{inl}(\mathrm{refl})$、$d(1_{\mathbf 2},1_{\mathbf 2}):\equiv\mathrm{inl}(\mathrm{refl})$、$d(0_{\mathbf 2},1_{\mathbf 2}):\equiv\mathrm{inr}(\nu)$、$d(1_{\mathbf 2},0_{\mathbf 2}):\equiv\mathrm{inr}(\lambda p.\,\nu(p^{-1}))$ と定める。ここで $\nu:0_{\mathbf 2}\ne1_{\mathbf 2}$ は prop-mltt-bool-distinct の項である。よって $\mathbf 2$ は決定可能な等号をもち、thm-mltt-hedberg により集合である。$\mathbb N$ も決定可能な等号をもち、集合である（UFP13 p. 225）。
例と反例
加法 $\mathrm{add}\colon\mathbb N\to\mathbb N\to\mathbb N$ を第 1 引数についての帰納法で $\mathrm{add}(0,m):\equiv m$、$\mathrm{add}(\mathrm{succ}(n),m):\equiv\mathrm{succ}(\mathrm{add}(n,m))$ と定め、$n+m$ と書く。このとき $0+m\equiv m$ は定義上成り立つ。一方 $n+0=n$ は、$n$ についての帰納法で示す命題である：$n\equiv0$ なら $0+0\equiv0$ なので $\mathrm{refl}_0$、$p:n+0=n$ なら $\mathrm{succ}(n)+0\equiv\mathrm{succ}(n+0)$ なので $\mathrm{ap}_{\mathrm{succ}}(p):\mathrm{succ}(n)+0=\mathrm{succ}(n)$ である。よって $\prod_{n:\mathbb N}(n+0=n)$ に項がある。しかし変数 $n$ について $n+0\equiv n$ は成り立たない。定義上の等しさは計算規則で同じ正規形に簡約されることであり（UFP13 §A.4, p. 433）、$n+0$ は $\mathrm{add}$ の計算規則が当てはまらない正規形で、$n$ と異なるからである（簡約の合流性と正規化は UFP13 §A.4 による事実で、この記事では証明しない）。同様に $n+m=m+n$ は証明できるが $n+m\equiv m+n$ ではない（UFP13 p. 101）。
定理の仮定を 1 つ外した反例を表にまとめる。どちらの反例も単一性公理（ホモトピー型理論）のもとでのもので、単一性公理は Martin-Löf 型理論と両立する（下の「メタ理論」の節）。
| 外す条件 | 反例 | 成り立たなくなること |
|---|---|---|
| 等号の決定可能性（thm-mltt-hedberg） | 単一性公理を満たす宇宙 $\mathcal U$ | 集合であること |
| 族の両端点が自由に動くこと（道の帰納法） | 端点を固定したループの族 $C(p):\equiv(p=\mathrm{refl}_{\mathbf 2})$、$p:\mathbf 2=_{\mathcal U}\mathbf 2$ | $C(\mathrm{refl})$ からすべての $p$ について $C(p)$ |
1 行目：単一性公理のもとで、$\mathbf 2$ の入れ替えから作った道 $p:\mathbf 2=_{\mathcal U}\mathbf 2$ は $\mathrm{refl}_{\mathbf 2}$ と等しくない（ホモトピー型理論 の定理「宇宙は集合でない」）。$\mathcal U$ は決定可能な等号をもたない（もてば Hedberg の定理により集合になる）。2 行目：同じ $p$ について $C(\mathrm{refl}_{\mathbf 2})$ は $\mathrm{refl}$ で成り立つが、$C(p)$ は成り立たない。
メタ理論
次の事実はこの記事では証明しない。
- 単位型・和型・自然数・恒等型・宇宙などをもつ Martin-Löf 型理論（UFP13 §A.1 の体系）では、型の付いた項は強正規化可能であり、空型 $\mathbf 0$ の閉じた項はない（無矛盾性）。$\mathbb N$ の閉じた項は数字 $\mathrm{succ}^k(0)$ に簡約され、項が型をもつかどうかは決定可能である（UFP13 Theorem A.4.2, Corollary A.4.5–A.4.7, pp. 433–434）。
- 道の帰納法だけからは UIP（すべての型が集合であること）は証明できない（UFP13 §5.8, p. 171）。等しさの証明を亜群の射と読むモデルは Hofmann と Streicher による（UFP13 p. 102）。
- 関数外延性「各点で等しい関数は等しい」は、この記事の規則からは導けず、公理として加える（UFP13 第 1 章の注, p. 54）。
- 単一性公理と高次帰納的型を加えた体系の無矛盾性は、今のところ意味論的なモデル（Kan 複体のモデルなど）によって示されている（UFP13 p. 434）。単一性公理を満たす宇宙を 1 つもつ場合は、ZFC に到達不能基数を 2 つ加えた体系に相対的に無矛盾である（KL18 p. 3、Theorem 3.4.3, p. 36）。
関連項目
参考文献
Mathpediaは寄付と、参考文献の書籍リンク（Amazonアソシエイト）の紹介料で運営されています。 支援について ／ 寄付する
