3 ms·

Using Scott encoding in the Lambda Calculus it is actually possible to define a 'usable' infinite natural number as a recursive construction (essentially its pr

Using Scott encoding in the Lambda Calculus it is actually possible to define a 'usable' infinite natural number as a recursive construction (essentially its predecessor is defined as itself). Interestingly enough, constructions for add, (natural) subtract and multiply work as you would expect with this infinite number without needing special handling. E.g. for all n, n + inf == inf, n - inf == 0, n * inf == inf. Furthermore, the construction for (natural) div yields this infinite term (or at least something that behaves exactly like it) when the denominator is 0. Even more interestingly, 0/0 == inf for this system. EDIT: Why might this be useful? Well now when you 'take n' from a list, n=inf will give you the whole list, regardless of how long (or even if it is infinite - i.e. lazy). Likewise 'drop n' will return the empty list - except with an infinite list, whereupon the calculation will fail to terminate. EDIT: inf - inf == non-termination in this system, suggesting that not only inf - inf != 0, but it != inf either, and in fact it is something unreachable (in this system) (note the correspondence between 'subtract' and 'drop').

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.
dependenttypes 6y ago
> n * inf == inf I would expert this to be 0 actually.
- teraflop 6y ago
  Why would you want the product of two non-zero values to equal zero? Among other things, this would have the unpleasant effect of making expressions like "0÷1" undefined, because the result could equal either zero or infinity.
  - dependenttypes 6y ago
    Apologies, I meant for 0 * inf = 0. Since in n * inf n can be 0 the result should be able to be 0.
    - somewhereoutth 6y ago
      You are correct - it should indeed be zero (and * can be constructed accordingly)

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.

dependenttypes 6y ago

> n * inf == inf I would expert this to be 0 actually.

teraflop 6y ago
Why would you want the product of two non-zero values to equal zero? Among other things, this would have the unpleasant effect of making expressions like "0÷1" undefined, because the result could equal either zero or infinity.
- dependenttypes 6y ago
  Apologies, I meant for 0 * inf = 0. Since in n * inf n can be 0 the result should be able to be 0.
  - somewhereoutth 6y ago
    You are correct - it should indeed be zero (and * can be constructed accordingly)