[luso_brazilian]

> But is Pony doing something unsound? Absolutely not. It is totally fine to define 1/0 = 0. Nothing breaks

It actually does break something, the symmetry between division and multiplication and the many pieces of code that assume that (x / y) * y equals x. Here is a naive and non practical example, but it is not impossible to find a real world example where this simplified code manifests itself accidentally or by design

  function do_something_with_x(x, y) {
    let ratio = x / y;
    if (do_something_with_ratio(ratio)) {
      return x * y;
    }
    else return null;
  }

Again, this is a naive example but one that could manifest itself with a very imprecise result when y = 0

[gjulianm]

I think OP means that nothing breaks mathematically. It is not inconsistent and not false, so you can work with it. The only issue is to deal specially with the case of division by zero, which you have to do anyways. Code that assumes that (x/y) * y = x is wrong if you don't check for y = 0, independently of what you define x/0 to be.

[godelski]

You do realize that division is the inverse operation of multiplication, right? Like subtraction is the inverse of addition. By defining addition we define subtraction. By defining multiplication we define division. This is where the author fails. Division is multiplication of a fractional value. This is VERY important.

And just because it is mathematically a field does not mean it is particularly the right choice. A field is not strictly definitely by addition and multiplication, it is definitely by two operators where one is an abelian group (addition in our case) and the other forms and abelian group over the non identity term of the first (eg multiplication is an abelian group over non zero terms). The complex numbers create a field, which is really how we do addition and multiplication in 2D space. 3D space you can't form one, so you have a ring. Which is why quaternions are so important, because they form a field.

But the author is wrong because they think division is a different operation than multiplication. It's just a short hand.

[gowld]

In a field, division by zero is not the inverse operation of anything.

[gjulianm]

The usual definition of division is the multiplicative inverse, yes. But that does not mean that, as an intellectual curiosity (which is how I take this post) you can't define "division" as having other value. Sometimes that's useful, sometimes it's not. Most of the time it is fun to see how things break and don't break. For example, the infamous 1+2+3+... = -1/12 sum[1]: for most purposes it's a divergent sum but you can find ways to assign a finite value and make that useful.

1: https://en.wikipedia.org/wiki/1_%2B_2_%2B_3_%2B_4_%2B_%E2%8B...

[godelski]

The OP says

> The field definition does not include division, nor do our definitions of addition or multiplication.

This is clearly a misunderstanding of not realizing that the definition of division is a symbolic shorthand for inverse multiplication.

Sure, you're right that we can define it another way. But I don't know what we would call an object with three operators. (Someone more knowledgeable in field theory please let me know, it's hard to Google) in the normal field we work with (standard addition and multiplication) we only have two unique operators. Everything else is a shorthand. In fact, even multiplication is a shorthand.

>For example, the infamous 1+2+3... = -1/12

Ramanujan Summation isn't really standard addition though. It is a trick. Because if you just did the addition like normal you would never end up at -1/12, you end up at infinite (aleph 0, a countable infinity). But the Ramanujan Summation is still useful. It just isn't "breaking math" in the way I think you think it is.

But I encourage you to try to break math. It's a lot of fun. But there's a lot to learn and unfortunately it's confusing. But that's the challenge :)

[gjulianm]

The fact that it's a shorthand means that it's not in the definition, just a convention. In fact, nowhere in my studies I saw anyone using 'division' when working explicitly with fields in algebra, it's always multiplicative inverse.

By the way, you cannot do the addition like normal on that series, you don't end up at anything. You can say it diverges and its limit is +infinity (not aleph0, aleph0 is used for cardinality of sets so I think no one would use it as the result of a divergent series). When I said it 'broke math' what I meant was that, in the same way that OP did, it is a way to assign values to things that usually don't have one. I know it does not actually break math.

[jle]

That's not necessarily the definition of division, there are many commonly used definitions in different contracts that are different.

[throwawaymath]

Bravo, that's a great explanation. I think you've done a better job here than my comments elsewhere in this thread. Nice tie in to dimensionality, the complexes and quaternions too.

There are legitimate reasons to advocate for defining division by 0 in the context of a programming language. But the attempt at mathematical rigor really distracts from those reasons. It feels like the author made a decision and reached for some odd mathematics that seems to support it but doesn't. Floating numbers don't even form a field. If we define division by 0 in a field it stops being a field and becomes a ring or some sort of weird finite field with a single element...

[rrampage]

> Division is multiplication of a fractional value

Thus, division by 0 is multiplying by (1/0). Does such a fraction exist? It can go along two potentially different paths depending on the limit we take.

Alternatively, there is information lost when you multiply something by 0: a x 0 = 0, b x 0 = 0. When you perform an inverse by dividing, will you get back a or b (or any number)? Thus, it is not invertible at least at 0.

Disclaimer: Not a mathematician

[godelski]

>Alternatively, there is information lost when you multiply something by 0: a x 0 = 0, b x 0 = 0. When you perform an inverse by dividing, will you get back a or b (or any number)? Thus, it is not invertible at least at 0.

>>A field is not strictly definitely by addition and multiplication, it is definitely by two operators where one is an abelian group (addition in our case) and the other forms and abelian group over the non identity term of the first (eg multiplication is an abelian group over non zero terms).

[pmiller2]

It is inconsistent. If 1/0 = 0, then 1 = 0*0.

[throwawaymath]

This should not be getting downvoted. The author of the article made an incorrect refutation of this point under the "Objections" heading. Division by 0 in fields is undefined precisely because it leads to contradictions like this. The full statement of a proof that 1/0 = 0 includes the temporary assumption that you have defined division by 0 such that it is no longer undefined.

You can't logically refute that proof by saying, "well no, you have yet to define division by 0 according to the field axioms, so you can't use that division as part of your proof." That's the point! The proof does not demonstrate that division by 0 results in 1, it demonstrates that you cannot define division by 0 while maintaining the algebraic structure of a field.

If the author wants to talk about defining division by 0 in wheels or something esoteric they're more than welcome to. But among fields, and among the real numbers, it's not possible. This whole exercise of trying to refute what has been commonly accepted for over a century is frankly ridiculous for trying to justify undefined behavior in a programming language.

[imh]

But the point is you keep the structure of a field for everything that already has it, right? No structure is taken away. All statements valid on any subset of the reals are still valid without modification under this new definition. The algebraic structure is still a field obeying the same axioms. There are just some new valid statements too.

[throwawaymath]

No that's not correct, and this is why I think the author's entire point is pretty inane. If you're going to start off your argument with the full formalism of field axioms and consequent theorems, you need to be prepared to split hairs about whether or not your definitions constitute a field.

Mathematics is thoroughly pedantic about definitions for a reason. If those formalisms don't matter because what you've done is "close enough", then skip the song and dance about field definitions and stop trying to use it to justify the behavior of an undefined operation in a programming language. Just say you're defining 1/0 to be equal to whatever you want because the world doesn't break down. It actually detracts the author's point to so confidently (and incorrectly) refute something that is robustly proved in the first few weeks of an undergraduate analysis course. Why is this even in a blog post about a programming language?!

This is essentially the same point as the extended real (or complex) number systems. The sets of all real and complex numbers (respectively) form fields under the axioms of addition and multiplication. But you can define division by 0 and division by infinity in a way that works with familiar arithmetic (I explained how to do this in another comment barely two weeks ago [1]). But the key point here is that in doing this you sacrifice the uniqueness of real numbers.

The author tries to refute this observation by claiming the proof uses an undefined division operation, but that's a red herring. The real assertion is that you cannot define division as an inverse operation from multiplication to be inclusive of division by the unique unit (i.e. 0, in the real field) unless you are willing to state that every number is equal to every other number in the entire field. And you can do that, but it trivially follows that you no longer have a field without a nonzero element.

So really the actual proof is that division by 0 is undefined for any field with at least one nonzero element.

__________________________________

1. https://news.ycombinator.com/item?id=17599087#17601806

[imh]

Is there a proof or something elsewhere you can link to? To be honest I can't really tell the point you're trying to make.

[imh]

This is explicitly talked about in OP about 2/3 of the way down the page. "If 1/0 = 0, then 1 = 0 * 0" is untrue. Your argument is "1/0 = 0, so multiply both sides by zero: 1/0 * 0 = 0 * 0, and then take 1/0 * 0 = 1 * 0/0." That last step isn't the case for reasons covered in the article we're ostensibly discussing.

[sclv]

Right. So the multiplicative inverse property _breaks_! He just points out that it breaks, and thus you need to use a more complicated property instead. That doesn't mean that the property doesn't break.

[gmfawcett]

He's not saying that it breaks; quite the opposite, he repeatedly states that 0⁻ doesn't exist. He's just defining division in a specific way.

The MI property states that every element except 0 has a multiplicative inverse. He's defining division via two cases: If b≠0, then a/b = a*b⁻ (multiplicative inverse). If b=0, then a/b=0. This definition does not imply that 0⁻ exists, so there's no violation of MI.

[sclv]

The problem this and the other replies miss is that the standard definition of division is multiplication by the inverse. The entire argument rests on a notational slight of hand. The property that held before -- that _when defined_ division has the inverse property -- no longer holds. Thus many equational identities that otherwise would hold do not hold.

[improv32]

You missed the part where he defines division as a/c = a * inverse(c) for all c != 0

[imh]

Multiplicative inverse is already broken. x / 0 * 0 is either 0 or ⊥ (aka exception). It wasn't true to begin with. I happen to like the exception/partial function version, so I'm playing devil's advocate, but it really was already broken when we're talking about zero.

[ASalazarMX]

Wait, if 1 / 0 = infinity, then infinity * 0 = 1

This seems just as bizarre, since zero times anything shouldn't become 1, no matter how big or how many times you do it.

[umanwizard]

According to the standard definition of division, 1/0 does not equal infinity. It doesn't equal anything. It is undefined.

[hexane360]

Yes, that's correct. The fact that 1/0 shouldn't be defined as infinity isn't an argument that it should be defined as 0.

[jacobolus]

There are many contexts where defining either 1/0 = -1/0 = ∞ or 1/0 = +∞ and –1/0 = –∞ is better than the alternatives, especially when working in an approximate number system like floating point.

In geometric modeling kinds of applications, I would say that these definitions are typically desirable, with 1/0 = undefined only better in unusual cases. As a simple example, it is typically much more useful for the “tangent” of a right angle to be defined as ∞ than left undefined.

But anyhow, there are no “facts” involved here. Only different choices of mathematical models, which can be more or less convenient depending on context / application.

[gmfawcett]

Yes, exactly, I have no idea why you're being downvoted.

[milesvp]

Look up the dirac delta function. It's a spike thats infinitely tall and infinitely narrow, with an area of 1. It's established now as a very useful tool in EE. But many people fought it tooth and nail because of this logic.

[lmm]

> This seems just as bizarre, since zero times anything shouldn't become 1, no matter how big or how many times you do it.

It isn't bizarre, because there's an equal and opposite argument that anything times infinity is infinity, no matter how small the thing you multiply by.

If you actually do infinity * 0 you get NaN since there's no way to determine (without more information) whether the result should be 0, infinity, or anything in between.

[FlipperBucket]

1/0 = undef (cast to 0)

1 != 0*0

I don't see the inconsistency. Abstract math vs practical application.

[pmiller2]

You’re doing something different than real number arithmetic. Saying 1/0 = x, and then treating x like a real number is inconsistent. But just saying “we are going to augment the real numbers with an element x that is not a real number, and then define some properties of x and prove things about it” is not.

[FlipperBucket]

> You’re doing something different than real number arithmetic

Computer languages execute on rules that are not utilizing real number arithmetic. I didn't want to mention it, but there's these things called floats...

Edit: Pony took out the "normal" version of division by zero and suggest to write a wrapper to check beforehand.

[pmiller2]

Where did I say anything about computers? I’m referring to real numbers.

[tzs]

It's not inconsistent. See this article [1] for an explanation. It's the first thing covered in the "Objections" section.

[1] https://www.hillelwayne.com/post/divide-by-zero/

[Confusion]

So according to you, 0*0 = 0, thus 0/0 = 0?

[mreome]

If division by zero is not undefined, yes. But how does this disagree with the assertion that it's mathematically inconsistent (as opposed to programmatically inconsistent)? If any case exists that leads to a logically false conclusion, then it's not logically consistent.

[pmiller2]

Nope. If 0/0 = 0, then x * 0/0 = x * 0, so 1/0 = 1, implying 1 = 0.

[yati]

You didn't read the article, did you?

[FlipperBucket]

> the many pieces of code that assume that (x / y) * y equals x

The same issue if division by zero throws an exception. This is simply a more practical approach that dispenses with the exception handling (ie becomes a less irregular test case). Edit: Not buggy behavior, when expected.

[Jaxan]

I would say an exception is much more convenient. Buggy code that silently continues to run is very hard to debug!

[cousin_it]

I used to think the same way: let's throw an exception on divide by zero, and forget NaN like a bad dream! But then someone explained to me that it's common to feed a billion numbers into a long calculation, then look at the results in the morning and find them okay, apart from a few NaNs. If each NaN led to an exception, you'd come back in the morning and find that your program has stopped halfway through. So there's a certain pragmatism to having numeric code silently continue by default.

[seanmcdirmid]

Typically, divide by zero throws for integers because they can’t express NaN, which can instead be returned for floating point. In any case, integers can’t express special values, so you get exceptions instead. And this is actually defined at the processor level (for x86 among others), the trap is free (well, a sunk cost), why not take it?

Zero is not a very good NaN.

[cousin_it]

Yeah, agreed. The thing with 1/0=0 is bizarre, I guess my comment was more about why NaNs are okay.

[dan-robertson]

What of a language without exceptions? A correct program can not assume that (x / y) * y = x because such an equality does not hold in general. Therefore the program must do something right in the case that y is zero before it tries dividing x by y to be correct. It shouldn’t really matter what x / 0 is because if a program relies on its value then it is probably wrong.

[cryptonector]

It's not convenient at all in a language like Coq.

[antidesitter]

Can you elaborate?

[nanimo]

It's common to think of an exception as the program stopping and never being started again. In that sense, the invariant is still maintained, because the program never sees it violated. This has non-trivial consequences - for example, Rust lets exceptions and endless loops produce any value at all, even though they obviously can't actually do that.

[lmm]

Assuming an exception is equivalent to any non-exceptional value doesn't break anything. See "Fast and Loose Reasoning is Morally Correct".

[sclv]

Holy moly that is not at all what that paper says! It specifically argues that certain equational properties of a given total language continue to hold in the total fragment of a given partial language. It is an embedding theorem combined with lifting properties, not a license to perform _any_ reasoning at all regarding the non-total portion of the language it considers!

[leereeves]

> (x / y) * y equals x

Even without Pony's assumption, that's only true when y != 0.

[umanwizard]

Yeah, (x/y)*y = x is true whenever it's a meaningful statement. x/y has no meaning in standard mathematics when y=0. 1/0 isn't infinity or anything else in standard math, it's literally un-grammatical nonsense.

[chess19]

It should be true for every y that is allowed in the denominator.

That is how fractions are handled in higher math. (Either called "localization" or "ring of fractions").

[lmm]

It's true up to NaNs, which we can treat as bottoms.

[tlb]

It's talking about integer arithmetic, so it's already not true that (x / y) * y == x. For example, (5 / 2) * 2 == 4.

[klodolph]

> …any pieces of code that assume that (x / y) * y equals x…

What? If you’re using integers or floating-point numbers, that has never been true in general. Consider x=1, y=49 in the realm of IEEE doubles. Addition isn’t even associative, consider 1e-50 + 1 - 1.

[vmchale]

Also just defining division to be whatever you want in the moment is not actually pragmatic, it's stupid and trivial. There's a reason we define a symplectic manifold the way we do. There's not a reason to say `1/0 = 0`, aside from the fact that the Pony designers didn't care to find a good solution to the problem.

[ballenf]

What if number types were Optionals after any operation that could result in any kind of unusual number (sqrt(-1), Infinity, NaN)? Or maybe after every operation, since any operation could overflow the type.

Do any languages do that? Seems more consistent (if way more hassle) than giving a mathematically false result out of pragmatism. At least in a strictly typed language.

[JadeNB]

You know what would happen. Math is ubiquitous in lots of code, so syntactic shortcuts would be introduced. Thus, we wouldn't use `a >>= (\x -> 2x) >>= (\x -> x^2)`, but would soon introduce syntactic sugar. For example, we could re-define `[asterisk]` so that it had type `Maybe Number -> Maybe Number -> Maybe Number`. You'd need a `return` (or `Just`) at the beginning, but soon that would be elided too, so that numeric literals would be auto-promoted to `Maybe Number`s. Then the language would add silent mechanisms to allow `Maybe Number`s to be displayed easily. You should check if your `Maybe Number`s are `Just Number`s before letting them out to play, but, if the language doesn't force you, then you know you won't. And then we're right back in the current situation.

[AnIdiotOnTheNet]

Zig defines checked versions of mathematical operators in its std lib [0], which return an Error Union. It's like an Optional (which Zig also has), but with an error instead of null. Your code can choose to handle this error however it wants.

[0] https://ziglang.org/documentation/master/#Standard-Library-M...

[zokier]

Isn't that essentially what floats already are? A sum type of numbers, infinities, and NaN(s).

[Someone]

Yes and no. I think the OP is looking for a strongly typed language where you can’t do any operation on that sum type, forcing you to check results after every operation.

[klodolph]

JavaScript does that…

[ballenf]

How so without optionals or static typing?

[RReverser]

That's usually what NaN is used for (basically "None" for numbers).