3 ms·

> The whole problem is one of formalization. "Undefined", as it's used in mathematics, is very much informal. It is used to say that a certain expression, 1/0,

> The whole problem is one of formalization. "Undefined", as it's used in mathematics, is very much informal. It is used to say that a certain expression, 1/0, while "grammatically" correct, is meaningless. Formal systems simply cannot do that: the expression 1/0 must either be ill-formed (can be done with dependent types but is often inconvenient) or it must mean something in the semantic domain of the language. Different formal system define what that something is, but whatever it is, it is no longer "undefined" in the informal sense. We're substantially in agreement here. This circles back to my core thesis - there is no point in defending the implementation of something mathematically undefined in a programming language by retreating to the formal axioms of fields (or any other algebraic structure, for that matter). Your other point about 1/0 = x for whatever you'd like x to be is something I mentioned in my comment. The extended real number system does something similar by defining arithmetic of positive and negative infinities. But the extended real number system is not a field. It's a fine and useful system, but you insert pathologies into the real field by trying to accept infinity as a real number. Likewise if you want 1/0 to be equal 42, that's fine. But you're going to "infect" everything that 42 touches in the process. You won't compromise arithmetic, but you will compromise the definition of a field. What I'm getting at is that 1) mathematically speaking, the author's entire preamble about division by 0 is both incorrect and irrelevant, 2) we should not be trying to justify implementation behavior in systems which cannot use real numbers through the wizardry of field theorems.

pron 8y ago
> But you're going to "infect" everything that 42 touches in the process How so? Remember that, e.g. ∀x . 0x ≠ 1 still holds, and it is not true that 0((1/0)(1/42)) = 1 because associativity doesn't apply, because associativity for division stems from the existence of a multiplicative inverse exists, and none does even though 1/0 = 42. > You won't compromise arithmetic, but you will compromise the definition of a field. Not at all. Formal systems of mathematics define fields (in general, not just in arithmetic) specifically with 1/0 = 0. Can you show a single field axiom or theorem that would be affected by this? Perhaps you could if you insisted on stating a theorem by using an informal term such as "wherever foo is defined," but 1/ those theorems can always be stated in more precise terms that don't make use of the informal notion of definedness, and 2/ very few formal systems formalize definedness in a way that means an undefined value must not be 42 (i.e. where you can actually prove 1/0 ≠ 42 or where 1/0 is ill-formed) -- see Feferman https://math.stanford.edu/~feferman/papers/definedness.pdf https://math.stanford.edu/~feferman/papers/definedness.pdf -- and AFAIK, such systems are very, very rarely used in practice.
- throwawaymath 8y ago
  At this point I've written a number of comments throughout this thread which explain why division by zero is not possible in a field - specifically, a field which contains nonzero elements. You are asking me to show you an axiom or theorem proving this, but I don't know how else to explain this to you since I've already explained it in a number of different ways. In a sibling comment I even write out the formal proof, and in others I've explained why the author's refutation is incorrect. I'm not sure what else to say. The author is wrong - it is not at all controversial among mathematicians that the algebraic structure of a field cannot support division by zero. Perhaps I'm simply a poor teacher - in that case I would refer you to [1], [2] and [3] for a better explanation. As I've said elsewhere, you can make a coherent algebra by extending a field - then division by 0 or infinity is possible. But it stops being a field - just as it cannot be many other algebraic structures. Therefore I feel very confident stating that 1) the author is wrong, 2) I've sufficiently explained why in these comments and 3) the burden isn't really on anyone to disprove that division by 0 works at this point. In any case, this entire discourse is ridiculous because the author should not be trying to defend programming language decisions using abstract mathematics. This kind of nuance and ambiguity is neither necessary nor relevant for justifying an implementation of defined behavior for division by zero. The whole exercise is a farcical distraction, to put it bluntly. Mathematics is pedantic by design, but this sort of definitional rigor is laughably unneeded and for defining integer and float-based arithmetic. The author does a disservice to what is an otherwise reasonable point by (incorrectly) justifying it with axiomatic field theory. It's self-indulgent over-engineering to try to prove division by zero in fields "works, no really!" from first principles for a programming language blog post; especially when mathematics is essentially united in saying, "no actually, it doesn't." __________________ 1. https://www.reddit.com/r/math/comments/3b5i6p/can_you_divide.. https://www.reddit.com/r/math/comments/3b5i6p/can_you_divide.... 2. http://mathworld.wolfram.com/DivisionbyZero.html http://mathworld.wolfram.com/DivisionbyZero.html 3. https://en.m.wikipedia.org/wiki/Division_by_zero https://en.m.wikipedia.org/wiki/Division_by_zero
  - deleted 8y ago
    [deleted]
  - 8y ago

pron 8y ago

> But you're going to "infect" everything that 42 touches in the process How so? Remember that, e.g. ∀x . 0x ≠ 1 still holds, and it is not true that 0((1/0)(1/42)) = 1 because associativity doesn't apply, because associativity for division stems from the existence of a multiplicative inverse exists, and none does even though 1/0 = 42. > You won't compromise arithmetic, but you will compromise the definition of a field. Not at all. Formal systems of mathematics define fields (in general, not just in arithmetic) specifically with 1/0 = 0. Can you show a single field axiom or theorem that would be affected by this? Perhaps you could if you insisted on stating a theorem by using an informal term such as "wherever foo is defined," but 1/ those theorems can always be stated in more precise terms that don't make use of the informal notion of definedness, and 2/ very few formal systems formalize definedness in a way that means an undefined value must not be 42 (i.e. where you can actually prove 1/0 ≠ 42 or where 1/0 is ill-formed) -- see Feferman https://math.stanford.edu/~feferman/papers/definedness.pdf https://math.stanford.edu/~feferman/papers/definedness.pdf -- and AFAIK, such systems are very, very rarely used in practice.

throwawaymath 8y ago
At this point I've written a number of comments throughout this thread which explain why division by zero is not possible in a field - specifically, a field which contains nonzero elements. You are asking me to show you an axiom or theorem proving this, but I don't know how else to explain this to you since I've already explained it in a number of different ways. In a sibling comment I even write out the formal proof, and in others I've explained why the author's refutation is incorrect. I'm not sure what else to say. The author is wrong - it is not at all controversial among mathematicians that the algebraic structure of a field cannot support division by zero. Perhaps I'm simply a poor teacher - in that case I would refer you to [1], [2] and [3] for a better explanation. As I've said elsewhere, you can make a coherent algebra by extending a field - then division by 0 or infinity is possible. But it stops being a field - just as it cannot be many other algebraic structures. Therefore I feel very confident stating that 1) the author is wrong, 2) I've sufficiently explained why in these comments and 3) the burden isn't really on anyone to disprove that division by 0 works at this point. In any case, this entire discourse is ridiculous because the author should not be trying to defend programming language decisions using abstract mathematics. This kind of nuance and ambiguity is neither necessary nor relevant for justifying an implementation of defined behavior for division by zero. The whole exercise is a farcical distraction, to put it bluntly. Mathematics is pedantic by design, but this sort of definitional rigor is laughably unneeded and for defining integer and float-based arithmetic. The author does a disservice to what is an otherwise reasonable point by (incorrectly) justifying it with axiomatic field theory. It's self-indulgent over-engineering to try to prove division by zero in fields "works, no really!" from first principles for a programming language blog post; especially when mathematics is essentially united in saying, "no actually, it doesn't." __________________ 1. https://www.reddit.com/r/math/comments/3b5i6p/can_you_divide.. https://www.reddit.com/r/math/comments/3b5i6p/can_you_divide.... 2. http://mathworld.wolfram.com/DivisionbyZero.html http://mathworld.wolfram.com/DivisionbyZero.html 3. https://en.m.wikipedia.org/wiki/Division_by_zero https://en.m.wikipedia.org/wiki/Division_by_zero
- deleted 8y ago
  [deleted]
- 8y ago