Why don't we define “imaginary” numbers for every “impossibility”? (2012)

Re:Why don't we define “imaginary” numbers for every “imposs... by ndsipa_pomu on Monday April 10, 2023 @10:41AM (#35512900)

Thanks - I was not aware that theorem provers often allow "division" by zero.

Looking at https://xenaproject.wordpress.com/2020/07/05/division-by-zer... I see that they don't use mathematical division, but define a slightly different operator with an additional condition for handling zero. This appears to be far more convenient for theorem provers.

The trade-off would be that "division" is no longer the inverse of multiplication.

[ Parent | on HN ]

Re:Why don't we define “imaginary” numbers for every “imposs... by momentoftop on Monday April 10, 2023 @12:29PM (#35514134)

Ah, thanks for the link. I suggested the reason that Isabelle/HOL does this is because it requires total functions and you don't have a convenient way to do refinement types. But that's not an adequate explanation, because Lean does allow such refinements, but it still turns out to be inconvenient for division.

I will note that setting a - b = 0 for a <= b is pretty standard, and is often called "partial subtraction."

[ Parent | on HN ]