はじめに
Inductive型における帰納原理とは何か？
その公理的な意味について、自然数の公理であるペアノの公理を例に見ながら解説していきます。
ペアノの公理
以下の公理を満たす集合$N$を自然数全体の集合と呼び、その要素を自然数と呼ぶ。
- $0 \in N$が存在する
- 関数$S : N \to N$が存在する
- [単射性]$S$は単射
- [一意性]任意の$n \in N$に対し、$S\,n \neq 0$
- [帰納原理]任意の$P: N \to 2$つまり$P \in 2^N$に対し、$P\,0$かつ、(任意の$n \in N$に対し$P\,n$ならば$P\,(S\,n)$)を満たすとき、任意の$n \in N$に対し$P\,n$
この公理のうち、上2つはInductive型におけるコンストラクタの存在を表していて、3番目はそれら全ての単射性を表しています($0$は引数を取らないコンストラクタなので公理を書く必要がない)
4つ目は任意の要素は高々1つのコンストラクタでのみ書き表せるということを表していて、最後の公理が数学的帰納法、つまり自然数における帰納原理を表しています。
つまりペアノの公理を一般のInductive型で表すなら、4番目の公理までは以下のように表せます。
一般のInductive型の帰納原理を除いた公理
$n$個のコンストラクタ$\{C_i : A_{i,0} (X) \to \cdots \to A_{i,m_i-1}(X) \to X\}_{i < n}$を持つInductive型$X$の帰納原理以外の公理は以下のように表せる。
(ただし$A_{i,j} : \operatorname{Type} \to \operatorname{Type}$とする)
- [単射性]任意の$i < n$に対し、$C_i\,x_0\,\cdots\,x_{m_i-1} = C_i\,y_0\,\cdots\,y_{m_i-1}$ならば任意の$k < m_i$に対し$x_k = y_k$
- [一意性]任意の$i,j < n$に対し, $C_i\,x_0\,\cdots\,x_{m_i-1} = C_j\,y_0\,\cdots\,y_{m_j-1}$ならば$i = j$
この単射性と一意性はその意味からシンプルに一般化できますが、帰納原理は任意の$P:X \to 2$を引数にとって、結論が$\forall x \in X, P\,x$となること以外、特にその帰納法の仮定において単純な一般化が難しいです。
そこで本記事ではペアノの公理を例に帰納原理の公理的な意味を考え、一般のInductive型において、どのような性質を満たす帰納原理が公理として相応しいのかを考察していきます。
この公理的な意味を考えるために帰納原理を除いたペアノの公理を考えていきます。
帰納原理を除いたペアノの公理
まず帰納原理を除いたペアノの公理を考えます。
これを本記事では準ペアノの公理と呼ぶことにすると、以下の集合は準ペアノの公理を満たします。
- $\mathbb{N}$
- $\mathbb{N} + \mathbb{N}$
- $\mathbb{N} + \mathbb{Z}$
- 任意の$n,m \in \mathbb{N}$に対して、$\mathbb{N} + \sum_{i \leq n}\mathbb{N} + \sum_{i \leq m}\mathbb{Z}$
- 1点集合$1 := \{\emptyset\}$上の二分木$\operatorname{btree}\,1$
ここで5番目の例は$0 := \operatorname{leaf} \in \operatorname{btree}{1}$かつ$S := \operatorname{node}\,\emptyset\,\operatorname{leaf} : \operatorname{btree}\,1 \to \operatorname{btree}\,1$で実現できます。
これらのうち、$\mathbb{N}$だけを特徴づけをする、つまり公理を満たす集合が一意に定まるようにするのが帰納原理の役割になります。
ペアノの公理は準ペアノの公理を満たす最小の集合
ペアノの公理を満たす集合$(\mathbb{N},0,S)$は上で述べた準ペアノの公理を満たす最小の集合、すなわち任意の準ペアノの公理を満たす集合$(N,0_N,S_N)$に対して以下の性質を満たす$f : \mathbb{N} \to N$が存在します。
- $f\,0 = 0_N$
- 任意の$n \in \mathbb{N}$に対し、$f\,(S\,n) = S_N\,(f\,n)$
- $f$は単射
この3つのうち、上2つが各コンストラクタ対する準同型性を表していて、最後の単射性が$\mathbb{N}$の最小性を表しています。
実際にこれを示していきます。
Fixpoint関数を使って準同型写像を定義する
前回の記事「自然数を定義するペアノの公理から再帰関数が定義できることを証明する
」よりペアノの公理を満たす集合$\mathbb{N}$上には以下を満たすFixpoint関数$F:\forall A, A \to (A \to \mathbb{N} \to A) \to \mathbb{N} \to A$が存在します。
任意の$x_0 \in A$, $f_S:A \to \mathbb{N} \to A$に対し、$f := F\,x_0\,f_S$とした時
f\,0 = x_0
\forall n \in \mathbb{N}, f\,(S\,n)=f_S\,(f\,n)\,n
このFixpoint関数を利用して以下の関数$f:\mathbb{N} \to N$を作ります。
f := F\,0_N\,(\lambda a n.S_N\,a)
これが以下を満たすことを示します。
- $f\,0 = 0_N$
- 任意の$n \in \mathbb{N}$に対し、$f\,(S\,n) = S_N\,(f\,n)$
- $f$は単射
1つ目と2つ目はFixpoint関数の満たす性質より明らかなので、あとは単射性を示すだけです。
単射性
3つ目の単射性は、任意の$n \in \mathbb{N}$に対して$\forall m \in \mathbb{N}, f\,n = f\,m \to n = m$を満たすことを帰納原理を使って示します。
$n=0$の時、$f\,n = 0_N$より任意の$m \in \mathbb{N}$に対して$f\,m = 0_N \to m = 0$を帰納原理を用いて示す。
$m=0$の時は明らか
$m=S\,m'$ときは仮定として$0_N = f\,(S\,m) = S_N\,(f\,n)$があるが、これは$N$の準ペアノの公理に反するので矛盾
よって$f\,m = 0_N \to m = 0$
$n = S\,n'$のとき、帰納法の仮定より$\forall m \in \mathbb{N}, f\,n' = f\,m \to n' = m$が成り立つ。
今$f\,(S\,n') = S_N\,(f\,n')$が成り立つので、任意の$m \in \mathbb{N}$に対して$S_N\,(f\,n') = f\,m \to S\,n' = m$を示せばいい。これを帰納原理を使って示します。
$m=0$の時は$f\,0=0_N$より仮定の$S_N\,(f\,n') = 0_N$が$N$の公理に矛盾
$m = S\,m'$の時、仮定は$S_N\,(f\,n') = f\,(S\,m') = S_N\,(f\,m')$となるが、$N$の公理より$S_N$は単射なので$f\,n' = f\,m'$を満たす。
今、任意の$m \in \mathbb{N}$に対して$f\,n' = f\,m \to n' = m$を満たすことにより$n' = m'$が成り立つ。
すなわち$n = S\,n' = S\,m' = m$
以上により$f$は単射。
これらの結論から$f$が準同型写像であることが示せました。
ペアノの公理を満たす集合の一意性
上で定義した準同型写像を用いると、ペアノの公理を満たす集合は同型を除いて一意に定まります。
すなわち$N$が帰納原理を満たす時、準同型写像$f:\mathbb{N} \to N$が全単射になることを示します。
単射性は上で示した通りなので全射性を示せば十分です。
任意の$y \in N$に対し、$f\,n = y$となる$n \in \mathbb{N}$が存在することを$N$上の帰納原理を用いて示します。
$y=0_N$の時、$f\,0=0_N$より明らか。
$y=S_N\,y'$の時、帰納法の仮定より$f\,n = y'$となる$n \in \mathbb{N}$が存在する。この$n$に対して$f\,(S\,n) = S_N\,(f\,n) = S_N\,y' = y$より$f\,n = y$となる$n \in \mathbb{N}$が存在する。
以上により$f$は全射、すなわち$f$は同型写像であり、ペアノの公理を満たす集合は同型を除いて一意に定まる。
帰納原理の役割
上のことから言えるのは帰納原理によってペアノの公理を満たす集合は準ペアノの公理を満たす最小の集合であり、特に一意性が成り立つということです。それは準ペアノの公理を満たす集合のうち、帰納原理によって自然数の特徴付けができるということでもあります。
一般のInductive型においても帰納原理の存在によって、それを除いた公理の中で最小性と一意性を満たすということが帰納原理の特徴になると言えるでしょう。
まとめ
Inductive型における帰納原理の満たす性質について、自然数の公理であるペアノの公理を例に見ていきました。