I am a maths researcher at the university of Cologne and adressed this in a thesis I wrote in 2016. See chapter 3, especially the first part of section 3.1.

Dividing by zero is totally well defined for the projectively extended real numbers (only one unsigned infinity inf) but the argument for the usual extended real numbers (+-inf) not working is not based on field theory, but of infinitisemal nature, given you can approach a zero-division both from below and above and get either +inf or-inf equally likely.

Defining 1/0=0 not only breaks this infinitiseminal form, it‘s also radically counterintuïtive given how the values behave when you approach the division from small numbers, e.g. 1/10, 1/1, 1/0.1, 1/0.001…

lim x->0 1/x = 0 makes no sense and is wrong in terms of limits.

See the thesis where I proved a/0=inf to be well-defined for a!=0.

tl;dr: There‘s more to this than satisfying the field conditions. If you redefine division, this has consequences on higher levels, in this case most prominently in infinitisemal analysis.

I used to be a maths researcher, and would just like to point out that some of the people who define division by zero to mean infinity do it because they’re more interested in the geometric properties of the spaces that functions are defined on than the functions themselves. This is the reason for the Riemann sphere in complex analysis, where geometers really like compact spaces more than noncompact ones, so they’re fine with throwing away the field property of the complex numbers. The moment any of them need to compute things, however, they pick local coordinates where division by zero doesn’t happen and use the normal tools of analysis.

Thanks for laying this out and pointing out the issue with +/- Inf

Could you summarize here why +Inf is a good choice. As a practical man I approach this from the limit standpoint - usually when I end up with a situation like this it’s because the correct answer is +/- Inf and it depends on the context which one it should be. Here context means on which side of zero was my history of the denominator.

The issue is that the function 1/x has a discontinuity at 0. I was taught that this means 1/0 is “undefined”. IMO in code this means throw an exception.

In practical terms I end up adding a tiny number to the denominator (e.g. 1e-10) and continuing, but that implicitly means I’m biased to the positive side of line.

It is not +inf, but inf. For the projectively extended real numbers, we only extend the set with one infinite element which has no sign. Take a look at page 18 of the thesis which includes an illustration of this. Rather than having a number line we have a number circle.

Dividing by zero, the direction we approach the denominator does not matter, even if we oscillate around zero, given it all ends up in one single point of infinity. We really don’t limit ourselves here with hat as we can express a limit to +inf or -inf in the traditional real number extension by the direction from which we approach inf in the projectively extended real numbers (see remark 3.5 on page 19).

1/x is discontinuous at 0, this is true, but we can always look at limits. :) I am also a practical man and hope this relatively formal way I used to describe it did not distract from the relatively simple idea behind this.

Pony’s approach is reasonable within field theory, but it’s not really useful when almost the entire analytical building on top of it collapses on your head. NaN was invented for a reason and given the IEEE floating-point numbers use the traditional +-inf extension, they should just return the indeterminate form on division by zero in Pony.

NaN only exists for floating point, not integers. If you want to use NaN or something like it for integers, you will need to box all integer numbers and take a large performance hit.

I when I have more time (work is very busy) will be writing up the rational and features etc that lead Pony to the place that a decision like this had to be made. No one on the Pony team liked ending up there. But fortunately we are a 1.0 language and can continue to evolve and change things. We also thought it was very important to call to call out the issue because it is surprising.

It’s easy for a Pony user to create their own integer division operation that will be partial. Additionally, a “partial division for integers” operator has been been in the works for a while and will land soon. Its part of operators that will also error if you have integer overflow or underflow. Those will be +?, /?, *?, -?.

For those wanting the rationale, this is in the same Pony article:

“From a practical perspective, having division as a partial function is awful. You end up with code littered with trys attempting to deal with the possibility of division by zero. Even if you had asserted that your denominator was not zero, you’d still need to protect against divide by zero because, at this time, the compiler can’t detect that value dependent typing. So, as of right now (ponyc v0.2), divide by zero in Pony does not result in error but rather 0.”

Im sure many of us would find it interesting. I have a total, mental block on divide by zero given it’s always a bug in my field. This thread is refreshingly different. :)

Totally, but I am saying that there are specific cases where this may still throw people off and cause bugs - even when the typing is as expected here.

Another system where division by zero is possible is wheel theory, which is similar to the system described here in that 1/x is not always the multiplicative inverse of x, as indeed it isn’t when x = 0.

Theory. I think the confusion stems from using the same symbol to denote two different functions. If we denote addition by a, multiplication by m and inverse by i then the problem can be summarised as follows:

a and m are functions from K × K to K.

i is a function from K \ { 0 } to K.

When we see x / y we usually think of a function d(x, y) = m(x, i(y)) and this is a function from K × K \ { 0 } to K.

However, we can define a different function d’ from K × K to K such that the restriction of d’ to K × K \ { 0 } is d.

Using / to denote both d and d’ is what is causing confusion. Some people see 1 / 0 = 1 and assume it means 1 · 0⁻¹ = 1 (and I find this thought natural) but what is really meant is f(1, 0) = 0 where f could be d or d’ or something else entirely.

Here’s an unsurprising summary: You can define an arbitrary function f on a field and it won’t “break” the field in any way. You can introduce an inconsistency if in addition to the definition you add some claims about it’s properties that are related to the field but a definition alone cannot wreak havoc.

Practice. There are practical implications though. This whole discussion proves that there’s a lot of confusion over what the / symbol actually means. People assume it’s function d written using an infix notation. I think that making / denote d’ can be surprising to lots of people and cause them to introduce bugs.

If I see code like

if a / b == 0:
...

then it is natural for me to conclude that: a is zero and b is non-zero. In other words, it’s natural for me to think of function d and not of d’ or any other function. However, if / means d’ then my reasoning does not hold.

We can define / to mean anything we want, swap + and -, swap the meaning of digits, and do all sorts of syntactic changes without changing the meaning of these symbols. Computers don’t care but programmers do and this whole discussion is the best evidence that this change will cause lots of confusion.

Mathematicians generally avoid defining this d’ in any way because there is no canonical choice of what the extra value should be. In category theoretic terms, there is no universal property that such a function satisfies that forces a choice unique up to isomorphism.

This means that everyone is free to pick their own value that makes sense for them, which leads to inconsistencies and, for the lack of a better word, portability problems of theorems between theories that picked different values. That’s again why we generally don’t see people picking any value to define a d’, and when they do anything of the sort they usually have their sights set on things that don’t depend heavily on that value.

this fails with 1/0 = 0 because 1 is not equal to 0*0.

Edit: I was wrong, it is mathematically sound. You can define x/0 = f(x) any function of x at all. All the field axioms still hold because they all have preconditions that ensure you never look at the result of division by zero.

There is a subtlety because some people say (X) and others say (Y)

(X) a/b = c should be equivalent to a = c*b when the LHS is well defined

(Y) a/b = c should be equivalent to a = c*b when b is nonzero

If you have (X) definition in mind it becomes unsound, if you are more formal and use definition (Y) then it stays sound.

It seems like a very bad idea to make division well defined but the expected algebra rules not apply to it. This is the whole reason we leave it undefined or make it an error. There isn’t any value you can give it that makes algebra work with it.

It will not help programmers to have their programs continue on unaware of a mistake, working on with corrupt values.

It will not help programmers to have their programs continue on unaware of a mistake, working on with corrupt values

That was my initial reaction too. But I don’t think Pony’s intended use case is numerical analysis; it’s for highly parallel low-latency systems, where there are other (bigger?) concerns to address. They wanted to have no runtime exceptions, so this is part of that design tradeoff. Anyway, nothing prevents the programmer from checking for zero denominators and handling them as needed. If you squint a little, it’s perhaps not that different from the various conventions on truthy/falsey values that exist in most languages, and we’ve managed to accommodate to those.

Those truthy/falsey values are an often source of errors.

I may be biased in my dislike of this “feature”, because I cannot recall when 1/0 = 0 would be useful in my work, but have no difficulty whatsoever thinking of cases where truthy/falsey caused problems.

It will not help programmers to have their programs continue on unaware of a mistake, working on with corrupt values.

I wonder if someone making a linear math library for Pony already faced this. There are many operations that might divide by zero, and you will want to let the user know if they divided by zero.

It’s easy for a Pony user to create their own integer division operation that will be partial. Additionally, a “partial division for integers” operator has been been in the works for a while and will land soon. Its part of operators that will also error if you have integer overflow or underflow. Those will be +?, /?, *?, -?.

While I don’t think I agree that it’s a good idea, note that the RISC-V ISA also allows division by zero, producing all-bits-set instead of a trap. (See the commentary in section 6.2 here for their rationale.)

“We considered raising exceptions on integer divide by zero, with these exceptions causing a trap in
most execution environments. However, this would be the only arithmetic trap in the standard
ISA (floating-point exceptions set flags and write default values, but do not cause traps) and
would require language implementors to interact with the execution environment’s trap handlers
for this case. Further, where language standards mandate that a divide-by-zero exception must
cause an immediate control flow change, only a single branch instruction needs to be added to
each divide operation, and this branch instruction can be inserted after the divide and should
normally be very predictably not taken, adding little runtime overhead.

The value of all bits set is returned for both unsigned and signed divide by zero to simplify
the divider circuitry. The value of all 1s is both the natural value to return for unsigned divide,
representing the largest unsigned number, and also the natural result for simple unsigned divider
implementations. Signed division is often implemented using an unsigned division circuit and
specifying the same overflow result simplifies the hardware.”

Does it also set a flag? If so, that seems perfectly reasonable. The value returned shouldn’t matter as long as you can use out-of-band info to check for divide by zero. Although, I suppose you could just check for zero before the divide… Hmm. So I guess really it doesn’t matter at all. It makes sense to have the result be whatever is easiest to implement.

It appears it just returns the special value with no flags or traps. You have to explicitly check for it on every division. They claim this is to simplify circuitry.

I think it’s fine to make fun of things. Also I think it’s a bad idea but mostly because it really should be a different type so I can account for when I have a divide by 0, because usually when I divide by zero it’s by accident and I probably meant to actually do something else. Maybe in some domain though this isn’t true. They also claim not to have the concept of null so it’s hard as a casual passerby to understand why you wouldn’t want to be able to express a space for a specific type that is yet to be filled.

You cannot define 1/0 and still have a field. There’s no value that works. Even when you do things like the extended real numbers where x/0 = infinity, you’re really just doing a kind of shorthand and you acknowledge that the result isn’t a field.

You can of course define any other algebraic structure you want and then say that operating on the expression 1/0 is all invalid because you didn’t define anything else and no other theorem applies, but this is not very helpful. You can make bad definitions that don’t generalise, sure, definitions that aren’t fields. But to paraphrase a famous mathematician, the difficulty lies not in the proofs but in knowing what to prove. The statement “1/0 = 0 and nothing else can be deduced from this” isn’t very interesting.

I want to make an attempt to clarify the discussion here because I think there is some substance I found interesting. I don’t have a strong opinion about this.

The article actually defines an algebraic structure with three operators: (S, +, *, /) with some axioms. It happens that these axioms makes it so (S, +, *) is a field (just like how the definition of a field makes (S, +) a group).

The article is right in saying that these axioms do not lead to a contradiction. And there are many non-trivial such structures.

However, the (potential) issue is that we don’t know nearly as much about these structures than we do about fields because any theorem about fields only apply to (S, +, *) instead of (S, +, *, /). So all the work would need to be redone. It could be said that the purpose of choosing a field in the first place is to benefit from existing knowledge and familiar expectations (which are no longer guarantteed).

I guess formally adding an operator means you should call it something else? (Just like how we don’t call fields a group even though it could be seen as a group with an added * operator.)

This has no bearing on the 1/0 = 0 question however, which still works from what’s discussed in the article.

As I understand it, you’ve only defined the expression 1/0 but you are saying that /0 isn’t shorthand for the multiplicative inverse of 0 as is normally the case for /x being x^-1, by definition. Instead, /0 is some other kind of magical non-invertible operation that maps 1 into 0 (and who knows what /0 maps everything else into). Kind of curious what it has to do with 0 at all.

So I guess you can do this, but then you haven’t defined division by zero at all, you’ve just added some notation that looks like division by zero but instead just defined some arbitrary function for some elements of your field.

If you do mean that /0 is division by zero, then 1/0 has to be, by definition, shorthand for 1*0^-1 and the arguments that you’ve already dismissed apply.

The definition of a field makes no statements about the multiplicative inverse of the additive identity (https://en.wikipedia.org/wiki/Field_(math)#Classic_definition). Defining it in a sound way does not invalidate any of the axioms required by the field, and, in fact, does define division by zero (tautologically). You end up with a field and some other stuff, which is still a field, in the same way that adding a multiplication operator on a group with the appropriate properties leaves you with a group and some other stuff.

The definition of the notation “a / b => a * b^-1” assumes that b is not zero. Thus, you may define the case when b is 0 to mean whatever you want.

That people want to hold on to some algebraic “identities” like multiplying by the denominator cancels it doesn’t change this. For that to work, you need the assumption that the denominator is not zero to begin with.

And when b is zero, what is division? That’s the whole point of this argument. What properties does an operation need to have in order to be worthy of being called a division?

Indeed, it is the whole point. For a field, it doesn’t have to say anything about when you divide by zero. It is undefined. That doesn’t mean that you can’t work with and define a different, but still consistent, structure where it is defined. In fact, you can add the definition such that you still have the same field, and more.

edit: Note that this doesn’t mean that you’re defining a multiplicative inverse of zero. That can’t exist and still be a field.

In what way is it consistent? Consistent with what? As I understand it, you’re still saying that the expression 1/0 is an exception to every other theorem. What use is that? You still have to write a bunch of preconditions, even in Coq, saying how the denominator isn’t zero. What’s the point of such a definition?

It seems to me that all of this nonsense is about not wanting to get an exception when you encounter division by zero, but you’re just delaying the problem by having to get an exception whenever you try to reason with the expression 1/0.

I mean that the resulting structure is consistent with the field axioms. The conditions on dividing by zero never go away, correct. And yes, this is all about avoiding exceptions in the stack unwinding, programming language sense. The article is a response to the statements that defining division by zero in this way causes the structure to not be a field, or that it makes no mathematical sense. I am also just trying to respond to your statements that you can’t define it and maintain a field.

It really doesn’t make mathematical sense. You’re just giving the /0 expression some arbitrary value so that your computer doesn’t raise an exception, but what you’re defining there isn’t division except notationally. It doesn’t behave like a division at all. Make your computer do whatever you want, but it’s not division.

Mathematical sense depends on the set of axioms you choose. If a set of axioms is consistent, then it makes mathematical sense. You can disagree with the choices as much as you would like, but that has no bearing on the meaning. Do you have a proof that the resulting system is inconsistent, or even weaker, not a field?

I don’t even know what the resulting system is. Is it, shall we say, the field axioms? In short, a set on which two abelian operations are defined, with two distinct identities for each abelian operation, such that one operation distributes over the other? And you define an additional operation on the distributing operation that to each element maps its inverse, except for the identity which instead is mapped to the identity of the distributed-over operation?

It’s a field where the definition of division is augmented to include a definition when the divisor is zero. It adds no new elements, and all of the same theorems apply.

That doesn’t make it not a field; you don’t have to have a division operator at all to be a field, let alone a division operator that is defined to be multiplication by the multiplicative inverse.

zeebo gave the same answer I would give: a / b is a multiplied by the multiplicative inverse of b when b is not zero. This article is all about how a / 0 is not defined and so, from an engineering perspective, you can define it to be whatever you want without losing the property that your number representation forms a field. You claimed that defining a / 0 = 1 means that your numbers aren’t a field, and all I’m saying is that the definition of the division operator is 100% completely orthogonal to whether or not your numbers form a field, because the definition of a field has nothing to say about division.

Also, this whole “a field definition doesn’t talk about division” is a bit of misunderstanding of mathematical idioms. The field definition does talk about division since “division” is just shorthand for “multiplicative inverse”. The reason the definition is written the way it is (excluding 0 from having a multiplicative inverse) is that giving zero a multiplicative inverse results in contradictions. When you say “ha! I won’t let that stop me! I’m going to define it anyway!” well, okay, but then either (1) you’re not definining a multiplicative inverse i.e. you’re not defining division or (2) you are defining a multiplicative inverse and you’re creating a contradiction.

(I had a whole comment here, but zeebo is expressing themselves better than I am, and there’s no point in litigating this twice, especially when I feel like I’m just quoting TFA)

@hwayne Calling the pony developers smug for that is a bit misleading with the missing context… Pony has checked exceptions, calls that can fail need to be annotated with ‘?’ . If division could fail a whole bunch of functions would need annotations defeating the value of ‘?’ as a documentation tool.

This means 1/0 == 0 is practical in pony to avoid typing ‘?’ everywhere.

It’s not 100% clear but I’m referring to the original tweet being smug: the person who made the “we men of industry” tweet. I cut off their username to anonymize them.

I am a maths researcher at the university of Cologne and adressed this in a thesis I wrote in 2016. See chapter 3, especially the first part of section 3.1.

Dividing by zero is totally well defined for the projectively extended real numbers (only one unsigned infinity inf) but the argument for the usual extended real numbers (+-inf) not working is not based on field theory, but of infinitisemal nature, given you can approach a zero-division both from below and above and get either +inf or-inf equally likely.

Defining 1/0=0 not only breaks this infinitiseminal form, it‘s also radically counterintuïtive given how the values behave when you approach the division from small numbers, e.g. 1/10, 1/1, 1/0.1, 1/0.001…

lim x->0 1/x = 0 makes no sense and is wrong in terms of limits.

See the thesis where I proved a/0=inf to be well-defined for a!=0.

tl;dr: There‘s more to this than satisfying the field conditions. If you redefine division, this has consequences on higher levels, in this case most prominently in infinitisemal analysis.

I used to be a maths researcher, and would just like to point out that some of the people who define division by zero to mean infinity do it because they’re more interested in the geometric properties of the spaces that functions are defined on than the functions themselves. This is the reason for the Riemann sphere in complex analysis, where geometers

reallylike compact spaces more than noncompact ones, so they’re fine with throwing away the field property of the complex numbers. The moment any of them need to compute things, however, they pick local coordinates where division by zero doesn’t happen and use the normal tools of analysis.Thanks for laying this out and pointing out the issue with +/- Inf

Could you summarize here why +Inf is a good choice. As a practical man I approach this from the limit standpoint - usually when I end up with a situation like this it’s because the correct answer is +/- Inf and it depends on the context which one it should be. Here context means on which side of zero was my history of the denominator.

The issue is that the function 1/x has a discontinuity at 0. I was taught that this means 1/0 is “undefined”. IMO in code this means throw an exception.

In practical terms I end up adding a tiny number to the denominator (e.g. 1e-10) and continuing, but that implicitly means I’m biased to the positive side of line.

I think Pony’s approach is flat out wrong.

It is not +inf, but inf. For the projectively extended real numbers, we only extend the set with one infinite element which has no sign. Take a look at page 18 of the thesis which includes an illustration of this. Rather than having a number line we have a number circle.

Dividing by zero, the direction we approach the denominator does not matter, even if we oscillate around zero, given it all ends up in one single point of infinity. We really don’t limit ourselves here with hat as we can express a limit to +inf or -inf in the traditional real number extension by the direction from which we approach inf in the projectively extended real numbers (see remark 3.5 on page 19).

1/x is discontinuous at 0, this is true, but we can always look at limits. :) I am also a practical man and hope this relatively formal way I used to describe it did not distract from the relatively simple idea behind this.

Pony’s approach is reasonable within field theory, but it’s not really useful when almost the entire analytical building on top of it collapses on your head. NaN was invented for a reason and given the IEEE floating-point numbers use the traditional +-inf extension, they should just return the indeterminate form on division by zero in Pony.

NaN only exists for floating point, not integers. If you want to use NaN or something like it for integers, you will need to box all integer numbers and take a large performance hit.

Just curious, but why isn’t 1/0=1? Would 1/0=Inf not require that infinity exists between 0 and 1?

I’m not sure I understand your question. Does 1/2=x require x to be between 1 and 2?

A couple of notes:

I when I have more time (work is very busy) will be writing up the rational and features etc that lead Pony to the place that a decision like this had to be made. No one on the Pony team liked ending up there. But fortunately we are a 1.0 language and can continue to evolve and change things. We also thought it was very important to call to call out the issue because it is surprising.

It’s easy for a Pony user to create their own integer division operation that will be partial. Additionally, a “partial division for integers” operator has been been in the works for a while and will land soon. Its part of operators that will also error if you have integer overflow or underflow. Those will be

`+?`

,`/?`

,`*?`

,`-?`

.https://playground.ponylang.org/?gist=834f46a58244e981473c0677643c52ff

For those wanting the rationale, this is in the same Pony article:

“From a practical perspective, having division as a partial function is awful. You end up with code littered with trys attempting to deal with the possibility of division by zero. Even if you had asserted that your denominator was not zero, you’d still need to protect against divide by zero because, at this time, the compiler can’t detect that value dependent typing. So, as of right now (ponyc v0.2), divide by zero in Pony does not result in error but rather 0.”

I’m going to be (when I have time) writing a longer and more detailed discussion of the issue.

Im sure many of us would find it interesting. I have a total, mental block on divide by zero given it’s always a bug in my field. This thread is refreshingly different. :)

I’ll post it on lobste.rs when its done and I’ve had several people review and give feedback.

Thanks!

This is very true. The fact that division by zero causes us to write so many guards can cause major issues.

I wonder, though, won’t explicit errors be better than implicit unexpected results which may be caused by this unusual behavior?

I guess if you write a test before writing code, it should be possible to spot the error either way?

It would be good to push this to the type system exactly so that we don’t have to remember to test for it.

Totally, but I am saying that there are specific cases where this may still throw people off and cause bugs - even when the typing is as expected here.

Sure…

ifyou write a test…Another system where division by zero is possible is wheel theory, which is similar to the system described here in that 1/x is not always the multiplicative inverse of x, as indeed it isn’t when x = 0.

Here’s an interesting Stack Exchange post.

Theory. I think the confusion stems from using the same symbol to denote two different functions. If we denote addition bya, multiplication bymand inverse byithen the problem can be summarised as follows:aandmare functions from K × K to K.iis a function from K \ { 0 } to K.d’from K × K to K such that the restriction ofd’to K × K \ { 0 } isd.Using

`/`

to denote bothdandd’is what is causing confusion. Some people see 1 / 0 = 1 and assume it means 1 · 0⁻¹ = 1 (and I find this thought natural) but what is really meant is f(1, 0) = 0 wherefcould bedord’or something else entirely.Here’s an unsurprising summary: You can define an arbitrary function

fon a field and it won’t “break” the field in any way. You can introduce an inconsistency if in addition to the definition you add some claims about it’s properties that are related to the field but a definition alone cannot wreak havoc.Practice. There are practical implications though. This whole discussion proves that there’s a lot of confusion over what the`/`

symbol actuallymeans. People assume it’s functiondwritten using an infix notation. I think that making`/`

denoted’can be surprising to lots of people and cause them to introduce bugs.If I see code like

then it is natural for me to conclude that:

ais zero andbis non-zero. In other words, it’s natural for me to think of functiondand not ofd’or any other function. However, if`/`

meansd’then my reasoning doesnothold.We can define

`/`

to mean anything we want, swap`+`

and`-`

, swap the meaning of digits, and do all sorts of syntactic changes without changing the meaning of these symbols. Computers don’t care but programmers do and this whole discussion is the best evidence that this change will cause lots of confusion.Mathematicians generally avoid defining this

d’in any way because there is no canonical choice of what the extra value should be. In category theoretic terms, there is no universal property that such a function satisfies that forces a choice unique up to isomorphism.This means that everyone is free to pick their own value that makes sense for them, which leads to inconsistencies and, for the lack of a better word, portability problems of theorems between theories that picked different values. That’s again why we generally don’t see people picking any value to define a

d’, and when they do anything of the sort they usually have their sights set on things that don’t depend heavily on that value.Bad idea, it should error or give NaN.

It’s not mathematically sound.

a/b = c should be equivalent to a = c*b

this fails with 1/0 = 0 because 1 is not equal to 0*0.

Edit:I was wrong, it is mathematically sound. You can define x/0 = f(x) any function of x at all. All the field axioms still hold because they all have preconditions that ensure you never look at the result of division by zero.There is a subtlety because some people say (X) and others say (Y)

(X) a/b = c should be equivalent to a = c*b when the LHS is well defined

(Y) a/b = c should be equivalent to a = c*b when b is nonzero

If you have (X) definition in mind it becomes unsound, if you are more formal and use definition (Y) then it stays sound.

It seems like a very bad idea to make division well defined but the expected algebra rules not apply to it. This is the whole reason we leave it undefined or make it an error. There isn’t any value you can give it that makes algebra work with it.

It will not help programmers to have their programs continue on unaware of a mistake, working on with corrupt values.

I really appreciate your follow-up about you being wrong. It is rare to see, and I commend you for it. Thank you.

This is explicitly addressed in the post. Do you have any objections to the definition given in the post?

I cover that exact objection in the post.

That was my initial reaction too. But I don’t think Pony’s intended use case is numerical analysis; it’s for highly parallel low-latency systems, where there are other (bigger?) concerns to address. They wanted to have no runtime exceptions, so this is part of that design tradeoff. Anyway, nothing prevents the programmer from checking for zero denominators and handling them as needed. If you squint a little, it’s perhaps not that different from the various conventions on truthy/falsey values that exist in most languages, and we’ve managed to accommodate to those.

Those truthy/falsey values are an often source of errors.

I may be biased in my dislike of this “feature”, because I cannot recall when 1/0 = 0 would be useful in my work, but have no difficulty whatsoever thinking of cases where truthy/falsey caused problems.

1/0 is integer math. NaN is available for floating point math not integer math.

I wonder if someone making a linear math library for Pony already faced this. There are many operations that

mightdivide by zero, and you will want to let the user know if they divided by zero.It’s easy for a Pony user to create their own integer division operation that will be partial. Additionally, a “partial division for integers” operator has been been in the works for a while and will land soon. Its part of operators that will also error if you have integer overflow or underflow. Those will be

`+?`

,`/?`

,`*?`

,`-?`

.https://playground.ponylang.org/?gist=834f46a58244e981473c0677643c52ff

While I don’t think I agree that it’s a good idea, note that the RISC-V ISA also allows division by zero, producing all-bits-set instead of a trap. (See the commentary in section 6.2 here for their rationale.)

“We considered raising exceptions on integer divide by zero, with these exceptions causing a trap in most execution environments. However, this would be the only arithmetic trap in the standard ISA (floating-point exceptions set flags and write default values, but do not cause traps) and would require language implementors to interact with the execution environment’s trap handlers for this case. Further, where language standards mandate that a divide-by-zero exception must cause an immediate control flow change, only a single branch instruction needs to be added to each divide operation, and this branch instruction can be inserted after the divide and should normally be very predictably not taken, adding little runtime overhead.

The value of all bits set is returned for both unsigned and signed divide by zero to simplify the divider circuitry. The value of all 1s is both the natural value to return for unsigned divide, representing the largest unsigned number, and also the natural result for simple unsigned divider implementations. Signed division is often implemented using an unsigned division circuit and specifying the same overflow result simplifies the hardware.”

Does it also set a flag? If so, that seems perfectly reasonable. The value returned shouldn’t matter as long as you can use out-of-band info to check for divide by zero. Although, I suppose you could just check for zero before the divide… Hmm. So I guess really it doesn’t matter at all. It makes sense to have the result be whatever is easiest to implement.

It appears it just returns the special value with no flags or traps. You have to explicitly check for it on every division. They claim this is to simplify circuitry.

I think it’s fine to make fun of things. Also I think it’s a bad idea but mostly because it really should be a different type so I can account for when I have a divide by 0, because usually when I divide by zero it’s by accident and I probably meant to actually do something else. Maybe in some domain though this isn’t true. They also claim not to have the concept of null so it’s hard as a casual passerby to understand why you wouldn’t want to be able to express a space for a specific type that is yet to be filled.

This is ill-advised.

You cannot define 1/0 and still have a field. There’s no value that works. Even when you do things like the extended real numbers where x/0 = infinity, you’re really just doing a kind of shorthand and you acknowledge that the result isn’t a field.

You can of course define any other algebraic structure you want and then say that operating on the expression 1/0 is all invalid because you didn’t define anything else and no other theorem applies, but this is not very helpful. You can make bad definitions that don’t generalise, sure, definitions that aren’t fields. But to paraphrase a famous mathematician, the difficulty lies not in the proofs but in knowing what to prove. The statement “1/0 = 0 and nothing else can be deduced from this” isn’t very interesting.

Could you explain why, formally, defining 1/0=0 means you no longer have a field?

I want to make an attempt to clarify the discussion here because I think there is some substance I found interesting. I don’t have a strong opinion about this.

The article actually defines an algebraic structure with

threeoperators: (S, +, *, /) with some axioms. It happens that these axioms makes it so (S, +, *) is a field (just like how the definition of a field makes (S, +) a group).The article is right in saying that these axioms do not lead to a contradiction. And there are many non-trivial such structures.

However, the (potential) issue is that we don’t know nearly as much about these structures than we do about fields because any theorem about fields only apply to (S, +, *) instead of (S, +, *, /). So all the work would need to be redone. It could be said that the purpose of choosing a field in the first place is to benefit from existing knowledge and familiar expectations (which are no longer guarantteed).

I guess formally adding an operator means you should call it something else? (Just like how we don’t call fields a group even though it could be seen as a group with an added * operator.)

This has no bearing on the 1/0 = 0 question however, which still works from what’s discussed in the article.

As I understand it, you’ve only defined the expression 1/0 but you are saying that /0 isn’t shorthand for the multiplicative inverse of 0 as is normally the case for /x being x^-1, by definition. Instead, /0 is some other kind of magical non-invertible operation that maps 1 into 0 (and who knows what /0 maps everything else into). Kind of curious what it has to do with 0 at all.

So I guess you can do this, but then you haven’t defined division by zero at all, you’ve just added some notation that looks like division by zero but instead just defined some arbitrary function for some elements of your field.

If you

domean that /0 is division by zero, then 1/0 has to be, by definition, shorthand for 1*0^-1 and the arguments that you’ve already dismissed apply.The definition of a field makes no statements about the multiplicative inverse of the additive identity (https://en.wikipedia.org/wiki/Field_(math)#Classic_definition). Defining it in a sound way does not invalidate any of the axioms required by the field, and, in fact, does define division by zero (tautologically). You end up with a field and some other stuff, which is still a field, in the same way that adding a multiplication operator on a group with the appropriate properties leaves you with a group and some other stuff.

The definition of the notation “a / b => a * b^-1” assumes that b is not zero. Thus, you may define the case when b is 0 to mean whatever you want.

That people want to hold on to some algebraic “identities” like multiplying by the denominator cancels it doesn’t change this. For that to work, you need the assumption that the denominator is not zero to begin with.

In what way, whatever it is you defined /0 to be, considered to be a “division”? What is division? Kindly define it.

Division, a / b, is equal to a * b^-1 when b is not zero.

And when b is zero, what is division? That’s the whole point of this argument. What properties does an operation need to have in order to be worthy of being called a division?

Indeed, it is the whole point. For a field, it doesn’t have to say anything about when you divide by zero. It is undefined. That doesn’t mean that you can’t work with and define a different, but still consistent, structure where it

isdefined. In fact, you can add the definition such that you still have the same field, and more.edit: Note that this doesn’t mean that you’re defining a multiplicative inverse of zero. That can’t exist and still be a field.

In what way is it consistent? Consistent with

what? As I understand it, you’re still saying that the expression 1/0 is an exception to every other theorem. What use is that? You still have to write a bunch of preconditions, even in Coq, saying how the denominator isn’t zero. What’s the point of such a definition?It seems to me that all of this nonsense is about not wanting to get an exception when you encounter division by zero, but you’re just delaying the problem by having to get an exception whenever you try to reason with the expression 1/0.

I mean that the resulting structure is consistent with the field axioms. The conditions on dividing by zero never go away, correct. And yes, this is all about avoiding exceptions in the stack unwinding, programming language sense. The article is a response to the statements that defining division by zero in this way causes the structure to not be a field, or that it makes no mathematical sense. I am also just trying to respond to your statements that you can’t define it and maintain a field.

It really doesn’t make mathematical sense. You’re just giving the /0 expression some arbitrary value so that your computer doesn’t raise an exception, but what you’re defining there isn’t division except notationally. It doesn’t behave like a division at all. Make your computer do whatever you want, but it’s not division.

Mathematical sense depends on the set of axioms you choose. If a set of axioms is consistent, then it makes mathematical sense. You can disagree with the choices as much as you would like, but that has no bearing on the meaning. Do you have a proof that the resulting system is inconsistent, or even weaker, not a field?

I don’t even know what the resulting system is. Is it, shall we say, the field axioms? In short, a set on which two abelian operations are defined, with two distinct identities for each abelian operation, such that one operation distributes over the other? And you define an additional operation on the distributing operation that to each element maps its inverse, except for the identity which instead is mapped to the identity of the distributed-over operation?

It’s a field where the definition of division is augmented to include a definition when the divisor is zero. It adds no new elements, and all of the same theorems apply.

I’m bailing out, this isn’t a productive conversation for either of us. Sorry.

You are correct. The field axioms are all still true, even if we extend / to be defined on 0.

The reason for this is that the axioms never “look at” any of the values x/0. They never speak of them. So they all hold regardless of what x/0 is.

That said, even though you can define x/0 without violating axioms it doesn’t mean you should. In fact it seems like a very bad idea to me.

That doesn’t make it not a field; you don’t have to have a division operator at all to be a field, let alone a division operator that is defined to be multiplication by the multiplicative inverse.

What is division?

zeebo gave the same answer I would give:

`a / b`

is`a`

multiplied by the multiplicative inverse of`b`

when`b`

is not zero. This article is all about how`a / 0`

is not defined and so, from an engineering perspective, you can define it to be whatever you wantwithout losing the property that your number representation forms a field. You claimed that defining`a / 0 = 1`

means that your numbers aren’t a field, and all I’m saying is that the definition of the division operator is 100% completely orthogonal to whether or not your numbers form a field, because the definition of a field has nothing to say about division.What is an engineering perspective?

Also, this whole “a field definition doesn’t talk about division” is a bit of misunderstanding of mathematical idioms. The field definition does talk about division since “division” is just shorthand for “multiplicative inverse”. The reason the definition is written the way it is (excluding 0 from having a multiplicative inverse) is that giving zero a multiplicative inverse results in contradictions. When you say “ha! I won’t let that stop me! I’m going to define it anyway!” well, okay, but then either (1) you’re not definining a multiplicative inverse i.e. you’re not defining division or (2) you are defining a multiplicative inverse and you’re creating a contradiction.

(I had a whole comment here, but zeebo is expressing themselves better than I am, and there’s no point in litigating this twice, especially when I feel like I’m just quoting TFA)

Me too, I’m tapping out.

@hwayne Calling the pony developers smug for that is a bit misleading with the missing context… Pony has checked exceptions, calls that can fail need to be annotated with ‘?’ . If division could fail a whole bunch of functions would need annotations defeating the value of ‘?’ as a documentation tool.

This means 1/0 == 0 is practical in pony to avoid typing ‘?’ everywhere.

It’s not 100% clear but I’m referring to the

original tweetbeing smug: the person who made the “we men of industry” tweet. I cut off their username to anonymize them.Oh ok, btw, your twitter account is a lot of fun. thanks for the laughs - everyone reading this follow him :)

a ÷ b means a ⋅ b⁻¹. Saying that 1 divided by 0 is 0 is nonsensical. It’s not well-defined.