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

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

TAPL 21章によれば

$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$ を示すのがゴールです。
  • そのため、$X$ の規則にしたがって以下を確認します。
    • $0 \in \mathbb{N}$
      • $F$ の $\{0\}$ 規則と、$F(\mathbb{N}) \subseteq \mathbb{N}$ からわかります。
    • $0 = 0(0 + 1) / 2$
      • 実際に計算すると両辺が同じになるのでOKです。
• $\{S\ n \mid n \in X\}$ の規則の場合
  • この規則の前提より $n \in X$ であることがわかっています。ここから以下がわかります。
    • $n \in \mathbb{N}$（1）
    • $0 + 1 + \dots + n = n(n + 1) / 2$（帰納法の仮定）
  • この規則で生成される要素は $S\ n$ なので、$S\ n \in X$ を示すのがゴールです。
  • そのため、$X$ の規則にしたがって以下を確認します。
    • $S\ n \in \mathbb{N}$
      • （1）と $F$ の $\{S\ n \mid n \in X\}$ 規則と、$F(\mathbb{N}) \subseteq \mathbb{N}$ からわかります。
    • $0 + 1 + \dots + S\ n = (S\ n)(S\ n + 1) / 2$
      • 左辺から出発します。
      • $0 + 1 + \dots + S\ n$
      • $= 0 + 1 + \dots + n + S\ n$
      • 帰納法の仮定より、
      • $= n(n + 1) / 2 + (S\ n)$
      • $= n(S\ n) / 2 + (S\ n)$
      • $= (n(S\ n) + 2(S\ n)) / 2$
      • $= (S\ n)(n + 2) / 2$
      • $= (S\ n)(S\ n + 1) / 2$
      • 右辺と同じになったのでOKです。

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

$\mu F$ は $\mathbb{N}$ で、$X$ は等式が成り立つような $n$ の集合でした。

つまり $n \in \mathbb{N}$ ならば、$n \in \text{等式が成り立つnの集合}$ です。したがって、今回の等式は自然数全体で成り立つと言えます。

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

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

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

と取ります。

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

• $X$ の規則は $\{\infty\}$ だけなので、要素は $\infty$ だけです。
• なので、$\infty \in F(X)$ がゴールです。
• $\infty$ の定義より
• $S\ \infty \in F(X)$
• $\infty \in X$ と $F$ の $\{S\ n \mid n \in X\}$ 規則よりOKです。

というわけで、$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)$ の要素でもあることを示します。

• $X$ の規則は $\{(\infty + n, \infty) \mid n \in \mathbb{N} \cup \{\infty\}\}$ だけなので、要素は $(\infty + n, \infty)$ という形です。
  • また規則の前提より $n \in \mathbb{N} \cup \{\infty\}$ です（1）
• なので、$(\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$
• （1）と $X$ の $\{(\infty + n, \infty) \mid n \in \mathbb{N} \cup \{\infty\}\}$ 規則により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$ についての帰納法で示すという方針もあるそうです。ただ、この方針で行ける場合と行けない場合があるらしいです。

まとめ

帰納法と余帰納法の気持ちになってみました。

数年前にTAPLの21章を読んだときよりは理解が進んだように思います。そういえば、同じく数年前に読んだSICPの3章にも、余データっぽいやつがいたなぁという気持ちで、数年経っても味がするのは良い本だからだろうなと思います。

ここから圏論方面に進むと、双対性についてより深く理解できるそうです。試しに始代数や終余代数について調べてみたのですが、圏論の基礎が無いので？？？になってしまいました。機会があれば、今回のように順を追って理解してみたいところです。

議論の一部は、Rocqで確認しています。プログラミングとか証明とかは、型検査なしだと99割くらいミスる体質なんですよね。太古の昔はJSを書いてたのでどうやってたんだろ？と思い返してみたのですが、普通に99割バグってただけな気がしてきました。

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

近所のスーパーで299円（税抜き）でした。

参考文献

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