351–360 of 593 posts
When a CPU is asked to divide by zero it generates an exception. This exception would cause the OS to jump to the interrupt handler in the IDT for divide by zero exceptions. This handler generally results in the OS terminating the process. Does the Pony runtime register its own signal handler with the OS for a divide by zero exception?
Earlier quoted context omitted.
I can give you a simple proof by contradiction. 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 th…
>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 multiplica…
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.
Earlier quoted context omitted.
> 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. Dif…
> 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 f…
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.... 2. http://mathworld.wolfram.com/DivisionbyZero.html
Earlier quoted context omitted.
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/ 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.
Your argument is flawed because your zero is positively biased. Why infinity and why not negative infinity.
Earlier quoted context omitted.
> 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 f…
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…
So anyway, IANAM. What I learned was that 1/0 is infinity. And in software, that generally means a divide-by-zero error. But I also learned the utility of making approximations and exploring behavior at limits. And 1/x obviously increases exponentially as x approaches zero.
So how, then, can 1/x all of a sudden be zero when x is zero? It makes no sense to me. Call it undefined if you like. But it's obviously not zero.
Earlier quoted context omitted.
It seems like he covered that in the article. There is no multiplicative inverse of zero. But that isn't the same as defining a division operation.
He didn't cover that in the article, or at least not in a way that actually supports his point. Since there is no multiplicative inverse of 0, division by 0 is undefined behavior. Trying to remediate that by refuting the "proof" that it's undefined while still asserting that we can define it as something else is mathematically incoherent. If you want to see why it doesn't work from a number of different angles, read…
He does not refute any proofs by citing that division by 0 is undefined. He refutes them by asserting that the multiplicative inverse doesn't exist. These are very different statements.
Neither the standard field nor his modified field use the zero inverse, 0⁻. The proofs he's criticizing do erroneously use 0⁻. That's what he's calling out, I believe.
Earlier quoted context omitted.
Is there a proof or something elsewhere you can link to? To be honest I can't really tell the point you're trying to make.
I can give you a simple proof by contradiction. 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 th…
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.
Earlier quoted context omitted.
> 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 f…
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…
The references you linked to are irrelevant as they refer to informal mathematics. Of course you can't meaningfully divide by zero (in the sense that the value of division corresponds with our intuitive understanding of what division is). But when it comes to formalization you must assign some meaning to 1/0 or work out a complex system where it becomes ill-formed (i.e. a "syntax error"). The only question is whether that meaning -- that must exist in formal mathematics even though it should not in informal mathematics -- causes an actual contradiction or not, even though it doesn't "make (an informal) sense" either way.
"Mathematics does not give us truths, it gives us consequences." I'd like to point out that, as I stated in another comment in this thread, the author's supposed refutation of the inconsistency inherent in division by zero within fields is incorrect. Their refutation is as follows: The problem is in step (3): our division theorem is only valid for c ≠ 0, so you can’t go from 1/0 0 to 1 * 0/0. The “denominator is nonz…
First, mathematics does not give us true statements about the world, it gives us consequences that must follow if we accept various axioms or definitions. Isn't a consequence in itself a true statement?