はじめに
はじめまして。記事を開いていただきありがとうございます。
これから、形式体系を扱う際に頻出する帰納的定義及び再帰的定義の数学的取り扱いについて紹介していこうと思います。
例えば、ラムダ計算におけるラムダ式を定義する際、よく以下のような書き方がされます。
変数の集合をVとし、集合Aに対してA^*でA上の有限列全体の集合を表すとします。
例：ラムダ式の帰納的定義
集合\Lambda\subseteq(V\cup\{\lambda, (, ), .\})^*を次を満たす（集合の包含関係において）最小の集合として定義する。
- \forall x\in V, x\in\Lambda
- \forall M, N\in\Lambda, (MN)\in\Lambda
- \forall x\in V, M\in\Lambda, (\lambda x.M)\in\Lambda
しかし、これは本当に定義になっているのでしょうか？
そもそも上記の条件をすべて満たす集合がある保証もありませんし、存在したとしても最小元が本当に存在するのかも怪しいです。
また、次のような関数の再帰的定義もよく見かけます。
例：ラムダ式の長さの再帰的定義
ラムダ式M\in\Lambdaの長さを取得する関数\mathrm{len}:\Lambda\to\mathbb{N}を以下で定義する。
-
M\equiv xのとき
-
M\equiv M_1M_2のとき
- \mathrm{len}((M_1M_2)) = \mathrm{len}(M_1) + \mathrm{len}(M_2) + 2
-
M\equiv\lambda x.M_0のとき
- \mathrm{len}((\lambda x.M_0)) = \mathrm{len}(M_0) + 5
関数\mathrm{len}を定義したいのに、右辺に\mathrm{len}が現れていますが大丈夫でしょうか。
また、この場合分けは何に基づいた場合分けなのでしょうか。そもそもちゃんと排他的かつ包括的な場合分けになっているのでしょうか。
この記事では、最初のような集合の定義方法を帰納的定義と、その次のような関数の定義方法を再帰的定義と呼ぶことにし、それぞれの定義の数学的な妥当性を与えていこうと思います。
また、帰納的に定義された集合上の数学的帰納法について、帰納原理の観点から妥当性を紹介していこうと思います。
よろしくお願いします。
帰納的閉包
ラムダ式の集合のような、いくつかの生成規則の集合（変数、関数抽象、関数適用）から生成される集合は帰納的閉包として厳密に定義することが出来ます。
集合A, Bに対し、AからBへの関数すべての集合を(A\to B)と書くとします。
定義1: 帰納的閉包
集合Uを固定する。集合F\subseteq\bigcup_{n\in\mathbb{N}}(U^n\to U)を取り、2^U上の関数F:2^U\to 2^Uとみなす。
そのとき、Fの最小不動点をFの帰納的閉包と呼び、\overline{F}と書く。
ただし、F(X)は以下で定める。（f:U^n\to Uのときnを関数fのランクといい、r(f)と書く。明らかな場合は断りなく単にrと書く。）
F(X)=\{f(x_1, ..., x_r)\mid f\in F, x_i\in X\text{ for } 1\le i\le r\}
この帰納的閉包こそが「〇〇を満たす最小の集合」の正体となります。
このとき、以下のKnaster-Tarskiの最小不動点定理からFの最小不動点の存在が言えます。
定理2: Knaster-Tarskiの最小不動点定理
(L, \le)を完備束、f:L\to Lを単調関数とする。
そのとき、\wedge\{x\in L\mid f(x)\le x\}はfの最小前不動点であり、かつ不動点である。（故に最小不動点となる。）
証明（結構好き）
fの前不動点の集合を\mathrm{Pre}(f)とすると、
\forall x\in\mathrm{Pre}(f), \wedge\mathrm{Pre}(f)\le x
fの単調性及びxが前不動点より、
\forall x\in\mathrm{Pre}(f), f(\wedge\mathrm{Pre}(f))\le f(x)\le x
故に、f(\wedge\mathrm{Pre}(f))\le \wedge\mathrm{Pre}(f)となり、確かに\wedge\mathrm{Pre}(f)はfの前不動点であり、\wedgeの定義より最小前不動点となる。
また、逆側の不等式も示して\wedge\mathrm{Pre}(f)が不動点となることも証明する。
fの単調性より、
f(f(\wedge\mathrm{Pre}(f)))\le f(\wedge\mathrm{Pre}(f))
よって、f(\wedge\mathrm{Pre}(f))は前不動点であり、\wedge\mathrm{Pre}(f)は最小前不動点だったので、
\wedge\mathrm{Pre}(f)\le f(\wedge\mathrm{Pre}(f))
\square
今、(2^U, \subseteq)は完備束であり、またFが単調関数であることは容易に確認できます。
ところで、帰納的閉包は、与えられた全体集合Uの特定の部分集合を定義する手法であることに注意してください。
特に、コンピュータサイエンスのような分野では、与えられたアルファベット（=記号の有限集合）\Sigma上の有限長文字列全体の集合\Sigma^*を全体集合Uとして用いることが多く、特に\Sigma^*の部分集合L\subseteq\Sigma^*を言語と言います。
言語を与える手法の一つに、BNF記法があり、BNF記法も帰納的閉包として定式化されます。
（ここでは簡単のため、メタ変数が一つのみのBNF記法について定義しますが、相互再帰があってもF:2^{\Sigma^*\times\Sigma^*}\to 2^{\Sigma^*\times\Sigma^*}のような関数を考えれば大丈夫です。）
定義3: BNF記法
\Sigmaを適当なアルファベットとする。その時、有限集合B=\{X_1, ..., X_n\}\subseteq_{\mathrm{fin}}(\Sigma\cup\{e\})^*を\Sigma上のBNF記法といい、以下のように表記する。
（eはメタ変数と呼ばれるe\not\in\Sigmaなる適当な記号）
このとき、BNF記法Bが定める言語L(B)\subseteq\Sigma^*をL(B)=\overline{F_B}として定義する。
ただし、F_B=\{f_X\mid X\in B\}について、各f_X:(\Sigma^*)^m\to\Sigma^*を以下で定める。
f_X(a_1, ..., a_m)=X[a_1/e_1, ..., a_m/e_m]
ここで、\{e_1, ..., e_m\}はX上のメタ変数eのすべての出現の集合であり、mは出現の個数を表す。
また、X[a_1/e_1, ..., a_m/e_m]\in\Sigma^*はX上の各出現e_iに文字列a_i\in\Sigma^*を代入した文字列を表す。
（ここでの「出現」や「代入」の厳密な定義は面倒なので与えない。また、L(B)、特に各f_Xがeに依らないことも示す必要がある。）
具体例としてここでもラムダ式の正確な定義をBNF記法により与えます。（相互再帰が含まれますがご容赦ください。）
例: BNF記法によるラムダ式の定義
\begin{array}{ll}
x ::= & \texttt{v}\mid x' \\
e ::= & x\mid (\lambda x.e)\mid (ee)
\end{array}
この定義に従うと、(\lambda\texttt{v}.(\texttt{v}''\texttt{v}'))や((\lambda\texttt{v}'.\texttt{v}')\texttt{v})などがラムダ式の一例となります。また、アルファベットは\Sigma=\{\lambda, \texttt{v}, ', (, ), .\}となります。
意地悪なBNF記法も許されるの？
私が初めてBNF記法を見たとき、BNF記法は人々の良心によって成り立ってるのかと思っていました。つまり、次のようなBNF記法は文法上許されないのかと思っていました。
しかし、定義に基づいて確認すれば、これはFに(U^0\to U)の元が存在しないということになり、F(\emptyset)=\emptysetとなるわけです。
故に、最小不動点は空集合となります。
言い換えれば、先程のBNF記法が定める言語は空集合となり、しっかり意味のあるBNF記法となっていることがわかります。（意味はあっても意義はない。）
帰納原理（数学的帰納法）
続いて、帰納的閉包には帰納法が有効であることを述べます。
以下の定理は、特にBNF記法で定義された言語等に対する構造帰納法の妥当性の根拠になります。
定理4: 帰納原理
集合U、集合F\subseteq\bigcup_{n\in\mathbb{N}}(U^n\to U)を固定する。
任意のP\subseteq\overline{F}に対し、PがFの前不動点ならばP=\overline{F}
Proof:
\overline{F}はFの最小前不動点なので\overline{F}\subseteq P、故にP=\overline{F}
\square
意味を説明します。今、ある性質Pが帰納的閉包\overline{F}の任意の元x\in\overline{F}について成り立つことを示したいとします。
Pは\overline{F}の部分集合とみなすことができます。つまり、x\in Pを「xは性質Pが成り立つ」、x\not\in Pを「xは性質Pが成り立たない」と読むわけです。
すると、もともと示したかった「任意のx\in\overline{F}でPが成り立つ」は、P=\overline{F}と言い換えることができ、上述の定理よりP=\overline{F}を示すにはPがFの前不動点であることを言えば十分であることがわかります。
まとめると、「任意のx\in\overline{F}でPが成り立つ」ことを言うには「各規則f\in Fについて、x_1, ..., x_nが全て性質Pを満たすならばf(x_1, ..., x_n)もPを満たす」ことを言えば十分であり、これは数学的帰納法そのものとなります。
再帰的定義
最後に、関数の再帰的定義について説明します。
再帰的定義の際には、原則以下のように「〇〇の形のとき、〜のように定義する」という形を取ります。
例：長さ関数の再帰的定義
ラムダ式M\in\Lambdaの長さを取得する関数\mathrm{len}:\Lambda\to\mathbb{N}を以下で定義する。
-
M\equiv xのとき
-
M\equiv M_1M_2のとき
- \mathrm{len}((M_1M_2)) = \mathrm{len}(M_1) + \mathrm{len}(M_2) + 2
-
M\equiv\lambda x.M_0のとき
- \mathrm{len}((\lambda x.M_0)) = \mathrm{len}(M_0) + 5
この際、ラムダ式Mが同時に二つ以上の形を取らないという暗黙の仮定があります。
すなわち、「MがM_1M_2の形でもあり、同時に\lambda x.M_0の形でもある」という状況は起きないと考えております。
そこで、生成規則の集合Fに曖昧性がない、すなわち、各x\in\overline{F}を生成する方法が常にただ一つであるように条件をつけてみます。
定義5: 自由に生成された集合
集合U、集合F\subseteq\bigcup_{n\in\mathbb{N}}(U^n\to U)を固定する。
このとき、帰納的閉包\overline{F}は以下を満たすとき自由に生成された集合という。
- \forall x\in\overline{F}, \exists!f\in F, \exists!x_1, \ldots, x_r\in\overline{F}
イメージとしては、等式を持たずに生成された集合と考えてください。
例：自由生成でない例
群(G, \cdot)では、\forall g\in G, g\cdot g^{-1}=eという等式によってg\cdot g^{-1}もh\cdot h^{-1}も潰されてしまいeと等しくなってしまう。
そこで、関数の再帰的定義の定義をします。
定理6: 再帰的定義の一意性
集合A, U、定義5の条件を満たす集合F\subseteq\bigcup_{n\in\mathbb{N}}(U^n\to U)を固定する。
さらに、各関数f\in Fに対して、\llbracket{f}\rrbracket:A^r\to Aが与えられているとする。
そのとき、以下の条件を満たす関数\phi:\overline{F}\to Aが唯一つ存在する。
- \forall f\in F, \forall x_1, \ldots, x_r\in\overline{F}
\phi(f(x_1, \ldots, x_r)) = \llbracket{f}\rrbracket(\phi(x_1), \ldots, \phi(x_r))
このようにして自由に生成された集合を定義域とする関数\phiを定義することを、\phiの再帰的定義という。
証明（cpoの知識を仮定、cpoの議論のポイントが詰まってるよ）
flat cpo A_\botに対し、(\overline{F}\to A_\bot)に各点順序を入れてcpoと見なす。すなわち、f, g\in(\overline{F}\to A_\bot)に対し、f\le g\iff\forall x\in\overline{F}, f(x)\le g(x)とした。
そこで、方程式の解は不動点によって得られる事実に注意して、関数\varphi:(\overline{F}\to A_\bot)\to(\overline{F}\to A_\bot)を次で定義する。
\varphi(\phi)(x) := \llbracket{f}\rrbracket(\phi(x_1), \ldots, \phi(x_r))
ただし、f, x_iは唯一つ存在するx=f(x_1, \ldots, x_r)なるf, x_iである。
（このとき、\llbracket{f}\rrbracket:A_\bot^r\to A_\botは引数に一つでも\botがあれば\botを出力する関数とみなす。その際、\llbracket{f}\rrbracketは連続関数となる。）
このとき、\varphiが不動点を持つことを確かめるために、\varphiが連続関数となることを示す。
単調性について
\phi_1\le\phi_2\in(\overline{F}\to A_\bot)に対し、\varphi(\phi_1)\le\varphi(\phi_2)、つまり、\forall x\in\overline{F}, \varphi(\phi_1)(x)\le\varphi(\phi_2)(x)を示す。
flat cpoの定義より、
\varphi(\phi_1)(x)=\bot\text{ or }\varphi(\phi_1)(x)=\varphi(\phi_2)(x)
を示せばよい。
\varphi(\phi_1)(x)\not=\botとする。\llbracket{f}\rrbracketの定義より、各x_iで\phi_1(x_i)\not=\botが言える。今、\phi_1\le\phi_2だったので、各x_iで\phi_1(x_i)=\phi_2(x_i)となり、\varphi(\phi_1)(x)=\varphi(\phi_2)(x)が分かる。
連続性について
\forall D\subseteq(\overline{F}\to A_\bot):\text{directed}, \varphi(\sqcup D)=\sqcup\varphi(D)を示す。
（このとき、\varphi(D)が有向集合であることは、\varphiの単調性より保証される。）
ここで、poset Pにおける、みんな大好きな次の有名定理を用いる。
\forall d\in P, (a\le d\iff b\le d)\implies a = b
さらに、上限の性質 \sqcup D\le d_0\iff\forall d\in D, d\le d_0にも注意する。
（つまり、上記の定理を用いれば\sqcupを\forallと見なせるので、だいぶ議論がしやすくなる。）
\phi_0\in(\overline{F}\to A_\bot)を固定する。
\begin{array}{lll}
& \sqcup\varphi(D)\le\phi_0 & \\
\iff & \forall\phi\in D, \varphi(\phi)\le\phi_0 & \\
\iff & \forall x\in\overline{F}, \forall\phi\in D, \varphi(\phi)(x)\le\phi_0(x) & \\
\iff & \forall x\in\overline{F}, \forall\phi\in D, \llbracket{f}\rrbracket(\phi(x_1), \ldots, \phi(x_r))\le\phi_0(x) & \\
\iff & \forall x\in\overline{F}, \sqcup_{\phi\in D}\llbracket{f}\rrbracket(\phi(x_1), \ldots, \phi(x_r))\le\phi_0(x) & \\
\iff & \forall x\in\overline{F}, \llbracket{f}\rrbracket\sqcup_{\phi\in D}(\phi(x_1), \ldots, \phi(x_r))\le\phi_0(x) & \because \text{continuity of }\llbracket{f}\rrbracket\\
\iff & \forall x\in\overline{F}, \llbracket{f}\rrbracket(\sqcup_{\phi\in D}(\phi(x_1)), \ldots, \sqcup_{\phi\in D}(\phi(x_r)))\le\phi_0(x) & \because\text{property of sup in product cpo}\\
\iff & \forall x\in\overline{F}, \llbracket{f}\rrbracket(\sqcup{D}(x_1), \ldots, \sqcup{D}(x_r))\le\phi_0(x) & \because\text{property of sup in function cpo}\\
\iff & \forall x\in\overline{F}, \varphi(\sqcup D)(x)\le\phi_0(x) & \\
\iff & \varphi(\sqcup D)\le\phi_0 &
\end{array}
（上記の議論は、5, 6行目の同値変形が本質であり、事実上\llbracket{f}\rrbracketの連続性以外何も使っていない。つまり、その他の行は議論を\llbracket{f}\rrbracketの連続性に帰着させるためのおまけにすぎない。
しかし、\sqcupをほとんど\forallとして扱えることで、おまけ部分を機械的に変形できることが最大のメリットであり、本質部分にのみ着目できるようになる。
今回は非常に丁寧に記述したが、慣れてきたらおまけ部分はもっと簡略化してもよい。）
以上より、\varphiは連続関数となり、最小不動点\phi := \mathrm{fix}(\varphi)\in(\overline{F}\to A_\bot)を持ち、\varphiの定義より次を満たす。
\phi(x) = \llbracket{f}\rrbracket(\phi(x_1), \ldots, \phi(x_r))
このとき、\forall x\in\overline{F}, \phi(x)\not=\botが示せれば、\phiが命題の条件を満たす。
これは帰納原理を用いれば、次と同値であり、成り立つのは明らかである。
- \forall f\in F, \forall x_1, \ldots, x_r\in\overline{F}
\phi(x_i)\not=\bot\text{ for }1\le i\le r\implies\phi(f(x_1, \ldots, x_r))\not=\bot
一意性については、もし他に命題の条件を満たす\phi'があれば、これも\varphiの不動点になるため、\phiの最小性より、\phi\le\phi'となるが、\phi\in(\overline{F}\to A)から分かる\phiの（cpo (\overline{F}\to A_\bot)における）極大性より\phi=\phi'が言える。
\square
帰納的閉包のinitialityについて（圏の知識を微小に仮定）
集合U、集合F\subseteq\bigcup_{n\in\mathbb{N}}(U^n\to U)を固定します。
圏\mathbf{Set}において、関手G:\mathbf{Set}\to\mathbf{Set}を次で定義します。
G(a\xrightarrow{g} b) := \coprod_{f\in F}a^{r(f)}\xrightarrow{\coprod_{f\in F}g^{r(f)}}\coprod_{f\in F}b^{r(f)}
ただし、\coprodは集合の直和を表し、射a_1\xrightarrow{f_1}b, a_2\xrightarrow{f_2}bに対しては、一意に存在する射の直和（？）をa_1\coprod a_2\xrightarrow{[f_1, f_2]}bと書くとします。
さらに、a_1\xrightarrow{f_1}b_1, a_2\xrightarrow{f_2}b_2に対し、a_1\coprod a_2\xrightarrow{f_1\coprod f_2 := [\iota_1\circ f_1, \iota_2\circ f_2]}b_1\coprod b_2とします。
また、a^nでn個のaの直積を表すとします。
そのとき、帰納的閉包は関手Gの始代数(x, Gx\xrightarrow{[f]_{f\in F}}x)として得られます。
すなわち、G-代数(a, Ga\xrightarrow{\alpha}a)を対象に持ち、次を可換にする\mathbf{Set}の射a\xrightarrow{f}bを射(a, Ga\xrightarrow{\alpha}a)\xrightarrow{f}(b, Gb\xrightarrow{\beta}b)として持つ圏の始対象となります。
\begin{matrix}
Ga & \xrightarrow{Gf} & Gb \\
\downarrow{\alpha} & & \downarrow{\beta} \\
a & \xrightarrow{f} & b
\end{matrix}
G-代数(a, Ga\xrightarrow{\alpha}a)が始代数のとき、射Ga\xrightarrow{\alpha}aは同型射、\mathbf{Set}でいう全単射になります。
つまり、帰納的閉包はまさに（最小）不動点により得られることになります。
今、始代数は始対象なので、他の各G-代数に対して唯一の射を持ち、この性質をinitialityといいます。
initialityは「存在」と「一意性」からなる性質ですが、「存在」パートが再帰的定義に対応し、「一意性」パートが数学的帰納法に対応します。
「帰納法で定義する」という言い回しがされることがあり、一見「証明手法で定義するってどういうこと？」と思いますが、これは広義の帰納法の「存在」パートを定義に用いているという意味です。
このあたりは、Jacobsのチュートリアル論文に詳しく書いてありました。
代数と余代数について、具体例を豊富に用いてこれでもかというくらい丁寧な説明をしており、圏論の知識も原則不要なため誰でも読みやすいと思います。
規則帰納法
規則帰納法は重要なので、章を使い説明します。
ただし、前章の具体例にすぎないので、形式化にはこだわず簡単な説明のみで終わらせます。
この辺の厳密な取り扱いを知りたかったらWinskelの『プログラミング言語の形式的意味論入門』第三章を読むとよいです。
関係も帰納的閉包として定義することがあります。
例：関係の帰納的定義
\frac{}{\overline{n}\to n}
\frac{a\to n\quad b\to m}{\texttt{add}(a, b)\to n+m}
\frac{a\to n\quad b\to m}{\texttt{mult}(a, b)\to n\times m}
これは、「上の式が成り立つとき下の式が成り立つ」という形の規則の集合で関係\toの定義を表したものです。
特に、上の式が空欄のときは、無条件に下の式が成り立つことに注意してください。
今、\texttt{mult}(\texttt{add}(\overline{1}, \overline{3}), \overline{2})\to 8は上記の規則を用いることで導くことができます。
そこで、そのことを\vdash\texttt{mult}(\texttt{add}(\overline{1}, \overline{3}), \overline{2})\to 8と書き、判断と呼びます。
そのとき、\forall c, \forall n\in\mathbb{N}, (\vdash c\to n\implies 0\leq n)のように判断を仮定部に持つような命題は規則帰納法を用いることで証明ができます。
例：規則帰納法
-
\frac{}{\overline{n}\to n}のとき
-
c\equiv\overline{n}で、c\in\{\overline{0}, \overline{1}, \ldots\}より、0\le n
-
\frac{a\to n\quad b\to m}{\texttt{add}(a, b)\to n+m}のとき
-
帰納法の仮定より、0\leq n, mゆえ、0\leq n+m
-
\frac{a\to n\quad b\to m}{\texttt{mult}(a, b)\to n\times m}のとき
-
帰納法の仮定より、0\leq n, mゆえ、0\leq n\times m
このように、各規則の形ごとに場合分けをして、規則の上の式については帰納法の仮定を適用することができます。
規則帰納法と構造帰納法は適宜雰囲気で使い分けてください。ただ、規則帰納法が適用できそうな命題は大抵規則帰納法を用いたほうがうまく行きやすいです。
（上記の命題を\forall c, P(c)の形だからといって、cの構造帰納法で証明しようとするとどうなるかはご自分で確かめてみてください。）
おわりに
お疲れ様でした。ここまで読んでいただきありがとうございました。
このような話を厳密に議論している本は非常に少ないにかかわらず、このような分野では知らぬ間に常識として扱われていることが多い内容です。
ラムダ計算や論理学など形式体系を扱うどの分野でも知っておくべき事柄だと思いますので、もしも知らなかったということがありましたら、ぜひこの機会にしっかり理解して帰っていただければ幸いです。
改めて、本当にありがとうございました。
Discussion