Comment by somewhereoutth | Hacker News Reader

Comment by somewhereoutth | Hacker News Reader

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').

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)

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

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.

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.

> n * inf == inf

I would expert this to be 0 actually.

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.

Apologies, I meant for 0 * inf = 0. Since in n * inf n can be 0 the result should be able to be 0.

You are correct - it should indeed be zero (and * can be constructed accordingly)

Reply on news.ycombinator.com