Re:Division by zero in type theory: a FAQ
by enriquto on Tuesday July 07, 2020 @05:25AM
(#23757257)
> if a mathematician sees this convention, their reaction is likely to be "that's just silly, 1/0 is obviously 'halt and catch fire'"
mathematician here. The expression 1/0 is not "obviously" halt and catch fire. Extended real numbers (either projectively or affinely) are a well-known thing. If you see the expression 1/0 or 1/f(x) where f(x) may take the 0 value you do not halt and catch fire; you assume that the operations are taking place in a place where they make sense. A very common usage is when f(x)=0 for a zero-measure set of x, and then 1/f(x) has dirac masses at these points (weighted by the absolute value of the derivative of f).
On the other hand, I agree that "type theory" would sound like a ridiculously unnecessary abstraction to most of us.
mathematician here. The expression 1/0 is not "obviously" halt and catch fire. Extended real numbers (either projectively or affinely) are a well-known thing. If you see the expression 1/0 or 1/f(x) where f(x) may take the 0 value you do not halt and catch fire; you assume that the operations are taking place in a place where they make sense. A very common usage is when f(x)=0 for a zero-measure set of x, and then 1/f(x) has dirac masses at these points (weighted by the absolute value of the derivative of f).
On the other hand, I agree that "type theory" would sound like a ridiculously unnecessary abstraction to most of us.