3 ms·
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.
by 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 agoWell, 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)