Email Gateway (Aug 22 2022 at 19:04): Email Gateway (Aug 22 2022 at 19:04):From: José Manuel Rodríguez Caballero <josephcmac@gmail.com>
This is just a short technical clarification (I do not see any motive to go
further in this discussion). There are peer-reviewed publications about the
so-called "division by zero calculus". For example,
Pinelas, Sandra, and Saburou Saitoh. "Division by zero calculus and
differential equations." *International Conference on Differential &
Difference Equations and Applications*. Springer, Cham, 2017.
https://link.springer.com/chapter/10.1007/978-3-319-75647-9_33
The fact that the definition x/0 = 0 has important applications in
mathematics can be explained, from a topological point of view, as the
identification between the zero and the infinity in the Riemann sphere. You
can see this idea illustrated in the following draw:
https://www.researchgate.net/figure/Division-by-zero_fig2_267659202
The moral of the division by zero calculus is that, when something is
undefined in simple type theory, like the value of 1/n for n = 0, it is
natural to define it in a way corresponding to some elegant topological
structure. For example, defining 1/0 = 5 is not useful, because it does not
correspond to an elegant topological structure. So, simple type theory
makes us discover new facts about mathematics that otherwise will
be unnoticed.
Kind Regards,
Jose M
Email Gateway (Aug 22 2022 at 19:04):From: Christian Sternagel <c.sternagel@gmail.com>
Just to clarify: My statement was meant in the context of Isabelle/HOL,
not in general math. That is, what I wanted to say is that Isabelle/HOL
does not (intentionally, at least as far as I know) use a "division by
zero calculus". I would guess that defining (/) in such a way that "x /
0 = 0" was just pragmatism. - chris
Email Gateway (Aug 22 2022 at 19:04):From: José Manuel Rodríguez Caballero <josephcmac@gmail.com>
I would guess that defining (/) in such a way that "x /
0 = 0" was just pragmatism. - chris
The reason for the introduction of x/0 = 0 in Isabelle/HOL was because many
laws involving division will then hold unconditionally, an example being
(ab)/(cd) = (a/c)*(b/d).
Why the laws hold unconditionally with x/0 = 0, but they do not otherwise,
e.g., with x/0 = 5?
A topological explanation of this phenomenon is by means of the
identification between zero and infinity in the Riemann sphere, i.e., the
division by zero calculus. These are two different level of analysis.
For example,
(ab)/(cd) = (a/c)*(b/d)
when b is 0 becomes
0/(c*d) = (a/c)/0
which in the Riemann sphere is
0 = infinity (this equality is true by definition of the topological
indentification between zero and infinity).
Why is this important for Isabelle/HOL?
Well, the topology gives a clue of how to define some values for functions
which are undefined in dependent type theory, e.g., x/0 is undefined in
Coq. Topology and programming are the same thing, described in two
different ways.
Kind Regards,
José M.
El jue., 28 feb. 2019 a las 3:30, Christian Sternagel (<
c.sternagel@gmail.com>) escribió:
Just to clarify: My statement was meant in the context of Isabelle/HOL,
not in general math. That is, what I wanted to say is that Isabelle/HOL
does not (intentionally, at least as far as I know) use a "division by
zero calculus". I would guess that defining (/) in such a way that "x /
0 = 0" was just pragmatism. - chrisOn 2/28/19 1:10 AM, José Manuel Rodríguez Caballero wrote:
chris wrote:
A short answer is: there is no "division by zero calculus".This is just a short technical clarification (I do not see any motive to
go further in this discussion). There are peer-reviewed publications
about the so-called "division by zero calculus". For example,Pinelas, Sandra, and Saburou Saitoh. "Division by zero calculus and
differential equations." /International Conference on Differential &
Difference Equations and Applications/. Springer, Cham, 2017.
https://link.springer.com/chapter/10.1007/978-3-319-75647-9_33The fact that the definition x/0 = 0 has important applications in
mathematics can be explained, from a topological point of view, as the
identification between the zero and the infinity in the Riemann sphere.
You can see this idea illustrated in the following draw:
https://www.researchgate.net/figure/Division-by-zero_fig2_267659202The moral of the division by zero calculus is that, when something is
undefined in simple type theory, like the value of 1/n for n = 0, it is
natural to define it in a way corresponding to some elegant topological
structure. For example, defining 1/0 = 5 is not useful, because it does
not correspond to an elegant topological structure. So, simple type
theory makes us discover new facts about mathematics that otherwise will
be unnoticed.Kind Regards,
Jose M
Last updated: Apr 19 2024 at 08:19 UTC