2
$\begingroup$

I'm puzzled by this question, which is more about relation between two type theoretic approaches. Nevertheless, It can be shortened to the question :

When it is correct (if ever) to construct natural numbers as lists of units?

Here is my line of thought:

In Type theory we can define Type of natural numbers inductively:

$\dfrac{\quad}{0 : \mathbb{N}}$ $\dfrac{n : \mathbb{N}}{S(n) : \mathbb{N}}$

And there is also a mathematical induction rule:

$$ \frac{C:\mathbb{N} \to \mathrm{Type},b : C(0),i: \forall n \in \mathbb{N}. C(n) \to C(S(n))}{\mathrm{ind}(C,b,i):\forall n \in \mathbb{N} . C(n)} $$

and primitive recursion (which can be proved from natural induction): $$ \frac{a: X, f:X \to X}{\mathrm{iter}(f,a):\mathbb{N}\to X,\mathrm{prec}(f,a) : (\mathrm{iter}(f,a)(0) =_X a) (\forall n : \mathbb{N} . \mathrm{iter}(f,a)(S(n))=_X f(\mathrm{iter}(f,a)(n))) } $$ As I understood members of this type will be equivalent to natural numbers from classical set-theoretic mathematics. However we also can define type of lists $L(T)$ over another type $T$ by this recursive algebraic expression: $$L(T) = () | (T \times L(T) )$$ Where $()$ indicates empty set. It seemed natural to me that we can rewrite our definition for natural numbers as $\mathbb{N}' = L(()) = 0 | (0 \times\mathbb{N}')$ (Having $0 = ()$ in order to assure $0 \in \mathbb{N} $) . That is, represent them as lists of units. However, in some programming languages like Haskell, infinite lists will be considered as proper objects of type $L(T)$. This means that $\mathbb{N}'$ will contain an infinite sequence of units or from set theoretic point of view, $\mathbb{N}' = \mathbb{N} \cup \{ \infty \}$. If we view this $\infty$ structure then we can see that $S(\infty) =\infty$. So $\mathbb{N}'$ are not proper natural numbers construction. At first I thought that the reason of this is difference between recursive and infuctive definitions? However, Wikipedia says that they are the same things, so I am confused right now. However, it can be the case that infinite lists may be members of such inductive types only in Haskell, and not in a real type theory (for which first definition of natural numbers were proposed). Where is a mistake in my reasoning?

Thank you!

p. s.

It seems that the best reading for this topic is this essay by Veronica Gaspes

update:

As it turns out it can be proved for $\mathbb{N}$ by primitive recursion that $1 \neq 0$, and then by mathematical induction that $\forall n \in \mathbb{N} . n \neq \infty$ where $\infty$ is defined by recursive relation $\infty = S(\infty) $. So we can prove with very basic machinery that $\infty \not \in \mathbb{N}$. On the other hand, there is another monster: a sequence of infinities such that $\infty : \mathbb{N} \to \mathbb{N}$, $\infty(S(n)) = S(\infty(n))$. Basically, an infinite decreasing sequence of natural numbers. Proving that it doesn't exists will be equivalent to statement that every subset of naturals has least element which in its turn will be equivalent to the law of excluded middle. So now I can see three solutions:

  1. Strict Constructivism: condemn both $\infty$ and $\infty(n)$ to be non-constructive. So hopefully we will have $\mathbb{N} \cong \mathbb{N}'$. As price we will also ban infinite list and some other coinductive constructions or at least will have to redefine them in more complex way.
  2. Classical Approach: Accept law of excluded middle. Then we can prove that $\infty(n)$ is not a member of $\mathbb{N}$. However we still will have to prove properties of $\mathbb{N}'$. It's properties will depend on how we define properties of $\times$ product in definition of $\mathbb{N}'$
  3. Nonproductive numbers: Accept existence of $\infty(n)$ as an axiom. Which will make induction behave weird.
$\endgroup$
  • $\begingroup$ There are no infinite natural numbers; if you represent a number as a list of strokes (or units), then every list "produced" by the definition must be finite. $\endgroup$ – Mauro ALLEGRANZA Mar 8 '16 at 16:48
  • $\begingroup$ I understand this fact. Intuitively this is correct. However, if that definition "verify" structures instead of "producing" them then recursive object $\infty = (1,\infty)$ can not be verified by proposed definition. So my question was more about when 'generating type' theory turns into 'verifying' Type theory, or how infinite lists can coexist with natural numbers in the same type theoretic framework. $\endgroup$ – Nik Pronko Mar 8 '16 at 17:02
  • 1
    $\begingroup$ The standard definition of list types does not admit infinite lists. It seems to me that you are confusing inductive data structures with coinductive data structures. $\endgroup$ – Zhen Lin Mar 9 '16 at 8:35
  • $\begingroup$ Thank you. I will look up coinductive data structures $\endgroup$ – Nik Pronko Mar 9 '16 at 10:16
  • 1
    $\begingroup$ @ZhenLin To be fair, in Haskell they are the same thing. $\endgroup$ – gallais Mar 9 '16 at 12:24
1
$\begingroup$

I think that issue in your reasoning is in assuming that when you define a type of lists $L(T)$ by $L(T) = ()|(T \times L(T))$, that this somehow captures the inductive construction of finite lists, As you noticed, it does not. This construction in Haskell is not the same as the construction of an inductively defined set in mathematical foundations.

We do have an inductive definition for the naturals: a natural number is either 0, or is S followed by a natural number. We can write this in Backus-Naur form as a grammar:

< N > := 0 | "S" < N >

But, when this is read as an inductive definition, it says that an object matches on the left side if and only if there is a finite sequence of applications of the grammar - a finite parse tree - to verify it. The definition of "inductive definition" includes this finiteness requirement. So the inductive definition does not give the full type $L(T)$ from above - only some elements of that type meet the inductive definition, namely the ones that have a finite parse tree.

The essay by Veronica Gaspes uses terminology in a (mathematically) nonstandard way. There are no "infinite natural numbers" like her infty on page 3. Of course, the discussion of lazy evaluation in Haskell is fine, and infty is a fine object of a certain type. But it does not seriously imply that infty is a natural number. (Similarly, NaN is a legal value for a floating point number, but this does not make NaN a real number.)

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.