Hacker News Reader

Comment by ykonstant | Hacker News Reader

Amusingly, in the Lean proof assistant, division by zero in both Naturals and Integers results in zero:

    #eval (1/0 : Nat) -- 0
    #eval (1/0 : Int) -- 0

There are good reasons for this convention in the context of Lean, although I doubt that teacher had formal verification in mind :D

View on HN

I feel like a proof assistant is amongst the worst places to have something like this rather than (I don’t know how lean works) raising an error. What are the justifications for this convention?

> I feel like a proof assistant is amongst the worst places to have something like this

It's one of the best places! You know how in programming, your code looks like this?

    func my_function(inputs) -> output  { do something }

In theorem proving, it's almost the same:

    theorem my_theorem(assumptions) -> conclusion { prove something }

But there's a single crucial difference: in programming, the "do something" is really important, whereas in Lean, the "prove something" isn't important at all: as long as the typechecker is happy with it, everyone can forget about it once it's written.

So as long as your assumptions and conclusion don't involve any division by zero, it doesn't matter what goes on inside the proof.

Regarding division by zero, you sort of have three options:

* Output an error / checked null when there's division by zero.

* Require a proof that the denominator is nonzero before you're even allowed to use division.

* Allow division by zero, making it return some nonsense. Then, add an assumption that the denominator is nonzero to all your theorems about division.

The first two options (especially the second one) make the definition of functions that involve division horrifically messy. (Idk, it might be easier if Lean had exceptions, but that also sounds messy.) I think that's why Lean goes with the third option.

https://xenaproject.wordpress.com/2020/07/05/division-by-zer...

You typically can't "raise an error" in such contexts in formal reasoning tools. There's no "runtime" per se to raise an error from -- the expressions themselves are manipulated to derive truths -- the division by zero may simply be implicit e.g. in a statement about division by some arbitrary number.

Trying to solve the problem with e.g. dependent typechecking quickly gets complicated (both implementation and theory). And adding a concept such as infinity may complicate proofs which now need to deal with infinity being a "number" but which behaves differently from other numbers.

Thankfully mathematics has the nice property that you can define concepts any way you want so long as they're self-consistent and match one's expectations. So rather than treating division by zero as an exceptional case -- either by disallowing it in the typesystem, "raising an error", or by introducing a "special" value -- some (most?) verification languages simply define division by zero to have a numeric value, and make it known that this is the case. Users know that they must then write expressions to be explicit about division by zero if they care about that case. (This turns out to be not much different than having to write expressions to satisfy a dependent type system.)

Yes, but to make this "self-consistent" 0 * 0 = 1 would need to hold. And I'm totally sure that they don't have that...

((x / y) * y) = x is not a true statement about real numbers, regardless of if division by zero is defined as an error or as being equal to 0. The true statement is ( y != 0 -> ((x / y) * y) = x ), and this holds no matter how you define division by zero.

More generally, in normal math, every theorem that involves division by some value Y which could be zero must have as hypothesis that Y is not equal to zero. All these theorems still work in systems like Lean where division by zero is defined to be zero, so nothing is lost.

> You typically can't "raise an error" in such contexts in formal reasoning tools.

You could write all your formulas in the Maybe / Option monad (which I guess is the same as 'introducing a "special" value') but that sounds painful...

> There are good reasons for this convention in the context of Lean

There are good reasons for the convention of assigning nonsense values to computations that are formally invalid. The convention is so important that it is introduced in the Natural Number Game, where the remarks include a brief discussion of why the predecessor of 0 is defined to be 37.

I don't think there's any particular reason why you'd assign 0 as the nonsense value?

Reply on news.ycombinator.com