私の趣味は数学の証明のリファクタリングである。教科書に書かれた数学の証明は、まずはそのまま、書かれた通りに理解すればよいのだが、自分で書き直すことによって「より深く理解できた」という満足感が得られることが多い。この作業を、プログラミングにおけるリファクタリングになぞらえて私はそう呼んでいる。
リファクタリングを行なっている間は楽しいのだが、いざ出来上がってみると完成品ばかり眺めてしまい、振り返って過程を追うのはなかなか億劫になる。今回は、あえてそれを書き記してみる。
クラトフスキの流儀による順序対の集合論的コーディング\[(a,b)=\{\{a\},\{a,b\}\}\]の妥当性に関する証明を例にとる。リファクタリング前の証明は下記の通り。
【命題】\[\{\{a\},\{a,b\}\}=\{\{a'\},\{a',b'\}\}\tag{★}\]ならば\[a=a'かつb=b'\]である。
・\(a=b\)のとき：
★の左辺は\(\{\{a\},\{a,a\}\}\)すなわち\(\{\{a\}\}\)、あるいは\(\{\{b\}\}\)とも書けるから、\(\{\{a\}\}=\{\{b\}\}=\{\{a'\},\{a',b'\}\}\)により\(\{a\}=\{b\}=\{a'\}=\{a',b'\}\)、したがって\(a=b=a'=b'\)である。
・\(a\neq b\)のとき：
★から\(\{a\}\)は\(\{a'\},\{a',b'\}\)の少なくとも一方に等しいが、もしも後者に等しければ\(a=a'=b'\)から★の右辺は\(\{\{a\}\}\)となり、すると★から\(\{a,b\}=\{a\}\)となってしまい\(a\neq b\)に反する。よって\(\{a\}=\{a'\}\)から\(a=a'\)を得る。
再び★から\(\{a,b\}\)は\(\{a'\},\{a',b'\}\)の少なくとも一方に等しいが、前者は\(a\neq b\)に反するので\(\{a,b\}=\{a',b'\}\)である。すると\(b\)は\(a',b'\)の少なくとも一方に等しいが、すでに\(a=a'\)が言えていることにより、前者は\(a\neq b\)に反する。したがって\(b=b'\)である。■
（この証明は田中康友『集合論』を参考に、途中までリファクタリングしたもの。）
上の方法の特徴は、\(\{a,b\}\)が2点集合とは限らない（\(a=b\)かもしれない）ことに留意して、見た目に惑わされてしまいそうなケースを先に済ませていることである。それならばもっと「\(a\neq b\)のときは惑わされずに済む」という恩恵にあずかろう、という欲求が生じてくる。★の成立のもとでは\[\begin{array}{ccc}a\neq b\mbox{（$\{a,b\}$は2点集合）}&\Leftrightarrow&\{a\}\neq\{a,b\}\mbox{（★の左辺は2点集合）}\\&&\Updownarrow\mbox{（★）}\\a'\neq b'\mbox{（$\{a',b'\}$は2点集合）}&\Leftrightarrow&\{a'\}\neq\{a',b'\}\mbox{（★の右辺は2点集合）}\end{array}\]という同値関係があるので、\(a\neq b\)のときは★の両辺ともに見た目の通り「1点集合と2点集合からなる、2点集合」になる。サイズの異なる集合同士が等しくなることはないから\(\{a\}=\{a'\}\)かつ\(\{a,b\}=\{a',b'\}\)、前者から\(a=a'\)、すると後者（2点集合同士）において\(b\)に等しい相手は\(b'\)となる。このように証明すれば、三度繰り返される「\(a\neq b\)に反する」を一度も言う必要がなくなる。これがリファクタリング案の一つ目である。
別の案を検討するために、もとの証明の「・\(a\neq b\)のとき」の前半を見返してみよう。ここでは\(a=a'\)を示すことが目標となっているが、途中の
もしも後者に等しければ\(a=a'=b'\)から（中略）\(a\neq b\)に反する。
という箇所では奇妙なことが起こっている。本来は「こんなケースは起こり得ない」ということを言いたいわけだが、よく読むと（目標であるはずの）\(a=a'\)が言えてしまっている。それならば「もしも後者に等しければ\(a=a'(=b')\)である。前者に等しい場合も……」で済ませてしまってはいけないのだろうか？実際に起こり得ないケースで何かが成り立つと主張するのはいかにも気持ちが悪いが、論証としては何ら問題ない。我々が普段行なっている場合分けにおいても、起こり得ないことに気づかずに証明しているかもしれない。「起こらないことは起こらないと分かる証明のほうが明瞭でよろしい」という立場もあるが、今回の証明において「起こらない」ことの根拠となる「\(a\neq b\)」という前提は、そもそも自分で導入したものである。つまり、少なくとも\(a=a'\)を言うまでは、「\(a=b\)か\(a\neq b\)か」で分ける必要がなかったことになる。実際に書き直してみると、例えば次のようになる：
★から\(\{a\}\)は\(\{a'\},\{a',b'\}\)の少なくとも一方に等しいが、いずれにせよ\(\{a\}\ni a'\)となるので\(a=a'\)である。
\(a=b\)かどうかで分けるのは、この後からでも遅くない。しかしここまで来ると、「後半部に残る二箇所の『\(a\neq b\)に反する』も消してしまえるのではないか？そうすれば\(a=b\)か否かは全く無関係になるのではないか？」という欲が出てくる。最後の箇所を先に検討してみよう。ここでは\(\{a,b\}=\{a',b'\}\)と\(a=a'\)を用いて\(b=b'\)を導いているが、果たしてこれは\(a\neq b\)の場合に限った話だろうか？いま\(b\in\{a',b'\}\)かつ\(\{a,b\}\ni b'\)であることに注意すると、かりに\(b\neq b'\)とすれば\(b=a'\)かつ\(a=b'\)となって\(a=a'\)に矛盾するのであり、この議論には\(a\neq b\)であることを使っていない。一般に、次の補題が成り立つ。
【補題】\(\{p,q\}=\{p,r\}\)ならば、\(q=r\)である。
（証明）\(q\neq r\)と仮定すると\(q=p=r\)となり矛盾。■
このように補題を見通したうえで、残る箇所に目を向けると、全く同じ構造の議論が適用できることに気づく。すなわち\(\{\{a\},\{a,b\}\}=\{\{a'\},\{a',b'\}\}\)と\(\{a\}=\{a'\}\)から\(\{a,b\}=\{a',b'\}\)を導きたいわけだが、\(\{a\}=\{a'\}\)を\(p\)、\(\{a,b\}\)を\(q\)、\(\{a',b'\}\)を\(r\)と見ればよい。以上により、\(a\neq b\)に依存する議論は完全に抹消できたことになる。後半部の証明を書き直すと、例えば次のようになる：
\(a=a'\)を★に反映すると\[\{\{a\},\{a,b\}\}=\{\{a\},\{a,b'\}\}\]となる。これに補題を適用すると\(\{a,b\}=\{a,b'\}\)、再度適用すると\(b=b'\)となる。■
プログラミングにおけるリファクタリングの楽しさを知っている人にとっては、「証明リファクタリングの快感も似たようなものである」という感想を抱くのではないだろうか。
