帰納法と余帰納法の何がどう双対なのか（初等的に）
（高校で習うはずの）数学的帰納法をはじめとする帰納法(induction)と、（π計算など並行プロセス計算に出てくる）双模倣(bisimulation)をはじめとする余帰納法(coinduction)は、双対(dual)であると言われます（例）。双対というのは、大雑把に言うと、論理式のド・モルガンの法則 ¬（A∨B） ⇔ ¬A∧¬B と ¬（A∧B） ⇔ ¬A∨¬B のように、何か一組のもの（ここでは∧と∨）をひっくり返しても同じ式が成り立つという関係です（例）。
しかし、自分は学部4年ぐらいのときに余帰納法（というか双模倣）を習って、「（数学的帰納法のような）帰納法と（双模倣のような）余帰納法が双対」と聞いても、何となく「余帰納法は結論を仮定する(?)から、仮定を仮定する(?)帰納法と反対なのかなあ」と思うぐらいで、恥ずかしながら何が双対なのかよくわかりませんでした。かといって、詳しい人に「何が双対なんですか」と下手に聞くと、高い確率で「始代数と終余代数が…」みたいなカテゴリー理論的(?)説明をされてしまい、それはそれで面白いし落ち着いて確かめれば形式的には（＝字面上は）意外と簡単(?)なのですが、（当時の）自分にとっては「数学的帰納法と双模倣の何が双対なのか」という素朴な疑問に対してピンと来る答にはなりませんでした。
仕方がないので（当時の）自分なりに思案した説明が以下です。教科書的定義から繰り返すと長くなってしまうので、単調関数の最小不動点と最大不動点がどうとかいう話は知っているとします（詳しく知りたい人はTAPLの21.1節がわかりやすいと思います。その章の元になった論文の2節も、短いですが証明以外の大まかな内容はほぼ同じです）。すると、例えば自然数の集合Nは
- 0∈X
- ∀n.n∈X⇒n+1∈X
（の両方）を満たす最小の集合X、すなわち
- F(X) = {0}∪{n+1 | n∈X}
なるFの最小不動点と定義されます。高校で習う（はずの）いわゆる数学的帰納法（すなわち自然数に関する帰納法）は、自然数に関する命題（すなわち自然数の集合）Pが
- 0∈P
- ∀n.n∈P⇒n+1∈P
（の両方）を満たせば∀n∈N.n∈Pを満たす、という（自然数の集合Nの）性質を利用した証明法です。これは論理的に
- 集合PがP⊇F(P)を満たせばN⊆Pを満たす … (1)
と言いかえられるので、「NはX⊇F(X)を満たす最小の集合X」という自然数（の集合）の定義にも合います。
これに対し、余帰納法は、単調関数Fの最大不動点S（すなわちX⊆F(X)なる最大のX）に対し、
- 集合RがR⊆F(R)を満たせばS⊇Rを満たす … (2)
という性質を利用した証明法です。具体例としては、プロセスの組の集合（すなわちプロセス上の二項関係）Xに対し
- F(X) = {(p,q) | ∀p'.p→p'⇒∃q'.q→q'∧(p',q')∈X}
とすると、Fの最大不動点Sはプロセスの模倣性(similarity)関係になります（ただし、→はプロセスの遷移を表す二項関係で、ここでは詳しく定義しません）。これを用いて、例えばあるプロセスp1が別のプロセスq1を模倣(simulate)することを示したかったら、(p1,q1)∈RかつR⊆F(R)なるRを一つ「発見」する（ないし「構成」する）ことができれば、(2)よりS⊇Rなので、めでたく(p1,q1)∈Sが言えます。
(1)と(2)は見た目から明らかに「双対っぽい」ですし、教科書的説明に出てくる式ですが、それらの「使い方」も
- 帰納法は「集合Pに対し、Fの最小不動点Nに属する任意の要素nが、Pに属する」ことを示したいときに使う … (1')
- 余帰納法は「集合Rに対し、Rに属する任意の要素(p,q)が、Fの最大不動点Sに属する」ことを示したいときに使う … (2')
と言えば「双対っぽい」感じになります（もちろん、(p,q)とかはあくまで例で、一般に組である必要はありません）。
細かい用語や記法は「いいかげん」ですし、すぐにわかる人には当たり前すぎる話かもしれませんが、（昔の）自分はすぐにわからなかったので、ひょっとしたら他人の参考になるかもしれないと思い恥を忍んで(?)久しぶりにエントリを書いてみました。最近の老化により記憶（と認知）が怪しい（笑）ので、何か大ボケ（ないし小ボケ）があったら是非ともご指摘ください。(_ _)
