帰納法と余帰納法の気持ち

圏論を使わずに（使えずに）、帰納法と余帰納法の気持ちになるですよ。

TAPLによれば

$U$ を普遍集合、$P(U)$ を $U$ の冪集合、$X$ を $P(U)$ の要素（$U$ の部分集合）とし、$F$ は $P(U)$ から $P(U)$ への関数で生成関数と呼びます。

クナスター・タルスキの定理から、¹

• $\mu F = \bigcap \{X \mid F(X) \subseteq X\}$
• $\nu F = \bigcup \{X \mid X \subseteq F(X)\}$

とのことです。ここで、$\mu F$ は $F$ の最小不動点、$\nu F$ は $F$ の最大不動点を表します。

帰納法とは、ある $F$ と $X$ について $F(X) \subseteq X$ を示すことで、$\mu F \subseteq X$ を主張することらしいです。

余帰納法とは、ある $F$ と $X$ について $X \subseteq F(X)$ を示すことで、$X \subseteq \nu F$ を主張することらしいです。

？？？

まったく意味がわからないので、順番に考えてみます。

不動点

普遍集合を、以下の文法規則で生成される有限および無限の要素の集合とします。

• $U ::=$
  • $0$
  • $\text{バナナ}$
  • $S\ U$

$U$ の部分集合は、例えば以下のようなものが考えられます。

ここで、$\infty$ は $S\ S\ S\ \dots$ と限りなく続くやつで、$\infty = S\ \infty$ とします。

生成関数 $F$ を以下のようにします。

$F$ の不動点とは、$X = F(X)$ となる $X$ のことです。これは以下の2つの条件に分解できます。

• $F(X) \subseteq X$
  • 気持ち：$F$ によって生成可能なら、$X$ に含まれる
• $X \subseteq F(X)$
  • 気持ち：$X$ に含まれるなら、$F$ によって生成可能

実際に、さきほどの集合が不動点かどうか確認してみます。

• ❌ $F(X) \subseteq X$ でない
• ✅ $X \subseteq F(X)$ である

• ❌ $F(X) \subseteq X$ でない
• ✅ $X \subseteq F(X)$ である

• ❌ $F(X) \subseteq X$ でない
• ❌ $X \subseteq F(X)$ でない

• ✅ $F(X) \subseteq X$ である
• ✅ $X \subseteq F(X)$ である

• ✅ $F(X) \subseteq X$ である
• ❌ $X \subseteq F(X)$ でない

• ✅ $F(X) \subseteq X$ である
• ✅ $X \subseteq F(X)$ である

候補のうち、不動点は以下の2つでした。小さい方は自然数そのもので最小不動点、大きい方は自然数に $\infty$ を足したもの（余自然数）で最大不動点となるらしいです。

• $\mu F = \mathbb{N} = \{0, S\ 0, \dots\}$
• $\nu F = \mathbb{N} \cup \{\infty\} = \{0, S\ 0, \dots, \infty\}$

帰納法の例

すべての自然数 $n$ について、$0 + 1 + \dots + n = n(n + 1) / 2$ が成り立つことを言いたいとします。$X$ を

と取ります。

$F(X) \subseteq X$ を示します。$F(X)$ の各要素が $X$ の要素でもあることを示します。

• $F(X)$ の要素について、生成に使った規則で場合分けします。
• $\{0\}$ の規則の場合
  • この規則で生成される要素は $0$ です。
  • $0 \in X$ を示します。$0 \in \mathbb{N}$ であり、$0 = 0(0 + 1) / 2$ なのでOKです。
• $\{S\ n \mid n \in X\}$ の規則の場合
  • この規則で生成される要素は $S\ n$ の形です。
  • $n \in X$ であることがわかっています。ここから以下がわかります。
    • $n \in \mathbb{N}$
    • $0 + 1 + \dots + n = n(n + 1) / 2$（帰納法の仮定）
  • $S\ n \in X$ を示します。$S\ n \in \mathbb{N}$ は自明です。等式が成り立つのは以下でわかります。
    • $0 + 1 + \dots + S\ n = (S\ n)(S\ n + 1) / 2$
    • $0 + 1 + \dots + n + S\ n = (S\ n)(S\ n + 1) / 2$
    • 帰納法の仮定で左辺を書き換えます。
    • $n(n + 1) / 2 + S\ n = (S\ n)(S\ n + 1) / 2$
    • $n(n + 1) / 2 + S\ n = (S\ n)(n + 2) / 2$
    • $n(n + 1) / 2 + S\ n = (S\ n)n / 2 + (S\ n)$
    • $n(n + 1) / 2 = (S\ n)n / 2$
    • $n(n + 1) / 2 = n(n + 1) / 2$
    • 両辺が同じなので成り立ちます。

というわけで、$F(X) \subseteq X$ である $X$ が1つ見つかりました。クナスター・タルスキの定理より、$F(X) \subseteq X$ である他の集合も全部見つけてきて共通部分を取る（要素を減らす）と $\mu F$ になるらしいので、$\mu F$ は $X$ より小さいか、あるいは同じです（今回の例では同じです）。なので $\mu F \subseteq X$ が主張できます。

つまり、

なので、$0 + 1 + \dots + n = n(n + 1) / 2$ は自然数全体でも成り立つと言えます。

今思い返してみると、確かに高校の数学の時間にやらされたような内容になっていますね。

余帰納法の例1：シンプルなやつ

$\infty$ が $\nu F$ に含まれることを確認してみます。ここまでの議論で明らかなのですが、余帰納法の流れを体感するためにシンプルな例で試します。$X$ を

と取ります。

$X \subseteq F(X)$ を示します。$X$ の各要素が $F(X)$ の要素でもあることを示します。

今回の $X$ の要素は $\infty$ だけです。$\infty \in X$ と $\{S\ n \mid n \in X\}$ 規則より $S\ \infty \in F(X)$ ですが、$S\ \infty = \infty$ なので、結局 $\infty \in F(X)$ です。

というわけで、$X \subseteq F(X)$ である $X$ が1つ見つかりました。クナスター・タルスキの定理より、$X \subseteq F(X)$ である他の集合も全部見つけてきて和集合を取る（要素を増やす）と $\nu F$ になるらしいので、$\nu F$ は $X$ より大きいか、あるいは同じです。なので $X \subseteq \nu F$ が主張できます。

したがって、$\infty \in \nu F$ です。

余帰納法の例2：双模倣

$n \in \mathbb{N} \cup \{\infty\}$ として、$\infty + n = \infty$ を言いたいと思います。

ここでは双模倣によってこれを示してみたいと思います。双模倣とは、観測（生成の逆、ここでは例えば $S$ の構造に着目したり、その結果 $S$ を1つ剥がして中身を取り出したりする操作）によって区別できないことで同じとみなす、という考え方らしいです。

ここでは普遍集合を $U \times U$ に取り替えます。$X$ を2項関係として、そのような関係の生成関数 $G$ を

とおきます。特に最後の規則は、両方から $S$ が1つ剥がせて、さらにその中身も観測によって区別できないのならもとのペアも区別がつかない、という意味になっています。

こうすると、$\nu G$ は観測によって区別できないペアが最大限集まった集合になるので、$(n, m) \in \nu G$ のとき、$n = m$ とみなすことにします。

足し算を以下のように定義しておきます。²

• $0 + m = m$
• $\text{バナナ} + m = m$
• $S\ n + m = S\ (n + m)$

今回示したい2項関係である $X$ を

と取ります。

$X \subseteq G(X)$ を示します。$X$ の各要素が $G(X)$ の要素でもあることを示します。

• $(\infty + n, \infty) \in G(X)$ がゴールです。
• $\infty$ の定義より
• $(S\ \infty + n, S\ \infty) \in G(X)$
• 足し算の定義より
• $(S\ (\infty + n), S\ \infty) \in G(X)$
• $G$ の $\{(S\ n, S\ m) \mid (n, m) \in X\}$ 規則より
• $(\infty + n, \infty) \in X$
• $X$ の定義そのものなのでOKです。

というわけで $X \subseteq G(X)$ から $X \subseteq \nu G$ が主張でき、$X$ のペアは観測によって区別できないので、$\infty + n = \infty$ と言えます。

帰納法では？

何らかの $X$ について、$G(X) \subseteq X$ を示す方針を考えてみます。$\infty$ を含むペアを持たない $G$ の不動点が以下のように見つかり、

最小不動点である $\mu G$ も同様です。なので、$\mu G \subseteq X$ から $\infty + n = \infty$ とは主張できません。

他には「$\infty + n$ と $\infty$ は、深さ $k$ まで観測すると一致する」ことを、$k$ についての帰納法で示すという方針もあるそうです。ただ、この方針で行ける場合と行けない場合があるらしいです。

まとめ

わかったようなわかってないような気持ちになりました。

ここから圏論方面に進むと、双対性についてより深く理解できるそうです。始代数や終余代数について調べてみましたが、僕は圏論がなにもわからないので、なにもわからないという結果となってしまいました。

証明の構成についても99割くらいミスるので、Opus先輩にRocqで確認してもらいました。

冒頭の画像は、この分野で有名な余帰納京子という架空のキャラクターの好物と思われるラムレーズンです。

参考文献

Pierce, Benjamin C. 型システム入門 プログラミング言語と型の理論. 株式会社 オーム社, 2013.