翻訳完了

src/division_by_zero/README.md

@@ -51,16 +51,27 @@
 
 Lean チャットでこのことを愚痴ったところ，数学者の慣習の愚かさを指摘され，Lean 流の慣用的なやり方を教えられました．それは，負の数のようなゴミ入力を平方根関数に許可し，ゴミ出力を返すことです．非負の仮定は**定理**の中に置きます．例えば，$\sqrt{ab}=\sqrt{a}\sqrt{b}$ という定理には, $a,b\geq 0$ であるという仮定を持たせます．$ab\geq 0$ という仮定は持たせないことに注意してください．というのも，証明の中で導くことができるので，この定理のユーザにそれを示させる必要がないからです．これは関数に仮定を持たせる数学者流のアプローチとは対照的です．数学者流では，$\sqrt{\phantom{2}}$ という表記自体が非負性を要求するので，$ab\geq 0$ も示す必要がありました．
 
-## So you’re saying this crazy way is actually better?
+<!-- ## So you’re saying this crazy way is actually better? -->
+## じゃあ, このクレイジーなやり方の方が本当はいいってこと？
 
-No, not really. I’m saying that it is (a) mathematically equivalent to what we mathematicians currently do and (b) simply more convenient when formalising mathematics in dependent type theory.
+<!-- No, not really. I’m saying that it is (a) mathematically equivalent to what we mathematicians currently do and (b) simply more convenient when formalising mathematics in dependent type theory. -->
 
-What actually is a field anyway? For a mathematician, a field is a set $F$ equipped with $0,1,a+b,-a,a\times b,a^{-1}$ where the inversion function $a^{-1}$ is only defined for non-zero $a$. The non-zero elements of a field form a group, so we have axioms such as $x\times x^{-1}=1$ for $x\not=0$ (and this doesn’t even make sense for $x=0$). Let’s say we encountered an alien species, who had also discovered fields, but their set-up involved a function $\iota :F\to F$ instead of our $x^{-1}$. Their $\iota$ was defined, using our notation, by $\iota(x)=x^{-1}$ for $x\not=0$, and $\iota(0)=0$. Their axioms are of course just the same as ours, for example they have $x\times \iota(x)=1$ for $x\not=0$. They have an extra axiom $\iota(0)=0$, but this is no big deal. It’s swings and roundabouts — they define $a/b:=a\times\iota(b)$ and their theorem $(a+b)/c=a/c+b/c$ doesn’t require $c\not=0$, whereas ours does. They are simply using slightly different notation to express the same idea. Their $\iota$ is discontinuous. Ours is not defined everywhere. But there is a canonical isomorphism of categories between our category of fields and theirs. There is no difference mathematically between the two set-ups.
+いや, そこまで言っていません．私が言っているのは，(a) 私たち数学者が現在行っていることと数学的に同等であり，(b) 従属型理論で数学を形式化する際に，単純により便利であるということです．
 
-Lean uses the alien species convention. The aliens’ `\iota` is Lean’s `field.inv` , and Lean’s `field.div x y` is defined to be `field.mul (x, field.inv y)`.
+<!-- What actually is a field anyway? For a mathematician, a field is a set $F$ equipped with $0,1,a+b,-a,a\times b,a^{-1}$ where the inversion function $a^{-1}$ is only defined for non-zero $a$. The non-zero elements of a field form a group, so we have axioms such as $x\times x^{-1}=1$ for $x\not=0$ (and this doesn’t even make sense for $x=0$). Let’s say we encountered an alien species, who had also discovered fields, but their set-up involved a function $\iota :F\to F$ instead of our $x^{-1}$. Their $\iota$ was defined, using our notation, by $\iota(x)=x^{-1}$ for $x\not=0$, and $\iota(0)=0$. Their axioms are of course just the same as ours, for example they have $x\times \iota(x)=1$ for $x\not=0$. They have an extra axiom $\iota(0)=0$, but this is no big deal. It’s swings and roundabouts — they define $a/b:=a\times\iota(b)$ and their theorem $(a+b)/c=a/c+b/c$ doesn’t require $c\not=0$, whereas ours does. They are simply using slightly different notation to express the same idea. Their $\iota$ is discontinuous. Ours is not defined everywhere. But there is a canonical isomorphism of categories between our category of fields and theirs. There is no difference mathematically between the two set-ups. -->
 
-## OK so I can see that it can be made to work. Why do I still feel a bit uncomfortable about all this?
+体とは何かを考えてみましょう．数学では，体とは $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つの定義の間に数学的な違いはありません．
 
-It’s probably for the following reason. You are imagining that a computer proof checker will be checking your work, and in particular checking to see if you ever divided by zero, and if you did then you expect it to throw an error saying that your proof is invalid. What you need to internalise is that Lean is just using that function $f$ above, defined by $f(x,y)=x/y$ for $y\not=0$ and $f(x,0)=0$. In particular you cannot prove false things by applying $f$ to an input of the form $(x,0)$, because the way to get a contradiction by dividing by zero and then continuing will involve invoking theorems which are true for mathematical division but which are not true for $f$. For example perhaps a mathematician would say $a/a=1$ is true for all $a$, with the implicit assumption that $a\not=0$ and that this can be inferred from the notation. Lean’s theorem that `real.div a a = 1` is only proved under the assumption that $a\not=0$, so the theorem cannot be invoked if $a=0$. In other words, the problem simply shows up at a different point in the argument. Lean won’t accept your proof of $1=2$ which sneakily divides by $0$ on line 8, but the failure will occur at a different point in the argument. The failure will still however be the assertion that you have a denominator which you have not proved is nonzero. It will simply not occur at the point when you do the division, it will occur at the point where you invoke the theorem which is not true for `real.div`.
+<!-- Lean uses the alien species convention. The aliens’ `\iota` is Lean’s `field.inv` , and Lean’s `field.div x y` is defined to be `field.mul (x, field.inv y)`. -->
 
-Thanks to Jim Propp and Alex Kontorovich for bringing this up on Twitter. I hope that this clarifies things.
+Lean は今の話でいう異星人流の慣例を使っています．異星人の $ι$ は Lean の `field.inv` に相当します．そして体での割り算は，Lean では `field.div x y` であり，これは `field.mul (x, field.inv y)` として定義されています．
+
+<!-- ## OK so I can see that it can be made to work. Why do I still feel a bit uncomfortable about all this? -->
+## オーケー，それで上手くいくことはわかった. でも何故まだ違和感を感じるんだろう？
+
+<!-- It’s probably for the following reason. You are imagining that a computer proof checker will be checking your work, and in particular checking to see if you ever divided by zero, and if you did then you expect it to throw an error saying that your proof is invalid. What you need to internalise is that Lean is just using that function $f$ above, defined by $f(x,y)=x/y$ for $y\not=0$ and $f(x,0)=0$. In particular you cannot prove false things by applying $f$ to an input of the form $(x,0)$, because the way to get a contradiction by dividing by zero and then continuing will involve invoking theorems which are true for mathematical division but which are not true for $f$. For example perhaps a mathematician would say $a/a=1$ is true for all $a$, with the implicit assumption that $a\not=0$ and that this can be inferred from the notation. Lean’s theorem that `real.div a a = 1` is only proved under the assumption that $a\not=0$, so the theorem cannot be invoked if $a=0$. In other words, the problem simply shows up at a different point in the argument. Lean won’t accept your proof of $1=2$ which sneakily divides by $0$ on line 8, but the failure will occur at a different point in the argument. The failure will still however be the assertion that you have a denominator which you have not proved is nonzero. It will simply not occur at the point when you do the division, it will occur at the point where you invoke the theorem which is not true for `real.div`. -->
+
+それはおそらく次のような理由からでしょう．コンピュータの証明チェッカーがあなたのコードをチェックし, 特にゼロで割ったことがあるかどうかをチェックし，もし割ったことがあれば，証明が無効であるというエラーを投げるだろうと期待していませんか．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` に関して正しくない定理を呼び出した時点で起こるのです．
+
+<!-- Thanks to Jim Propp and Alex Kontorovich for bringing this up on Twitter. I hope that this clarifies things. -->
+ツイッターでこの件を取り上げてくれた Jim Propp と Alex Kontorovich に感謝します．これで物事が明確になることを願っています．