Division by zero in type theory: a FAQ 日本語訳
ねえ, Lean では 1/0=0 だって聞いたんだけど, 本当?
本当ですよ.Coq や Agda,その他多くの証明支援系と同じです.
それは矛盾にならないの?
いいえ.Lean の real.div
と呼ばれます.
でも,混乱しない?
確かに Twitter では混乱を招いているようですね.しかし,証明支援系で数学を行うときに混乱することはありません.数学者は0で割り算をしませんから,real.div
と数学的割り算(1/0
は定義されない)の違いに気づくことはないのです.実際,Lean における 1/0
の定義を気にしている数学者がいたとしたら,その理由を尋ねられるでしょう.知っての通り,数学では 0
での割り算は許されていませんから,数学をする上では関係ないはずだからです.実のところ,real.div
と数学的な割り算は同じと考えてよいものです.すべての real.div
に関する定理は数学的な割り算に翻訳できますし,逆も然りです.real.div
を実装することは,数学的な割り算を実装することと等価です.
こんな慣例ばかげてる!
ゼロ除算以外にも例があります.自然数 nat.sub
が定義されていて,x - y
と書きます.これは2つの自然数を与えられたら1つの自然数を返します.仮に x < y
だったとしたら,x - y
は 0
です.real.sqrt
という関数もあり,これは実数を1つ与えられたら実数を1つ返します.-1
を入力したら,何が返されるかはよくわかりませんが実数が返ってくることは保証されています.real.sqrt
は使いません.なぜなら実数で答えを出したくないからです.一方で real.sqrt
の型は ℝ → ℝ
です.
数学者がやるような常識的な方法では何がまずいの?
素晴らしい質問ですね.2017 年に私は試してみました.証明支援系ではとても不便な方法だということがわかりました!
私が Lean を学んでいたときのことです.私は「普通の数学者」として,学部の証明入門コースに Lean を取り入れようと考えていました.私は当時定理証明の経験がなく, プログラミングの正式な素養もありませんでした.Lean での授業が実現可能か調査するために,学部生に配る予定だった問題集をすべて Lean でやってみました.これは Lean の数学ライブラリがもっと小さくて,real.sqrt
がまだ存在していなかった 2017 年当時の話です.しかし sup と inf の基本理論は形式化されていたので,私は 0 以上の x
に対して real.sqrt x
を
そして私の授業の問題集にあった real.sqrt
を使う問題です.言うまでもなく,私が使った定義では,2 > 0
を証明していても,次の行で norm_num
で済むのですが,私はすぐにこれをタイプするのが嫌になりました.
Lean チャットでこのことを愚痴ったところ,数学者の慣習の愚かさを指摘され,Lean 流の慣用的なやり方を教えられました.それは,負の数のようなゴミ入力を平方根関数に許可し,ゴミ出力を返すことです.非負の仮定は定理の中に置きます.例えば,
じゃあ, このクレイジーなやり方の方が本当はいいってこと?
いや, そこまで言っていません.私が言っているのは,(a) 私たち数学者が現在行っていることと数学的に同等であり,(b) 依存型理論で数学を形式化する際に,単純により便利であるということです.
体とは何かを考えてみましょう.数学では,体とは
Lean は今の話でいう異星人流の慣例を使っています.異星人の field.inv
に相当します.そして体での割り算は,Lean では field.div x y
であり,これは field.mul (x, field.inv y)
として定義されています.
オーケー,それで上手くいくことはわかった. でも何故まだ違和感を感じるんだろう?
それはおそらく次のような理由からでしょう.コンピュータの証明チェッカーがあなたのコードをチェックし, 特にゼロで割ったことがあるかどうかをチェックし,もし割ったことがあれば,証明が無効であるというエラーを投げるだろうと期待していませんか.Lean は上記の real.div a a = 1
という Lean の定理は, real.div
に関して正しくない定理を呼び出した時点で起こるのです.
ツイッターでこの件を取り上げてくれた Jim Propp と Alex Kontorovich に感謝します.これで物事が明確になることを願っています.
訳者: @Seasawher
Discussion