2018年8月24日金曜日

1/0 = 0 ゼロ除算　DIVISION By ZERO

1/0 = 0 ゼロ除算　DIVISION By ZERO

NEW !
テーマ：

1/0 = 0

 Posted on
Have a tweet:
Picture of original tweet, name blacked out
I have no idea if Pony is making the right choice here, I don’t know Pony, and I don’t have any interest in learning Pony. But this tweet raised my hackles for two reasons:
  1. It’s pretty smug. I have very strong opinions about programming, but one rule I try to follow is do not mock other programmers.1 Programming is too big and I’m too small to understand everything. Disagreeing is fine, laying out why people are wrong is fine, making fun of them is not fine.
  2. It’s saying that Pony is mathematically wrong. This is objectively false.
I tweeted a thing about why 1/0 = 0 is mathematically sound. Some people agreed, some people agreed with caveats, and some people called it bunk. A few people said it’s clear I don’t know real mathematics, because a real mathematician would never make such a mistake.
So in this post I’d like to clearly, formally lay out why it’s consistent to say that 1/0 = 0, why some of the common objections don’t apply, and what the real mathematicians say. Fair warning, this post is going to be a little more mathematically dense than my usual stuff. I’ve tried to make it clear but, well, math.

Consistency

First we need to explain what we mean by “consistency”. The formalism is sound if you can only use it to prove true statements. To say 1/0 = 0 is unsound is to either say that we can prove 1/0 ≠ 0 or that, given 1/0 = 0, we can prove something that’s false. These are actually equivalent statements but it’ll be useful to treat them as distinct for teaching purposes.
Next we need to explain what we mean by “division”. But to do that, I need to introduce fields.

Fields

A field is a set of elements (S) along with an addition operator (+) and a multiplication operator (*) that follow some properties:
  1. The set is closed under both operations. If x is an element of S and y is an element of S, then both x + y and x * y are elements of S.
  2. Both operations are commutative. a + b = b + a, and a * b = b * a.
  3. Both operations are associative. a + (b + c) = (a + b) + c, and a * (b * c) = (a * b) * c.
  4. Multiplication is distributive. a * (b + c) = a * b + a * c.
  5. There is an element that is the additive identity, or 0, such that a + 0 = a.
  6. There is an element that is the multiplicative identity, or 1, such that a * 1 = a.
  7. The two identities are different elements. 1 ≠ 0.
  8. Every element has an additive inverse, -a, such that a + (-a) = 0.
  9. Every element EXCEPT 0 has a multiplicative inverse, a⁻, such that a*a⁻ = 1.
These are all of the rules of a field. We can define S, +, and * any way we want, as long as all of the rules are followed. The real numbers, along with our conventional notion of addition and multiplication, form a field. This gives us the building blocks to discover properties of our system. In order to prove a theorem, we need to be able to derive it solely through the definitions of S/+/*, the definition of a field, and any axioms we have.2 For example, we can prove that for all a, a * 0 = 0:
  1. By the additive identity, 0 + 0 = 0, so a * 0 = a * (0 + 0)
  2. By the distributive property, a * (0 + 0) = a * 0 + a * 0
  3. By the additive inverse property, there is some - (a * 0) such that - (a * 0) + (a * 0) = 0.
  4. Combining (1) and (2), we get a * 0 = a * 0 + a * 0.
  5. Combining (3) and (4), we get - (a * 0) + (a * 0) = - (a * 0) + a * 0 + a * 0.
  6. Evaluating (5) gives us 0 = a * 0. QED.
Now that we have this as a theorem, we can use it to prove other theorems. Given this property, we can immediately show that there is no multiplicative inverse of 0:
  1. If 0 had a multiplicative inverse 0⁻, then 0 * 0⁻ = 1.
  2. For all real numbers, a * 0 = 0.
  3. Since 1 ≠ 0, there is no multiplicative inverse of 0⁻.
Okay, now we can talk about division in the reals.

Division

The field definition does not include division, nor do our definitions of addition or multiplication. This means we are free to define division however we want. We want to define it in a way that mostly follows our intuition and is sound. I say mostly because our intuition doesn’t generalize. As an example, we intuitively think of a * b as “a summed up b times”. So what’s -1 * π? How do you sum up something π times? While it would be nice if division didn’t have any “oddness” to it, we can’t guarantee that without kneecapping mathematics.
The intuitive definition of division is multiplying by the inverse. a/2 = a * 2⁻. Under this definition, we can get all of the properties of division we’re used to by proving that they hold. For example,
  • Theorem: a/a = 1. Proof: a/a = a * a⁻ = 1.
  • Theorem: a * (b/c) = b * (a/c). Proof: a * (b/c) = a * (b * c⁻). Since multiplication is commutative and associative, we can rearrange this to get b * (a * c⁻) = b * (a/c).
This is all great, except for one problem: 0 does not have a multiplicative inverse. Both of those proofs are invalid: if I write 0/0, I get 0 * 0⁻, which is an invalid equation. So we cannot prove that a/a = 1. We can, however, prove something weaker:
  • Theorem: IF a ≠ 0, THEN a/a = 1. Proof: same.
  • Theorem: IF c ≠ 0, THEN a * (b/c) = b * (a/c). Proof: same.
Note this does not go both ways: it does not follow that 0/0 ≠ 1. All we know is we cannot use this theorem to prove that 0/0 = 1. So we do not have that 0/0 ≠ 1. For any given number, we cannot prove that 0/0 is not that number! Since we’ve defined division as multiplying by the inverse, and zero does not have an inverse, our definition of division does not cover dividing by zero. It does not say anything about it, leaving it “undefined” if you will.
Since this form of division is not defined for 0, it is a partial function over the reals: there is some value in its domain that we have not specified. Practically, this is fine: we’re used to thinking of 1/0 as an impossible operation. But this has some weird consequences: one of our axioms is everything is equal to itself. So does 1/0 = 1/0? If you say that’s silly, we no longer have a = a! And even if you’re fine with that, what about the statement TRUE \/ (1/0 = 1/0)? It shouldn’t matter what the second clause is, because that statement should be true. But by the axiom of the excluded middle, we’d then have to say the second clause is either true or false. When trying to formalize math and logic, we have to find some way to address what happens if you write 1/0. So there’s generally three things mathematicians can do:3
  • We can say nope, sorry, you can’t even write 1/0, much less give it a value. This is what we do in our day-to-day lives, and the way that Agda and Idris handle division.
  • We can choose some value that isn’t a real number, such as “undefined” or infinity, and say x/0 = <whatever>. This is what some mathematicians do with the Riemann sphere.
  • We could choose some real number, like 19, and say that x/0 = 19. This is what Isabelle, Lean and Coq do.
All of these have tradeoffs. We already talked about some of the headaches with banning equations like 1/0. With an “undefined” value, division is no longer closed on the reals. In the last case, you explode everybody’s intuitive notion of division. But all of these are sound. Since our original notion of division does not say anything about dividing by zero, it does not rule out anything. None of these extensions lead to a contradiction.
The controversy is over the last case, so let’s focus on that. We’ll define division as follows: IF b = 0 THEN a/b = 1 ELSE a/b = a * b⁻.
Something I need to emphasize here: this does not give us an inverse of 0. 1/0 is not 0⁻. This means that while 0/0 = 1, 0 * 1/0 = 0. Division is only “multiply by the inverse” when the denominator isn’t 0. All we’ve done is special case dividing by zero and nothing else. And doing so is mathematically consistent, because under this definition of division you can’t take 1/0 = 1 and prove something false.

Objections

Here’s where a lot of people objected. They would take the fact 1/0 = 1 and prove something false, usually 1 = 0. None of these proofs, however, are sound. To see why, let’s dig into a couple example proofs and show where they break down.
Here’s a common argument:
  1. 1/0 = 1
  2. 1/0 * 0 = 1 * 0
  3. 1 * 0/0 = 0
  4. 1 = 0
The problem is in step (3): our division theorem is only valid for c ≠ 0, so you can’t go from 1/0 * 0 to 1 * 0/0. The “denominator is nonzero” clause prevents us from taking our definition and reaching this contradiction.
Here’s where people got tripped up. They assume we needed the nonzero clause on our division theorems because x/0 is undefined. “If x/0 is a value, then the theorem should extend to c=0, too.” This is wrong. The problem is not that 1/0 was undefined. The problem was that our proof uses the multiplicative inverse, and there is no multiplicative inverse of 0. Under our modified definition of division, we still don’t have 0⁻, which means our proof still does not work for dividing by zero. We still need the condition. So it is not a theorem that a * (b / 0) = b * (a / 0).
To be clear, this does not mean they must be different! All we know is that we cannot use this theorem to argue they are equal. Since the “proof” that 1 = 0 used that theorem, the proof is unsound.
Pretty much every counterargument makes this exact same mistake: it assumes that because 1/0 is now defined, there is now some 0⁻ that generalizes our theorems. But there’s not.
Another common objection is that if 1/0 = 1, then multiplicative inverses are no longer unique: 2/2 = 1, but also 2/0 = 1, so now 2 has two inverses. This, again, confuses cause and effect. 1/2 is the inverse of 2 not because of how we define inverses, but how we defined division. 2/2 = 1 because 2/2 = 2 * 2⁻. But, again, zero does not have an inverse, and 2/0 is not 2 * 0⁻. Since 0⁻ does not exist, it is not an inverse of 2, and every nonzero number still has a unique inverse.
If you want to prove that 1/0 = 1 leads to a contradiction, you must explicitly list every step you take and show that none of them assume that 0⁻ exists.

1/0 = 0

We’ve now established Let’s assume for now that if we choose some constant C, then defining division such that x/0 = C does not lead to any inconsistencies.4 It turns out that for certain choices of C, specifically 0, we can make some theorems stronger. We can do this by removing the conditions on (some of) our division theorems, and then add a special case to the proof itself. For example:
  • Theorem: a * (b/c) = b * (a/c). Proof: we already proved this for c ≠ 0. Now let c = 0. Then a * (b/0) = a * 0 = 0, and b * (a/0) = b * 0 = 0, and 0 = 0.
Under this definition of division step (3) in the counterargument above is now valid: we can say that 1/0 * 0 = 1 * 0/0. However, in step (4) we say that 0/0 = 1. This theorem does not get stronger:
  • “Theorem”: a/a = 1. Proof: we already proved this for a ≠ 0. Now let a = 0. Then a/a = 0/0 = 0, so 1 = 0 and wait shit nevermind
This is why Lean and Isabelle define 1/0 this way. Coq does it too, but as far as I can tell they don’t use it as an optimization.

The Real Mathematicians

A final objection is that I’m a CS person, not a mathmatician, so I don’t understand the math here. But what do the PhDs say?
Lawrence Paulson, professor of computational logic and inventor of Isabelle:
A bit of history: the first logic supported within Isabelle was Martin-Löf’s constructive type theory, and it is still there (CTT). And while developing arithmetic within that formalisation, I came up with a definition (necessarily primitive recursive and executable) of division. It delivered n/0 = 0. Since then a number of people have noticed that defining x/0 = 0 is convenient. This identity holds in quite a few different proof assistants now.
These things are conventions, exactly the same as announcing that x^-n = 1/x^n and that x^0 = 0 [sic].
Leslie Lamport, Math PhD and winner of the 2013 Turing Award:
[In ZF set theory] Since 0 is not in the domain of recip, we know nothing about the value of 1 / 0; it might equal √2, it might equal R, or it might equal anything else.
Matt Noonan, Math PhD and introducer of Ghost Proofs to Haskell:
looks all fine to me!
Arthur Azevedo de Amorim, an author of the introductory Coq textbook, reconstructs the same argument I did here.
I also chatted with a few math graduate student friends and emailed a couple of postdocs I know. So far people nobody’s said that letting 1/0 = 0 is unsound. If any end up getting back to me with that I will include their refutation of this post.

Conclusions

This was originally motivated by how Pony does division. So, is Pony doing the right thing here? No clue. Pony is a programming language, not a formal mathematical system. Consistency is less important than safety, convenience, and context. As a programmer, I don’t like it.5
But is Pony doing something unsound? Absolutely not. It is totally fine to define 1/0 = 0. Nothing breaks and you can’t prove something false. Everybody who was making fun of Pony programmers for being ‘bad at math’ doesn’t actually understand the math behind it.
Don’t make fun of other people. The world is big and we are small.
Thanks to Watson Ladd, Matt Noonan , Ron Pressler , Josh Lieber, and Edwin Brady for feedback.

Update 8 / 12

Some people pointed out I was using some terms ambiguously, which I’ve done my best to fix. A bunch of people also sent in more counterarguments, most of which fell along common themes.
ab = cb => a = c but with division by zero we have 1 * 0 = 2 * 0 => 1 = 2.
This is a common mistake a lot of people made: assuming that some property of division is somehow part of the definition, not something we have to show is true. But division has no “innate” properties: everything manipulation we make involving it is something we have to prove is a valid manipulation. For any contradiction, you must list out, for every manipulation of the equation you make, the theorem that makes that manipulation valid, and show that the proof of that theorem does not use 0⁻.
Letting 1/0 = 0 will lead to hidden errors in your program.
As mentioned before, this is not a post about what’s practically a good idea. All I’m arguing is that mathematically, we can extend division in this way without leading to a contradiction. Programming languages are different from mathematical formalisms, and should be different. I prefer that 1/0 is an error, because I’m not using my program to prove theories.
All languages need to make sacrifices of mathematical soundness in favor of safety, practicality, and predictability. It’s the same reason why, in almost every practically-used language, head has type [a] -> a, not [a] -> Maybe a.
We no longer have that division is the inverse of multiplication over its whole domain.
This is a common argument, and arguably is more about the “aesthetics” of division than what’s formalizable. This happens a lot when we extend functions. For example, over the naturals, a * b is just repeated addition. But if we extend multiplication over the rationals, then we lose that nice definition.
In general, I aesthetically “dislike” definitions and theorems that explicitly include a dependence on a function’s domain, because it leads to “side effects” when we extend them.
If 0/0 = 0 then lim_(x -> 0) sin(x) / x = sin(0) / 0 = 0, but by L’Hospitals’ Rule lim_(x -> 0) sin(x) / x = lim_(x -> 0) cos(x) / 1 = 1. So we have 0 = 1.
This was a really clever one. The issue is that the counterargument assumes that if the limit exists and f(0) is defined, then lim_(x -> 0) f(x) = f(0). This isn’t always true: take a continuous function and add a point discontinuity. The limit of sin(x) / xis not sin(0) / 0, because sin(x) / x is discontinuous at 0. For the unextended division it’s because sin(0) / 0 is undefined, while for our extended division it’s a point discontinuity. Funnily enough if we instead picked x/0 = 1 then sin(x) / xwould be continuous everywhere.
A couple of other people brought up limit arguments, but they all are addressed in a similar way.
It’s icky.
Don’t disagree.
  1. To be clear, I don’t live up to this standard. I try to follow it, but stumble regularly. As part of my tweetstorm I ribbed the original poster at one point and I still feel bad about that. [return]
  2. An axiom is something we take to be true without proving it. Some example axioms are “0 is a number” and “everything is either equal or unequal.” Different choices of axioms lead to very different mathematical frameworks. Most famously, rejecting the axiom that “every line has exactly one parrallel line that passes through a given point” leads us to non-Euclidian geometries. [return]
  3. Several people pointed out that there’s a fourth thing you can do: you can say that 1/0 is a real number but we don’t know what it is. This is how TLA+ is formalized, though TLC considers 1/0 an error. [return]
  4. A couple of people pointed out we didn’t actually establish this, just showed that some of the common arguments don’t apply. We can prove this to be the case, but the proof gets technical very fast. [return]
  5. One of developers of Pony reached out to me. They’re planning on writing a more in-depth explanation of why Pony chose 1/0 == 0, which I will linked when available. As I understand it, it’s because Pony forces you to handle all partial functions. Defining 1/0 is a “lesser evil” consequence of that. [return]
 
ゼロ除算の発見は日本です：
∞？？？    
∞は定まった数ではない・・・・・・・・
人工知能はゼロ除算ができるでしょうか：

とても興味深く読みました：2014年2月2日
ゼロ除算の発見と重要性を指摘した：日本、再生核研究所


ゼロ除算関係論文・本
割り算のできる人には、どんなことも難しくない
                           
世の中には多くのむずかしいものがあるが、加減乗除の四則演算ほどむずかしいものはほかにない。
                                                          
ベーダ・ヴェネラビリス（アイルランドの神学者）

数学名言集：ヴィルチェンコ編：松野武　山崎昇　訳大竹出版1989年
P199より

Please look the papers:
Reality of the Division by Zero z/0=0
DOI:
10.12732/ijam.v27i2.9.

Albert Einstein:

Blackholes are where God divided by zero.
I don’t believe in mathematics.

George Gamow (1904-1968) Russian-born American nuclear physicist and cosmologist remarked that "it is well known to students of high school algebra" that division by zero is not valid; and Einstein admitted it as {\bf the biggest blunder of his life} [1]：
1. Gamow, G., My World Line (Viking, New York). p 44, 1970.
無限遠点は、実は数で0で表されていた。

地球平面説→地球球体説
天動説→地動説
1/0=∞若しくは未定義　→1/0=0（628年→2014年2月2日）

リーマン球面における無限遠点は、実は、原点０に一致していました。

地球人はどうして、ゼロ除算1300年以上もできなかったのか？　
２０１５．７．２４．９：１０
意外に地球人は知能が低いのでは？ 仲間争いや、公害で自滅するかも。
生態系では、人類が がん細胞であった　とならないとも　限らないのでは？
Einstein's Only Mistake: Division by Zero
何故ゼロ除算が不可能であったか理由
                                                
１　割り算を掛け算の逆と考えた事
２　極限で考えようとした事
３　教科書やあらゆる文献が、不可能であると書いてあるので、みんなそう思った。

Matrices and Division by Zero z/0 = 0

直線上を　どこまでも行ったら、どこに行くでしょうか？　驚くべきことに　行き先があり、意外なところで　止まる。　これすごいことでは？　下記の図をよく見て、美しい解釈を考えてください。
我々の空間は実は　そうなっていたと言えると思います。簡単な論文ですが、新らしい世界を拓いている（２０１６．７．２４：０６：２１）： (2016) Matrices and Division by Zero z/0 = 0. Advances in Linear Algebra
& Matrix Theory, 6, 51-58.
DOI:10.12732/ijam.v27i2.9.

ビッグバン宇宙論と定常宇宙論について、http://detail.chiebukuro.yahoo.co.jp/qa/question_detail/q1243254887 #知恵袋_

もし1+1=2を否定するならば、どのような方法があると思いますか？ http://detail.chiebukuro.yahoo.co.jp/qa/question_detail/q12153951522 #知恵袋_
一つの無限と一つの∞を足したら、一つの無限で、二つの無限にはなりません。
2つの0を足しても一つのゼロです：

『ゼロをめぐる衝突は、哲学、科学、数学、宗教の土台を揺るがす争いだった』 ⇒ http://ameblo.jp/syoshinoris/entry-12089827553.html ……　→ゼロ除算（100/0=0, 0/0=0）が、当たり前だと最初に言った人は誰でしょうか・・・ 1+1=2が当たり前のように、

ゼロ除算（100/0=0, 0/0=0）が、当たり前だと最初に言った人は誰でしょうか・・・・ 1+1=2が当たり前のように
地球平面説→地球球体説　地球が丸いと考えた最初の人－ピタゴラス
地球を球形であることを事実によって証明しようとした人－マゼラン
地球を球形と仮定して初めて地球の大きさを測定した人－エラトステネス
天動説→地動説：アリスタルコス＝ずっとアリストテレスやプトレマイオスの説が支配的だったが、約2,000年後にコペルニクスが再び太陽中心説（地動説）を唱え、発展することとなった。https://ja.wikipedia.org/wiki/%E3%82%A2%E3%83%AA%E3%82%B9%E3%82%BF%E3%83%AB%E3%82%B3%E3%82%B9 …
何年かかったでしょうか????

1/0=∞若しくは未定義　→1/0=0
何年かかるでしょうか????


ゼロ除算の証明・図｜ysaitoh｜note（ノート）  https://note.mu/ysaitoh/n/n2e5fef564997
 
 
 
ダ・ヴィンチの名言 格言｜無こそ最も素晴らしい存在
                     
ゼロ除算の発見はどうでしょうか：
Black holes are where God divided by zero：

再生核研究所声明371（2017.6.27）ゼロ除算の講演―　国際会議　
https://ameblo.jp/syoshinoris/entry-12287338180.html

1/0=0、0/0=0、z/0=0
http://ameblo.jp/syoshinoris/entry-12276045402.html
1/0=0、0/0=0、z/0=0
http://ameblo.jp/syoshinoris/entry-12263708422.html
1/0=0、0/0=0、z/0=0
http://ameblo.jp/syoshinoris/entry-12272721615.html
Division By Zero（ゼロ除算）1/0=0、0/0=0、z/0=0
ゼロ除算（ゼロじょざん、division by zero）1/0=0、0/0=0、z/0=0

ソクラテス・プラトン・アリストテレス　その他
https://ameblo.jp/syoshinoris/entry-12328488611.html

ドキュメンタリー 2017: 神の数式 第２回 宇宙はなぜ生まれたのか
https://www.youtube.com/watch?v=iQld9cnDli4
〔NHKスペシャル〕神の数式 完全版 第3回 宇宙はなぜ始まったのか
https://www.youtube.com/watch?v=DvyAB8yTSjs&t=3318s
〔NHKスペシャル〕神の数式 完全版 第1回 この世は何からできているのか
https://www.youtube.com/watch?v=KjvFdzhn7Dc
NHKスペシャル 神の数式 完全版 第4回 異次元宇宙は存在するか
https://www.youtube.com/watch?v=fWVv9puoTSs

再生核研究所声明 411(2018.02.02): 　ゼロ除算発見4周年を迎えて
https://ameblo.jp/syoshinoris/entry-12348847166.html

再生核研究所声明 416(2018.2.20): 　ゼロ除算をやってどういう意味が有りますか。何か意味が有りますか。何になるのですか　－　回答
再生核研究所声明 417(2018.2.23): 　ゼロ除算って何ですか　－　中学生、高校生向き　回答
再生核研究所声明 418(2018.2.24): 　割り算とは何ですか？　ゼロ除算って何ですか　－　小学生、中学生向き　回答
再生核研究所声明 420(2018.3.2): ゼロ除算は正しいですか，合っていますか、信用できますか　－　回答

2018.3.18．午前中　最後の講演：　日本数学会　東大駒場、函数方程式論分科会　講演書画カメラ用　原稿
The Japanese Mathematical Society, Annual Meeting at the University of Tokyo. 2018.3.18.
https://ameblo.jp/syoshinoris/entry-12361744016.html より
再生核研究所声明 424(2018.3.29): 　レオナルド・ダ・ヴィンチとゼロ除算
再生核研究所声明 427(2018.5.8): 神の数式、神の意志　そしてゼロ除算

Title page of Leonhard Euler, Vollständige Anleitung zur Algebra, Vol. 1 (edition of 1771, first published in 1770), and p. 34 from Article 83, where Euler explains why a number divided by zero gives infinity.
私は数学を信じない。　アルバート・アインシュタイン / I don't believe in mathematics. Albert Einstein→ゼロ除算ができなかったからではないでしょうか。
1423793753.460.341866474681。

Einstein's Only Mistake: Division by Zero
God’s most important commandment

never-divide-by-zero-meme-66

Even more important than “thou shalt not eat seafood”
Published by admin, on October 18th, 2011 at 3:47 pm. Filled under: Never Divide By Zero Tags: commandment, Funny, god, zero • Comments Off on God’s most important commandment
http://thedistractionnetwork.com/.../never-divide.../page/4/


投稿者 時刻:

0 件のコメント:

コメントを投稿

登録: コメントの投稿 (Atom)