1/0 = 0 • Hacker News Board

Re: 1/0 = 0

#391

Post by ummonk » Sat, Aug 11, 2018, 3:41 AM UTC

lisael wrote: post #329

ajanuary wrote: post #155

Earlier quoted context omitted.

“Nothing breaks” in that it isn’t unsound, in that you can’t use it to prove a falsehood. Not that you can’t use the nice little shortcuts you’re used to. In practical terms, that _does_ have an impact, because people might use those shortcuts without realising the system they’re operating under doesn’t allow it. But you picked the wrong quote to make that point under.

To elaborate on the 'nice little shortcut' you mentioned, here it is: If a==b and N≠0 , then x==y EDIT: Formatting

No, that is not necessary.

"Given an x, y, and N such that x/N == y/N, it is true that x == y".

There is no need to say N != 0 under the ordinary definition of division.

Re: 1/0 = 0

#392

Post by throwawaymath » Sat, Aug 11, 2018, 3:42 AM UTC

a_wild_dandan wrote: post #357

throwawaymath wrote: post #276

Earlier quoted context omitted.

He didn't cover that in the article, or at least not in a way that actually supports his point. Since there is no multiplicative inverse of 0, division by 0 is undefined behavior. Trying to remediate that by refuting the "proof" that it's undefined while still asserting that we can define it as something else is mathematically incoherent. If you want to see why it doesn't work from a number of different angles, read…

> Trying to remediate that by refuting the "proof" that it's undefined He does not refute any proofs by citing that division by 0 is undefined. He refutes them by asserting that the multiplicative inverse doesn't exist. These are very different statements. Neither the standard field nor his modified field use the zero inverse, 0⁻. The proofs he's criticizing do erroneously use 0⁻. That's what he's calling out, I beli…

> He refutes them by asserting that the multiplicative inverse doesn't exist.

Yes - but in algebraic fields division by x is equivalent to multiplication by 1/x. This is precisely why you cannot have a field that admits division by 0: because 0 has no multiplicative inverse.

Re: 1/0 = 0

#393

Post by throwawaymath » Sat, Aug 11, 2018, 3:50 AM UTC

pron wrote: post #358

throwawaymath wrote: post #319

Earlier quoted context omitted.

I can give you a simple proof by contradiction. 1. Let F be a field containing an element x =/= 0. 2. Suppose we have defined division by zero in F such that, for all x in F , there exists an element y = x /0 (i.e. F adheres to the field axiom of multiplicative closure). Note that at this point it does not matter how we have defined division by 0, we will just generously continue and assume you've done it in a way th…

There is a mistake in your step 3, as it relies on an informal and imprecise "division is the inverse of multiplication". If you were to write that formally, you'd get `∀ x ≠ 0 . x(1/x) = 1`. This holds unchanged even if you define division by zero. Even if you could come up with another formalization that does cause a problem, e.g. `∀ x ∈ dom(1/t) . x(1/x) = 1` (and I would say that this is the only formalization th…

This is nonsense. If F is a field with elements x, y, then the quotient x/y is equivalent to the product x(1/y). If 0 has no multiplicative inverse, there is no division by 0. The two concepts are one and the same, just as is the case for subtraction and additive inverses. The problem is not that field theory doesn't tell you "what happens" when you divide by 0 - you haven't defined that, there is no what happens because nothing happens at all.

You can't engage with the problem because it only exists as a syntactical annoyance. You seem to acknowledge this, but then continue to argue when I explicitly tell you I am in agreement on that point. Then you proceed to argue the theoretical basis all over again.

I'm not going to continue arguing this with you. You're presently the only one in this thread who isn't following and I've tried to direct you to other resources. You've alternated between saying those proofs are either incorrect outright or not applicable because they don't have relevance for programming. If you actually believe division by 0 is possible in fields you have an immediately publishable math paper waiting for you to submit it.

Otherwise we're just talking past each other because my whole point here has been that the author's discussion of fields is irrelevant for programming language theory in the first place.

Re: 1/0 = 0

#394

Post by Zarel » Sat, Aug 11, 2018, 3:55 AM UTC

behringer wrote: post #373

spooneybarger wrote: post #234

Earlier quoted context omitted.

but with floating point units, 1.0/0.0 is infinity.

That's not correct mathematically though. You can't divide something 0 times and get any number. Adding zero + zero + zero infinite times does not equal 1.

It's plenty correct mathematically; the linked article even explains this.

Generally, your viewpoint comes from an incorrect understanding of mathematics, so let's explore what math actually is:

When we say "10 / 2 = 5", the result "5" doesn't come out of nowhere. It comes out of the definition of division.

There are several ways you could define division. You could interpret "10 / 2 = 5" as meaning any of:

• "If you had a 10-inch stick and you divided it into 2 equal parts, each part would be 5 inches."

• "If you had the equation 2 * X = 10, X = 5 would be a solution to it."

• "If you had 10 Pa of pressure in an enclosed box, and you increased the volume of the box to 2 times its previous volume, its new pressure would be 5 Pa."

• "A wave of wavelength 2cm would have a frequency of 5 per 10cm."

These definitions all lead to the same result – in other words, they're equivalent. When this happens, mathematicians usually don't particularly care which one is the "real" definition.

This applies to many different mathematical axioms. For instance compare the definition of the Parallel Postulate on Wikipedia:

"If a line segment intersects two lines, the two lines will intersect on the side that their angles with the line segment sum up to less than 180°"

– https://en.wikipedia.org/wiki/Parallel_postulate

with the definition on Wolfram MathWorld:

"If you have a straight line and a point not on it, there exists only one straight line which passes through that point and never intersects the first line."

– http://mathworld.wolfram.com/ParallelPostulate.html

These are different definitions. But since they lead to the same result, mathematicians don't really care to argue over which is the "real" definition.

Some definitions only apply over a subset of numbers. For instance, originally, "5 - 10" was undefined. Then negative numbers were invented, to expand the definition. The same thing happened with square roots and complex numbers.

That's the same thing with division. 1 / 0 was originally undefined. But you can come up with new number systems that define it, while preserving all the other properties that make division what it is. A common definition is 1 / 0 = Infinity, which is done in the Riemann sphere number system:

https://en.wikipedia.org/wiki/Riemann_sphere

There's nothing mathematically incorrect about doing any of this.

Re: 1/0 = 0

#395

Post by taneq » Sat, Aug 11, 2018, 4:00 AM UTC

innagadadavida wrote: post #365

Veedrac wrote: post #230

Earlier quoted context omitted.

My comment from when this came up on Reddit, slightly edited for context: `/`-by-0 is just an operation and it tautologically has the semantics assigned to it. The question is whether the specific behaviour will cause bugs, and on glance that doesn't sound like it would be the case. Principally, division is normally (best guess) used in cases where the divisor obviously cannot be zero; cases like division by constant…

What happens for 0 / 0? Is this also 0?

It's extra zero.

Re: 1/0 = 0

#396

Post by daveFNbuck » Sat, Aug 11, 2018, 4:11 AM UTC

thanatos_dem wrote: post #156

spooneybarger wrote: post #103

Hi, I'm on the Pony core team. I will be writing in more detail about this decision. A few short notes until then: 1) no one on the team has ever been happy with ending up here, understanding why the decision was made involved understand how partial functions (one that can produce errors like division by zero) are handled in Pony and interesting ergonomic issues that can result that is a large part of what my post wi…

> 2) this applies only to integer division wherein division by zero is undefined. 1.0/0.0 uses the available Infinity value. Oh jeeze... to me that almost nullifies all of the points in the article. It does an alright job explaining how 1/0 = 0 is at least consistent with other notions in the language, but to hear that the same logic can’t be applied to floats is just... well, objectively it’s a mess.

As pointed out by others, floats work differently from ints in programming languages. Division in ints is usually defined such that if x = d * y + m, x / y = d and x % y = m. You can make this work by choosing the right m for every d, but when y is not 0, there are a few conventions you can choose to pick a sensible d and m. When y = 0, the m = a and d is completely free, so there really isn't a right answer from how division works.

Division with floats doesn't usually have a definition like that, so you don't end up in a similar situation. Plus, floating point math can have denominators get really close to 0 and have the result of the division tend toward the infinity value. Ints don't have values close to 0 or an infinity to represent what that division would tend toward.

Re: 1/0 = 0

#397

Post by PopeDotNinja » Sat, Aug 11, 2018, 4:22 AM UTC

lisael wrote: post #313

PopeDotNinja wrote: post #120

Meanwhile, in Python v3.7.0... >>> 1 / 0 Traceback (most recent call last): File " ", line 1, in ZeroDivisionError: division by zero >>> 0 / 0 Traceback (most recent call last): File " ", line 1, in ZeroDivisionError: division by zero >>> 1 / 0.0 Traceback (most recent call last): File " ", line 1, in ZeroDivisionError: float division by zero >>> 0.0 / 0.0 Traceback (most recent call last): File " ", line 1, in ZeroD…

Meanwhile, in Python... In [1]: 255 + 1 is 256 Out[1]: True In [2]: 256 + 1 is 257 Out[2]: False Every language has its inconsistencies, when it comes to math, because they run on real-world computers. All these are "slow" interpreted languages that allow runtime failures and don't use plain machine integers. Just a different trade-off. Anyway, the Inf/NaN trick is not better than the 0 trick in my opinion, because a…

When I make a language, there will be a OuchMyHeadHurtsCommaSpaceGotSomeAspirinQuestionMarkError.

Re: 1/0 = 0

#398

Post by nanimo » Sat, Aug 11, 2018, 4:23 AM UTC

spooneybarger wrote: post #171

thanatos_dem wrote: post #156

Earlier quoted context omitted.

> 2) this applies only to integer division wherein division by zero is undefined. 1.0/0.0 uses the available Infinity value. Oh jeeze... to me that almost nullifies all of the points in the article. It does an alright job explaining how 1/0 = 0 is at least consistent with other notions in the language, but to hear that the same logic can’t be applied to floats is just... well, objectively it’s a mess.

Hillel is talking about math. Unfortunately computers don't really do "math". For example, math doesn't have overflow and underflow to deal with. The floating point standard says that division by 0.0 should be Infinity and provides a value for it. The integer math, all possible values are used for numbers, so division by zero is undefined behavior. And from there, every language is potentially going to have a mess of…

Underflow and overflow and 2's complement are all just modular arithmetic, which is definitely math.

Re: 1/0 = 0

#399

Post by pron » Sat, Aug 11, 2018, 4:36 AM UTC

throwawaymath wrote: post #393

pron wrote: post #358

Earlier quoted context omitted.

There is a mistake in your step 3, as it relies on an informal and imprecise "division is the inverse of multiplication". If you were to write that formally, you'd get `∀ x ≠ 0 . x(1/x) = 1`. This holds unchanged even if you define division by zero. Even if you could come up with another formalization that does cause a problem, e.g. `∀ x ∈ dom(1/t) . x(1/x) = 1` (and I would say that this is the only formalization th…

This is nonsense. If F is a field with elements x , y , then the quotient x / y is equivalent to the product x (1/ y ). If 0 has no multiplicative inverse, there is no division by 0. The two concepts are one and the same, just as is the case for subtraction and additive inverses. The problem is not that field theory doesn't tell you "what happens" when you divide by 0 - you haven't defined that, there is no what happ…

> If 0 has no multiplicative inverse, there is no division by 0. The two concepts are one and the same.

But formalizing the statement "there is no division" poses challenges. If you agree that a formalization of fields that is acceptable to you exists, please write a formal axiom/theorem in that theory which would break if we were to extend the definition of division.

> just as is the case for subtraction and additive inverses.

No, because subtraction is not partial, and therefore poses no challenge for formalization.

> there is no what happens because nothing happens at all.

This is fine when working informally, but doesn't work for formalizations, and formalizations of fields do exist.

> You can't engage with the problem because it only exists as a syntactical annoyance.

But that is the heart of the problem. Either you say one cannot formalize fields at all, or you must admit that some acceptable formalizations do not break. No one is claiming that one should be able to divide by zero in informal mathematics.

> I'm not going to continue arguing this with you.

That's fine, but settling this argument is very easy: write a theorem of fields in a formal language that would break if we extend division, one that cannot be equivalently written in an acceptable formalization in a form that does not break. This can literally be done in one line. If you cannot write such a theorem, then there really is no point arguing, because you cannot provide a counter-argument. Repeating the same informal theorems over and over is indeed pointless.

> You've alternated between saying those proofs are either incorrect outright or not applicable because they don't have relevance for programming.

I've not alternated on anything. Your proofs are incorrect in formal systems that you yourself would find acceptable.

> and I've tried to direct you to other resources

Resources about informal mathematics, on which everyone agrees. That the informal concept of division cannot be extended to 0 is obvious. The only question is whether a formal definition of division would necessarily break formal field theorems if extended to division by zero. You seem to claim that's the case, yet have not stated a single formal theorem of the kind.

> If you actually believe division by 0 is possible in fields you have an immediately publishable math paper waiting for you to submit it.

I would if only that result (doesn't merit a paper) had not already been published by at least Paulson and Avigad, two of the world's best known logicians. The formal field theory in the Lean proof assistant explicitly allows division by zero. That division coincides with the informal division everywhere but at zero, and the extension introduces no inconsistencies to the theory.

> the author's discussion of fields is irrelevant for programming language theory in the first place.

It's not about programming, but about any formalization (which includes, but is not limited to programming).

Anyway, see my comment https://news.ycombinator.com/item?id=17738558, which distills the debate into a concise, precise form.

Re: 1/0 = 0

#400

Post by skybrian » Sat, Aug 11, 2018, 4:42 AM UTC

throwawaymath wrote: post #392

a_wild_dandan wrote: post #357

Earlier quoted context omitted.

> Trying to remediate that by refuting the "proof" that it's undefined He does not refute any proofs by citing that division by 0 is undefined. He refutes them by asserting that the multiplicative inverse doesn't exist. These are very different statements. Neither the standard field nor his modified field use the zero inverse, 0⁻. The proofs he's criticizing do erroneously use 0⁻. That's what he's calling out, I beli…

> He refutes them by asserting that the multiplicative inverse doesn't exist. Yes - but in algebraic fields division by x is equivalent to multiplication by 1/ x . This is precisely why you cannot have a field that admits division by 0: because 0 has no multiplicative inverse.

Maybe all this talk about fields is a distraction? Integer arithmetic isn't a field anyway. Other than 1 and -1, no integer has a multiplicative inverse that's an integer.

Integer division just isn't the same operation as division on rationals or reals. The same laws don't apply.

(For floats, division by zero can return Inf, -Inf or NaN and there's no reason to define it differently.)

It looks like the theorem-proving languages that define 1/0 to be 0 tend to be using natural numbers as a fundamental type. Not only do they define division differently, they also don't have negative numbers, and so define 2-3 to be 0.

https://coq.inria.fr/library/Coq.Init.Nat.html