1/0 = 0
hillelwayne.com
hillelwayne.com
When encountering such unanticipated corner cases, it's almost always better to throw an error. That prevents any further data/state corruption from happening. It prevents your user from getting back a bad result which she thinks she can trust and rely on. It highlights the problem very clearly, so that you know you have a problem, and that you have to fix it. Simply returning a 0 does the exact opposite.
If you're one of the 0.1% who did anticipate all this, and correctly intended for your program to treat 1/0 as 0, then just check for this case explicitly and make it behave the way you wanted. The authors of pony are welcome to design their language any way they want. But in this case, they are hurting their users far more than they are helping.
Because frequently division by zero indicates a bug. But similarly frequently, I end up crapping out annoying little bits of code like
if (foo == 0):
return 0
else:
return bar / fooA "strict" mode is usually always an afterthought once we have errors & people run it in strict mode and facepalm.
One of the first "utilities" I wrote for PHP was something called "pecl/scream", which turned off all the "unchecked" operations across the whole VM.
And in general, this works out poorly for code quality.
You can always (as in OS with lazy allocation) allocate enough memory to get OOM no matter how safe your language is.
Isn't this reason the the point of having a utils library with commonly used pieces of code?
Unfortunately, GCC only lets you enable this globally (within a program): see http://www.gnu.org/software/libc/manual/html_node/FP-Excepti....
You say that you frequently have to write your little shim but honestly I don't remember writing code like that in recent memory.
You talk about progress bars, I suppose it makes sense if you somehow try to copy 0 elements for instance, and you end up dividing by zero when computing the progress, like:
pos_percent = (copied_elems * 100) / total_elems
It's also a bit odd because it introduces a discontinuity: as the divisor goes towards zero the result of the operation gets greater until it reaches exactly zero and it yields 0. Wouldn't it make more sense to return INT_MAX (for integers) or +inf for floats? If you're writing a game for instance it might work better.
I guess it just goes to show that it probably makes a lot of sense to leave it undefined and let people write their own wrapper if necessary to do what works best for them in their given scenario.
Of course, it's context dependent. As others mention, your code might be full of stuff like X / (divisor || 1).
X / (divisor || 1).
% cat >division.c <<EOF
#include <stdio.h>
int main(void)
{
printf("1/0 = %d\n", 1 / (0 || 1));
printf("1/2 = %d\n", 1 / (2 || 1));
printf("1.0/0 = %f\n", 1.0 / (0 || 1));
printf("1.0/2 = %f\n", 1.0 / (2 || 1));
}
% gcc -Wall -o divison divison.c
% ./divison
1/0 = 1
1/2 = 1
1.0/0 = 1.000000
1.0/2 = 1.000000
% python3
>>> 1 / (0 or 1)
1
>>> 1. / (0 or 1)
1.0
>>> 1 / (0 or 1)
1
>>> 1. / (2 or 1)
0.5
% python3
>>> 1 / (0 or 1)
1.0
>>> 1 / (2 or 1)
0.5C doesn't have booleans and treat them as integers 0 or 1, it can do the math and will always return 1.
https://en.cppreference.com/w/cpp/language/implicit_conversi... (under "Integral promotion")
And C has a boolean type as of C99.
x / (divisor ?: 1)Also, if loading total elements takes a significant amount of time, shouldnt this loading also be reflected in the progess bar?
Defining x / 0 = 0 gets this behavior for free, while leaving zero as an exception means it has to be caught for every single signal calculation, which is a pain when there are potentially dozens of different signals, all of which are counting different things (and have different divisors). I've actually defined a helper function to do this automatically, which also lets me change the default "null object" easily if I choose a different representation or want to apply some baseline value.
Unless you're using unsigned ints, the discontuity will exist no matter what you do, because of negative divisors.
return (foo == 0) ? 0 : bar / foo
return bar / max(1, foo)
just for fun, in kotlin (making use of expressions removes some verbosity):
return where(den) {
0 -> 0
else -> num / den
}
return if (den == 0) { 0 }
else { num / den } return foo && bar / fooJust try INT_MIN/-1, can blow most "foolproof" divide logic away.
pub fn checked_div(self, rhs: u8) -> Option<u8>
Checked integer division. Computes self / rhs, returning None if rhs == 0.
You would use this as lhs.checked_div(rhs).unwrap_or(your sane default)
This is dramatically better than always returning zero silently, as doing so is bound to be wrong in certain cases. If you run into a situation where you are afraid your RHS may be 0 but still want to do the right thing, this is what you'd use.
if (foo == 0):
return MAX_FLOAT
else:
return bar / foo
Then use MAX_FLOAT as an error flag instead of 0, which could have been the result of a legal operation (with bar==0).
Edit: Although Pony claims that programs should never crash, the language designers clearly understand the pragmatism of an unrecoverable error because it happens on OOM and stack overflow
Let’s say some program calculates the mean of an array and then adds that mean to some accumulator.
For purposes of updating the accumulator, the mean of an empty array is perfectly well-defined: it should add nothing to the accumulator (add 0).
This might be a major operating requirement for the mean function, such that rather than guarding or pattern-matching on an empty array and handling a failure is far worse than having a better 0-length convention.
Consider the difference between the “head” function of some List type, which has to either raise an exception or wrap the return value in some Maybe structure, because it’s literally not definable, vs the “length” function which has an obvious natural definition for empty arrays that is often highly preferred to some design where length(empty_list) throws an exception and everyone has to handle it in little bits of custom code to specify 0.
To me this topic is all about usability and not about some parochial claim that some operation is nonsensical.
Why would you want to do this rather than validating understanding of the data before computing on this?
> For purposes of updating the accumulator, the mean of an empty array is perfectly well-defined: it should add nothing to the acculator (add 0).
That's not a mean, though, that's a quirk of how you decide to (incorrectly) compute a mean. What's the point of such a program? It should refuse to compute when it's given no values--that's clearly a category error.
Otherwise, you're not using a mean, you're using a mean-or-0-when-lacking-a-mean. Might as well not call it a mean at all so other people can read your code.
Yes, this is pedantic, but this kind of subtle changing meaning of terms is exactly what leads to bugs. Name your functions accurately.
Consider needs to vectorize a large column-wise mean calculation across columns of a large data matrix (where NaN values are sparse but appreciable).
The NaNs might be perfectly reasonable, expected pieces of data, but you still want to understand the distribution of the non-NaN data, and adding extra work to filter it out first might be hugely costly, or even actually wrong depending on what other operations the NaN data is planned to be passed to and how those operations natively handle NaN.
And simple columnar summary stats are just the tip of the iceberg. It gets much more complicated.
By no means is the solution of “diagnose why there are NaNs ahead of time and preprocess them accordingly” even remotely realistic in most use cases. This is why libraries like pandas, numpy and scipy for instance provide specific nan-ignoring functions or function parameters.
You bring up the history of CS, but even there you have debates about what convention to use for defining 1/0 for function totality and theorem provers.
There’s no aspect of pure math derivation of number systems on up through vector spaces that definitively makes a zero mean for an empty array ill-defined. Whatever choice you make, positive infinity, undefined, 0, or any finite values, etc., any such choice is purely down to convention that depends precisely on your use case.
It’s not conceptually wrong, it just means the “mean” you’re referring to calculates a different value than the “mean” we’re taught in school. So, underlying assumptions about the differences in “mean” should be communicated where it’s used.
For example, if we examine a sample of zero elephants, then we end up estimating the average elephantine mass as being zero.
This shows to be wildly off as soon as we upgrade our statistical wherewithal to work with a sample size of one.
A center of mass is a kind of average. If we have an empty object made of no particles of matter at all, can we arbitrarily pin its center of mass to the (0, 0, 0) origin of the coordinate system we are using?
Wouldn’t that be a (potentially very different) case of 0/0? If there are 0 elements, you wouldn’t have a nonzero numerator, right?
Even Javascript is better with "NaN"
Oh well :)
It's 0.
>> 1 / 0
Infinity
>> 1 / -0
-InfinitySo 1/0 is infinity, and 1/-0 is -infinity.
How could you possibly make an assertion like this without knowing why they made said choice[1]? Per the article, they didn't do it for fun, or to avoid exceptions (as you point out, more like defer exceptions). FTA:
> 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.
Do you know enough about Pony's language design and decision process to support your claim that this decision (and all its second-order consequences) is hurting users far more than helping them?
[1] On the off chance that you are familiar with the tradeoffs Pony made and do know what you're talking about: care to clarify?
I will be writing up a post about why we made this decision.
`/`-by-0 is just an operation and it tautologically has the semantics assigned to it. The question is whether the specific behaviour will cause bugs, and on glance that doesn't sound like it would be the case.
Principally, division is normally (best guess) used in cases where the divisor obviously cannot be zero; cases like division by constants are very common, for example. The second most common usage (also best guess) is to extract a property from an aggregate, like `average = sum / count` or `elem_size = total_size / count`. In these cases the result is either a seemingly sane default (`average = 0` with no elements, `matrix_width = 0` when zero-height) or a value that is never used (eg. `elem_size` only ever used inside a loop iterated zero times).
It seems unlikely to me that `/` being a natural extension of division that includes division by zero would be nontrivially error-prone. Even when it does go wrong, Pony is strongly actor-based, has no shared mutability and permits no unhandled cascading failures, so such an event would very likely be gracefully handled anyway, since even mere indexing requires visible error paths. This nothing-ever-fails aspect to Pony is fairly unique (Haskell and Rust are well known for harsh compilers, but by no means avoid throwing entirely), but it gives a lot more passive safety here. This honestly doesn't seem like a bad choice to me.
x = 2/(1/a +1/b)
This is a form of average where you are giving increased importance to the smaller number. It frequently pops up in science/engineering, e.g. in hydrology when you are computing flow of water underground.
In this case, it's "obvious" that when e.g. a is zero, you want 1/a to be zero so you simply return b. There's typically a clear, big distinction between "smallest realistic number", for instance 1e-3, and a zero, whether actual zero or 1e-34.
For instance Numpy offers a nice way of doing this:
def safeInv(a):
tol = 1e-16
return np.division(1.0,a,out=np.zeros_like(a),where=np.where(a>tol))
In this case, though, the programmer understands this division is somehow special and should allow div-by-zero, so it is handled specially.
If, say, `a` is mathematically very small (and `x` is accordingly expected very small`) but `a` become zero due to rounding behavior, then having `1/a=inf` results in `x=0` which is arguably closer to the expected result than e.g. `x=2b`.
As someone involved with numerical methods, I have very often relied on `1/0=inf` because it would ultimately warrant the proper behavior in case of rounding errors in the denominator.
b obviously isn't what you want from this harmonic mean when a is 0. And in any case x will be 2b if 1/a is 0, not b.
https://www.rdocumentation.org/packages/lmomco/versions/2.3....
Imagine a Mars lander program that looks at the average of altitude measurements to decide when it's ok to jettison the parachute, sees no measurements, and decides that altitude is zero.
Pony is made for a more typical scenario where every failure case is a new, untested error path, and history shows that general developers handle errors badly. Pony makes a heroic effort to remove the error path from the language semantics entirely: every failure is explicitly annotated in the code, and has to be handled there. This is much better for the typical developer, allowing them to produce very robust code without NASA's degree of investment towards it. Giving Pony a special unwinding mode just for division by zero would be very dangerous, because this is a new path that only exists for a rarely-encountered sort of error; you cannot assume a sudden shutdown is going to do less damage.
Having Pony present the error cases inline on division by zero would certainly be safer, but there is a degree of disproportionality here: most divisions are impossible to go wrong in this way, and I suspect most of the rest are benign or would be quickly caught by the check after. Since Pony aims to compete against incumbents that are generally less safe in this regard (C++ has UB, Python has exceptions but makes it hard to handle them correctly, etc.), a compromise seems sensible.
UB is not the only way. You can have NULLs (they come with their own sets of problems, but still).
In many cases no value is better than incorrect value.
And the whole point is that this is meant to catch unforeseen interactions as soon as possible. If you add a check it's no longer unforeseen, and it may easily slip the programmer's mind.
Let me elaborate then.
Average credit card balance predicts probability of default. Joe who maxed out his credit card is higher risk than Jane who pays back her entire credit card balance every month. Now we have Jack with no credit card. We predict that Jack is low risk because his average credit card balance is zero.
Second example, defibrillator that monitors blood pressure and shocks the patient when his heart stops (blood pressure drops to zero). We attach the defibrillator to a patient, turn it on, and it shocks the patient immediately because there are no blood pressure measurements yet and therefore it thinks the average is zero.
Third example, a thermostat that turns on the freezer if average temperature is above a set threshold. It never turns on because average (of zero observations) is already zero.
Of course you can hard-code handling of those special cases, but if you did not, failing would be preferable to continuing to work incorrectly.
Credit scores don't work this way. Zero is not a valid credit score, and the things you mentioned describe different components of the score.
I work a lot with survey data, to be interpreted by humans. In this problem domain, zero is a sane value for an empty average, though "N/A" is usually better. I wish our language would let us define it as zero so long reports don't die in the middle. But it's about your problem domain, as usual.
But in this case it's irrelevant because average balance is independent variable (input of the scoring model).
Credit risk is based on total debt, and since credit cards are a revolving line of credit, the entire credit limit is considered debt, even if the balance is zero. That's why you can improve your credit score by closing out a credit card that you never use and that carries a zero balance (which we did in order to qualify for a mortgage several years ago). In other words, it's a sum, not an average; there's no division involved.
Setting aside the fact that there are much more reliable ways to detect a stopped heart than blood pressure: If you're taking a running average of BP over time, a low reading after a heart attack would just be a single data point, and you'd probably have to accumulate a bunch of them in order for it to register (particularly if you got a high reading just before the event). Even if you take a reading every five minutes, which is ridiculously frequent for BP, the patient will be long dead by the time you notice. You should be acting based on the last reading; again, no division involved.
I don't see why a freezer would be based on running averages rather than the most recent reading either. Thermostats generally work off of two thresholds: a higher one above which the compressor turns on, and a lower one below which it turns off. That smooths out any measurement noise without taking averages. Even if you do use averages for some reason, though, presumably it will start measuring at _some_ point and the compressor will turn on; I don't see why the average would stay at zero.
I'm not convinced that `1/0 = 0` is correct in any meaningful way, but I feel like any situation where it would cause bugs more critical than a UI issue probably points to a deeper design flaw. After all, if the alternative is to crash on a failed assertion, that's not necessarily preferable in a life-or-death situation.
It is normally addressed with floors and ceilings or something like Laplace rule of succession, so that no data at all results in a reasonable number. Very rarely that reasonable number is zero.
I'm not saying taking the average is necessarily good in the examples given, just that if you are computing the average, then that computation should not silently return zero if there's no data to average.
That's the way AVG() in SQL or mean() in R work, they return NULL or NA rather than 0. If you know that NA should be 0 you can explicitly COALESCE, but that should be your decision rather than the default behavior.
1. The program should "soldier on" if it can.
2. The program should go immediately to jail, it must not pass Go, and must not collect $200.
I'm solidly in the latter camp. If a program has entered a state unanticipated by the programmer, then there is no way to know how it entered that state (until it is debugged), and hence no way to know what the program might do next (such as load malware).
1/0 is a bug, and the program should immediately halt.
I don't know much about Pony, but given that it is also actor based, I'd imagine this would be a great opportunity to crash early and eagerly. It gives you all the advantages of catching a bug early while not crippling a production app under what might be a pretty low-impact, low-frequency bug.
Special care must be taken if threads are manipulating shared data structures, especially inside a "critical section" where the data structure invariants must be maintained. This is why automatically terminating the JVM when OutOfMemoryError occurs is a best practice, as code is often not paranoid enough to handle it.
This is an area where the design of Java/JVM is badly screwed up.
[1] JVM, really. It's pretty unavoidable on most (all?) JVM languages.
Swallowing exceptions is a really poor idea. Does Java really do that?
The divisor in your code went through a non-ECC DRAM module (maybe in a disk drive) that runs hotter than its specified operating temperature would allow and a random bit-flip changes your `1` into a `0`.
On this topic, the talk on Bitsquatting from Artem Dinaburg during Defcon 19 is worth watching. The most interesting part on bit flips starts around 15:05 minutes: https://youtu.be/9WcHsT97suU?t=15m5s
... or kill the patient ( https://en.wikipedia.org/wiki/Therac-25 ) or set the company bankrupt overnight ( https://en.wikipedia.org/wiki/Knight_Capital_Group ), or simply delete all your data (happened to me with some buggy media player that though my $HOME directory belonged to its download cache).
Programming languages don't generally allow us to "handle", from inside the faulty process, stuff like NULL-pointer dereference, double-free, or segmentation faults. And that's a good thing, because as you said, at this point, there's a very high probability the program is in some rogue state.
(Making special cases for NullPointerException or OutOfBoundsException, like some languages do, is, IMHO, a bad idea, that spreads the confusion between programming mistakes (i.e coming from the source code) and invalid runtime conditions (coming from environment). (I'm avoiding the ambiguous terms "errors" or "bugs" here)).
Making "divide by zero" non-fatal belongs to the same family than making "((int)0)" return zero, or making "((int)0) = x" a no-op. At first, it seems like this will only hide programming mistakes ; but this impression comes from my current programming habits, which are tailored to avoid these situations.
But maybe there are advantages in being able to write these things on purpose (at the cost of losing the runtime detection of some programming mistakes). After all, I'm perfectly happy with "free(NULL)".
Actually if you check out the interviews with Java designers the checked exceptions mechanism was designed for that purpose: unchecked exceptions are for bugs that should never happen in a well written code while checked exceptions are for conditions that can happen regardless to how good is your code (e.g. i/o errors).
See: https://www.artima.com/intv/solid.html
There are of course also Errors for fatal conditions that should been be caught (actually in CLR even if you catch the exceptions will be re-raised automatically at the end of the handler).
Another interesting thing in CLR is Constrained Execution Regions that allow you to run the cleanup code reliably even when such a fatal condition is encountered (but the code to be run is limited e.g. it cannot allocate).
[0] NumberFormatException is a RuntimeError as are all IllegalArgumentException, WTF?
And that's why I like dual error mechanisms, like the panic vs manual error handling mechanism in Go (despite all its verbosity). It's very important to make the difference between an external error (that should be considered something "normal" to deal with) and an invalid state (that should lead to a halt of the program, maybe after logging something, or before trying to restart the program from zero).
Traditional expection mechanisms (à la try/catch) make it too hard to deal with an external error, and too easy to think you can recover from an invalid state.
Failures of the former throw an Error, the latter Exception.
If a program is running under a supervisor, it makes sense to bail, as a new clean instance will become available.
If it was the code of the life support machine that displays data on the LEDs that I was connected to, I prefer that it solder on rather than stop functioning altogether because data for one of the digits was out of 0-9 range.
I'm sure there's been many instances where spacecraft had partially malfunctioning software that was remotely corrected because it didn't entirely give up but rather continued to accept input.
What is absolutely NOT done is soldiering on with a computer in an unknown state.
Any software system that is life critical is either designed this way or is very badly engineered. I've written a couple articles about this:
https://www.digitalmars.com/articles/b39.html https://www.digitalmars.com/articles/b40.html
My point of view is that a program should abort if it encounters an irrecoverable error, such as imminent memory corruption. However, if it's designed to fail functional, then it could continue to work, either by reinitialising itself, or by aborting the current operation. However, it must be said that it's hard to design such programs, so the option of bailing out is very attractive.
Example: an out of bounds access is a typical programmer error. This should probably result in an abort during development, so that it can be fixed. However, it is possible to not want to abort just because something is not accessible when in production. The program could instead raise an exception and clean up the call stack up to its initialisation point, then notify the surrounding system that a problem was encountered and resume service. The surrounding system could then keep track of the encountered issues and try to perform a recovery after a threshold is reached: this is how Android recovery works for e.g. crashing system services, if I recall correctly, it first cleans some application settings, then system settings, then does an OS reinstall. Now in this example the trigger condition is a crash, but it doesn't necessarily have to be like that.
What seems much more important to me is that the behavior is well documented. If I am working with a system where 1 / 0 is defined to be zero, I will deal with that just as I deal with other peculiarities like 1 / 3 being 0 and 1.0 / 3.0 only approximately being a third in some systems. It's a practical concern like many others in programming.
The lesson I took from this is that neither of these two options is acceptable in software that has to work all the time, like much real-time software. Instead, we should detect all the bugs in such software before runtime, which is only feasible for small systems such as seL4[1]. So we should diligently minimize this software.
For other programs, the best way to handle an error is context-dependent. If a rendering bug will result in a glitch showing in a texture onscreen, that's preferable to exiting the game in the middle of a raid. If a PID motor control system for a robot arm has a division by zero, halting the program without first slowing the motors to a stop could be catastrophic, even causing fatalities. And of course there are numerous cases where continuing execution in the face of such an error is far worse.
[0]: https://web.archive.org/web/20000815230639/http://www.esrin.... [1]: http://sel4.systems/
[1] The author has a dislike of the notion that 1/0 = 0 in a programming language. The author identifies this as a personal preference; I'm sure that preference is based on falsiable notions, but the author doesn't elaborate. The author _DOES_ elaborate their motivation for writing the post: The post debunks the notion that 1/0 = 0 is 'bad math'.
[2] Pony chose 1/0 = 0 because the language of Pony is set up to enforce the coder to complete all functions; if you go with the strict definition of division, which is an operation which has no definition if the second operand is 0, it's not complete anymore. I agree with your sentiment; this feels like the wrong answer, but it's definitely not as simple as just saying: Why don't the pony folks redefine things such that dividing by 0 raises some sort of error condition?
It's such a common case to consider, I don't think that's compelling. Knowing that a division by zero throws an exception or casts to zero, is similarly considered.
> they are hurting their users far more than they are helping.
There's no evidence of this.
I'm on the Pony core team. I will be writing in more detail about this decision. A few short notes until then:
1) no one on the team has ever been happy with ending up here, understanding why the decision was made involved understand how partial functions (one that can produce errors like division by zero) are handled in Pony and interesting ergonomic issues that can result that is a large part of what my post will be about.
2) this applies only to integer division wherein division by zero is undefined. 1.0/0.0 uses the available Infinity value.
3) Partial function math is coming to Pony that includes 1/0 as partial (ie error producing) as well as handling integer overflow and underflow for operations: `+`, `-`, and `*`.
4) It's very straightforward even without that those operations to define your own division that will be partial (ie return an error) for division by zero.
Edit to include link to the comment below because it contains a good bit of the decisions that have to make when dealing with integer math:
https://news.ycombinator.com/item?id=17736637
Which is part of what I will touch on in my post about the decision process that Pony went through to reach to state we are currently at (which I want to highlight, is one we intend to improve- see #3 above).
Oh jeeze... to me that almost nullifies all of the points in the article. It does an alright job explaining how 1/0 = 0 is at least consistent with other notions in the language, but to hear that the same logic can’t be applied to floats is just... well, objectively it’s a mess.
The floating point standard says that division by 0.0 should be Infinity and provides a value for it. The integer math, all possible values are used for numbers, so division by zero is undefined behavior.
And from there, every language is potentially going to have a mess of inconsistency to deal with.
You can make 1/0 = Infinity so long as you box all your integers. That is, its not using the machine type, but I type that is a wrapper that can be the machine type or Infinity. And every user takes a large performance hit even if they will never divide by zero.
For some languages boxing integers is not a bad thing because they already do it. Why do they do it? Usually, because of another not math problem. Overflow and underflow:
What is 0 - 1? Well, its -1 right? Except of course if you have an unsigned integer, then its the max value of the integer. And what if you had 1 to the max value that the computer can represent? You wrap around. Some languages make all integers protect you from this and take a performance hit to be able to box and be able to represent numbers better as we expect them to work. In return, you can not do integer math as fast as you could.
Computers and numbers... its an inconsistent mess and a series of tradeoffs for any language of performance and various possible errors.
I'm going to talk about this and more in my post.
What does your favorite programming language return for 3/2 as compared to 3.0/2.0? Many will return different values.
EDIT:
for clarity of my point: integer math that uses machine types is pretty surprising compared to what we would expect from "math" in general for division.
just so long as you don't expect a consistent answer between python2.7 and 3.x... >.>
Division with floats doesn't usually have a definition like that, so you don't end up in a similar situation. Plus, floating point math can have denominators get really close to 0 and have the result of the division tend toward the infinity value. Ints don't have values close to 0 or an infinity to represent what that division would tend toward.
Floating point doesn't even form a Ring, because the operation is not associative[0]. Coq, for instance, defines the operation for QArith, which are the rational numbers. The representation is a pair (Z, positive), where Z is an integer and positive is a positive number (i.e., 1,2,...). QArith does form a field in the usual sense.
Integers are not a Field (unless you pick Z/p for some prime p), and machine words, signed or unsigned are even less of a mathematical object with the usual operations. So you can do almost anything you want to them from a programming perspective, including 1/0 = 0.
As Hillel writes, what to do will make sense in some settings, but not in others. You may want MAX_INT in some situations, and 0 in others. And this requires a check, partiality or not. Rejection of the case x/0 has more to do with the notion that it is usually a corner case where you want the programmer to think about what the result should be.
[0] The reason is that any addition can incur information loss, and the further away from 0 you are, the more information is lost. Thus, the order in which you add values matter.
So you may be saving some developers time in operator overloading, etc. More important than the actual binary decision itself is having well-documented behavior. Have not tried Pony yet, but will take a look. Good discussion, keep it up!
Generally, your viewpoint comes from an incorrect understanding of mathematics, so let's explore what math actually is:
When we say "10 / 2 = 5", the result "5" doesn't come out of nowhere. It comes out of the definition of division.
There are several ways you could define division. You could interpret "10 / 2 = 5" as meaning any of:
• "If you had a 10-inch stick and you divided it into 2 equal parts, each part would be 5 inches."
• "If you had the equation 2 * X = 10, X = 5 would be a solution to it."
• "If you had 10 Pa of pressure in an enclosed box, and you increased the volume of the box to 2 times its previous volume, its new pressure would be 5 Pa."
• "A wave of wavelength 2cm would have a frequency of 5 per 10cm."
These definitions all lead to the same result – in other words, they're equivalent. When this happens, mathematicians usually don't particularly care which one is the "real" definition.
This applies to many different mathematical axioms. For instance compare the definition of the Parallel Postulate on Wikipedia:
"If a line segment intersects two lines, the two lines will intersect on the side that their angles with the line segment sum up to less than 180°"
– https://en.wikipedia.org/wiki/Parallel_postulate
with the definition on Wolfram MathWorld:
"If you have a straight line and a point not on it, there exists only one straight line which passes through that point and never intersects the first line."
– http://mathworld.wolfram.com/ParallelPostulate.html
These are different definitions. But since they lead to the same result, mathematicians don't really care to argue over which is the "real" definition.
Some definitions only apply over a subset of numbers. For instance, originally, "5 - 10" was undefined. Then negative numbers were invented, to expand the definition. The same thing happened with square roots and complex numbers.
That's the same thing with division. 1 / 0 was originally undefined. But you can come up with new number systems that define it, while preserving all the other properties that make division what it is. A common definition is 1 / 0 = Infinity, which is done in the Riemann sphere number system:
https://en.wikipedia.org/wiki/Riemann_sphere
There's nothing mathematically incorrect about doing any of this.
Floating point infinity is not equal to math infinity. Floating point infinity means there was overflow of the representation we are using, not that the number is larger than any known number.
> Adding zero + zero + zero infinite times does not equal 1.
Sometimes it does. That’s what an integral is.
For example Riemann integral is just limit of sums built on tagged partitions of a closed interval with largest sub-interval approaches zero. But no single sub-interval is equal to zero, their lengths just approach zero while being strictly positive values.
Calculus does not divide by zero, calculus explores what happens when we move to zero as close as we can and even closer.
Yes, certainly it is.
"You can't divide something 0 times and get any number. Adding zero + zero + zero infinite times does not equal 1."
The discussion is about mathematics, not elementary school arithmetic.
I don't know, does it even matter? What happens when you try to divide a physical object into 0 parts? It doesn't create infinite pieces. It doesn't make the object disappear. Seems like nothing happened. Maybe when we divide by 0 in a program it should halt and catch fire?
I hate logical arguments, I get sucked in and start arguing all the positions.
Sorry to be pedantic.
That's assuming we had rounding error from a positive number, not a negative number. Of course, if you are concerned about rounding, you shouldn't be using integer arithmetic.
>1/(a number approaching 0) produces ever increasing integers.
No. It produces a bunch of 0s, except when the denominator is 1 (where it produces 1) or the denominator is -1 (where it produces -1). Unless you're using a language like Python, in which case it produces -1 for all negative denominators.
There are lots of situations where it makes sense to keep computing even if you suspect the input data is wrong. It's not really good practice to always be crashing. You need to decide how to handle the bad input on a case-by-case basis.
https://tio.run/##K8jPq/z/PzG5JL9IwTcxM49LAQjyUssVkotSE0tSNV...
`I64.max_value() + 1` gives the expected result.
I'm going to have to look into that.
Thanks.
Unfortunately LLVM considers division overflow undefined: http://llvm.org/docs/LangRef.html#id109
If it's any use, you can see what Julia ended up doing here: https://github.com/JuliaLang/julia/issues/8188
And thank you for the additional info, I've updated the issue I opened accordingly:
If 1/0 = 0 sounds unusable to you, Pony's garbage collection scheme (which is brilliant, by the way) is going to make you think the language is insane.
Ah, that seems rather reasonable. For whatever reason, the OP had me thinking that Pony was replacing the ordinary semantics of IEEE 754 floating point division (probably because he talked about fields and multiplicative inverses).
Having 1/0 = 0 seems like a very reasonable choice, especially if you have 1%0 = 1 as well. Of course, if anyone thinks they will actually encounter division by 0 in their code, and needs to treat it as an error, they can always test for it.
And I was thinking that perhaps 0x80000000 (in two's complement arithmetic) would be a good value for integer NaN. This value is already fixed point with respect to negation, so why not make it into an exception on its own right?
But it would mean to rethink all the hardware which I don't think is an option.
In any case, I think to set 1/0 to 0 is a bad idea, but I could imagine setting x/0 to 0x80000000 (interpreted as NaN) to make more sense.
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.
x=170, y=10
x=17, y=1
x=1.7, y=0.1
x=0.17, y=0.01
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.
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;
}
Even 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:
∀ x ∈ dom(1/t). x(1/x) = 1
∀ x ≠ 0 . x(1/x) = 1
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 that something is true because it just has to be true, that's usually a hint that we may need to step back and consider whether what we're saying is really mathematically justified. What we have here is a case of multiple valid definitions that we can adopt, and there's no mathematical reason for not adopting one over the other. (There's a non-mathematical reason, namely “it breaks convention”, but the entire point is that we can break this convention.)
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.
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. 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.
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 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.
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.
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.
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.
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.
I've always thought that programming languages should have a nonzero number class in the vein of unsigned and float and that division should only be defined with a nonzero number class as the denominator. To divide a 64-bit float by another float, you'd have to either specify it as nonzero in the type or convert it somehow. Make division by zero impossible with the type-checker.
Setting your programming language to evaluate x/0 = 0 seems evil. You're taking a bug in the programmers code and then hiding the fact that something logically unsound happened and in a way that would be very difficult to debug or detect.
In fact, this is what happens when C# think it's being clever by returning infinity as the result of a division operation (which isn't even a number). It's a bug that winds up infecting every function that relies on that code without ever throwing an error.
A programming language shouldn't return NaN or Infinity or anything like that when it encounters division by zero. It should demand you use error-handling or ensure it can't happen. If it does happen, it should tell you exactly where the problem occurred and not assume that some arbitrary value will work just as well.
I'm on the Pony core team and I generally agree with you. The problem is, if you want to allow people to write high performance code, you are penalizing them becaues, for floating point:
1.0/0.0 is infinity. That's not C# being clever. That's C# following the floating point standard and using the math that the computer provides. To not use that standard means that you make every use of division slower, even if the programmer has in some way assert and otherwise knows that that they won't be dividing by zero.
Note that 1/0 is integer math and for that there is no standard and its undefined behavior. You can't return NaN or Infinity for that without boxing numbers which is a performance hit and would be penalizing programmers who want/need to go as fast as possible.
Also, given the performance profile that you are seeking to allow programmers to achieve, I think boxing all integers makes sense, then you can give folks protection from integer overflow and underflow and otherwise make how the computer does math more closely approximate what we expect from doing math.
I think that following my above reasoning that only having floating point math can also make sense. That is... in most programming languages 3 and 3.0 are different. Such that 3/ 2 = 1 and 3.0/2.0 = 1.5.
We allow for 3/2=1 because, integer math is faster than floating point math and we want to allow folks to go as fast as possible when doing things like addition, subtraction and multiplication and accept that we can't represent all the numbers that come from division and give an approximation.
Apparently this can work well with SIMD instructions.
Is it? I didn't measured it myself, but from reading Abrash's The Black Book I had got an idea that floating point division is faster on x86 with FPU.
How can 1 / 0 = 0 be fast? It's not a standard floating point instruction, so extra logic is needed to convert the Inf to a 0.
let a = 17
let b = 10
let c = 7
let d = a - (b + c) // throws AddsToZeroException
Forcing programmers to consider division by zero when it occurs can be done simply by having the language compiler force handling of a divide by zero exception when division occurs.
Which is what Pony originally did and, lordy that can be an ergonomic nightmare when I know I don't have 0 and can prove it except, I can't prove it to the compiler and the type system.
This problem is why integer division by zero is zero in Pony. Because, I can as a programmer prove that I won't divide by zero, but having a type system or compiler where I can prove it to it that is a computation engine that takes user input is a very non-trivial problem.
The solution in Pony is going to be a combination of "safe math operators" and adding value dependent typing to the compiler.
"safe math operations" would be: *?, /?, -?, +? that will error on division by zero as well as integer overflow and underflow (and have slower performance as well)
That's materially different than a non-zero type, and IMO it's meaningfully worse. The type checker is most useful when it moves information.
Explicit might be better than implicit most of the times, but it is possible to be too explicit.
That said, we can achieve this, although it's probably a bit trickier than you'd think at first. The best option I know is called "refinement typing", which basically allows you to specify types as subsets (ie "the set of integers which are not 0") and automatically verifies whether your functions actually return a value in the subset.
Liquid Haskell[1] is an example of a system you can use today to play with the idea. It uses an automatic logic solver (Z3) under the hood to automatically prove that your refinements hold. (For example, I believe it should be able to automatically verify that the function f x = abs x + 1 will never be 0.)
That's still a lot better than before. It's not too hard to read a function and be reasonably confident that it will always return a positive value. On the other hand, it's pretty hard to audit an entire codebase to make sure a value can never be negative, or something like that.
The main difference is probably only needing to do that audit once, when writing the function, instead of every time you need to rely on the function's return value being positive.
It would also save a lot of work because a lot of operations _can_ be detected automatically. positive * positive = positive, etc. So you would only have to manually assert in the cases it wouldn't be doable automatically, which would be significantly fewer than before.
Worse, division by zero is just the tip of the iceberg. There’s overflow and underflow (which both can happen with addition, subtraction, multiplication, and division) and invalid operations (0/0, √-1, arcsin(2), etc), and you might even want to extend this to detect inexact computations (e.g. to properly report whether you are sure a later division by zero actually is a division by zero)
IEE754 ‘won’ because it is relatively simple to use and many times good enough for real use.
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.
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?
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...
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 nonzero” clause prevents us from taking our definition and reaching this contradiction.*
This is a strawman, and it's not the way a formal proof that division by zero in fields is undefined would proceed. First and foremost, the conceptual purpose of the proof is to demonstrate that you cannot define division by zero while still retaining the algebraic structure of a field. Trying to refute this point by stating that the proof cannot make use of division by 0 is begging the question. The whole point is that the proof shows you any way you define division by 0 is going to compromise your definition of a field, or it's going to make fields with nonzero elements impossible.
What the author provided is a very contrived strawman for refutation that belies the actual point. You can define division by zero if you'd like, by using wheels, or extended number systems based on fields (i.e. positive and negativie infinities in the extended Real number system), but you cannot do it using fields. In fact, the modern, axiomatic definition of a field explicitly excludes the unit 0 from the otherwise sane rules of multiplicative inverses.
More generally, I'd like to make a couple of observations from both a philosophical and a practical standpoint. 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. You can define division by 0 if you'd like, and you can even do so in a sane and useful way. But you will not have a field. But much more importantly, it's conceptually unsound to base an argument about the practical, programmatic behavior of an undefined operation based on imperfect arguments about abstract mathematics. Technically speaking, computers don't even deal with real numbers. If you find yourself mounting a defense of your programming language's behavior by running through the first lecture of a real analysis or linear algebra course, something has gone very wrong with your enterprise.
But that isn't the same as defining a division operation.
If you want to see why it doesn't work from a number of different angles, read through the /r/math thread[1] or the Wolfram MathWorld blurb [2].
The formal problem comes down to one of uniqueness of elements. If you define division by zero in a field, you must end up in a place where it follows that every element is equal to every element. Then you only have one element - 0. So really we should be stating that division by zero is undefined behavior in fields with at least one nonzero element.
But again - we can neatly sidestep all of this, because trying to defend your choice of undefined behavior in a programming language based on the abstractions of field axioms is silly. In the actual world we don't even deal with real numbers computationally, let alone the particular nuances of whether or not our programming language implements number systems composing a field or any other algebraic structure.
__________________________
1. https://www.reddit.com/r/math/comments/3b5i6p/can_you_divide...
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.
Yes - but 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.
Integer division just isn't the same operation as division on rationals or reals. The same laws don't apply.
(For floats, division by zero can return Inf, -Inf or NaN and there's no reason to define it differently.)
It looks like the theorem-proving languages that define 1/0 to be 0 tend to be using natural numbers as a fundamental type. Not only do they define division differently, they also don't have negative numbers, and so define 2-3 to be 0.
But it does neither. All field theorems pertaining to inverses/division take the form `x ≠ 0 ⇒ ... x⁻¹ ...` None of them is compromised.
> In fact, the modern, axiomatic definition of a field explicitly excludes the unit 0 from the otherwise sane rules of multiplicative inverses.
Exactly, which is why defining 1/0 = 0 (or 42) poses no problem to fields (BTW, the Lean proof assistant defines 0⁻¹ = 0 for fields, even though it's not the inverse and 0*0 = 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.
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 -- and AFAIK, such systems are very, very rarely used in practice.
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
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.
What exactly are you looking for me to say here?
Very simple. Here is a theory of a field in FOL:
∀ x . x + 0 = x
∀ x . ∃ -x . x + (-x) = 0
∀ x, y . x + y = y + x
∀ x, y, z . (x + y) + z = x + (y + z)
∀ x, y . x – y = x + (-y)
∀ x . 1x = x
∀ x . x ≠ 0 ⇒ ∃ x⁻¹ . xx⁻¹ = 1
∀ x, y . xy = yx
∀ x, y, z . (xy)z = x(yz)
∀ x, y . y ≠ 0 ⇒ x/y = xy⁻¹
∀ x, y, z . x(y + z) = xy + xz
If your answer to both questions is no, then your only point may be that the extended definition of the symbol / does not deserve the name "division" because it does not conform to our intuitive, informal notion. That's fine but is a long way from claiming that there is no acceptable formalization of fields or that division by zero introduces a mathematical contradiction or breaks equational laws. Note that you cannot say that the original theory defines a field while the extended one doesn't, because the latter's models are a subset of the former's.
This then leaves open the matter of whether such a philosophical, aesthetic consideration trumps pragmatic ones or vice-versa, to which I don't think anyone has a universal answer, and it is not the issue, anyway.
A field is exactly defined by the field axioms: adding or removing any other axiom makes it no longer a field.
This is clearly not true. Adding axioms (as long as they don't introduce consistency) can only reduce the set of models. Anything that satisfies the larger theory also satisfies the smaller theory. This is exactly why a group is a monoid is a semigroup. This is why fields are rings. In fact, this is why the rationals or the reals are fields: they satisfy the field axioms, and more (for example, they are ordered).
> In the definition of a field ∀ x . x/0 = undefined, not 0 or any other value you might prefer.
What is "undefined"? First let's look at the logic itself: What is true ∨ undefined ? What is true ∧ undefined? Now at the theory: What is undefined + x ? What is 0 * undefined ? What is 0 = undefined ? etc.[0]
While it is possible to formally define this magic non-value (sometimes written as ⊥ in the logics that contain it) as is done in some programming languages (and it has been done), this would entail adding quite a few more axioms to FOL and to the theory of fields. When people say FOL, they mean a particular language[1], one that is considered by mathematicians to be sufficient to formalize all of mathematics and has very particular syntax and semantics. FOL + undefined is a very different language, which much more complicated semantics. If you think that when people refer to FOL they refer to FOL + undefined, I challenge you to find any mention of it in descriptions of standard FOL. Similarly, if you think that by common theories, say fields or sets, people really mean field + undefined or ZFC + undefined (what is {undefined}? What is undefined ∈ {undefined}? etc.), I challenge you to find any mention of the complex axioms required in treatments of these common theories.
But it's not just a matter of convention. The reason you won't find it in the standard logics/theories is that it's completely unnecessary. If you work it out, you'll find that the theory of fields I provided and the more complicated one involving undefined that you suggest is the common formalization are the very same theory, in the sense that they yield exactly the same theorems, except for those specifically involving undefined (i.e., your theory has more theorems than mine). You'll find that you cannot find a "bad" theorem that you can prove with the simple theory but cannot with the one involving undefined, and therefore it is unhelpful except for the purpose of satisfying a certain desire for intuition that requires significantly complicating the formal system.[2]
There's a paper by Sol Feferman[3] reviewing formal systems with explicit handling of "undefined." AFAIK, they are rarely if ever used. Such semantics are certainly not part of the trusty-old FOL, considered the default language of formal mathematics.
[0]: BTW, if you think that the meaning of every expression involving undefined is undefined, then you'll see that this doesn't work. For example, you have: x=0 ⇒ x(1/x)=1. This is a valid formula, and so it's true even when x=0, but then you have undefined on the right-hand side, so you want at least false ⇒ undefined to be equal to true. But A ⇒ B = ¬A ∨ B, which means you want at least true ∨ undefined = true. Similarly, you'll want at least 0 = undefined to be false etc.
[1]: https://en.wikipedia.org/wiki/First-order_logic
[2]: E.g., while in your theory you will be able to prove the rather useless theorem 1/0 ≠ 0, in my theory you will not be able to prove 1/0 = x for any x, so it really poses no issue.
[3]: https://math.stanford.edu/~feferman/papers/definedness.pdf
Look at for example the set of real numbers. If you add the complex numbers to it, you can no longer speak of the real numbers. The real numbers form a subset of the complex numbers. The same thing happens if you add definitions to a field. You create something which has mayber has a field as a subset, but you can no longer speak of a field.
What is "undefined"? First let's look at the logic itself: What is true ∨ undefined ? What is true ∧ undefined? Now at the theory: What is undefined + x ? What is 0 * undefined ? What is 0 = undefined ? etc.[0]
Undefined is just undefined, no value, not a magic one, or just a random one, or one you prefer. Just void, the empty set. To understand it, look for example at the graph of y = sqrt(x), where x and y are real numbers. You see no points at negative x. Its undefined in the domain x < 0. Yes you can say at x < 0, y = 3, that is now my definition sqrt(), but then you no longer have the sqrt function mathematicians talk about. The same thing applies to fields and 1/x.
>What is "undefined"? First let's look at the logic itself: >What is true ∨ undefined ? What is true ∧ undefined? Now at the theory: What is undefined + x ? What is 0 * undefined ? What is 0 = undefined ? etc.[0]
Now you apply boolean logic to the result of calculations, numbers and non-numbers, not on statements. I can also ask what is 5 AND true? Is that true? The question doesn't make sense, so the answer is: depends on the programming language.
What does this have to do with adding axioms? You don't get the complex numbers from the real numbers by adding axioms. For example, the following is provable for the reals, but not for complex numbers:
∀x,y . x < y ∨ x > y ∨ x = y
No. The class of all fields are all objects satisfying the field axioms. If you add axioms, you get get a subset of those fields. Each and every one of them is a field.
> Undefined is just undefined
I'm not looking for handwaving. Formal mathematics is math that can be done mechanically. Write down the axioms for undefined. Again -- I'm not saying it hasn't been done, but it's certainly not part of standard first-order logic, and it is unnecessary.
> To understand it, look for example at the graph
I understand what undefined means in informal mathematics. Try to see what it means in formal mathematics. But the important point is, try to understand why it is unnecessary in formal mathematics in most cases.
> Now you apply boolean logic to the result of calculations, numbers and non-numbers, not on statements.
No. You can write 1/x < 5 ∨ x > 20.
> The question doesn't make sense, so the answer is: depends on the programming language.
There is no such thing as "doesn't make sense" in formal math, even though there is such a thing in informal math. That's the whole point. Either the expression is ill-formed, i.e. not in the language or a "syntax error", or it must make some sense.
This is why it's useful and easy to say something is undefined in informal math, but not as useful and not as easy to do that in formal math.
> ∀x,y . x < y ∨ x > y ∨ x = y
Since R is a subset of C, you can write C as R with additional axioms. See for example:
http://www.math.mcgill.ca/gantumur/math249w15/numbers.pdf
>I'm not looking for handwaving. Formal mathematics is math that can be done mechanically. Write down the axioms for undefined. Again -- I'm not saying it hasn't been done, but it's certainly not part of standard first-order logic, and it is unnecessary.
Undefined is just undefined, that is no handwaving, it is a primitive notion. See https://en.wikipedia.org/wiki/Primitive_notion
You are trying to define the undefined in a formal system. Undefined is just the absence of a definition. Not 0, 3 , 2pi
> No. You can write 1/x < 5 ∨ x > 20. Yes, those are valid mathematical statements. 5 ∨ TRUE, or undefined V TRUE, I doubt it.
> There is no such thing as "doesn't make sense" in formal math, even though there is such a thing in informal math. >That's the whole point. Either the expression is ill-formed, i.e. not in the language or a "syntax error", or it must make some sense.
Well in language, in which I am corresponding with you, there is such a thing as 'makes no sense'.
You are somehow trying to capture everything in your logical system only to try to prove that 1/0 = 0 is part of a field, which it isn't. I've made my point here, it was nice talking to you.
That's not even remotely how it works. You may want to read up on logical theories and models[1].
> Well in language, in which I am corresponding with you, there is such a thing as 'makes no sense'.
Yes, and for the same reason we can have such a thing as "undefined" (that means more than merely 'not specified') in informal mathematics -- because both English and informal math are informal. But we are talking about formal languages[2], which do not have such a thing.
[1]: https://en.wikipedia.org/wiki/Theory_(mathematical_logic), https://en.wikipedia.org/wiki/Structure_(mathematical_logic)
Isn't a consequence in itself a true statement?
The underlying point here is mostly a philosophical one, but it has some bearing on the matter at hand. In effect, the definition (or lack thereof) for division by zero in fields is of no practical consequence for the real world impact of implementing an operation which admits division by zero. I can define an algebraic structure in which division by zero is sane (it is not in fields, despite what the article states!), or I can define an algebraic structure in which division by zero is insane. Both can be coherent, consistent and genuinely useful.
But whether or not I can define something that works has nothing to do with what happens "when the rubber meets the road", so to speak. It was a mistake to open up an argument about programming division by 0 using the field axioms in the first place. There is no "one truth", there are only facts which must follow as consequences from assumptions. This is especially the case for programming, considering that computers are fundamentally incapable of working with real numbers in the first place.
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
For those who still object to the argument, would you object to me defining the piecewise function f:R->R defined to be 1/x for x =/= 0 and 0 for when x=0?
Are they? I see nothing in the article about the negative consequences of surprising users with silent failure, for example. Or the fact that it makes little sense in real-world scenarios.
would you object to me defining the piecewise function f:R->R defined to be 1/x for x =/= 0 and 0 for when x=0?
What do you mean by objecting to you defining a function?
That's because the article is purely about the mathematical consistency of using 1 / 0 = 0. It explicitly and repeatedly mentions that it's not about real-world logistics.
> "What do you mean by objecting to you defining a function?"
The author is defining the division function with this special mapping, f, which includes 0 in the domain. Damn near everyone in this thread is confusing that definition with defining the multiplicative inverse, 0⁻.
It's an understandable confusion, but also honestly getting pretty frustrating. That's what he or she is getting at.
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.
A basic theorem is that for any field we must have that a/b = c/d if, and only if, ad = bc. See theorem 2 in this classic text here for a proof[1]
So if 1/0 = 0, then we also have 1/0 = 0/1, which implies 1 x 1 = 0 x 0 which is a contradiction. But then we also have 1/0 = 0/x for any x, hence we also have shown x=0 for any x, which is an infinite number of contradictions. Is this a problem which is addressed in the post that I missed?
By the way, I have spent more time than it's polite to discuss in public studying the topic of dividing by zero, and also what 0/0 means. If you are also interested in this topic, the best youtube video is by Mathologer and I highly recommend it to everyone. See here [2]
[1] https://books.google.com/books?id=3ApEDwAAQBAJ&lpg=PP1&pg=PA...
x = a/b + c/d + e/(f*g/h)
if(b == 0 || d == 0 || f == 0 || g == 0)
if(isFinite(x))
I have to say that using a single check on the result seems significantly less prone to bugs then having to check all the values that could produce an invalid result.
Still, I agree that a NaN value(s) is(are) preferable for this reason.
I would REALLY hate having to write a geometry library without NaN values. Both because of error checking, and the fact that NAN/INF is often the 'correct' answer when it's the result of a calculation.
One of those proposals which can only be made when you don't take time to understand and appreciate use cases the current solution was created for.
It makes sense if we have signed zeros; then +0 represents an infinitesimal positive value. IEEE 754 has signed zeros, though the signs may sometimes not match programmers' expectations, e.g. 1 - 1e-50 - 1 == +0.
Maybe 1/+0 == +inf is reasonable, but would you agree that there's no reasonable answer for 0/0? So IMO, reasonable languages must define division as a partial function, or a function that can throw an error (or return NaN, Nothing, etc).
And if division is a partial function anyway, it seems best to not allow division by zero at all, since even 1/+0 == +inf can have unexpected consequences.
> > These things are conventions, exactly the same as announcing that x^-n = 1/x^n and that x^0 = 0.
Say what? x^0 is 1, and not by convention, other than in the 0^0 = 1 case.
It's around since 2013 and was found in a unit test coverage improvement effort in Feb. 2018.
Given that pypy is mostly used for hard-core math and scientific computations, how the hell this bug wasn't found earlier by a user ?
My bet is that ZeroDivisionErrors are very rare. Do you even remember a ZeroDivisionError in production code ? I don't.
1/0 is my dirty little trick to add a breakpoint when I'm too lazy to launch a debuger. Why does this work? Here again, because nobody never catch ZeroDivisionErrors, because they don't happen.
So, what a fuss for such a tiny convention. Granted, it breaks the math correctness, as do ±Infinity. CPU integer math is broken anyway. In what world does 2^31 - 1 + 1 == -2^31 ?
I took a fairly large, used and old repository, Django and I search for ZeroDivisionError:
https://github.com/django/django/search?q=ZeroDivisionError&...
guess what:
- 4 occurrences in the tests
- 3 occurences in the issues
- last, but not least 1 occurrence in the code:
except ZeroDivisionError:
result = '0'But you try to slide one little real number without an inverse by and everyone freaks out.
There is no proof in this post that 1/0 = 0 maintains consistency. Rather, it contains refutations of one or two arguments that claim inconsistency, along with appeals to authority.
However, while I'm a bit rusty, I think it basically has to be true. For there to be an inconsistency, 1/0 = 0 must either
a) imply the negation of some previous theorem of arithmetic or
b) imply that 1/0 = x, for x != 0.
I think a) can only be true by way of b), since no existing theorem of arithmetic involves the expression y/0 for any y. I confess, I don't know the right way to prove that b cannot be a consequence, but it doesn't look like one.
Edit: I think it's just trivial to take a model of the existing axioms, then add n/0 = 0 to the division relation.
(a+b)/c = a/c + b/c
(in particular, for C != 1, as the author claimed it would work not just for 0 for for any real number)
Now to say this is true you have to say "unless c = 0", whereas before that was automatic from the definition of division.
forall c != 0, (a+b)/c = a/c + b/c
is true before and after.
It may be helpful to observe that while using the same symbol '/' in both cases is confusing, mathematical theorems are not about symbols, but about particular mathematical objects. The old theorem is about the division relation defined for real numbers != 0, the new one is a relation defined for all real numbers, that just happens to coincide.
The theorem doesn't need the stipulation that c != 0 since you have already excluded c from the domain.
let a/b mean, in my programming language's syntax, = { a divided by b when b is not zero, or 0 otherwise.
Yeah, it's not "mathematically invalid," but it punches a hole in the fidelity between numerical methods and the math that they approximate.
As the denominator gets smaller, the result is bigger and bigger and bigger. The closer the denominator gets to zero the larger the result. Why would we want to pick an answer that is small when instead it should be larger than any number?
One might argue that 1/0 should be MAXINT or IEEE 754 plus infinity due to the limitations of our hardware, but I’ve never wanted 1/0 to result in zero in any program I’ve ever written.
I would prefer that it be treated as an error or possibly some reserved value that behaves like INF while still being an integer in the programming language.
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.
If I divide one thing into zero groups, how many items do I have in each group? Zero. Edited per comment below.
If I were really pedantic, I'd say that in the above, it's almost like the input "1" is not being divided, but grouped.
The funny thing then, is that if I am grouping instead of "dividing", then if I enter 1 modulo 0, I'd expect to get 1. i.e. the modulo zero should be an identity function: 1%0 = 1, c%0 = c.
However, nobody stops people from defining their own Algebras or Fields on languages that support it. On C++ this should be a no-brainer, if the sentiments of the article is true that consistency is no problems. Being a "man of industry" myself, 1/0 throwing or at least becoming infinity doesn't seem a problem to me. Similar to not using gotos or so.
FWIW, JavaScript an underrated language when it comes to weird corner-cases does the right thing. It doesn't throw an error, instead the result becomes Infinity. When I multiply it with a finite number it stays Infinity. When I multiply it with 0 it becomes NaN which is totally sound because in a real-world application one could come to these numbers because of limitations of the storage. 0.00000......1 becomes 0 thus the real result of 1/0 x 0 in that case can indeed be literally everything. The beautiful thing about JavaScript is how it continues to handle this, when I say 1 < NaN or 1 > NaN it stays false. So the algorithms are likely to fail much more graceful than in other languages.
The issue here is hardware integers, which have no signalling bits beyond possibly sign.
The convention that x^0 = 1 (including 0^0 = 1) is genuinely useful because it removes a case distinction from lots of combinatorial formulas. Hence this: http://tinyurl.com/zeropowerzero
x^0 = 0 seems to me to be - I won't say "wrong" because you're free to define things the way you like - in general less useful than x^0 = 1.
For similar reasons, (0 * log 0) = 0 makes sense when computing entropies and stuff in certain machine learning applications. This one can also be justified as the limit of x * log(x) as x -> 0 is 0, but I've seen at least one person just trying to define "log 0 = 0" which I consider less elegant; in the kind of application where this convention is useful, you'll rarely if ever see a log 0 that's not multiplied by a plain 0.
Where it gets really weird is when you do KL divergence and can end up with 0 * log (0/0), but again you can save a case distinction by just declaring this to be 0. The elegant way to do this is to define d(p, q) = p * log(p/q) when p, q != 0 and 0 otherwise. In this particular application, just going with 1/0 = 0 seems to work fine in practice as in a term q * log(q/0) you can rewrite the whole thing by flipping the sign to get 0 * log(0/q) in that term, which we have already declared to be 0 (whether or not q is 0 itself).
In this case it's not a bug in the code, it's being able to handle probability distributions with mass 0 on some points at the level of arithmetic rather than as a special case in the formula.
If you set 1/0 = 1 (as the author claimed causes no inconsistency), then (2 + 1)/0 = 2/0 + 1/0 is false
If you come to rely on division by zero behaving a certain way (as happens to all features/bugs of any language), then suddenly silly decisions about how to implement a formula can cause wildly different behavior. Good luck refactoring!
Therefore (2 + 1)/0 = 2/0 + 1/0 is not even false, it just means nothing.
BTW, you didn't mention Infinity explicitly, but it would lead to the same inconsistency, if you think about it:
(2 - 1)/0 = 2/0 - 1/0
:)
Using "infinity" (which is not how it's actually done in math) requires you to rule out the possibility of operations like infinity - infinity.
While reading the article and the comments I realized that it will work perfectly in my NISC processor [1]. I just need to update my specification.
To extend the simple first specification to include multiply is very simple. I just need to have a MUL register which, when written, multiplies the written value by the value in the accumulator with the low part of the result being left in the ACC and the high part in the MUL register.
Extending to include integer divide is a little more complicated. I will have to add a DIV register and a DIVEX register. Writing to DIV will divide the value in the ACC by the value written leaving the result in the ACC and the remainder in the DIV register. DIVEX will contain the address of the routine to call when division by zero is attempted which means that DIVEX must be loaded before division is used. If I specify that DIVEX is initialized to zero by the hardware and that DIVEX==0 means that divide by zero leaves zero in the ACC and the remainder (former contents of ACC) is left in the DIV register then 1/0 = 0 will be the default behavior with the ability to change that behavior simply by writing the address of the divide exception handler to the DIVEX register.
I leave it as an exercise for the reader to determine how to deal with this in high level languages. I can fully support it in machine code and assembly language.
For instance, I made a game, and I might accidentally end up with a value that won’t modulus correctly due to zero denominator. In that app, mathematical accuracy for this single outlier does me no good at all because it manifests as “might crash randomly” when I want “doesn’t crash, period”. I therefore wrote a “safe modulus” routine that essentially guards against zero and makes a command decision to return a value. The added robustness against crashes is preferable, since I may not know if I have found every stupid case of the math accidentally working out to exactly zero.
In fact, more generally, exact zeroes mask lots of bugs. They are often default initial values, meaning you might not notice something working accidentally. Sometimes I use a really tiny float as my “meant to be zero” to distinguish, e.g. 0.0001 means “item was supposed to appear at coordinate 0”, that way anything that accidentally ended up at 0 is easier to detect.
Edit: it seems that Pony is only doing this for integer "division", which isn't regular division anyway, and the standard rules don't apply.
On the other hand, the author of the article seems to push for a general, mathematical definition of 1/0 as 0. First of all, good luck with that, as there is no standards-issuing body in mathematics. And whether the author likes it or manages to overturn a very long tradition, division is defined when we grow up as multiplying by the multiplicative inverse, with some occasional notes like "Division by zero is undefined for the real numbers and most other contexts [1] or "In general, division by zero is not defined [2], pointing to settings where clearly you won't find consensus.
I refer to when we grow up because we should not forget the intuitive definition Wikipedia gives first and, I guess understandably, MathWorld gives last: "separating an object into two or more parts". As we know, this restriction of two parts can (more and then less) intuitively be loosened to one, negative numbers, rational numbers, real numbers, etc., but only arbitrarily for zero. But then again, even if we unanimously agreed on one value, what does it give you?
For real numbers though, division by zero will always diverge or be undefined, no matter how you represent them. All computations on real numbers are continuous and there is no continuous extension of division which includes 0 in the domain of the denominator.
One can get around this by switching to projective reals (essentially reals extended with a new element that's both +infinity and -infinity). This is no longer totally ordered and has some other problems, but it's actually a great choice for a lot of numerical computations. Yet, I've never seen something like this implemented in hardware, aside from John Gustafson's unum concept.
But having said that, I do not remember when I last saw a Divide-by-Zero-error in the wild. In practical terms, this is the last kind of bug I worry about.
https://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? ∞(±∞)
The idea behind this is you're never going to get the computer to program itself with exceptions, so better not to let it produce code it will not be able to execute fully without human intervention.
infix operator /? : MultiplicationPrecedence
extension FloatingPoint {
static func /? (lhs: Self, rhs: Self) -> Self? {
return rhs == 0 ? nil : lhs / rhs
}
}
extension BinaryInteger {
static func /? (lhs: Self, rhs: Self) -> Self? {
return rhs == 0 ? nil : lhs / rhs
}
}
10 /? 2 ?? 0 // -> 5
10 /? 0 ?? 0 // -> 0
10 /? 0 ?? 10 // -> 10/?, *?, +? and -? are coming to Pony. We call them "safe math operators" and will error on integer overflow, underflow, and division by zero.
I see this with investments that have infinity ROI. If you get into an investment using only other people's money (OPM) and you make a profit then you have made x / 0. Saying I made an infinity return makes more logical sense than I made 0 return.
There's a saying about the difference between a mathematician and an engineer. If there is a $100 bill on a table and each step you take must be half the remaining distance or less the mathematician will never get there, but the engineer will get there no problem.
It's a non-sensical debate IMO but from the investing scenario that I described above, for all practical purposes, it makes more sense to consider it infinity.
Note that this only works if the denominator approaches 0 from a positive side. Otherwise it's 0. This is the idea behind the extended real numbers.
The function sqrt(x) is undefined for negative x in the real number system. Is it therefore zero? No. Just because a value is not in a domain doesn't mean just pick one.
Most math textbooks I know and Wikipedia define division as the inverse of multiplication. You are saying that there is a distinction, the inverse of multiplication is not the same as division: you can write 1/0, but that is not the same as 1 * 0⁻.
This is unconventional to say the least, and the only argument you give to make this destinction is your desire to define 1/0 as 0.
However, to extend an operation usefully to a larger set of numbers, we can isolate some properties that we want to keep, for example:
1. Division is linear in the first argument: (ab + c)/x = a(b/x) + c/x, for all a,b,c,x.
2. If x has a multiplicative inverse, then x * (1/x) = 1.
3. Taking reciprocals twice gets back to the original number: 1/(1/x) = x for all x.
The choice 1/x = 0 is consistent with all the above, and so probably still “useful”. What properties do you want out of a division function?
Perhaps it's not a good design to have division as an operator a programming language? Just like
Maybe<int> i = ParseInt("foo")
one should also do this for division:
Maybe<int> q = Div(n, d)
Is there any language that does this (returns an option for default division?)
Obviously, this is also the case for ALL other operations on finite number types because of overflow. But overflow is MUCH rarer than division by zero issues, at least in my experience.
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.
<rant> I see a lot of software engineers trying to get rid of the cost of writing robust programs. It's not possible. Stop trying. You are either safe, or you are not. You either handle all cases, or you don't. </rant>
But, falling back to 0 is not the correct error handling result for all situations. In other situations, an error is the correct result. The language designers should include proper division, and this style of division should be labeled a "safe" division; or, a division that throws an error should be labeled an "unsafe" division.
I have serious doubts about a language if it chooses one-size-fits-all error handling like this.
It may be true that 1/0=0 can be part of a reasonably consistent system, but that doesn't mean it's a good one. Can we define 1/0 as ∞?
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.)
Basically the reason why 1/0 = 0 is wrong is the fact that you cant reproduce 1 by taking the answer 0 and multiplying it by 0 to get the number being divided. Which goes on to break a bunch of other fundamental rules of mathematics.
That is to say, if you took 6 / 2 = 3 you can reverse the division by doing 3 * 2 = 6.
However if you have 6 / 0 = 0 and you were to try and reverse it then you would have 0 * 0 != 6. Then you have bizarre circumstance where everything decided by zero logically equals the same thing. Where (2 + 2) / 0 all of a sudden equals (Einsteins laws of gravity) / 0. And there is no logical way to really explain what that is supposed to mean.
Also if you try to use limits to find a solution of f(x) = 1/x where x is defined as the limit of 1 and -1 as it approaches 0 from both sides. You end up with the answer that is even more confusing when you try to graph it.
That is x = +inf and -inf. Which on a graph is represented as two curves where the limit as 1 -> 0 from the positive side of the x axis curves up along the y axis to infinity without intersecting where x=0. And from the negative side where we approach 0 from -1 we end up with a curve that moves down the -y axis without intersecting at 0.
So frankly, n / 0 = 0 just doesn't make sense because just trying to approach it from both sides suggests that the closer you try to move to zero from both sides the further apart the answer moves away from converging together at the origin. Which would be expected if n / 0 = 0 was actually true.
So at least that's something
It's also nothing. :-)
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?
1.0 / 0
=> Float::INFINITY
0 * Float::INFINITY
=> Float::NAN
It's like WWE Raw Smackdown, Hulk Hogan vs. The Rock and everyone has to take a side.
And it's literally Friday night.
Sorry we're not supposed to comment like this buy y'all (I suppose 'we') are a really funny bunch sometimes.
Another interesting example is array access. What should a[len(a)+1] be if your language doesn't have runtime errors?
Elm returns a Maybe type. However, this would be very awkward if you're actually doing a lot of calculations using arrays.
[Edit: Pony is different.]
Because of this rule, defining / as a partial function forces the user to fence every single division in a try clause.
Using boxed integer as Elm does is not an option as Pony targets high-speed computing, not browser rendering. Different fields, different trade-offs.
Defensive users can well define `div(I32, I32): I32?` that throws an error and use it instead of `/`.
As repeated in this thread, 1/0 is undefined because nonsensical. So, it's OK to have any sane, consistent and well documented behaviour. At least with Pony, the user can choose speed and convenience when they're sure there is no possible 0 at this place. Well, TBH, I think it's always the case. Because there is no such thing as a division by zero, you're algorithm is simply wrong and unsound if it ends up dividing by 0, and that's where this case differs from integer overflow
Note: in Pony literature, "partial" means "can throw an error". "partial" as in "doesn't apply to the whole domain of the arguments types"
I prefer this because if you have a function converging on 0 then you will see growth towards Inf - then Inf - rather than growth followed by a cliff; which could then propagate into all your other calculations and move you from the very small to the very large in an instant.
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.
>>> 1 / 0
Traceback (most recent call last):
File "<stdin>", line 1, in <module>
ZeroDivisionError: division by zero
>>> 0 / 0
Traceback (most recent call last):
File "<stdin>", line 1, in <module>
ZeroDivisionError: division by zero
>>> 1 / 0.0
Traceback (most recent call last):
File "<stdin>", line 1, in <module>
ZeroDivisionError: float division by zero
>>> 0.0 / 0.0
Traceback (most recent call last):
File "<stdin>", line 1, in <module>
ZeroDivisionError: float division by zero
iex(1)> 1 / 0
** (ArithmeticError) bad argument in arithmetic expression: 1 / 0
:erlang./(1, 0)
iex(1)> 0 / 0
** (ArithmeticError) bad argument in arithmetic expression: 0 / 0
:erlang./(0, 0)
iex(1)> 1.0 / 0.0
** (ArithmeticError) bad argument in arithmetic expression: 1.0 / 0.0
:erlang./(1.0, 0.0)
iex(1)> 0.0 / 0.0
** (ArithmeticError) bad argument in arithmetic expression: 0.0 / 0.0
:erlang./(0.0, 0.0)
irb(main):001:0> 1 / 0
Traceback (most recent call last):
3: from /Users/mpope/.rbenv/versions/2.5.1/bin/irb:11:in `<main>'
2: from (irb):1
1: from (irb):1:in `/'
ZeroDivisionError (divided by 0)
irb(main):002:0> 0 / 0
Traceback (most recent call last):
3: from /Users/mpope/.rbenv/versions/2.5.1/bin/irb:11:in `<main>'
2: from (irb):2
1: from (irb):2:in `/'
ZeroDivisionError (divided by 0)
irb(main):003:0> 1 / 0.0
=> Infinity
irb(main):004:0> 0.0 / 0.0
=> NaN
> echo 1 / 0;
>
INF
Division by zero :1
> echo 0 / 0;
>
NAN
Division by zero :1
> echo 1 / 0.0;
>
INF
Division by zero :1
> echo 0.0 / 0.0;
>
NAN
Division by zero :1
Infinity
> 1 / 0
Infinity
> 0 / 0
NaN
> 1 / 0.0
Infinity
> 0 / 0.0
NaN In [1]: 255 + 1 is 256
Out[1]: True
In [2]: 256 + 1 is 257
Out[2]: False
Anyway, the Inf/NaN trick is not better than the 0 trick in my opinion, because all subsequent operations result happily in NaN. I've never seen in any NaN language a program that checks for NaN the result of each and every division.
with a NaN-kind of language, it would be:
a = b/c
if a == NaN:
print "oops"
a = b/c
if a == 0 and c == 0:
print "oops"
So, there's one data point in favor. :-)
Out of curiosity, could you describe what you were doing and why 1/0 = 0 would have returned the correct result?
So the code was given a path described by line segments p0-p1-p2-...pN, and what it wanted to do was find the point s distance along the path.
It's iterating over pairs of points (pI, pJ) and looking at the segment length. Is the segment length > the remaining length? If so, then we know our point is somewhere on the segment (pI, pJ). In particular, it is (remaining length) divided (segment length) pct along the segment.
This code was dying on zero-length segments (i.e., a repeated point) because of the divsion above. I wasn't thinking too clearly and fixed the problem by just skipping 0 length segments.
But actually, the only way that code can even trigger is if the original distance along the path was negative, in which case we actually just want to always return the start of the path.
So, in summary, my particular case was buggy either way, and 1/0 behavior doesn't hurt or help (except it caused a crash instead of an incorrect line in some cases; not really sure if that's better or worse).
For the case where we do have a zero-length segment, 1/0 = 0 would give desired behavior (just scale to first point in segment). (But of course, when it's a zero length segment, any value would be OK, since it would just get multiplied by zero again.)
y = 1/x
will result in 2 nice asymptotes with a dot in the middle (0,0)
1/0 = 0 doesn't make sense to me, even because lim x->0+ 1/x is infinite and lim x->0- 1/x is -infinite
so the value that makes more sense for 1/0 is infinite
The Post JavaScript Apocalypse https://youtu.be/99Zacm7SsWQ?t=2434
So that's it. I read your proof. You try cloaking it in pseudo-mathematical formulation, but what you are really doing is defining division as a derived operator, rather than the axiomatic operator it is in mathematics. I can say 1= infinity in my universe and as long as I am consistent, it is sound.
You're saying this is a useful property to have, and certainly that holds merit in certain conditions, but it is not a correct property.
Your article title should be clarified to state "1/0=0 (in my universe)." But then it wouldn't be controversial would it? After all, this is just an experiment to gain some visibility for Pony, isn't it?
In your link, division is defined as the inverse of multiplication. However, the inverse of multiplication is one of the axioms of the field, so by transitivity, division is an axiom as well (it's simply a convenient label for "the inverse of multiplication"). One can put the name "Division" to some other axiom or derived property, absolutely, but then "the inverse of multiplication" still needs to be dealt with. The author, if you note, conveniently omits the multiplicative inverse from their stated axioms.
I'm far from a pure mathematician, but even I can see through the facade, implying that it's pretty thin.
[1] https://en.wikipedia.org/wiki/GF(2)
> "It is totally fine to define 1/0 = 0."
No, it's not, at least not useful. If you define it that way, you will not have a field. Then you don't have +, -, *, and / operations with the commonly assumed behavior. However, it is definitely possible to define some operation such that 1 `op` 0 := 0, just not the inverse operation of multiplication.
If you read the post this is actually exactly what the OP is saying.
I, for one, will respectfully decline to use any programming language that defines 1/0 to be 0.
I say neigh (sorry if you didn't catch that joke, I'm a little horse).
If x/0 =0 then, since division is inverse of multiplication x= 0*0 this fails to hold for any x not 0
But the story says there is no defined multiplicative inverse of zero (undefined) so that they are free to choose any value they want. And they choose 0.
This is unsatisfactory to me because it seems to break the intuitive pattern of x/n getting larger as n approaches zero from the positives. 1/4 .25< 1/3 .33 < 1/2 .5 < 1/1 1 >1/0 0 >1/-1 -1 < 1/-2 -.5 < 1/-3 -.333
You see that sign flip thingy happening around 1/0?
Maybe I am misunderstanding.
This is playing semantic games. A whole lot does break: / no longer has its usual properties, and if you use those usual properties you can certainly prove false things. It's no different from saying that it's totally fine to define 2 + 2 = 5 and nothing breaks, you then just have to say that 5 isn't the arithmetic successor of 4 any more.
Thought of another reason besides below comment why I was wrong, but thanks goes to below comment too!
If you allow 0 to have a multiplicative inverse 1/0, then the product of 0 and 1/0 must be equal to the multiplicative identity, which is 1. Then it follows that 0 = 0 * 0 = 1. From here it's straightforward to prove that x = y for all x, y in the field F.
A multiplicative inverse is a division. You cannot define division by x in fields without defining multiplication by 1/x and vice versa. The article is plainly incorrect in its attempt to refute this point (and in any case, shouldn't be using field theory to justify its purpose in the first place).
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.
You know.. dividing is like breaking something up [..]
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.
Who is mocking anyone though?
The set of integers represented by the integer types of pony can be treated as a field, since they have discrete ranges.
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".