did someone muck with the backend here

## Re: x/0 = 0

1

FOUR. I just posted FOUR topics.

Posted by: heebie-geebie | Link to this comment | 08-13-18 7:55 AM
2

This is a fun read. In our recent conversation I was lazy and equated division with multiplication by the inverse; this person is more of a stickler than me, and is right to be so.

The fact that we should have, symbolically, 1/0 = 1/0, is particularly amusing. In IEEE floating pointing, 1/0 resolves to NaN, Not-a-Number. Multiple bit-strings are defined as being NaN (I forget if these correspond to different error codes, or whether there's some flexibility to make implementation easier). However, NaNs are defined as having the very weird property of not being equal to themselves This leads, bizarrely, to the implementation of Java's Double.isNaN(double x) being x != x.

There is a bit of a bait and switch here, though:

Since this form of division is not defined for 0, it is a partial function over the reals: there is some value in its domain that we have not specified. Practically, this is fine: we're used to thinking of 1/0 as an impossible operation. But this has some weird consequences: one of our axioms is everything is equal to itself. So does 1/0 = 1/0? If you say that's silly, we no longer have a = a!

No, that's not a weird consequence of it. 1/0 is meaningless. Function notation is syntactic sugar for a set of ordered pairs (in one construction of mathematics!). If f is defined only on the reals, f(1+i) is meaningless as none of its ordered pairs have 1+i as the first element. Likewise, if division is a partial function on R^2, for every x the division set does not contains ((1,0),x).

Of course, for any extension of division to cover the entirety of R^2 (or Q^2, etc.), it is true that 1/0 = 1/0.

They make a good point about the typing of head. There are trade-offs in doing this, and in practice I'd probably feel unnecessarily wary.

Posted by: dalriata | Link to this comment | 08-13-18 8:24 AM
3

Algebra does not equal programming, despite their happy co-dependent relationship. You only get one with the other, so to speak.

Posted by: montisimoo | Link to this comment | 08-13-18 8:39 AM
4

Better metaphor: Programming is the cranky uncle/aunt of maths. The one who is smart and very logical and also always wants to tell you about their new insight into base layer things that don't make sense when you just remove X as an assumption (it's always YOUR assumption).

Best to pat them on the head for really opening your eyes and move on...

Posted by: montisimoo | Link to this comment | 08-13-18 8:43 AM
5

Wait until this explorer discovers the Riemann series theorem.

Posted by: lw | Link to this comment | 08-13-18 8:43 AM
6

The idea that we're throwing continuity out the window annoys me. 1/$\epsilon$ should be close to 1/0.

Posted by: heebie-geebie | Link to this comment | 08-13-18 8:43 AM
7

Oh, don't you know? As you move arbitrarily far away from the origin, you get arbitrarily close to 19.

Posted by: dalriata | Link to this comment | 08-13-18 8:46 AM
8

Anyway, the programmer lolz seem a bit uncalled for, because 1) computer science is not programming, and 2) a bunch of proof systems support this. This is a logistician's game, not a programmer's.

Posted by: dalriata | Link to this comment | 08-13-18 8:48 AM
9

Logistician? Logician. It's Monday.

Posted by: dalriata | Link to this comment | 08-13-18 8:49 AM
10

I just posted FOUR topics

You already got enough credit for the last group of four things you produced.

Posted by: Todd | Link to this comment | 08-13-18 8:50 AM
11

As you move arbitrarily far away from your base of supply, your stocks get arbitrarily close to 0.

Posted by: Mossy Character | Link to this comment | 08-13-18 8:53 AM
12

For some reason I always thought the Bard's Love Minus Zero/No Limit was a reference to division by zero.

Posted by: bill | Link to this comment | 08-13-18 8:55 AM
13

And I though the Oxfordian theory was ridiculous.

Posted by: Mossy Character | Link to this comment | 08-13-18 8:56 AM
14

8: and as he says, he asked several math folks to look it over.

Heebie, is it less continuous this way? 1/epsilon isn't close to "not defined", is it?

Posted by: nosflow | Link to this comment | 08-13-18 8:57 AM
15

It's totally less continuous, because in the usual case division is continuous on its entire domain.

Posted by: dalriata | Link to this comment | 08-13-18 8:59 AM
16

Seems like a trick!

Posted by: nosflow | Link to this comment | 08-13-18 9:01 AM
17

10: Was it Kittens? or Snakes? are they loose in the house????

Posted by: montisimoo | Link to this comment | 08-13-18 9:01 AM
18

I didn't really get much out of this article. Sure you can define a function however you'd like if you don't care what properties it has! You could define 5/7 to be 0 too if you wanted. What I don't understand is why you'd want to define x/0 = 0. The people making Coq and Lean are smart people, so I'm sure there's some reason, but this article doesn't touch on it at all.

Posted by: Unfoggetarian: "Pause endlessly, then go in" (9) | Link to this comment | 08-13-18 9:02 AM
19

8: I didn't mean this specific programmer, specifically, just in general. Given [author] is a programmer, without math background, it doesn't seem like lulz to quip about. [x] is exploring and I read the article. Seems fair to me.

Posted by: montisimoo | Link to this comment | 08-13-18 9:05 AM
20

But you couldn't, because 7 has a multiplicative inverse? The whole point was that you can do this while preserving division's properties (those which were enumerated anyway).

Posted by: nosflow | Link to this comment | 08-13-18 9:05 AM
21

18:Buffer overruns. IT'S ALWAYS THE BUFFER OVERRUNS.

Posted by: montisimoo | Link to this comment | 08-13-18 9:06 AM
22

You'd still have versions of those properties, if you simply check that the numbers involved weren't 5 and 7.

Posted by: Unfoggetarian: "Pause endlessly, then go in" (9) | Link to this comment | 08-13-18 9:08 AM
23

You'd still have versions of those properties, if you simply check that the numbers involved weren't 5 and 7.

Posted by: Unfoggetarian: "Pause endlessly, then go in" (9) | Link to this comment | 08-13-18 9:08 AM
24

You could define 5/7 to be 0 too if you wanted.

There's some funny apocryphal story about ill-suited names for things and all I remember about is that it started, "Let 6 be a group..."

Posted by: heebie-geebie | Link to this comment | 08-13-18 9:10 AM
25

Heebie, is it less continuous this way? 1/epsilon isn't close to "not defined", is it?

When pressed on what "infinity" means, I usually say "it's a direction, not a number", which is useful here for seeing how 1/epsilon approaches infinity as epsilon goes to zero. Or, the extended real line is nice too.

Posted by: heebie-geebie | Link to this comment | 08-13-18 9:12 AM
26

What does he want to define 2/2 mod 6 to be? 0 again? 1? 4?

Posted by: Unfoggetarian: “Pause endlessly, then go in” (9) | Link to this comment | 08-13-18 9:20 AM
27

Working in logic, I would expand out the statement that a function is continuous everywhere like this:

forall x. f is continuous at x
forall x. forall y. forall e. exists d. |x-y| < d => |f(x)-f(y)| < e

So there's a question now of how to treat this. Are functions sets of ordered pairs, or should we use the function symbols built in to most logics? As far as I can recall, the function symbols don't allow partial functions, so that makes them ill-suited for this approach. If we take the former approach, I'd expand it out as

forall x. forall y. exists z. exists w. (x,z) in f and (y,w) in f => forall e. exists d. |x-y| < d => |z-w| < e

which regular division satisfies (with any value you'd like for z when x = 0), and wacky 19=1/0 division doesn't.

Posted by: dalriata | Link to this comment | 08-13-18 9:22 AM
28

I like to assume e = pi. It makes things easier.

Posted by: Moby Hick | Link to this comment | 08-13-18 9:24 AM
29

I had a cat named Epi, but that's not why.

Posted by: heebie-geebie | Link to this comment | 08-13-18 9:26 AM
30

Also all the stuff about fields in the post just reads to me as "see I do know math!"-defensiveness, and doesn't really add anything to the argument.

Posted by: Unfoggetarian: “Pause endlessly, then go in” (9) | Link to this comment | 08-13-18 9:27 AM
31

My son is personally offended by i.

Posted by: Moby Hick | Link to this comment | 08-13-18 9:28 AM
32

31: Teach him about Galois and field extensions, and why it's more important to be good at dueling than good at math.

Posted by: dalriata | Link to this comment | 08-13-18 9:29 AM
33

I'd be much happier defining x/0 = 17. At least then you're unlikely to accidentally have equalities work out, and when you debug and suddenly think "why are these 17s here?" you can remember "oh yeah, I made x/0=17 for some reason" and find the source of the error.

Posted by: Unfoggetarian: “Pause endlessly, then go in” (9) | Link to this comment | 08-13-18 9:31 AM
34

Posted by: Moby Hick | Link to this comment | 08-13-18 9:33 AM
35

Round numbers make people suspicious.

Posted by: Moby Hick | Link to this comment | 08-13-18 9:36 AM
36

31: Not a fan of e.e. cummings?

Posted by: peep | Link to this comment | 08-13-18 9:37 AM
37

Anyway, that 0/0 != 1 in that formulation makes it pretty worthless. You still have cases where you'd have to special case for zero, even for purely algebraic concerns. Multiplying by a form of 1 should be safe and useful.

Posted by: dalriata | Link to this comment | 08-13-18 9:37 AM
38

Round numbers make people suspicious.

17 is way less round than 16.8. Look at all those curves.

Posted by: heebie-geebie | Link to this comment | 08-13-18 10:05 AM
39

You'd still have versions of those properties, if you simply check that the numbers involved weren't 5 and 7.

The point is that you don't need "versions" of those properties with the extension in the article. You have the same properties, because they were already, quite reasonably, formulated so as not to apply to division by zero.

Also all the stuff about fields in the post just reads to me as "see I do know math!"-defensiveness, and doesn't really add anything to the argument.

What do you think the argument even is?

Posted by: nosflow | Link to this comment | 08-13-18 10:28 AM
40

What do you think the argument even is?

It's not good to be smug, because you're bound to be wrong sooner or later.

Posted by: peep | Link to this comment | 08-13-18 10:35 AM
41

What do you think the argument even is?

Also, numbers are surprisingly complicated.

Posted by: peep | Link to this comment | 08-13-18 10:37 AM
42

The argument is that if you have a function that's partially defined, then you can extend it everywhere in any way you like, and any statement about the original function will still hold so long as you restrict said statements to the original domain. It has nothing to do with multiplication, division, or fields.

Posted by: Unfoggetarian: "Pause endlessly, then go in" (9) | Link to this comment | 08-13-18 10:42 AM
43

Infinity divided by zero is the same as infinity squared.

Posted by: Moby Hick | Link to this comment | 08-13-18 10:52 AM
44

So, two divided by zero is four.

Posted by: Moby Hick | Link to this comment | 08-13-18 10:53 AM
45

Which journal should that go to?

Posted by: Moby Hick | Link to this comment | 08-13-18 10:54 AM
46

Pacing!/0

Posted by: fake accent | Link to this comment | 08-13-18 11:36 AM
47

There was an interesting, if depressing, story by Ted Chiang where a mathematician finds an obscure corner of mathematics where all the assumptions break down and you start being able to prove a = -a, forcing the understanding that mathematics is fundamentally a set of parlor tricks that is useful in real life but has no transcendent unity or meaning. It makes her suicidal.

That's what I was reminded of when I got to "It turns out that for certain choices of C, specifically 0, we can make some theorems stronger." Probably inappositely, as I don't think I actually understand this.

Isn't it assuming part of its conclusion with axiom 9, "Every element EXCEPT 0 has a multiplicative inverse"? Why must that be an axiom?

Posted by: Minivet | Link to this comment | 08-13-18 11:43 AM
48

I said this in a previous thread that I'm too lazy to look up, but assume zero has a multiplicative inverse, Z. You're going to get the problems that people think of when they hear "division by zero."

0 = 0 (Reflexivity oof equality)
0 + 0 = 0 (Additive identity)
(0 + 0)*Z = 0*Z (Easy equality theorem)
0*Z + 0*Z = 0*Z (Distributivity)
1 + 1 = 1 (Z is multiplicative inverse of 0)
1 + 1 - 1 = 1 - 1 (Easy equality theorem)
1 + 0 = 0 (Additive inverse)
1 = 0 (Additive identity)

It's taken as an axiom that 1 != 0, but if you don't take that as an axiom, you can then show that for all x, x = 0:

1 = 0
1*x = 0*x
x = 0

So therefore you must be in a trivial, single-element space.

For what it's worth, there are a few places in the fundamentals of mathematics--sometimes philosophically, sometimes logically--where we aren't on as firm of ground as we'd like to be. But I think most people who think about that sort of thing aren't very worried about it.

Posted by: dalriata | Link to this comment | 08-13-18 11:53 AM
49

But I think most people who think about that sort of thing aren't very worried about it.

Presumably because they also have real worries like toothaches, disobedient children, mortgage payments etc.

Posted by: peep | Link to this comment | 08-13-18 11:59 AM
50

Honestly, having bought fifteen years ago really helps with one worry.

Posted by: Moby Hick | Link to this comment | 08-13-18 12:03 PM
51

What do you think the argument even is?

Talk less, smile more.

Posted by: lw | Link to this comment | 08-13-18 12:07 PM
52

I think it was a more popular thing to worry about in the first half of the 20th century (somebody with a better sense of the history here, please chime in). There was a lot of work that had to be done to get people to be comfortable, especially after Erdos changed everything.

Posted by: dalriata | Link to this comment | 08-13-18 12:08 PM
53

s/Erdos/Godel/, jeez! They're both mathematicians with names that are five letters long and have a diacritic I tend to omit.

Posted by: dalriata | Link to this comment | 08-13-18 12:10 PM
54

Isn't that the name of the super-trippy book from when I was 14?

Posted by: heebie-geebie | Link to this comment | 08-13-18 12:15 PM
55

25. One complication with the idea that 1/0->inf is that one needs to decide on which infinity, whether +inf, -inf, or complex-inf.

Posted by: BA | Link to this comment | 08-13-18 1:29 PM
56

I just assumed epsilon was approaching zero by swirling around the complex plane as |ε|ei/|ε| where |ε| → 0, and then restrict it to the positive reals. Why borrow trouble?

Posted by: heebie-geebie | Link to this comment | 08-13-18 1:52 PM
57

This guy. This guy. What a bullshit artist. Let me quote from https://tutorial.ponylang.org/gotchas/divide-by-zero.html

In Pony, integer division by zero results in zero. That's right,
let x = I64(1) / I64(0)
results in 0 being assigned to x. Baffling right? Well, yes and no. From a mathematical standpoint, it is very much baffling. From a practical standpoint, it is very much not.

Similarly, floating point division by zero results in inf or -inf, depending on the sign of the numerator.

I search his essay, for the words "integer", "real" and "floating". No instances other than "real math" (and its variants). He's cleverly (maybe even to himself) obscured the distinction between these two kinds of division. Oh, and: his "real mathematicians" are Paulson (computer scientist and mathematical logician), Lamport (computer scientist) and two Haskell/Coq guys who might have been mathematicians, but are today CS types.
This is .... underwhelming evidence that mathematicians agree with him. And why? B/c (setting aside Lamport, who's a CS guy thru and thru) they're mathematicial logicians. And that's like mathematics, in the way that pr0n is like a real sexual relationship. Crikey, it's so embarrassing.

If he'd said:

I've defined this function div1(x) =def= if x == 0 then 1 else 1/x, aren't I clever? It's almost like division, but it has this neato special case!
I'd say "sure man, whatever floats your boat, mang".

P.S. I lived in that world (of formal methods, constructivism) for a decade. I wrote Coq V5.10.
P.P.S. He says "do not mock other programmers". And yet, the people who defined the ANSI floating point standard are almost *certainly* more "real" programmers than the constructivists and logicians he cites.

Posted by: Chet Murthy | Link to this comment | 08-13-18 2:04 PM
58

I don't think the distinction between integer and floating point math really matters much to his point. And it's possible that the original tweeter is the one who scrubbed the distinction, or that the Pony maintainers changed it since that tweet. Here's the tweet, so the lack of reference to non-integer math is not on the blogger. (And honestly, getting a lot of attention via a viral tweet is a good reason to clarify your documentation.)

I disagree with the implementers of Pony that this is practical. Putting on my programmer hat, if I divide by zero, even integer zero, I probably screwed up and would like to fail fast via an exception or similar means. Even if we can extend the division function a value that doesn't lead to inconsistencies when we work in the restricted domain, it doesn't let me know when I've walked off the edge of the map.

I feel like the hypothetical quote you give is basically what he's saying? He's only referencing experts just in case you don't believe his arguments about consistency hold.

Posted by: dalriata | Link to this comment | 08-13-18 2:29 PM
59

||

Quite the comedy-of-manners shaping up between Azalea Banks, Grimes, and Elon Musk.

I guess when people get super-rich enough they revert to the Wodehouse materteral-estate model where nodding acquaintances might stay for days on your whim.

|>

Posted by: Minivet | Link to this comment | 08-13-18 4:09 PM
60

I was actually thinking earlier today "this would make way more sense if he were talking about integer division." The point is integer division a/b is really giving you the quotient (which is an integer) and a remainder which is maybe an integer but maybe is better thought of as a congruence class modulo b. The key relationship is a = bq + r. If b is zero then r lives in the integers mod 0, and so is just a, which means a should be zero. It's very defensible to say integer division by 0 gives 0, and totally nutty to say real division by 0 is 0.

There's a related error in his twitter which is claiming there's no justification for 0^0=1. That's true for real exponentiation, but for integer exponentiation there's an easy reason: a^b is the number of maps from an a element set to a b element set. So 0^0 is the number of maps from the empty set to itself, which is certainly 1.

Posted by: Unfoggetarian: “Pause endlessly, then go in” (9) | Link to this comment | 08-13-18 5:07 PM
61

Sorry there's errors in my comment. At any rate, for integer division any quotient makes sense (a = 0 q +a works no matter what q is), while for real division no quotient makes sense (you can't have 0 x/0 = x).

Posted by: Unfoggetarian: “Pause endlessly, then go in” (9) | Link to this comment | 08-13-18 5:10 PM
62

I'm not sure what to think about the link in the post.

I had trouble figuring out the types he was talking about. Integers or rationals? I don't think reals or IEEE 754 floats work.

There is a point to getting your definitions so your theorems don't have special case clauses.

Sorta on topic - were there mathematicians before the 19th century who worked out non-Euclidean geometries but could not accept them as consistent because of the surprising consequences?

Posted by: Robert | Link to this comment | 08-13-18 5:30 PM
63

Yes. That was Rule 33.

Posted by: Moby Hick | Link to this comment | 08-13-18 7:32 PM
64

61: Or alternatively there's a quotient that makes sense for every value except 0/0, and you've just reduced your number of undefined cases from uncountably infinite to one.

Good point on integer multiplication, though.

The 0^0 thing was a question on a test I had to take for placement in my engineering school, and I remember being intensely frustrated by it--I had a very bad memory back then, and I couldn't figure out how to derive from first principles which function to make discontinuous.

Posted by: dalriata | Link to this comment | 08-13-18 8:29 PM
65

Maybe I am being silly about types.

The author of the linked story explicitly distinguishes between the multiplicative inverse of 3 and 1/3. He wants to have a theorem that connects them, with a clause in the theorem about zero. But he starts with a field, not a commutative ring with unity.

Posted by: Robert | Link to this comment | 08-13-18 10:29 PM
66

If you enjoyed this you'll love this:

https://aip.scitation.org/doi/full/10.1063/1.4940236

It turns out loss aversion is only a thing if you assume wealth doesn't compound and running out of cash isn't a problem - and the source of the silly assumptions is that economists didn't integrate non-ergodicity when that became a thing in the 19th century. Also, Bernouilli got his sums wrong and nobody noticed.

Fortunately it was the gambling problem rather than aerodynamics:-)

Posted by: Alex | Link to this comment | 08-14-18 3:01 AM
67

I'm not sure whether to be sad or happy that my company blocks the domain of the OP link.

Incidentally, Floats/Doubles are not Rational Numbers, they are Integers in drag.

Posted by: DaveLMA | Link to this comment | 08-14-18 5:05 AM
68

48: My math is old (in the years sense) but this one stumped me.

0*Z + 0*Z = 0*Z (Distributivity)
1 + 1 = 1 (Z is multiplicative inverse of 0)

Isn't multiplicative inverse applicable only to non-zero stuff?

Posted by: montisimoo | Link to this comment | 08-14-18 8:35 AM
69

67: You'd think getting up in drag would make them better at associating, not less.

68: Yes, it is. This was explicitly assuming that such a multiplicative inverse exists, to see the weird state it gets you in. (It isn't quite a proof by contradiction, if you're willing to accept that sometimes 1 = 0.)

Posted by: dalriata | Link to this comment | 08-14-18 8:40 AM
70

Thanks! Weirdness is inherent when the OP is just ignoring stuff for his field then we use non-field properties.

I mean the whole OP boils down to computers don't like dividing by zero because it causes blue screens of death, does this mean zero is divisible? Some thoughts!!!!

Posted by: montisimoo | Link to this comment | 08-14-18 9:40 AM
71

I had the same reaction as 18 -- I don't really get the point. You necessarily have either a partial function that satisfies all the equations that you'd like, and a total function that doesn't. In either case the fact that the equations don't hold unconditionally will sometimes bite you.

In primitive recursive arithmetic, which is only defined for natural numbers, you define 0 - 1 to be 0. Why? Because for this setting it's easier to work with total functions.

Posted by: Walt Someguy | Link to this comment | 08-14-18 2:14 PM
72

FORTRAN defined 1/0 as 0 for years. So did most machine languages. Of course the set of integers from 0 to 2^N-1 isn't a ring. Nowadays, 1/0 triggers an error to be handled as an exception, either that or it returns NaN which is IEEE for not a number.

Posted by: Kaleberg | Link to this comment | 08-14-18 9:38 PM