Division by zero in type theory: a FAQ 日本語訳

原文は Division by zero in type theory: a FAQ です．

ねえ, Lean では 1/0＝0 だって聞いたんだけど, 本当？

本当ですよ．Coq や Agda，その他多くの証明支援系と同じです．

それは矛盾にならないの？

いいえ．Lean の $/$ 記号が数学的な割り算を意味しないというだけです．$\mathbb{R}$ を実数全体とします．関数 $f:\mathbb{R}^2\to\mathbb{R}$ を $y\not=0$ に対しては $f(x,y)=x/y$ であり，$y=0$ のとき $f(x,0)=0$ を満たすようなものとして定義します．この定義が数学に矛盾をもたらすでしょうか？もちろんそんなことはありません！単なる定義です．Lean は $/$ 記号を $f$ の意味で使います．Coq や Agda と同じようにです．この関数は Lean では実際には $f$ ではなく，real.div と呼ばれます．

でも，混乱しない？

確かに Twitter では混乱を招いているようですね．しかし，証明支援系で数学を行うときに混乱することはありません．数学者は0で割り算をしませんから，real.div と数学的割り算（1/0 は定義されない）の違いに気づくことはないのです．実際，Lean における 1/0 の定義を気にしている数学者がいたとしたら，その理由を尋ねられるでしょう．知っての通り，数学では 0 での割り算は許されていませんから，数学をする上では関係ないはずだからです．実のところ，real.div と数学的な割り算は同じと考えてよいものです．すべての real.div に関する定理は数学的な割り算に翻訳できますし，逆も然りです．real.div を実装することは，数学的な割り算を実装することと等価です．

こんな慣例ばかげてる！

ゼロ除算以外にも例があります．自然数 $\lbrace 0,1,2,\ldots \rbrace$ には引き算 nat.sub が定義されていて，x - y と書きます．これは2つの自然数を与えられたら1つの自然数を返します．仮に x < y だったとしたら，x - y は 0 です．real.sqrt という関数もあり，これは実数を1つ与えられたら実数を1つ返します．$2$ を入力したら出力は $\sqrt{2}$ です．-1 を入力したら，何が返されるかはよくわかりませんが実数が返ってくることは保証されています．$0$ かもしれませんし，$1$ かもしれません．$37$ かも? どうだっていいことです．私は数学者であり，負の実数の平方根を取りたい場合 real.sqrt は使いません．なぜなら実数で答えを出したくないからです．一方で real.sqrt の型は ℝ → ℝ です．

数学者がやるような常識的な方法では何がまずいの？

素晴らしい質問ですね．2017 年に私は試してみました．証明支援系ではとても不便な方法だということがわかりました！

私が Lean を学んでいたときのことです．私は「普通の数学者」として，学部の証明入門コースに Lean を取り入れようと考えていました．私は当時定理証明の経験がなく, プログラミングの正式な素養もありませんでした．Lean での授業が実現可能か調査するために，学部生に配る予定だった問題集をすべて Lean でやってみました．これは Lean の数学ライブラリがもっと小さくて，real.sqrt がまだ存在していなかった 2017 年当時の話です．しかし sup と inf の基本理論は形式化されていたので，私は 0 以上の x に対して real.sqrt x を $\mathrm{Sup}\lbrace y\in\mathbb{R} ∣ y^2\leq x\rbrace$ として定義しました．そして，平方根関数を扱うのに必要な $\sqrt{ab}=\sqrt{a}\sqrt{b}$ や $\sqrt{a^2}=a$ や $\sqrt{a^2b}=a\sqrt{b}$ などの基本的な定理を証明しました．(ここで $a, b$ は非負実数です．私の定義した平方根関数は非負実数しか受け付けません．)

そして私の授業の問題集にあった $\sqrt{2}+\sqrt{3}<\sqrt{10}$ に取り掛かりました．電卓を使わずに，代数的な操作だけを使って証明せよという問題です．つまり，real.sqrt を使う問題です．言うまでもなく，私が使った定義では，$\sqrt{\phantom{2}}$ を使うたびに毎回平方根の中が非負であることを証明する必要があります．毎度毎度平方根が現れるたびにです．たとえ前の行で 2 > 0 を証明していても，次の行で $\sqrt{2}$ があればまた示す必要があるのです．もちろん証明は norm_num で済むのですが，私はすぐにこれをタイプするのが嫌になりました．

Lean チャットでこのことを愚痴ったところ，数学者の慣習の愚かさを指摘され，Lean 流の慣用的なやり方を教えられました．それは，負の数のようなゴミ入力を平方根関数に許可し，ゴミ出力を返すことです．非負の仮定は定理の中に置きます．例えば，$\sqrt{ab}=\sqrt{a}\sqrt{b}$ という定理には, $a,b\geq 0$ であるという仮定を持たせます．$ab\geq 0$ という仮定は持たせないことに注意してください．というのも，証明の中で導くことができるので，この定理のユーザにそれを示させる必要がないからです．これは関数に仮定を持たせる数学者流のアプローチとは対照的です．数学者流では，$\sqrt{\phantom{2}}$ という表記自体が非負性を要求するので，$ab\geq 0$ も示す必要がありました．

じゃあ, このクレイジーなやり方の方が本当はいいってこと？

いや, そこまで言っていません．私が言っているのは，(a) 私たち数学者が現在行っていることと数学的に同等であり，(b) 従属型理論で数学を形式化する際に，単純により便利であるということです．

体とは何かを考えてみましょう．数学では，体とは $0,1,a+b,-a,a\times b,a^{-1}$ を持つ集合 $F$ のことです．ただし逆元を取る操作 $a^{-1}$ はゼロでない $a$ に対してのみ定義されます．体のゼロでない要素は群を形成し，$x\not=0$ に対して $x\times x^{-1}=1$ という公理を満たします．($x = 0$ のときこれは意味をなしません)ここで我々が異星人と遭遇し，その異星人も体を発見していたとしましょう．しかし異星人の定義では，$x^{-1}$ ではなく関数 $\iota :F\to F$ を使用していたとします．その $\iota$ は，我々の表記法を用いると $x\not=0$ のとき $\iota(x)=x^{-1}$ で，$\iota(0)=0$ を満たすとします．もちろん異星人の公理は我々のものと同じで，たとえば $x\not=0$ に対して $x\times \iota(x)=1$ が成り立っています．異星人の体は追加の公理 $\iota(0)=0$ を持っていますが，これは大きな問題にはなりません．一長一短です． ーー 異星人流には $a/b:=a\times\iota(b)$ と定義され，彼らの定理 $(a+b)/c=a/c+b/c$ には我々が必要とするような $c\not=0$ という仮定が必要ありません．同じアイデアを表現するために，少し違った表記を使っているだけなのです．異星人の $\iota$ は不連続です．我々のは体全体で定義されていません．しかし彼らの体の圏と我々の体の圏の間には，正準な同型があります．2つの定義の間に数学的な違いはありません．

Lean は今の話でいう異星人流の慣例を使っています．異星人の $ι$ は Lean の field.inv に相当します．そして体での割り算は，Lean では field.div x y であり，これは field.mul (x, field.inv y) として定義されています．

オーケー，それで上手くいくことはわかった. でも何故まだ違和感を感じるんだろう？

それはおそらく次のような理由からでしょう．コンピュータの証明チェッカーがあなたのコードをチェックし, 特にゼロで割ったことがあるかどうかをチェックし，もし割ったことがあれば，証明が無効であるというエラーを投げるだろうと期待していませんか．Lean は上記の $y\not=0$ に対しては $f(x,y)=x/y$ であり，$y=0$ のとき $f(x,0)=0$ と定義された関数 $f$ を使っているだけであることを思い出す必要があります．特に, $(x,0)$ の形の入力に $f$ を適用することで誤ったことを証明することはできません．数学の割り算ではゼロで割ってから続けることで矛盾が得られますが，$f$ では得られません．例えば, 数学者が $a/a=1$ はすべての $a$ に対して真であると言っているとき，$a\not=0$ という暗黙の前提があり，これは表記から推測できます．real.div a a = 1 という Lean の定理は, $a\not=0$という仮定の下でのみ証明されるので, $a=0$ の場合は定理を使えません．言い換えれば，ゼロ除算の問題が現れる場所が変わるだけなのです．Lean は $0$ でこっそり割ることで $1=2$ を示そうとする証明を受け入れませんが，エラーはゼロで割るときではなく別のところで起きるでしょう．ゼロでないことを証明していない分母があるということが問題になるのは変わりません．問題は単に割り算をした時点で起こるのではなく，real.div に関して正しくない定理を呼び出した時点で起こるのです．

ツイッターでこの件を取り上げてくれた Jim Propp と Alex Kontorovich に感謝します．これで物事が明確になることを願っています．