Integer division by zero

Learn
1

I am new to Elm and until now I could not figure out why the expressions
0//5
and
5//0
both evaluate to 0. Mathematically, the first is ok, the second is wrong.

What’s the reason for this behavior?

Johannes

2

Under the hood it’s written as:

var _Basics_idiv = F2(function(a, b) { return (a / b) | 0; });

And in JavaScript, Infinity | 0 is equal to 0.

3

Reasons are practical, and not really as mathematically wrong as you might at first think, see also 1/0 = 0 by Hillel Wayne. Qouting from the conclusion

But is Pony doing something unsound? Absolutely not. It is totally fine to define 1/0 = 0 . Nothing breaks and you can’t prove something false.

4 Likes
4

My understanding is that division is defined as the inverse of multiplication such a / b = c if and only if a = b * c. Using that definition, it follows that if 1 / 0 = 0 then 1 = 0 * 0 = 0. This is a contradiction in the usual system of mathematics since 1 is assumed to be not equal to 0.

So I agree that it’s not mathematically wrong but it also doesn’t make sense in the typical system where 1 is not equal to 0 and division is defined as above.

1 Like
5

I think the key statement in the link @folkertdev provides that refutes your ‘inverse’ definition is that “0 does not have a multiplicative inverse”, so does not apply in this case.

I was always taught at school that the division operator is simply undefined for a denominator of 0, so any argument that states what the “mathematical” value should be is dubious at best. Better I think is to evaluate the implications of assigning a value (0 in the case of Elm’s //0) for this undefined operation, as @folkertdev’s link does.

1 Like
6

An issue with having division by 0 fail, is that the // function could not return Int. It would need to return Maybe Int to capture that case, making it very inconvenient to use.

I therefore think that this behavior is a compromise for practicality.

7

Just FTR, the same practical decision was taken in the Coq standard library. The functions have to be total so the options were using an option type (equivalent of Maybe) or a default value. Note that it could have been any value but zero is just the most natural. This doesn’t break any standard mathematical theorems because all these theorems already have to include a precondition that the denominator is nonzero (whether there is a default value or the division by zero is undefined).

2 Likes
8

Thank you all for your explanations. I’ve learned a lot.

Johannes

1 Like
9

This topic was automatically closed 10 days after the last reply. New replies are no longer allowed.