4 ms·

Mathlib does indeed define the extended real numbers, but they also need to define division on the reals. This is similar to the definition of subtraction havin

by zodiac 6y ago

Mathlib does indeed define the extended real numbers, but they also need to define division on the reals. This is similar to the definition of subtraction having to be done for integers and for naturals (mentioned in the article)

somewhereoutth 6y ago
I presume though that Mathlib does not define the extended naturals? If they did then 1:N / 0:N would be valued at this infinity. What I found interesting about the Scott encoding was that natural infinity was trivial to define, and arises directly from a straightforward construction of the div function (for naturals). The encoding is as follows (\x indicates lambda abstraction for identifier x. Recursion is assumed, of course it could be made explicit with the Y combinator): zero := \f \x n succ := \n \f \x f n infinite := \n succ (infinite n) infinity := infinite zero subn := \n \m m (\p n (\q subn q p) n) n divn := \n \m (subn m n) (\p zero) (succ (divn (subn n m) m)) divn (succ zero) zero => infinity EDIT: Note that infinity does not have a normal form (does not terminate), but: subn n infinity => zero
- zodiac 6y ago
  The extended reals can also arise directly from the definition of reals either as Cauchy sequences of rationals (as unbounded increasing sequences, etc) or Dedekind cuts (let the lower cut contain all rationals) :) for reals IIRC the main reason to exclude the extended reals is to make it a field. However I don't think any of this matters for the point the article made. The problem is not that 1:N/0:N has "nothing sensible" to return, the problem is that if you define it in the way most mathematicians do, a lot of your proofs will be littered with (inline) lemmas showing that the result of such-and-such a division is a finite natural / finite real. This is analogous the problem brought up in the article of having proofs littered with lemmas showing that the result of such-and-such a square root was real.
- leanuser57 6y ago
  In fact, there is also a type `enat` in mathlib. However, have `x/y` be a term of a type that is not the type of `x` and `y` comes with it's own sets of problems. It doesn't compose as smoothly as homogeneous division.

by zodiac 6y ago

somewhereoutth 6y ago

I presume though that Mathlib does not define the extended naturals? If they did then 1:N / 0:N would be valued at this infinity. What I found interesting about the Scott encoding was that natural infinity was trivial to define, and arises directly from a straightforward construction of the div function (for naturals). The encoding is as follows (\x indicates lambda abstraction for identifier x. Recursion is assumed, of course it could be made explicit with the Y combinator): zero := \f \x n succ := \n \f \x f n infinite := \n succ (infinite n) infinity := infinite zero subn := \n \m m (\p n (\q subn q p) n) n divn := \n \m (subn m n) (\p zero) (succ (divn (subn n m) m)) divn (succ zero) zero => infinity EDIT: Note that infinity does not have a normal form (does not terminate), but: subn n infinity => zero

zodiac 6y ago
The extended reals can also arise directly from the definition of reals either as Cauchy sequences of rationals (as unbounded increasing sequences, etc) or Dedekind cuts (let the lower cut contain all rationals) :) for reals IIRC the main reason to exclude the extended reals is to make it a field. However I don't think any of this matters for the point the article made. The problem is not that 1:N/0:N has "nothing sensible" to return, the problem is that if you define it in the way most mathematicians do, a lot of your proofs will be littered with (inline) lemmas showing that the result of such-and-such a division is a finite natural / finite real. This is analogous the problem brought up in the article of having proofs littered with lemmas showing that the result of such-and-such a square root was real.
leanuser57 6y ago
In fact, there is also a type `enat` in mathlib. However, have `x/y` be a term of a type that is not the type of `x` and `y` comes with it's own sets of problems. It doesn't compose as smoothly as homogeneous division.