> 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.
Based on the tweet, I don't expect it to be very enlightening. Since programmers write programs to solve real problems, and real problems define 1/0=undefined... then this is only going to mask bugs in those programs.
My two issue with this is it totally relies on a specially constructed definition, and it leads to unintuitive results.
The issue with special definitions is you can use them to say anything you want, turning regular, common operations into weirdness.
What does it mean to take a factorial on the real numbers, or to add only on the even integers? In both cases, we're twisting what are generally accepted mechanics and domains into something else to get a funny result, like 1/0 = 0.
He gets to that point here:
"
We can say that division’s domain is all the real numbers except zero. 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.
"
So, tiny change in definition --> big change in outcome.
You may not be familiar but a "factorial on the real numbers" is the gamma function and it has all sorts of useful applications. (it works on real and complex numbers except for non-positive integers)
The concerned reader might wonder how it is possible to assert that there is _one_ correct definition of an extension of the factorial function to the real/complex numbers. Why is the gamma function better than any other extension?
The answer is that the gamma function is the unique logarithmically convex extension of the factorial function.
There ISN'T one correct extension of a factorial function.
The properties of the standard gamma function are great, but some might prefer the properties of Hadamard's or Luschny's alternative gamma function.
Like many arbitrary extensions in mathematics -- be it the factorial function or the division function which deals with 1 / 0 differently -- it's a matter of taste and convenience!
Interestingly the arbitrariness of some mathematical choices seem to unnerve folks on an almost existential level. My guess is that it conflicts with their expectation of capital T truth from mathematics.
> What does it mean to take a factorial on the real numbers, or to add only on the even integers?
I don't think that's exactly the same problem.
It is perfectly valid to define an operation on a particular domain. Defining an add operation on even numbers is perfectly fine (If you had said odd, well...). Factorial on real numbers is more or less the Gamma function. The problem here is that the operation is defined on one domain...
> We can say that division’s domain is all the real numbers except zero.
...but then, for some reason, it is decided that will will be applied on a different domain. That is, that we're going to apply on all real numbers including zero. So now we need to modify the definition of the operation. And the thing is that, the new definition, created to accommodate the new domain, usually tends to produce friction precisely on the new elements added to the domain. We excluded zero initially because that way the operation was defined in a simpler way. Now, having to consider zero implies that our definition becomes more "complex".
Now, we can change the definition in different ways. Is any one of those objectively "better" or "worse" than the rest? Well, that's what the discussion is all about.
> 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
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.
> 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.
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.
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?
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.
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.
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!
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.
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.
> 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.
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.
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.
> 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.
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.
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.
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.
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.
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.
He's just adding 0 to the domain of d(x, y) to extend the definition, and deliberately not using xy⁻ for that particular element of the domain. No inverse needed.
I know what he's doing. The problem is when you make it a different function (even by just extending it) then you change its equational properties. So equational properties that held over the whole domain of the function no longer hold over the extended domain. This is repaired by modifying the equational properties. But the modified equational properties mean that you now have a different system than before. So the whole thing is just playing around with words.
> The problem this and the other replies miss is that the standard definition of division is multiplication by the inverse.
Try to state this definition formally. The statement: ∀ x,y . x/y = xy⁻¹ is not a theorem of fields or a definition of division. However, ∀ x, y . y ≠ 0 ⇒ x/y = xy⁻¹ is, but is completely unaffected by defining division at 0. Those who think they see a problem rely on informal and imprecise definitions. Could you formally state a theorem that is affected? That would help you get around issues that are merely artifacts of imprecision.
But let's entertain you, and state that what we really mean by the informal and vague statement, "division is the inverse of multiplication," could be stated formally as:
∀ x ∈ dom(1/t). x(1/x) = 1
You are absolutely correct that this equational theorem is broken by extending the domain of division. However, there is absolutely no way to say that the formalization of this theorem isn't actually
∀ x ≠ 0 . x(1/x) = 1
because the two are equivalent. You cannot then claim that something is necessarily broken if you choose to pick a formalization that is indeed broken, while an equivalent formalization exists, that is not broken (not to mention that the formalization that is broken requires a strictly richer language). All that means is that your formalization in this case is brittle, not that laws are broken.
I have to disagree -- this isn't sleight of hand. The standard definition isn't being violated here, because standard division isn't a total function. The denominator's domain in Hillel's function is a proper superset of the standard domain: when restricted to the standard domain, the two functions are precisely equivalent. Therefore, every standard identity still holds under Hillel.
The hole that he is filling here isn't one that he bored into the standard definition, but a hole that the standard definition already admitted. If something is explicitly undefined, there's nothing mathematically wrong with defining it, as long as the definition doesn't lead to inconsistency.
> If something is explicitly undefined, there's nothing mathematically wrong with defining it, as long as the definition doesn't lead to inconsistency.
The definition does lead to inconsistency...you can't look at the field axioms, observe that 0 has no multiplicative inverse, then proceed to define a special, one-off division rule that doesn't involve multiplicative inverses for that one element. Either your division rule is pathological and breaks a fundamental field property or you've introduced a division rule which is just a syntactical sugar, not a real operation (in the latter case you've introduced confusing notation, not a new division function). Why do you think mathematicians explicitly state that the real field with the augmentation of positive and negative infinity (which allow division by 0) is not a field?
I don't understand why there is so much resistance to this idea in this thread, but the simple fact remains that if you define division by an additive identity (0) in any way, the field containing that unit ceases to be a field. This is because all elements cease to be unique. You can quickly prove that every element is equal to every other element, including (critically) the additive and multiplicative identity elements. Fields are defined by closure under the operations of addition and multiplication, and that closure requires uniqueness of their respective identities. Upend that and your entire field structure breaks down, because all you're left with is a field with a single element 0.
Stating that you've defined division by 0 using a one-off case that permits all other field identities to remain consistent is like saying you've turned the complex field into an ordered field using lexicographic ordering. You haven't, because i admits no ordering, much like 0 admits no multiplicative inverse.
Onlookers reading these comments probably think those of us harping on this point are anal pedants with a mathematical stick up our ass. But this thread is increasingly illustrating my central point, which is that the author shouldn't have tried to justify numerical operation definitions in a programming language using field axioms of all things.
> you can't look at the field axioms, observe that 0 has no multiplicative inverse, then proceed to define a special, one-off division rule that doesn't involve multiplicative inverses for that one element
Why not? What mathematical axiom does this break?
> Either your division rule is pathological and breaks a fundamental field property
> or you've introduced a division rule which is just a syntactical sugar, not a real operation
Is this math? We define symbols in formal math using axioms. I am not aware of a distinction between "syntactical sugar" and a "real operation."
> Why do you think mathematicians explicitly state that the real field with the augmentation of positive and negative infinity (which allow division by 0) is not a field?
That's simple: because unlike the addition of the axiom ∀x . x/0 = 0, adding positive and/or negative infinity does violate axioms 2, 7 and possibly 11 (depending on the precise axioms introducing the infinities).
> I don't understand why there is so much resistance to this idea in this thread, but the simple fact remains that if you define division by an additive identity (0) in any way, the field containing that unit ceases to be a field.
Because a field is defined by the axioms I've given here (https://news.ycombinator.com/item?id=17738558) and adding division by zero does not violate any of them. If you could show what's violated, as I have for the case of adding infinities and as done in actual math rather than handwaving about it, I assume there would be less resistance. I don't understand your resistance to showing which of the field axioms is violated.
> You can quickly prove that every element is equal to every other element, including (critically) the additive and multiplicative identity elements.
So it should be easy to prove using the theory I provided, which is the common formalization of fields. Don't handwave: write proofs, and to make sure that the proofs aren't based on some vagueness of definitions, write them (at least the results of each step) formally. The formalization is so simple and straightforward that this shouldn't be a problem.
> Stating that you've defined division by 0 using a one-off case that permits all other field identities to remain consistent is like saying you've turned the complex field into an ordered field using lexicographic ordering. You haven't, because i admits no ordering, much like 0 admits no multiplicative inverse.
> Onlookers reading these comments probably think those of us harping on this point are anal pedants with a mathematical stick up our ass. But this thread is increasingly illustrating my central point, which is that the author shouldn't have tried to justify numerical operation definitions in a programming language using field axioms of all things.
You can't use your own stubbornness to justify itself.
I'm waiting for you to justify your claim that this extension to division breaks any of the field axioms. pron even made you a nice list of them.
Just name one equation/theorem that the new axiom would break.
I'm completely open to being convinced! But so far you've only given arguments about giving a multiplicative inverse to zero. Everyone agrees on that. It's the wrong argument.
Because a divisor cannot exist unless it is a multiplicative inverse. Therefore 0 is not a divisor.
This is getting to be Kafkaesque...it breaks the field axioms themselves. How many different explanations and external resources do I need to provide in this thread for you to be convinced that this is not a controversial point in modern mathematics? I just explained it in the comment you responded to.
You have exactly two options here.
If you define x/0, that definition must interact with the rest of the definitions and elements of the field. To maintain multiplicative closure (a field axiom!) there must be a unique y element equal to x/0. So tell me how you will define x/0 such that x is not equal to the product of 0 and y. Regardless of what you think the author has shown, the burden of proof is not on me at this point to show that you can't do it, because it follows directly from the field axioms. Trying to impose a one-off bizarro divisor function defined only on {0} is not only mathematically inelegant, it immediately eliminates the uniqueness of all field elements. Therefore your "field" just becomes {0}, and since it lacks a multiplicative identity it ceases to be a field. There is your contradiction. Why don't you tell me how you're going to prove any equation defined over a field that relies on the uniqueness or cancellation properties of fields?
On the other hand, let's say you tell me you want define x/0 so that the definition doesn't interact with any of the field definitions or elements. Then you haven't actually introduced any new operation or definition, you've just designed a notation that looks a lot like division but has no mathematical bearing on the field itself (i.e. absolutely nothing changes, including for 0). That's not a divisor function, it's just a confusing shorthand. You can't just add another axiom to a field and call it a field.
If you believe I'm stubborn, that's fine. I might be a poor teacher! There are ample resources online which will patiently explain this concept in mind numbing detail. It boggles my mind that there are people in this thread still fighting an idea in earnest which has been settled for over a century.
> Because a divisor cannot exist unless it is a multiplicative inverse. Therefore 0 is not a divisor.
So there are two separate issues here. One is whether we can extend the definition of the "/" operator, and the other is whether we call it "division".
I'm not interested in what we call it. I'm interested in the claim that extending "/" will break the field.
The dichotomy you're talking about is wrong. The two options are not "multiplicative inverse" and "does not interact with anything". "1/0 = 0" interacts with plenty! If I make a system where it's an axiom, I can calculate things like "1/0 + 5" or "sqrt(1/0)" or "7/0 + x = 7". I can't use it to cancel out a 0, but I can do a lot with it.
> It boggles my mind that there are people in this thread still fighting an idea in earnest which has been settled for over a century.
Remember, the question is not "should this be an axiom in 'normal' math?", the question is "does this actually conflict with the axioms of a field?"
> You can't just add another axiom to a field and call it a field.
Yes you can. There is an entire hierarchy of algebraic structures. Adding non-conflicting axioms to an X does not make it stop being an X.
Consider the following two functions, that we can define for any field F:
• Our first function f(x, y) is defined for all x in F, and all nonzero y in F. That is, the domain of this function f is (F × F\{0}). The definition of this function f is:
f(x, y) = x times the multiplicative inverse of y
(Note that in the definition of f(x,y) we could say "if y≠0", but whether we say it or not the meaning is the same, because the domain of f already requires that y≠0.)
• Our second function g(x, y) is defined for all x in F, and all y in F. That is, the domain of this function g is (F × F). To define this function g, we pick a constant C in F, say C=0 or C=1 (or any C∈F, e.g. C=17 if 17 is an element of our field). And having picked C, the definition of this function g is:
• g(x, y) = x times the multiplicative inverse of y, if y ≠ 0, and C otherwise [that is, g(x, 0) = C].
Note that this function is defined for all (x, y) in F×F, and when y≠0 it agrees with f, i.e. g(x,y) = f(x,y) when y≠0.
Would you agree that both of these are functions, on different domains?
Next, we have the notation x/y. To assign meaning to this notation (and to the word “division”), there are two conventions we could adopt:
• Convention 1: When we say "x/y", we will mean f(x,y) (as defined above) — that is, x * y^{-1}.
• Convention 2: When we say "x/y", we will mean g(x,y) (as defined above).
The point of the post is that we can well adopt Convention 2: with such a definition of "division", all the properties that were true of f (on the domain F×F\{0}) continue to be true of g, except that g is defined on a wider domain.
----------------------------------------------
Now, maybe Convention 2 offends you. Maybe you think there is something very sacred about Convention 1. In all your posts in this thread, you seem to be insisting that "division" or "/" necessarily have to mean Convention 1, and the provided justification for preferring Convention 1 seems circular to me — here are some of your relevant comments, with my comments in [square brackets]:
> Since there is no multiplicative inverse of 0, division by 0 is undefined behavior [This seems to be saying: Because of Convention 1, we cannot adopt Convention 2.]
> Since y = x/0, it follows that the product of y and 0 is equal to x, because division is the inverse of multiplication [Here, your reasoning is "because we adopt Convention 1"]
> 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. [Again, you're stating that Convention 1 has to hold, by fiat.]
> 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 [This is just stating repeatedly that we have to adopt Convention 1.]
> A multiplicative inverse is a division. [This is merely insisting that Convention 1 has to be adopted, not Convention 2]
> divisor cannot exist unless it is a multiplicative inverse [Again, stating Convention 1.]
> you can't look at the field axioms, observe that 0 has no multiplicative inverse, then proceed to define a special, one-off division rule that doesn't involve multiplicative inverses for that one element. [Why not?] ...you've introduced a division rule which is just a syntactical sugar [yes the same is true of Convention 1; what's the problem?]
All these comments, which emphatically insist on Convention 1, seem to ignore the point of the article, which is that Convention 2 has no more mathematical problems than Convention 1, because the function g is no less a “valid” function than the function f.
In mathematics when we use words like “obvious” or insist...
I follow everything you're saying. As I have said many times already, I have no problem with convention 2. But don't use field theory to justify convention 2, because it's mathematically incoherent and unnecessary. I broadly agree - there is no reason to be involving field theory in programming language design.
I don't take issue with division by 0 - you can do that in mathematics just fine! I take issue with defining that division and calling the consequent system a field when it's not a field, and acting as though everyone else is wrong. The author invited this criticism when they loaded in the full formalism of field theory without needing to.
If the author had just stated they wanted to define division by zero that wouldn't be a problem. I have no idea why they felt the need to pull in abstract mathematics. I'm not disagreeing with their point, I'm taking issue with the strange and incorrect way they defended it.
Note that in my top level comment I specifically said, "Mathematics does not give us truths, it gives us consequences." I will happily agree with you that there is usefulness and coherence in a definition of 0. There is no canonical truth about the world regarding that matter. But a direct consequence of defining any division by 0 is that you cease to have an algebraic field.
Therefore, using field theory to defend a system which defines division by 0 doesn't make sense. It's not that the system is "wrong" for some meaning of wrongness. It's that you shouldn't be trying to pigeonhole field theory to make it work, because you don't need to.
Glad you follow! But I'm not sure we agree yet, as there's still something puzzling when you say:
> But don't use field theory to justify convention 2, because it's mathematically incoherent
> defining that division and calling the consequent system a field when it's not a field
> a direct consequence of defining any division by 0 is that you cease to have an algebraic field
If you go back to my comment (the one you're replying to), both the functions f and g assume a field F, and they are well-defined functions on F×F\{0} and on F×F respectively. (Do you agree?) For example, F may be the field of real numbers. Forget about the word “division” for a moment: do you think there is something about the function g, that makes F not a field?
To put it differently: I agree with you that it is a direct consequence of defining a multiplicative inverse of 0 that you cease to have an algebraic field. But the only way this statement carries over when we use the word “division”, is if we already adopt Convention 1 (that “division” means the same as “multiplicative inverse”).
Again, I think you are implicitly adopting Convention 1: you're saying something like “if we adopt Convention 2, then x/y means the function g and includes the case when y=0, but [something about multiplicative inverses, implicitly invoking Convention 1], therefore there's a problem". But there's no problem!
It is not a direct consequence of defining the function g(x,y) that something ceases to be a field: it is a consequence only if you also insist on Convention 1, namely if you try to assign a multiplicative inverse to 0 (which everyone here agrees is impossible).
Let me emphasize: whether we adopt Convention 1 or Convention 2, there is no problem; we still have the same field F.
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.
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.
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.
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. 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 that maintains the other field axioms.
3. Since y = x/0, it follows that the product of y and 0 is equal to x, because division is the inverse of multiplication. By the field axioms, division does not exist if there is no multiplicative inverse with which to multiply.
4. But by the field axioms this implies that x = 0, which contradicts our initial assumption. Likewise, since we can repeat this procedure with any element x in F, this demonstrates that there exists no nonzero element x in F, and in fact F = {0}.
The failure in the article's refutation is that this proof is designed to permit you to assume you have suitably defined division by zero, then proceed to demonstrate without any loss of generality that you could not possibly have unless 1) F is not a field, or 2) F contains only 0. The fundamental algebraic property you sacrifice by defining division by zero is uniqueness, and uniqueness is a hard requirement in fields with nonzero elements.
>Since y = x/0, it follows that the product of y and 0 is equal to x, because division is the inverse of multiplication.
Can you explain how this follows? I thought division was only the inverse of multiplication for all nonzero denominators, which would mean we can't use that definition for deduction in x/0.
It might hinge on your next sentence:
>By the field axioms, division does not exist if there is no multiplicative inverse with which to multiply.
but I don't understand why that's necessarily true. I don't understand how the field axioms require division by x to require the existence of a multiplicative inverse of x when x is zero. Sorry to take a bunch of your Friday, but I'm very curious now. Explanation much appreciated.
-------
edit:
Come to think of it, couldn't I define x/y as cotton candy for all x,y in field F and still satisfy the field axioms? They just don't refer to division.
Any connection between x/y and y's multiplicative inverse is just a nice convention. That convention states that x/y = x * mult_inv(y) when y != 0, but nothing else. That definition has nothing to do with the field axioms and changing it doesn't require that I change anything about multiplicative inverses. That means I don't touch the field axioms and my field is still a field.
Your edit is starting to get it. If by the argument of the article x/y = cotton candy for all x,y, then probably the argument of the article isn't good. And the reason is precisely that division in a field is taken to be nothing but a notational shorthand for multiplication by the multiplicative inverse.
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 that causes an issue, and it requires the use of a language with a dom operator, something that is absolutely not required for theories of fields), it won't matter because the question is not whether one could come up with a formalization that leads to contradiction, but whether there are reasonable formalizations of fields where this does not happen, and there are (in fact, most of them satisfy this, as they do not rely on a dom operator).
In addition, it is not true that "by the field axioms, division does not exist if there is no multiplicative inverse with which to multiply." It's just that the field axioms do not define what the meaning of division is in that case. Defining it, however, does not lead to contradiction with the axioms, at least not a contradiction you've point out. In fact, most common languages of mathematics cannot even explicitly express the statement "x is not in the domain of f." All they can do is define f(x) for values of x in the domain, and not define f(x) for values outside it. The "exist" in your statement does not refer to ordinary mathematical existence (usually formally expressed with the existential quantifier) but to an informal notion of definedness (discussed by Feferman) that has no formal counterpart in most formal systems, because it is very rarely needed; it is certainly not needed to state the field axioms.
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.
> 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).
>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.
This is intuitively mistaken. If "when you divide by 0 .. nothing happens at all", then how come multiplication by 0 is zero, when they're both operations against 0? The problem is that mathematicians have forgotten the meaning of 0. Anything multiplied by zero is zero. Anything divided by zero is zero. This agrees with normal intuition on working with nothingness, and the original idea from Brahmagupta.[
https://www.storyofmathematics.com/indian_brahmagupta.html]
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.
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...
> 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.
>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).
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.
> 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 :)
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.
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.
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.
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.
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.
> …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.
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.
If a hn title said 1*0=0 could you reply "Oh, so 1=0/0?"
The entire point of the article was suggesting you can define a consistent system without multiplication and division being entirely symmetrical (as they already are not)
Multiplication by x and division by x are inverses, except there is already the sole special case of x=0 where that isn't true.
The common way to resolve that is and be consistent is to axiomatically decide:
1) there is no inverse of * 0
2) 0 is not part of the range permitted for 1/x
The point of the article is that another way to resolve it and be consistent is to axiomatically decide:
1) there is no inverse of * 0
2) 0 is part of the range permitted for 1/x, and the resulting value is 0.
As in, (x/y) * y=x is true either way only if y!=0. The only difference is whether when y=0 if it is not true because it is just illegal or if it is not true because (x/0) * 0 = 0 for all x.
> As in, (x/y) * y=x is true either way only if y!=0. The only difference is whether when y=0 if it is not true because it is just illegal or if it is not true because (x/0) * 0 = 0 for all x.
Sure, I understand this claim. What I don't understand is the precise meaning of the claim "multiplication and division already are not entirely symmetrical." I don't know any existing technical meaning of "entirely symmetrical" for a pair of operations, but let's suppose that I switch the operations in your statement:
> (x/y) * y = x is true [for all x] only if y != 0.
Then I get:
> (x * y)/y = x is true [for all x] only if y != 0.
Actually, that's the entire point of 0/0. It's indeterminate, meaning it can only take on a fixed value in the context of an operation to approach it (usually a limit).
> So it is _not_ a theorem that a * (b / 0) = b * (a / 0)
As the article explains, the whole issue about dividing by 0 is the lack of multiplicative inverse. If you define division for 0 as something other than multiplication by the multiplicative inverse, there is no longer an issue doing the division. Hope that helps.
I'm curious what you mean by this: there is nothing "privileged" about the system of arithmetic that we usually use and this alternate definition.
The math that we all learn up through highschool is a system with a carefully chosen set of axioms that happen to be useful in most cases and has become the default system, but there isn't some intrinsic property of it that makes it "math" and alternate consistent set of axioms "not math".
You know.. dividing is like breaking something up.. If you divide by 2, you break it up into 2 pieces.. if you divide by 0, from some standpoints, you do have nothing, because you broke it up into 0 pieces, and 0 pieces is 0.
> You know.. dividing is like breaking something up.. If you divide by 2, you break it up into 2 pieces.. if you divide by 0, from some standpoints, you do have nothing, because you broke it up into 0 pieces, and 0 pieces is 0.
And dividing by 0.5 is breaking into how many pieces exactly?
I guess its more flipped. How many pieces equal the whole, not how many pieces can the whole be broken up into. That's why you can't divide by 0, any number of nothing can't make a whole.
The function "division" is just like any other function. It takes two inputs, and gives an output.
The reason it's a useful function is it has some properties:
y=1/x is continuous except where x==0. That is, as you approach 0 from either side, it grows to either +- infinity. The developers of this language want to make this function ==0 when x is 0.
You can do that, sure, but it doesn't change the fact that when you go from +0.0000001 to -0.0000001, you now have 2 non-continuous jumps instead of just one.
I guess its more flipped. How many pieces equal the whole, not how many pieces can the whole be broken up into. That's why you can't divide by 0, any number of nothing can't make a whole.
So all that to say: We can't treat 0 like a number.
*disclaimer: I have no math background whatsoever, this is just a fun topic.
And as it follows, if you divide by 0.00000000001, you can fit a whole lot of pieces in your original value... so what should dividing by 0 (which is even smaller than 0.000000001) naturally do? 0, or +infinity?
I love how people without an actual mathematical background make these sort of arguments - not because they're wrong but because it helps me check when I make those assumptions myself.
Multiplying by the square root of 2 is also a fun one since you need limits to show people that real numbers only make sense with the least upper bound theorem and limits and things they expect to work "intuitively" (like division or multiplication) only have approximate meaning when they use the common operations.
We are talking about machine integers here... So division is actually all about evenly dividing counts of things with the possibility that you might have some left over.
Reals are fundamentally different and are not found in things like computers and in general are of no practical use. For work with values (as opposed to counts) we use something called floating point.
> if you divide by 0, from some standpoints, you do have nothing, because you broke it up into 0 pieces, and 0 pieces is 0.
This explains exactly why we shouldn't divide by 0. The pieces after breakage should, if one is so inclined, be able to be re-assembled into the whole; but, once you break something into 0 pieces, it is gone. Thus at best `0/0` could be defined … but the problem there is not that there's no answer but that every answer is equally good.
You know.. dividing is like breaking something up [..]
No. What it is 'like' is totally irrelevant and actively harmful to consider if you want to be able to get anything serious done with your programming language. This is not a place to start philosophizing. For consistent arithmetic it is important to know which axioms are fulfilled. Division needs to be a mathematically clearly defined operation.
I mean, you’re not wrong. Not right either (for technical reasons), but that kind of argument leads you to mathematical objects like the Cantor set: a set of line segments with zero total length. Mathematically, you have a bunch of objects; practically, you have nothing.
It's like in Ruby, when you divide 3/2 you get 1 (integer division) which is almost never the behavior you want (unless you cast all you numbers to float which is a pain to do).
When dealing with integer quantities and together with modulo, it's pretty natural. n/d gives the integer result, n%d gives the rest. n/2 for example always gives you the "middle" element. And in e.g. a loop where you e.g. transmit elements in blocks, you handle full blocks n/blocksize times, followed by a partial block with n%blocksize elements.
It's not always what you want, but it's pretty reasonable. The alternative would be if it always rounds up, which seems weirder to me. I don't think rounding to the nearest integer makes sense with integer quantities at all, that's strictly a real number operation.
When we first teach children about division we teach them that, "17/5 = 3 with a remainder of 2". It is only later that they learn about decimal points and learn to say that 3.4 is the answer.
> It's like in Ruby, when you divide 3/2 you get 1 (integer division) which is almost never the behavior you want
I dunno, if I'm dividing a quantized space, which is a fairly common thing to do, its exactly what I want.
> (unless you cast all you numbers to float which is a pain to do).
Using floats just gets you different wrong answers than using integers, unless you happened to somehow have ints to start and want a floating point approximation, which I find is less likely than wanting integer division.
What you really want for exact division where there are integers involved is to have at least one operand specified as a rational; this also takes less keystrokes, if its a literal, than changing it to a float to get an inexact answer.
Related to this, prior to Ruby 2.5, the standard library include "mathn", a library which monkey-patched all the numeric types so that operations on them acted pretty much like Ruby had a Scheme-style numeric tower, but since that has process-wide effects not restricted to where the library is required, that was deprecated in 2.2 and removed in 2.5.
> We’ve now established that if we choose some constant C, then defining division such that x/0 = C does not lead to any inconsistencies.
No, you haven't. You've merely failed to locate any. You've said "I'm not going to prove that this works. I'm going to assume that it does and act as if it did, and place the burden on you to prove otherwise."
Absolutely correct. That said, proof assistants are being used. Here's a quote from TFA:
> Lawrence Paulson, professor of computational logic and inventor of Isabelle:
> > [...] This identity holds in quite a few different proof assistants now.
> No, you haven't. You've merely failed to locate any. You've said "I'm not going to prove that this works. I'm going to assume that it does and act as if it did, and place the burden on you to prove otherwise."
Excellent point. It's not even known if we can get any inconsistencies without making this definition; and it's known that, if it's true that we can't get any inconsistencies without it, then we can't prove that it's true. Building on such possibly shaky foundations can't make them stronger.
(That's not mathematical maundering, by the way; it is a correct if informal statement of part of the incompleteness theorems. I appreciated excalibur (https://news.ycombinator.com/item?id=17736486 )'s point, and wanted to underline the significant, and mathematically precise, difference between "one apparent inconsistency is not present" and "there is no inconsistency.")
Wrong. Division is not part of the field axioms, it is a defined function, and changing its definition has absolutely no bearing on the consistency of your equational theory.
This article grinds my gears. He quotes a number of mathematicians that correctly state the undefined nature of 1/0. Then proceeds to interpret that this means that we can choose any specific value to represent as 1/0 that we want. NO. We have "NaN" for a reason and it is an important signal to the programmer that a mistake was made. The language that assigns it to 0 silently is bunk as is this article.
Erm, when we say it's "undefined" we mean it literally -- standard mathematical systems of arithmetic do not define a value for that division.
If you make another system of arithmetic you can define it how you want and be consistent with "regular maths" for the operations in which things are defined. It's an extension.
> We have "NaN" for a reason
Funnily enough, IEEE754 defines 1/0 as positive infinity, not Nan. But none of these things are "the truth" in any reasonable sense of the word, just "useful systems".
Defining it as 0 at least means floating point numbers are (presumably) closed under arithmetic operations, which could be handy.
Ah, of course. Still, this definition gets you to something stricter still -- the "things that normal people think of as numbers" are closed under those operations. (Depending on what happens for overflow and 0/0, I guess.)
The story of what happens if we defined, for example, 1/0 = 0 is a little more complicated. I will include it because it is sufficiently interesting.
Equality of fractions is defined differently when zero divisors are allowed in the denominator. A zero divisor is a non-zero number that can multiply with another non-zero number to get zero. For example, if we work mod 12 then 3 is a zero divisor because 3·4 = 0.
If we want to allow zero or zero divisors in our denominators then we say that a/b = c/d if and only if there is some value s such that s·(a·d - b·c) = 0 where s is anything allowable in the denominator. If we are working with the integers, including this s term does nothing because s has to be something that can be a denominator and we only allow non-zero denominators.
So, even if we define 1/0 = 0 then literally every fraction would be equal to every other fraction.
These conventions can be broken (like, for example, addition of floating point numbers is not associative as pointed out by other comments) but it is definitely not "natural". In other fields of mathematics, like measure theory, it is possible to define things like "zero times infinity is zero" which is traditionally undefined but is a convenient shortcut and does not break anything that people working in measure theory care about.
IMHO I think the problem here is that most people focus on the "wrong side" of 1/0.
I mean, what the mathematical definition of division says is not that 1/0 is indeed something and that that something is "undefined" or "NaN" or anything else really. What it says is "I cannot do 1/0, the division operation a/b does not apply when b is 0".
So 1/0 is not a thing in itself in mathematics; it's something which cannot be operated.
Now, back some time ago, "division by zero" simply threw an error. It signaled "this is not something that can be done". undefined, NaN, anything else, including 0, is not really something that has a mathematical justification. It's merely a practical approach to encapsulate that error into some form of pseudo-value to control it to some extent.
Personally, I don't really see how 1/0 = 0 is better than 1/0 = NaN or "undefined" or "Infinity".
The practical downside is that it might make equations go slightly wonky, rather than completely wonky if a non-number is returned.
For example, say if a zero divide happens with normalized values. Meaning the immediate result is only off by one at most. Odds of catching that are probably low. Meanwhile, a NaN will infect all numbers that come into contact with it, bubbling up faster...
Under this system, programs are easier to debug if they use bigger numbers... That property does not seem like a win to me.
If I attempt to open a file, but an access fault occurs, I'd rather be told the fault and given a chance to recover than receive an empty file.
It seems straightforwardly better to me, because the programmer/user gets an immediate "you messed up" signal, instead of silently returning the wrong values until someone eventually (hopefully) notices.
Are we reading the same FA? In the section titled "The Real Mathematicians" the author has quotes of mathematicians saying that defining division by zero as zero is OK.
I find particularly interesting Leslie Lamport's comment that "Since 0 is not in the domain of recip, we know nothing about the value of 1 / 0", which I think is the most correct mathematical stance.
Then again, I think it is all a red herring. This (Pony's decision) is not about the mathematical definition of division. This is about the trade-offs computational systems do to manage the situation.
"defining division by zero as zero is OK" And those mathematicians should be classed as wrong. If you treat zero as nothing, a value divided nothing does not make it magically disappear, it should just cancel out the mathematical operation. So 1/0 should be 1, 42/0=42 and so on. Otherwise to apply their logic, a*0=0 would have to be applied. Again if you take a value and multiply it with nothing, it should cancel out the maths operation. It is possible for whole areas of a science to follow down the wrong rabbit whole, medical science best shows this over the last 100-200yrs since scientific equipment has improved and the current thinking about something in the body has changed when new discoveries appear that contradict. Maths is not untouchable either, especially considering the fact Big G and the speed of light varies. Check out Rupert Sheldrakes of Cambridge Uni talks on this subject. The official bodies response was to mandate G and speed of light is now constant when its not.
Hrm ... argumentation by reference to authority (various Ph.D. people) is a sure way to lose a scientific argument.
But that isn't my only qualm.
In the construction of the fields, there is a simple definition of the division function. It is intrinsically the solution of a = r * b, where r is the unknown. If a is nonzero, and b is zero, then r, the ratio, is said not to exist. Put another way, there is no real value of r that can be chosen that satisfies r * 0 = a. See [1] for example, as 0 is not an invertible element of the field over the reals.
So ... I can't say I agree with their choice of 1/0 == 0. They may be free to choose any value they wish, but then from an aesthetic viewpoint, do they really want to surprise the user?
>In the construction of the fields, there is a simple definition of the division function. It is intrinsically the solution of a = r * b, where r is the unknown. If a is nonzero, and b is zero, then r, the ratio, is said not to exist. Put another way, there is no real value of r that can be chosen that satisfies r * 0 = a.
Exactly. That's the definition of division. Here, he is introducing a totally different definition and claiming it isn't wrong because it is consistent. I mean, by his logic I could define division as a/b := a-b and claim it is consistent and therefore not wrong, but that is obviously not division...
What proportion of the time will a programmer intend and expect 1/0 = 0?
What proportion of the time will a divide-by-zero operation be a symptom of a bug, where evaluating 1/0 as any valid number will make it harder to identify that bug?
There might be a mathematical justification for 1/0 = 0, but the computer science justification seems tenuous at best. The overwhelming majority of the time, I want divide-by-zero to throw an exception or evaluate to NaN. I'd far rather deal with the edge case of intentionally dividing by zero, rather than the not-at-all-uncommon case of unintentionally dividing by zero and getting unexpected behaviour as a result.
We’re talking here about integer math. Integer math on CPUs is usually fast at the expense of having coherent semantics. It isn’t even really “integer” math in any mathematical sense. It’s just “the fastest math that the CPU is capable of doing, which happens to look a lot like integer math most of the time.”
If you’re dividing floats, you will get NaN or Infinity as expected. Just like how, if you overfloat a float, you’ll get Infinity. Floating-point has well-defined semantics, which CPUs are required to adhere to, and languages just expose.
If you divide “CPU integers” by (CPU integer) 0, the result is undefined. Just like how, if you overflow a “CPU integer”, the result is undefined. There is no standard semantics being adhered to. There is no equivalent of IEEE754 for CPU integers. There is only convention, and convention has no universal answer at these edge-cases. Thus, a language is free to do whatever it wants in response to either. There are no formal semantics to expose.
Usually, a language that calls itself “safe” will choose to make CPU integers behave a lot like real integers, by generating checks and throwing exceptions for the edge cases.
And usually, a language that calls itself “low-level” will just expose whatever semantics the CPU integers of its host platform already possess. In the case where there’s still an impedance mismatch (i.e. in the case of division by CPU-integer-0 where you don’t actually get any output into a result register), the language has to make something up. To “go with the flow” of how CPU integers work, probably it should be something fast.
Thus, 1/0=0 kinda sorta makes sense. It is an operation on the field of “CPU integers” that vaguely “fits in” with the existing ones. No mathematical relevance, but just fine from the perspective of someone e.g. seeking to create a higher-level abstract machine targeting the Pony compiler, where you’d still just insert a divisor check before doing the division op if you wanted the result to make any sense.
When setting out to add a new axiom to a heavily studied area of mathematics, perhaps one should at least formulate an argument that isn't shown to be incomplete with the most basic wikipedia search.
I'm not seeing how the tweet is mocking the Pony developers. It seems to mirror the tone and the content of of the documentation in the screenshot. It looks like an absurdist spin on the ivory tower vs industry meme, and it doesn't make anyone the butt of the joke.
Thanks for replying! I took a look at the thread in question and you're totally right. In context, this is unambiguously snide. I've been fortunate that my learning and working environments have been absolutely free of this kind of mean-spirited nonsense, so it really took me by surprise.
> But is Pony doing something unsound? Absolutely not. It is totally fine to define 1/0 = 0. Nothing breaks
a=x/N
b=y/N
If a==b, then x==y
No longer true, with this change. Essentially a variety of mathematical properties of numbers in the Real space don't hold when you allow division by 0.
I think this is the crucial bit. Division by zero in fields means nothing, but if you want to tack on calculus (part of pretending that doubles are reals) then zero is a perfectly good limit for division and it turns out that defining it as anything at all breaks your system.
I didn't like the blogpost, because it's smug, and doesn't even mention this obvious objection.
No, you are assuming that 1/0= "undefined" where "undefined" is a magical value. It's not. It literally means 'That operation has no definition, and there is no reasonable result to return'.
Many languages handle this in a practical way by creating a special value "undefined", "NaN", or others that has special properties. But let's be clear that "0" is a normal number in the real number space, as so expectations about properties of real numbers are not going to hold up.
When there is no reasonable result to return does it really matter what result is returned? 1 / 0 == 0 is about the same as 1 / 0 == 3. To avoid this just don't do 1 / 0 in your program.
“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.
While I fully agree, I'd like to point out that reducing specifically to 0/0 = 0 is more generally useful (ie. maintains intuition) than x/0 = 0, which breaks intuition.
Given a/b = c, your intuition of finding c is to get a number such that c×b = a.
c×0 = 0 has an infinite number of solutions, 0 being a particularly practical one.
c×0 = 1 (and more generally a≠0) has no solution, especially in the reduced explanation of multiplication as taking integer multiples of a value.
(Also note that having 0/0 = 0 maintains symmetry and continuity of the function y = 0/x.)
Some people say "oh, that's easy, 1/0 is +Infinity". So the real fun is at 0/0.
The limit of x/y as x and y go to zero depends on which path across the xy plane you take towards the singularity. Along one approach, the limit is 0, along another approach the limit diverges to infinity, along yet another the limit is 17.
I'm not kidding! Go to https://www.geogebra.org/3d and enter "x/y" and spin the graph around. The "value" at x=0 y=0 is the entirety of the z-axis.
For another perspective, try http://www.wolframalpha.com/input/?i=z%3Dx%2Fy and turn on contour mode for the 3D plot. Notice how the contour lines radiate out from the z-axis; each of those is an "approach" to the singularity at a different z-value, and taking the limit along each line leads to a different value.
Take the limit as x goes to 0 of (17*x)/(x). Both numerator and denominator go to 0, so this is a representation of 0/0. The limit is then equal to 17.
Right, it just means the limit of that path tends to 17. It's not a well-defined limit.
In a function of one-variable, there's a distinction between one-sided and two-sided limits. I don't know what the terminology would be for multivariable functions, but this is closer in nature to a one-sided limit.
But think about what a limit is. Think of X and Y as their own functions. so something more like X(g) / Y(g). As g increases, X and Y can take any path across the plane that they want. We get to arbitrarily choose what X and Y are. All we are doing is describe how our limit behaves as we slide along the scale towards infinity. Just because g increased by went from 10 to 11 doesn't mean that X and Y behaved the same way. We can arbitrarily choose X and Y such the limit as g approaches infinity is 0 for both, but the way that X and Y are changing is different. Like the example above, if we choose X and Y such that X(g)/Y(g) is 17 for all g, but the X and Y both approach 0 as g approaches infinuty, then as g approaches infinity X and Y go to 0, but X / Y (0 / 0), goes to 17. It's not a true 0/0, because the functions we chose got to 0 at different rates.
The answer keeps being 17, even as x and y both get vanishingly close to zero.
I encourage you to play around with a 3D graphing calculator and see all the different paths you can take along that surface to reach the singularity. They all "reach" it at different heights.
In calculus you're supposed to learn that y/0 with y != 0 is "undefined" (±Inf with limit expressions), while 0/0 is "indeterminate" (can construct any value using a limit expression that contains x/x with x -> 0).
I would argue 1/0 is infinity. Not with mathematics, just logically. By using the wording "how many times does 0 go into 1?"
You bring up 0/0. But 0/<anything> is already defined, it's 0. So 0/infinity = 0
Programmatically, I think I've always wanted X/0 to be 0. For example: progress bars, currency, or damage in a video game. It wouldn't be very helpful to have infinity be an answer there.
I encourage you to look at the graphs. Yes, the value along the y-axis is 0, and the value along the x-axis approaches positive and negative infinity. It's path-dependent. Take a look.
In float yes. In int there's no Inf. There's only MAX_INT or 0 or throw an exception.
Normal langs throw. That what the checked int div will do. But the unchecked int div has no return type which allows throwing an error. And pony is strongly typed, unlike most other langs. That's why it can guarantee much more safeties and performance than all other languages.
I like your point here. I think 1/0 = Infinity+ is a satisfying expression. Its a clear concept which can be visualized in a simple graph.
I think 0/0 is a different concept than 1/0. It's a different expression. 0/0 doesn't explicitly express a particular "path" on the graph.
We can call it (0/0) different names if we want. They can say 0/0 = "undefined". I am currently satisfied with 0/0 simply equals to 0/0, or simply "undefined".
If we all agree it is "undefined" we ironically defined it.
>I like your point here. I think 1/0 = Infinity+ is a satisfying expression. Its a clear concept which can be visualized in a simple graph.
Except it isn't. It still depends on which side you take the path from - from the positive denominator or the negative denominator side. (This is why IEEE 754 has a single signless infinity).
No it doesn't. I don't know where you got that idea, but it can't be from ever writing any floating point code, or looking at the IEEE-754 standard, or the floating point format. Please see https://www.h-schmidt.net/FloatConverter/IEEE754.html and stop spreading radically wrong misinformation.
> It still depends on which side you take the path from - from the positive denominator or the negative denominator side.
In IEEE-754, 1/0 == Infinity and 1/-0 == -Infinity.
Since the "1/0 = 0" is only defined for integer division then I'd argue that the chosen constant should be MAX_INT. (or MIN_INT in case of signe values and negative numerator)
Unlike what the author says, this is the total opposite to a practical/pragmatic solution.
He does not prove that this is a useful representation, only that given his own axioms, this can be considered mathematically correct.
Very practical issues with 1/0 == 0:
- This result is counter-intuitive, took building a custom fields and responding to the incredulity of all.
- The main reason this is counter-intuitive is not mentionned in the post: division is no longer monotonous.
1/0.5 = 2
1/0.25 = 4
1/0.0001 = 10000
1/0 = 0
This is calling for an Ariane 5-type crash because an underflow error caused a value to suddenly fall from 10e6 to 0.
floating point numbers in Pony follow the standard and return Infinity for division by zero. integer division by zero is undefined behavior and something each programming language has to decide how to handle.
I think this is calling for a Pony programmer working with floating point to know how their own basic operators function. Wrapping division in a function that checks for zero will give you the proper result you would like to return.
> This is calling for an Ariane 5-type crash because an underflow error caused a value to suddenly fall from 10e6 to 0.
That’s the opposite of what happened. A value overflowed, which triggered an exception, which caused a module to emit diagnostic information, which was misinterpreted by other systems as flight data. Interestingly, the value which overflowed was part of a system which was only used until LT+7, which had aleady passed…
In short, if the overflow had simply saturated or wrapped around to 0 or given some other garbage result, the Ariane would have not crashed.
This thread is showing once again that reading comprehension is not our strong-suit here on HN.
The author does not once say that Pony's choice is a good one, only that whether it is a good or bad one should be settled by engineering consequences, and that there is no purely mathematical argument that precludes it.
I can't help but think it _is_ a bad idea, because it's easier to overlook a 0 appearing than a NaN. That argument isn't math, though.
The Pony devs did chime in and mentioned that they do define division by zero to be NaN (or positive infinity) where the underlying type supports it (e.g. IEEE 754 floats).
Most integer representations have no space for such a value, so the only choices available to language developers are:
1. Throw an exception or otherwise consider it an error
2. Define the result to be 0 or 1 or some other integer value (0 being the only good choice)
3. Use a non-standard integer representation
Most languages opt for option 1, Pony chose 2, and I've never seen 3, perhaps due to it requiring so much software interference and precluding inter-operation with other languages.
592 comments
[ 4.5 ms ] story [ 313 ms ] threadhttps://twitter.com/westurner/status/960508624849244160
> How many times does zero go into any number? Infinity. [...]
> How many times does zero go into zero? infinity^2?
What value does 1/x approach?
What about 2/x?
And then, what about ∞/x? What value would we expect that to approach? ∞(±∞)
https://en.wikipedia.org/wiki/Principle_of_least_astonishmen...
However:
> 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.
I am looking forward to this write up.
Saying that is easy and common. Can you come up with a contrived example?
But see renormalization. https://en.wikipedia.org/wiki/Renormalization?wprov=sfla1
The issue with special definitions is you can use them to say anything you want, turning regular, common operations into weirdness.
What does it mean to take a factorial on the real numbers, or to add only on the even integers? In both cases, we're twisting what are generally accepted mechanics and domains into something else to get a funny result, like 1/0 = 0.
He gets to that point here:
" We can say that division’s domain is all the real numbers except zero. 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.
"
So, tiny change in definition --> big change in outcome.
*I'm an undergrad
The answer is that the gamma function is the unique logarithmically convex extension of the factorial function.
The properties of the standard gamma function are great, but some might prefer the properties of Hadamard's or Luschny's alternative gamma function.
Like many arbitrary extensions in mathematics -- be it the factorial function or the division function which deals with 1 / 0 differently -- it's a matter of taste and convenience!
Interestingly the arbitrariness of some mathematical choices seem to unnerve folks on an almost existential level. My guess is that it conflicts with their expectation of capital T truth from mathematics.
I don't think that's exactly the same problem.
It is perfectly valid to define an operation on a particular domain. Defining an add operation on even numbers is perfectly fine (If you had said odd, well...). Factorial on real numbers is more or less the Gamma function. The problem here is that the operation is defined on one domain...
> We can say that division’s domain is all the real numbers except zero.
...but then, for some reason, it is decided that will will be applied on a different domain. That is, that we're going to apply on all real numbers including zero. So now we need to modify the definition of the operation. And the thing is that, the new definition, created to accommodate the new domain, usually tends to produce friction precisely on the new elements added to the domain. We excluded zero initially because that way the operation was defined in a simpler way. Now, having to consider zero implies that our definition becomes more "complex".
Now, we can change the definition in different ways. Is any one of those objectively "better" or "worse" than the rest? Well, that's what the discussion is all about.
So at least that's something
It's also nothing. :-)
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
Again, this is a naive example but one that could manifest itself with a very imprecise result when y = 0Even without Pony's assumption, that's only true when y != 0.
That is how fractions are handled in higher math. (Either called "localization" or "ring of fractions").
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.
Zero is not a very good NaN.
1 != 0*0
I don't see the inconsistency. Abstract math vs practical application.
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.
This seems just as bizarre, since zero times anything shouldn't become 1, no matter how big or how many times you do it.
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.
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.
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.
Standard definition of division function, d:
d(x, y) = x * y⁻, for all x and y EXCEPT 0
Author's modified, piecewise (https://en.wikipedia.org/wiki/Piecewise) definition:
d(x, y) = x * y⁻, for all x and y EXCEPT 0
d(x, y) = 0, for y = 0
He's just adding 0 to the domain of d(x, y) to extend the definition, and deliberately not using xy⁻ for that particular element of the domain. No inverse needed.
Er... that's what mathematics is. It's a word game - we build systems from arbitrary rules and then explore the results.
Look through https://www.mathgoodies.com/articles/numbers for a bunch of uncommonly-defined numbers.
Try to state this definition formally. The statement: ∀ x,y . x/y = xy⁻¹ is not a theorem of fields or a definition of division. However, ∀ x, y . y ≠ 0 ⇒ x/y = xy⁻¹ is, but is completely unaffected by defining division at 0. Those who think they see a problem rely on informal and imprecise definitions. Could you formally state a theorem that is affected? That would help you get around issues that are merely artifacts of imprecision.
But let's entertain you, and state that what we really mean by the informal and vague statement, "division is the inverse of multiplication," could be stated formally as:
You are absolutely correct that this equational theorem is broken by extending the domain of division. However, there is absolutely no way to say that the formalization of this theorem isn't actually because the two are equivalent. You cannot then claim that something is necessarily broken if you choose to pick a formalization that is indeed broken, while an equivalent formalization exists, that is not broken (not to mention that the formalization that is broken requires a strictly richer language). All that means is that your formalization in this case is brittle, not that laws are broken.The hole that he is filling here isn't one that he bored into the standard definition, but a hole that the standard definition already admitted. If something is explicitly undefined, there's nothing mathematically wrong with defining it, as long as the definition doesn't lead to inconsistency.
The definition does lead to inconsistency...you can't look at the field axioms, observe that 0 has no multiplicative inverse, then proceed to define a special, one-off division rule that doesn't involve multiplicative inverses for that one element. Either your division rule is pathological and breaks a fundamental field property or you've introduced a division rule which is just a syntactical sugar, not a real operation (in the latter case you've introduced confusing notation, not a new division function). Why do you think mathematicians explicitly state that the real field with the augmentation of positive and negative infinity (which allow division by 0) is not a field?
I don't understand why there is so much resistance to this idea in this thread, but the simple fact remains that if you define division by an additive identity (0) in any way, the field containing that unit ceases to be a field. This is because all elements cease to be unique. You can quickly prove that every element is equal to every other element, including (critically) the additive and multiplicative identity elements. Fields are defined by closure under the operations of addition and multiplication, and that closure requires uniqueness of their respective identities. Upend that and your entire field structure breaks down, because all you're left with is a field with a single element 0.
Stating that you've defined division by 0 using a one-off case that permits all other field identities to remain consistent is like saying you've turned the complex field into an ordered field using lexicographic ordering. You haven't, because i admits no ordering, much like 0 admits no multiplicative inverse.
Onlookers reading these comments probably think those of us harping on this point are anal pedants with a mathematical stick up our ass. But this thread is increasingly illustrating my central point, which is that the author shouldn't have tried to justify numerical operation definitions in a programming language using field axioms of all things.
Why not? What mathematical axiom does this break?
> Either your division rule is pathological and breaks a fundamental field property
It doesn't, or you could show one here: https://news.ycombinator.com/item?id=17738558
> or you've introduced a division rule which is just a syntactical sugar, not a real operation
Is this math? We define symbols in formal math using axioms. I am not aware of a distinction between "syntactical sugar" and a "real operation."
> Why do you think mathematicians explicitly state that the real field with the augmentation of positive and negative infinity (which allow division by 0) is not a field?
That's simple: because unlike the addition of the axiom ∀x . x/0 = 0, adding positive and/or negative infinity does violate axioms 2, 7 and possibly 11 (depending on the precise axioms introducing the infinities).
> I don't understand why there is so much resistance to this idea in this thread, but the simple fact remains that if you define division by an additive identity (0) in any way, the field containing that unit ceases to be a field.
Because a field is defined by the axioms I've given here (https://news.ycombinator.com/item?id=17738558) and adding division by zero does not violate any of them. If you could show what's violated, as I have for the case of adding infinities and as done in actual math rather than handwaving about it, I assume there would be less resistance. I don't understand your resistance to showing which of the field axioms is violated.
> You can quickly prove that every element is equal to every other element, including (critically) the additive and multiplicative identity elements.
So it should be easy to prove using the theory I provided, which is the common formalization of fields. Don't handwave: write proofs, and to make sure that the proofs aren't based on some vagueness of definitions, write them (at least the results of each step) formally. The formalization is so simple and straightforward that this shouldn't be a problem.
> Stating that you've defined division by 0 using a one-off case that permits all other field identities to remain consistent is like saying you've turned the complex field into an ordered field using lexicographic ordering. You haven't, because i admits no ordering, much like 0 admits no multiplicative inverse.
Stop handwaving. Show which axioms are violated.
You can't use your own stubbornness to justify itself.
I'm waiting for you to justify your claim that this extension to division breaks any of the field axioms. pron even made you a nice list of them.
Just name one equation/theorem that the new axiom would break.
I'm completely open to being convinced! But so far you've only given arguments about giving a multiplicative inverse to zero. Everyone agrees on that. It's the wrong argument.
This is getting to be Kafkaesque...it breaks the field axioms themselves. How many different explanations and external resources do I need to provide in this thread for you to be convinced that this is not a controversial point in modern mathematics? I just explained it in the comment you responded to.
You have exactly two options here.
If you define x/0, that definition must interact with the rest of the definitions and elements of the field. To maintain multiplicative closure (a field axiom!) there must be a unique y element equal to x/0. So tell me how you will define x/0 such that x is not equal to the product of 0 and y. Regardless of what you think the author has shown, the burden of proof is not on me at this point to show that you can't do it, because it follows directly from the field axioms. Trying to impose a one-off bizarro divisor function defined only on {0} is not only mathematically inelegant, it immediately eliminates the uniqueness of all field elements. Therefore your "field" just becomes {0}, and since it lacks a multiplicative identity it ceases to be a field. There is your contradiction. Why don't you tell me how you're going to prove any equation defined over a field that relies on the uniqueness or cancellation properties of fields?
On the other hand, let's say you tell me you want define x/0 so that the definition doesn't interact with any of the field definitions or elements. Then you haven't actually introduced any new operation or definition, you've just designed a notation that looks a lot like division but has no mathematical bearing on the field itself (i.e. absolutely nothing changes, including for 0). That's not a divisor function, it's just a confusing shorthand. You can't just add another axiom to a field and call it a field.
If you believe I'm stubborn, that's fine. I might be a poor teacher! There are ample resources online which will patiently explain this concept in mind numbing detail. It boggles my mind that there are people in this thread still fighting an idea in earnest which has been settled for over a century.
So there are two separate issues here. One is whether we can extend the definition of the "/" operator, and the other is whether we call it "division".
I'm not interested in what we call it. I'm interested in the claim that extending "/" will break the field.
The dichotomy you're talking about is wrong. The two options are not "multiplicative inverse" and "does not interact with anything". "1/0 = 0" interacts with plenty! If I make a system where it's an axiom, I can calculate things like "1/0 + 5" or "sqrt(1/0)" or "7/0 + x = 7". I can't use it to cancel out a 0, but I can do a lot with it.
> It boggles my mind that there are people in this thread still fighting an idea in earnest which has been settled for over a century.
Remember, the question is not "should this be an axiom in 'normal' math?", the question is "does this actually conflict with the axioms of a field?"
> You can't just add another axiom to a field and call it a field.
Yes you can. There is an entire hierarchy of algebraic structures. Adding non-conflicting axioms to an X does not make it stop being an X.
• Our first function f(x, y) is defined for all x in F, and all nonzero y in F. That is, the domain of this function f is (F × F\{0}). The definition of this function f is:
f(x, y) = x times the multiplicative inverse of y
(Note that in the definition of f(x,y) we could say "if y≠0", but whether we say it or not the meaning is the same, because the domain of f already requires that y≠0.)
• Our second function g(x, y) is defined for all x in F, and all y in F. That is, the domain of this function g is (F × F). To define this function g, we pick a constant C in F, say C=0 or C=1 (or any C∈F, e.g. C=17 if 17 is an element of our field). And having picked C, the definition of this function g is:
• g(x, y) = x times the multiplicative inverse of y, if y ≠ 0, and C otherwise [that is, g(x, 0) = C].
Note that this function is defined for all (x, y) in F×F, and when y≠0 it agrees with f, i.e. g(x,y) = f(x,y) when y≠0.
Would you agree that both of these are functions, on different domains?
Next, we have the notation x/y. To assign meaning to this notation (and to the word “division”), there are two conventions we could adopt:
• Convention 1: When we say "x/y", we will mean f(x,y) (as defined above) — that is, x * y^{-1}.
• Convention 2: When we say "x/y", we will mean g(x,y) (as defined above).
The point of the post is that we can well adopt Convention 2: with such a definition of "division", all the properties that were true of f (on the domain F×F\{0}) continue to be true of g, except that g is defined on a wider domain.
----------------------------------------------
Now, maybe Convention 2 offends you. Maybe you think there is something very sacred about Convention 1. In all your posts in this thread, you seem to be insisting that "division" or "/" necessarily have to mean Convention 1, and the provided justification for preferring Convention 1 seems circular to me — here are some of your relevant comments, with my comments in [square brackets]:
> Since there is no multiplicative inverse of 0, division by 0 is undefined behavior [This seems to be saying: Because of Convention 1, we cannot adopt Convention 2.]
> Since y = x/0, it follows that the product of y and 0 is equal to x, because division is the inverse of multiplication [Here, your reasoning is "because we adopt Convention 1"]
> 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. [Again, you're stating that Convention 1 has to hold, by fiat.]
> 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 [This is just stating repeatedly that we have to adopt Convention 1.]
> A multiplicative inverse is a division. [This is merely insisting that Convention 1 has to be adopted, not Convention 2]
> divisor cannot exist unless it is a multiplicative inverse [Again, stating Convention 1.]
> you can't look at the field axioms, observe that 0 has no multiplicative inverse, then proceed to define a special, one-off division rule that doesn't involve multiplicative inverses for that one element. [Why not?] ...you've introduced a division rule which is just a syntactical sugar [yes the same is true of Convention 1; what's the problem?]
All these comments, which emphatically insist on Convention 1, seem to ignore the point of the article, which is that Convention 2 has no more mathematical problems than Convention 1, because the function g is no less a “valid” function than the function f.
In mathematics when we use words like “obvious” or insist...
I don't take issue with division by 0 - you can do that in mathematics just fine! I take issue with defining that division and calling the consequent system a field when it's not a field, and acting as though everyone else is wrong. The author invited this criticism when they loaded in the full formalism of field theory without needing to.
If the author had just stated they wanted to define division by zero that wouldn't be a problem. I have no idea why they felt the need to pull in abstract mathematics. I'm not disagreeing with their point, I'm taking issue with the strange and incorrect way they defended it.
Note that in my top level comment I specifically said, "Mathematics does not give us truths, it gives us consequences." I will happily agree with you that there is usefulness and coherence in a definition of 0. There is no canonical truth about the world regarding that matter. But a direct consequence of defining any division by 0 is that you cease to have an algebraic field.
Therefore, using field theory to defend a system which defines division by 0 doesn't make sense. It's not that the system is "wrong" for some meaning of wrongness. It's that you shouldn't be trying to pigeonhole field theory to make it work, because you don't need to.
> But don't use field theory to justify convention 2, because it's mathematically incoherent
> defining that division and calling the consequent system a field when it's not a field
> a direct consequence of defining any division by 0 is that you cease to have an algebraic field
If you go back to my comment (the one you're replying to), both the functions f and g assume a field F, and they are well-defined functions on F×F\{0} and on F×F respectively. (Do you agree?) For example, F may be the field of real numbers. Forget about the word “division” for a moment: do you think there is something about the function g, that makes F not a field?
To put it differently: I agree with you that it is a direct consequence of defining a multiplicative inverse of 0 that you cease to have an algebraic field. But the only way this statement carries over when we use the word “division”, is if we already adopt Convention 1 (that “division” means the same as “multiplicative inverse”).
Again, I think you are implicitly adopting Convention 1: you're saying something like “if we adopt Convention 2, then x/y means the function g and includes the case when y=0, but [something about multiplicative inverses, implicitly invoking Convention 1], therefore there's a problem". But there's no problem!
It is not a direct consequence of defining the function g(x,y) that something ceases to be a field: it is a consequence only if you also insist on Convention 1, namely if you try to assign a multiplicative inverse to 0 (which everyone here agrees is impossible).
Let me emphasize: whether we adopt Convention 1 or Convention 2, there is no problem; we still have the same field F.
[1] https://www.hillelwayne.com/post/divide-by-zero/
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.
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
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 that maintains the other field axioms.
3. Since y = x/0, it follows that the product of y and 0 is equal to x, because division is the inverse of multiplication. By the field axioms, division does not exist if there is no multiplicative inverse with which to multiply.
4. But by the field axioms this implies that x = 0, which contradicts our initial assumption. Likewise, since we can repeat this procedure with any element x in F, this demonstrates that there exists no nonzero element x in F, and in fact F = {0}.
The failure in the article's refutation is that this proof is designed to permit you to assume you have suitably defined division by zero, then proceed to demonstrate without any loss of generality that you could not possibly have unless 1) F is not a field, or 2) F contains only 0. The fundamental algebraic property you sacrifice by defining division by zero is uniqueness, and uniqueness is a hard requirement in fields with nonzero elements.
Can you explain how this follows? I thought division was only the inverse of multiplication for all nonzero denominators, which would mean we can't use that definition for deduction in x/0.
It might hinge on your next sentence:
>By the field axioms, division does not exist if there is no multiplicative inverse with which to multiply.
but I don't understand why that's necessarily true. I don't understand how the field axioms require division by x to require the existence of a multiplicative inverse of x when x is zero. Sorry to take a bunch of your Friday, but I'm very curious now. Explanation much appreciated.
-------
edit:
Come to think of it, couldn't I define x/y as cotton candy for all x,y in field F and still satisfy the field axioms? They just don't refer to division.
Any connection between x/y and y's multiplicative inverse is just a nice convention. That convention states that x/y = x * mult_inv(y) when y != 0, but nothing else. That definition has nothing to do with the field axioms and changing it doesn't require that I change anything about multiplicative inverses. That means I don't touch the field axioms and my field is still a field.
Yes. That's the thesis of the article. Make an arbitrary choice for 1 / 0 = ?, and if it helps you, use it. It's mathematically, rigorously fine.
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 that causes an issue, and it requires the use of a language with a dom operator, something that is absolutely not required for theories of fields), it won't matter because the question is not whether one could come up with a formalization that leads to contradiction, but whether there are reasonable formalizations of fields where this does not happen, and there are (in fact, most of them satisfy this, as they do not rely on a dom operator).
In addition, it is not true that "by the field axioms, division does not exist if there is no multiplicative inverse with which to multiply." It's just that the field axioms do not define what the meaning of division is in that case. Defining it, however, does not lead to contradiction with the axioms, at least not a contradiction you've point out. In fact, most common languages of mathematics cannot even explicitly express the statement "x is not in the domain of f." All they can do is define f(x) for values of x in the domain, and not define f(x) for values outside it. The "exist" in your statement does not refer to ordinary mathematical existence (usually formally expressed with the existential quantifier) but to an informal notion of definedness (discussed by Feferman) that has no formal counterpart in most formal systems, because it is very rarely needed; it is certainly not needed to state the field axioms.
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.
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.
>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.
This is intuitively mistaken. If "when you divide by 0 .. nothing happens at all", then how come multiplication by 0 is zero, when they're both operations against 0? The problem is that mathematicians have forgotten the meaning of 0. Anything multiplied by zero is zero. Anything divided by zero is zero. This agrees with normal intuition on working with nothingness, and the original idea from Brahmagupta.[ https://www.storyofmathematics.com/indian_brahmagupta.html]
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.
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...
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
>>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).
1: https://en.wikipedia.org/wiki/1_%2B_2_%2B_3_%2B_4_%2B_%E2%8B...
> 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 :)
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.
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.
[0] https://ziglang.org/documentation/master/#Standard-Library-M...
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.
The entire point of the article was suggesting you can define a consistent system without multiplication and division being entirely symmetrical (as they already are not)
What do you mean?
The common way to resolve that is and be consistent is to axiomatically decide:
1) there is no inverse of * 0
2) 0 is not part of the range permitted for 1/x
The point of the article is that another way to resolve it and be consistent is to axiomatically decide:
1) there is no inverse of * 0
2) 0 is part of the range permitted for 1/x, and the resulting value is 0.
As in, (x/y) * y=x is true either way only if y!=0. The only difference is whether when y=0 if it is not true because it is just illegal or if it is not true because (x/0) * 0 = 0 for all x.
Sure, I understand this claim. What I don't understand is the precise meaning of the claim "multiplication and division already are not entirely symmetrical." I don't know any existing technical meaning of "entirely symmetrical" for a pair of operations, but let's suppose that I switch the operations in your statement:
> (x/y) * y = x is true [for all x] only if y != 0.
Then I get:
> (x * y)/y = x is true [for all x] only if y != 0.
That's also true. What's the asymmetry?
As the article explains, the whole issue about dividing by 0 is the lack of multiplicative inverse. If you define division for 0 as something other than multiplication by the multiplicative inverse, there is no longer an issue doing the division. Hope that helps.
The math that we all learn up through highschool is a system with a carefully chosen set of axioms that happen to be useful in most cases and has become the default system, but there isn't some intrinsic property of it that makes it "math" and alternate consistent set of axioms "not math".
And dividing by 0.5 is breaking into how many pieces exactly?
*disclamer: I have no math background whatso ever
The reason it's a useful function is it has some properties:
y=1/x is continuous except where x==0. That is, as you approach 0 from either side, it grows to either +- infinity. The developers of this language want to make this function ==0 when x is 0.
You can do that, sure, but it doesn't change the fact that when you go from +0.0000001 to -0.0000001, you now have 2 non-continuous jumps instead of just one.
So all that to say: We can't treat 0 like a number.
*disclaimer: I have no math background whatsoever, this is just a fun topic.
Multiplying by the square root of 2 is also a fun one since you need limits to show people that real numbers only make sense with the least upper bound theorem and limits and things they expect to work "intuitively" (like division or multiplication) only have approximate meaning when they use the common operations.
Reals are fundamentally different and are not found in things like computers and in general are of no practical use. For work with values (as opposed to counts) we use something called floating point.
This explains exactly why we shouldn't divide by 0. The pieces after breakage should, if one is so inclined, be able to be re-assembled into the whole; but, once you break something into 0 pieces, it is gone. Thus at best `0/0` could be defined … but the problem there is not that there's no answer but that every answer is equally good.
It's not always what you want, but it's pretty reasonable. The alternative would be if it always rounds up, which seems weirder to me. I don't think rounding to the nearest integer makes sense with integer quantities at all, that's strictly a real number operation.
When we first teach children about division we teach them that, "17/5 = 3 with a remainder of 2". It is only later that they learn about decimal points and learn to say that 3.4 is the answer.
I dunno, if I'm dividing a quantized space, which is a fairly common thing to do, its exactly what I want.
> (unless you cast all you numbers to float which is a pain to do).
Using floats just gets you different wrong answers than using integers, unless you happened to somehow have ints to start and want a floating point approximation, which I find is less likely than wanting integer division.
What you really want for exact division where there are integers involved is to have at least one operand specified as a rational; this also takes less keystrokes, if its a literal, than changing it to a float to get an inexact answer.
Related to this, prior to Ruby 2.5, the standard library include "mathn", a library which monkey-patched all the numeric types so that operations on them acted pretty much like Ruby had a Scheme-style numeric tower, but since that has process-wide effects not restricted to where the library is required, that was deprecated in 2.2 and removed in 2.5.
No, you haven't. You've merely failed to locate any. You've said "I'm not going to prove that this works. I'm going to assume that it does and act as if it did, and place the burden on you to prove otherwise."
> Lawrence Paulson, professor of computational logic and inventor of Isabelle: > > [...] This identity holds in quite a few different proof assistants now.
Excellent point. It's not even known if we can get any inconsistencies without making this definition; and it's known that, if it's true that we can't get any inconsistencies without it, then we can't prove that it's true. Building on such possibly shaky foundations can't make them stronger.
From this definition, I'd guess that pony isn't optimized for numerical code and floating point operations, because there it tends to make less sense.
1.0 / 0.0 = infinity per the standard.
1/0 = undefined behavior and is left to language implementers to decide how to handle.
Erm, when we say it's "undefined" we mean it literally -- standard mathematical systems of arithmetic do not define a value for that division.
If you make another system of arithmetic you can define it how you want and be consistent with "regular maths" for the operations in which things are defined. It's an extension.
> We have "NaN" for a reason
Funnily enough, IEEE754 defines 1/0 as positive infinity, not Nan. But none of these things are "the truth" in any reasonable sense of the word, just "useful systems".
Defining it as 0 at least means floating point numbers are (presumably) closed under arithmetic operations, which could be handy.
They already are closed. Floating point includes Inf and Nan for that reason. :-)
Mathematicians define equality of fractions by stating that a/b = c/d if and only if a·d = b·c. This means that if we define 1/0 = 1 then 0 = 1.
To be fair, this is perfectly consistent, except everything in our system is equal to zero.
Equality of fractions is defined differently when zero divisors are allowed in the denominator. A zero divisor is a non-zero number that can multiply with another non-zero number to get zero. For example, if we work mod 12 then 3 is a zero divisor because 3·4 = 0.
If we want to allow zero or zero divisors in our denominators then we say that a/b = c/d if and only if there is some value s such that s·(a·d - b·c) = 0 where s is anything allowable in the denominator. If we are working with the integers, including this s term does nothing because s has to be something that can be a denominator and we only allow non-zero denominators.
So, even if we define 1/0 = 0 then literally every fraction would be equal to every other fraction.
These conventions can be broken (like, for example, addition of floating point numbers is not associative as pointed out by other comments) but it is definitely not "natural". In other fields of mathematics, like measure theory, it is possible to define things like "zero times infinity is zero" which is traditionally undefined but is a convenient shortcut and does not break anything that people working in measure theory care about.
For more: https://en.wikipedia.org/wiki/Localization_of_a_ring#For_gen...
That's not implied, so far as I can tell.
a / b = 1 / 0, thus
a * d = b * c => 1 * d = 0 * c => d = 0
So all you can say is that d = 0, or at most that c / 0 = 0. Is there some extra step you're taking?
I mean, what the mathematical definition of division says is not that 1/0 is indeed something and that that something is "undefined" or "NaN" or anything else really. What it says is "I cannot do 1/0, the division operation a/b does not apply when b is 0".
So 1/0 is not a thing in itself in mathematics; it's something which cannot be operated.
Now, back some time ago, "division by zero" simply threw an error. It signaled "this is not something that can be done". undefined, NaN, anything else, including 0, is not really something that has a mathematical justification. It's merely a practical approach to encapsulate that error into some form of pseudo-value to control it to some extent.
Personally, I don't really see how 1/0 = 0 is better than 1/0 = NaN or "undefined" or "Infinity".
For example, say if a zero divide happens with normalized values. Meaning the immediate result is only off by one at most. Odds of catching that are probably low. Meanwhile, a NaN will infect all numbers that come into contact with it, bubbling up faster...
Under this system, programs are easier to debug if they use bigger numbers... That property does not seem like a win to me.
If I attempt to open a file, but an access fault occurs, I'd rather be told the fault and given a chance to recover than receive an empty file.
But I don't know anything about Pony or it's goals. So it may be preferable for them, I don't know.
(Sorry, I'm not sure which way you mean it)
I find particularly interesting Leslie Lamport's comment that "Since 0 is not in the domain of recip, we know nothing about the value of 1 / 0", which I think is the most correct mathematical stance.
Then again, I think it is all a red herring. This (Pony's decision) is not about the mathematical definition of division. This is about the trade-offs computational systems do to manage the situation.
But that isn't my only qualm.
In the construction of the fields, there is a simple definition of the division function. It is intrinsically the solution of a = r * b, where r is the unknown. If a is nonzero, and b is zero, then r, the ratio, is said not to exist. Put another way, there is no real value of r that can be chosen that satisfies r * 0 = a. See [1] for example, as 0 is not an invertible element of the field over the reals.
So ... I can't say I agree with their choice of 1/0 == 0. They may be free to choose any value they wish, but then from an aesthetic viewpoint, do they really want to surprise the user?
[1] https://en.wikipedia.org/wiki/Multiplicative_group
Exactly. That's the definition of division. Here, he is introducing a totally different definition and claiming it isn't wrong because it is consistent. I mean, by his logic I could define division as a/b := a-b and claim it is consistent and therefore not wrong, but that is obviously not division...
What proportion of the time will a divide-by-zero operation be a symptom of a bug, where evaluating 1/0 as any valid number will make it harder to identify that bug?
There might be a mathematical justification for 1/0 = 0, but the computer science justification seems tenuous at best. The overwhelming majority of the time, I want divide-by-zero to throw an exception or evaluate to NaN. I'd far rather deal with the edge case of intentionally dividing by zero, rather than the not-at-all-uncommon case of unintentionally dividing by zero and getting unexpected behaviour as a result.
If you’re dividing floats, you will get NaN or Infinity as expected. Just like how, if you overfloat a float, you’ll get Infinity. Floating-point has well-defined semantics, which CPUs are required to adhere to, and languages just expose.
If you divide “CPU integers” by (CPU integer) 0, the result is undefined. Just like how, if you overflow a “CPU integer”, the result is undefined. There is no standard semantics being adhered to. There is no equivalent of IEEE754 for CPU integers. There is only convention, and convention has no universal answer at these edge-cases. Thus, a language is free to do whatever it wants in response to either. There are no formal semantics to expose.
Usually, a language that calls itself “safe” will choose to make CPU integers behave a lot like real integers, by generating checks and throwing exceptions for the edge cases.
And usually, a language that calls itself “low-level” will just expose whatever semantics the CPU integers of its host platform already possess. In the case where there’s still an impedance mismatch (i.e. in the case of division by CPU-integer-0 where you don’t actually get any output into a result register), the language has to make something up. To “go with the flow” of how CPU integers work, probably it should be something fast.
Thus, 1/0=0 kinda sorta makes sense. It is an operation on the field of “CPU integers” that vaguely “fits in” with the existing ones. No mathematical relevance, but just fine from the perspective of someone e.g. seeking to create a higher-level abstract machine targeting the Pony compiler, where you’d still just insert a divisor check before doing the division op if you wanted the result to make any sense.
https://en.wikipedia.org/wiki/Division_by_zero
a=x/N
b=y/N
If a==b, then x==y
No longer true, with this change. Essentially a variety of mathematical properties of numbers in the Real space don't hold when you allow division by 0.
I didn't like the blogpost, because it's smug, and doesn't even mention this obvious objection.
Many languages handle this in a practical way by creating a special value "undefined", "NaN", or others that has special properties. But let's be clear that "0" is a normal number in the real number space, as so expectations about properties of real numbers are not going to hold up.
Sure, and both are bad.
> To avoid this just don't do 1 / 0 in your program.
If you're going to avoid doing it, better to have it throw an exception if you do it by accident.
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.
If a==b and N≠0, then x==y
EDIT: Formatting
"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.
Given a/b = c, your intuition of finding c is to get a number such that c×b = a.
c×0 = 0 has an infinite number of solutions, 0 being a particularly practical one.
c×0 = 1 (and more generally a≠0) has no solution, especially in the reduced explanation of multiplication as taking integer multiples of a value.
(Also note that having 0/0 = 0 maintains symmetry and continuity of the function y = 0/x.)
The Post JavaScript Apocalypse https://youtu.be/99Zacm7SsWQ?t=2434
The limit of x/y as x and y go to zero depends on which path across the xy plane you take towards the singularity. Along one approach, the limit is 0, along another approach the limit diverges to infinity, along yet another the limit is 17.
I'm not kidding! Go to https://www.geogebra.org/3d and enter "x/y" and spin the graph around. The "value" at x=0 y=0 is the entirety of the z-axis.
For another perspective, try http://www.wolframalpha.com/input/?i=z%3Dx%2Fy and turn on contour mode for the 3D plot. Notice how the contour lines radiate out from the z-axis; each of those is an "approach" to the singularity at a different z-value, and taking the limit along each line leads to a different value.
How would a path lead to 17?
17 / 1
1.7 / 0.1
0.17 / 0.01
0.017 / 0.001
...
0 / 0
In a function of one-variable, there's a distinction between one-sided and two-sided limits. I don't know what the terminology would be for multivariable functions, but this is closer in nature to a one-sided limit.
I encourage you to play around with a 3D graphing calculator and see all the different paths you can take along that surface to reach the singularity. They all "reach" it at different heights.
You bring up 0/0. But 0/<anything> is already defined, it's 0. So 0/infinity = 0
Programmatically, I think I've always wanted X/0 to be 0. For example: progress bars, currency, or damage in a video game. It wouldn't be very helpful to have infinity be an answer there.
Why infinity and why not negative infinity.
Normal langs throw. That what the checked int div will do. But the unchecked int div has no return type which allows throwing an error. And pony is strongly typed, unlike most other langs. That's why it can guarantee much more safeties and performance than all other languages.
I think 0/0 is a different concept than 1/0. It's a different expression. 0/0 doesn't explicitly express a particular "path" on the graph.
We can call it (0/0) different names if we want. They can say 0/0 = "undefined". I am currently satisfied with 0/0 simply equals to 0/0, or simply "undefined".
If we all agree it is "undefined" we ironically defined it.
Except it isn't. It still depends on which side you take the path from - from the positive denominator or the negative denominator side. (This is why IEEE 754 has a single signless infinity).
No it doesn't. I don't know where you got that idea, but it can't be from ever writing any floating point code, or looking at the IEEE-754 standard, or the floating point format. Please see https://www.h-schmidt.net/FloatConverter/IEEE754.html and stop spreading radically wrong misinformation.
> It still depends on which side you take the path from - from the positive denominator or the negative denominator side.
In IEEE-754, 1/0 == Infinity and 1/-0 == -Infinity.
Not for integers.
He does not prove that this is a useful representation, only that given his own axioms, this can be considered mathematically correct.
Very practical issues with 1/0 == 0:
- This result is counter-intuitive, took building a custom fields and responding to the incredulity of all. - The main reason this is counter-intuitive is not mentionned in the post: division is no longer monotonous.
1/0.5 = 2 1/0.25 = 4 1/0.0001 = 10000 1/0 = 0
This is calling for an Ariane 5-type crash because an underflow error caused a value to suddenly fall from 10e6 to 0.
That’s the opposite of what happened. A value overflowed, which triggered an exception, which caused a module to emit diagnostic information, which was misinterpreted by other systems as flight data. Interestingly, the value which overflowed was part of a system which was only used until LT+7, which had aleady passed…
In short, if the overflow had simply saturated or wrapped around to 0 or given some other garbage result, the Ariane would have not crashed.
The author does not once say that Pony's choice is a good one, only that whether it is a good or bad one should be settled by engineering consequences, and that there is no purely mathematical argument that precludes it.
I can't help but think it _is_ a bad idea, because it's easier to overlook a 0 appearing than a NaN. That argument isn't math, though.
Most integer representations have no space for such a value, so the only choices available to language developers are:
1. Throw an exception or otherwise consider it an error
2. Define the result to be 0 or 1 or some other integer value (0 being the only good choice)
3. Use a non-standard integer representation
Most languages opt for option 1, Pony chose 2, and I've never seen 3, perhaps due to it requiring so much software interference and precluding inter-operation with other languages.
https://news.ycombinator.com/item?id=17737308
https://news.ycombinator.com/item?id=17737158
That seems sub-optimal.
Devil's advocate: why not a maximum integer like 18446744073709551615 or 9223372036854775807?
0 looks like a valid number, while 18446744073709551615 is an obvious NaN for any programmer looking at the output.
In some domains it might be. In others it might not. It's no more right or wrong in my mind.
I think the size of the integer needs to be considered in your thinking as well:
If you have unsigned 8 bit integers, the max value is 255, is that really going seem NaN? How about 127 for a signed 8 bit integer?
And, should the result of division by zero vary based on the bit size of the integer? That's a discussion unto itself.