2 ms·

BTW, this is the same approach taken by the Coq, Isabelle and Lean theorem provers. In all of them, 1/0 = 0. It is certainly unconventional, but whether this is

by pron 8y ago

BTW, this is the same approach taken by the Coq, Isabelle and Lean theorem provers. In all of them, 1/0 = 0. It is certainly unconventional, but whether this is wrong is a matter of philosophy. Basically, division by zero is undefined, but you can define it to be zero and so extend the definition. This is consistent with the rest of arithmetic. You get more theorems (like for all a, b and c, a/c = b/c), but no inconsistencies.

OskarS 8y ago
You'd think that in these kinds of dependent type systems you would have to use the type system to prove that when doing a/b, b is never equal to 0.
- pron 8y ago
  Well, designing a language (even a mathematical one) is an art, and you need to trade off measures of convenience. The mathematical axioms that define division by zero to be equal to zero are consistent and so "correct" (if unconventional), and it turns out to be more convenient to define things in this way in those particular formalisms (rather than having to prove each time that you're not zero). You can define different theories in those systems that leave zero outside the domain of division or define it to be some value that means "undefined", but that's how it's done in the default arithmetical theories in those languages (and, BTW, Isabelle/HOL is not based on dependent types; Coq and Lean are). Other proof systems, like TLA+, do it differently. For a recent discussion about this on the Isabelle mailing list, see here https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-March/thread.html https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-Mar... (search for 1/0)
wafflebear 8y ago
The users of Coq and Isabelle are generally people with mathematics degrees who check their work. Not your average programmer.
- pron 8y ago
  You are correct that the requirements are different, but not exactly for the reasons you mention. Users of those languages use them to prove theorems, and the theorems you get are correct with respect to the arithmetical theory used. Programmers may want some error condition when dividing by zero, because that's what they believe their users expect (say, the program drives some actuator, and bad things may happen if division by zero is not detected). So yeah, the justification for this behavior needs to be different.

by pron 8y ago

OskarS 8y ago

You'd think that in these kinds of dependent type systems you would have to use the type system to prove that when doing a/b, b is never equal to 0.

pron 8y ago
Well, designing a language (even a mathematical one) is an art, and you need to trade off measures of convenience. The mathematical axioms that define division by zero to be equal to zero are consistent and so "correct" (if unconventional), and it turns out to be more convenient to define things in this way in those particular formalisms (rather than having to prove each time that you're not zero). You can define different theories in those systems that leave zero outside the domain of division or define it to be some value that means "undefined", but that's how it's done in the default arithmetical theories in those languages (and, BTW, Isabelle/HOL is not based on dependent types; Coq and Lean are). Other proof systems, like TLA+, do it differently. For a recent discussion about this on the Isabelle mailing list, see here https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-March/thread.html https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-Mar... (search for 1/0)

wafflebear 8y ago

The users of Coq and Isabelle are generally people with mathematics degrees who check their work. Not your average programmer.

pron 8y ago
You are correct that the requirements are different, but not exactly for the reasons you mention. Users of those languages use them to prove theorems, and the theorems you get are correct with respect to the arithmetical theory used. Programmers may want some error condition when dividing by zero, because that's what they believe their users expect (say, the program drives some actuator, and bad things may happen if division by zero is not detected). So yeah, the justification for this behavior needs to be different.