<p>Naturals are a much more fundamental concept than the integers.</p>

<p>Induction occurs over the naturals and the integers can be derived from the naturals with the simple addition of a unary inverse operator.</p>

<p>I would actual want to ask the reverse question:  why did early programming language (and register machine) designers enshrine integers as the basic data type when they are so secondary and so easily derived from naturals?  </p>

<p>I suspect it is just because there were some cool binary encodings that could handle integers elegantly. ;-)</p>

<p>Think how often you want to ignore the negative range of a programmatic integer, and consider the impulse to have an unsigned integer type to recover the lost bit.</p>

CC BY-SA 2.5
2010-12-14T00:57:44.147Z
Another reason: if you want something like Church numerals, a negative integer would have to denote function inversion. So in that context integers would be more natural in a calculus of computably bijective functions.
Per Vognsen
CC BY-SA 2.5
2010-12-18T18:51:59.203Z
@Per Vognsen: not sure which way you are arguing there.  But I think it is safe to say that the computably bijective functions are less fundamental than arbitrary computable functions most of the time. ;-)
Marc Hamann
CC BY-SA 2.5
2011-01-13T00:53:25.120Z
There is no question that complex numbers, which are at the top of number hierarchy Natural Numbers -> Integers -> Rational Numbers -> Real Numbers -> Complex Numbers are more fundamental than the others, because they have "nicer" algebraic properties. They are everywhere in science, but are conspicuously absent in "foundations" of math. So the answer to what is more "fundamental" integers or naturals really depends whom you ask: algorithmist or algebraist.
Tegiri Nenashi
CC BY-SA 2.5
2011-01-13T13:46:05.607Z
Since this is a TCS site, I think we are safe in privileging the view of computer science. ;-)  Computationally, that hierarchy is progressive: each new entry is literally built upon the previous one.  Since "fundamental" usually refers to something at the base, I think the naturals end is the right one to confer that title upon.
Marc Hamann
CC BY-SA 2.5
2010-12-13T19:24:35.590Z
2010-12-13T19:24:35.590Z
Marc Hamann
<p>There exists a computable bijection between $\mathbb{N}$ and $\mathbb{Z}$. Therefore it is sufficient to reason about computability and the like only using natural numbers, all the time knowing that your results generalize to integers (and rational numbers, and all other recursively enumerable sets).</p>

<p>Reasoning only on naturals is convenient because you have induction and $\mathbb{N}$ is a well-founded set with the natural order $\leq$. The latter one is especially important since it can be instrumentalized in termination proofs. While you can define a well-founded order on $\mathbb{Z}$, it is less convenient because it does not match the usual order.</p>

CC BY-SA 3.0
2010-12-13T20:51:25.637Z
2012-03-20T13:24:24.193Z
2012-03-20T13:24:24.193Z
Raphael
<p>Yet another reason (related to the ones already given, but this answer does add new information) is that there is a very simple, quotient-free construction of the naturals, which comes along with a nice induction principle [as has already been said].  What has not been expanded upon is <a href="https://mathoverflow.net/questions/29090/direct-construction-of-the-integers">how difficult</a> it is to come up with a quotient-free construction of the integers.</p>

<p>The more programming I do where I want high assurance, the more I need the naturals, and I find having only the integers pre-defined for me a real pain.</p>

CC BY-SA 3.0
2011-11-20T17:24:52.000Z
There are languages which have a basic type for naturals, you know.
Raphael
CC BY-SA 3.0
2011-11-20T17:31:50.410Z
@Raphael: I know.  But not the ones I otherwise like (namely Haskell and OCaml).  I am not quite ready to start 'programming' in Agda or Coq.
Jacques Carette
CC BY-SA 3.0
2011-11-20T22:28:01.877Z
What is so bad about quotients?
David Harris
CC BY-SA 3.0
2011-11-21T01:49:57.617Z
Quotients are great in the semantics.  They are much, much harder to deal with in actual computations and in concrete representations.  There are countless papers on how to deal with them in Coq, Isabelle, Agda, (type theory in general), etc.  I just assumed it was folklore knowledge in all communities that quotients are just a pain to deal with 'in reality'.
Jacques Carette
CC BY-SA 3.0
2012-03-20T13:43:57.547Z
I feel like this is the strongest answer of the bunch: Naturals are the simplest non-trivial inductive datatype. once you have given definition and proved simple properties for natural numbers, you've paved the way for more complex inductive data types, like lists or trees.
cody
CC BY-SA 3.0
2013-01-24T17:55:21.587Z
@cody: I voted your comment up because I couldn't vote this answer up twice.
Neil Toronto
CC BY-SA 3.0
2011-11-20T15:05:52.993Z
2011-11-20T15:05:52.993Z
2017-04-13T12:57:54.777Z
Jacques Carette
<p><em>Are there any good reasons why PL theorists prefer naturals instead of integers?</em> There are some, but in a text book on programming language semantics, I think there is no technical reason why they need to.  I can't think of any place other than dependent type systems, where induction on data is important in PL theory.  Other text books by <a href="http://books.google.co.uk/books?id=_QAnAAAAMAAJ" rel="nofollow">Mike Gordon</a>, <a href="http://books.google.co.uk/books?id=bWMZAQAAIAAJ" rel="nofollow">David Schmidt</a>, <a href="http://books.google.co.uk/books?id=K7N7QgAACAAJ" rel="nofollow">Bob Tennent</a> and <a href="http://books.google.co.uk/books?id=2OwlTC4SOccC" rel="nofollow">John Reynolds</a> don't do it.  (And, those books would probably be a lot more suitable for teaching people that care about general-purpose industrial PLs!)  </p>

<p>So, there, you have the proof that it is <em>not</em> necessary.  In fact, I would claim that a good PL theory text book should be <em>parametric</em> in the primitive types of the programming language, and it is misleading to suggest otherwise.</p>

CC BY-SA 3.0
2012-03-21T08:28:23.780Z
2013-01-24T12:22:21.960Z
2013-01-24T12:22:21.960Z
Uday Reddy
<p>Naturals and bools and operations on them can be encoded in the pure lambda calculus in a straightforward manner, as so-called Church numerals (and Church bools, I guess). It is not clear how one would encode integers nicely, though it can obviously be done.</p>

CC BY-SA 2.5
2010-12-14T08:17:49.080Z
I meant first of all typed lambda calculus. The course of the books I mentioned in top post is based on it. I guess untyped lambda not so vital in type theory and PL's theory nowadays (I may be wrong but that's what I see in those books.). Anyway thank you!
Artem Pelenitsyn
CC BY-SA 2.5
2010-12-14T07:56:41.810Z
2010-12-14T07:56:41.810Z
Dave Clarke
<p>Short answer: the naturals are the first limit ordinals. Hence they play a central role in axiomatic set theory (eg, the axiom of infinity is the assertion they exist) and logic, and PL theorists tend to share foundational preoccupations with logicians. We want to have access to the principle of induction to prove total correctness, termination, and similar properties, and the naturals are an (er) natural choice of well-order. </p>

<p>I don't want to imply that finite-width binary integers are any less cool objects, though. They are representations of the p-adics, and permit us to use power series methods in number theory and combinatorics. This means that their significance becomes more visible in algorithmics than PL, since this is when we start caring more about complexity rather than termination. </p>

CC BY-SA 2.5
2010-12-14T12:48:57.470Z
2010-12-14T12:48:57.470Z
Neel Krishnaswami
<p>I'm interested in why natural numbers are so beloved by the authors of books on programming languages theory and type theory (e.g. J. Mitchell, Foundations for programming languages and B. Pierce, Types and Programming Languages). Description of the simply-typed lambda-calculus and in particular PCF programming language are usually based on Nat's and Bool's. For the people using and teaching general-purpose industrial PL's it is great deal more natural to treat integers instead of naturals. Can you mention some good reasons why PL theorist prefer nat's? Besides that it is a little less complicated. Are there any fundamental reasons or is it just an honour the tradition?</p>

<p><strong>UPD</strong> For all those comments about “fundamentality” of naturals: I'm a quite aware about all those cool things, but I'd rather prefer to see an example when it is really vital to have those properties in type theory of PL's theory. E.g. widely mentioned induction. When we have any sort of logic (which simply typed LC is), like basic first-order logic, we do really use induction — but induction on derivation tree (which we also have in lambda).</p>

<p>My question basically comes from people from industry, who wants to gain some fundamental theory of programming languages. They used to have integers in their programs and without concrete arguments and applications to the theory being studied (type theory in our case) why to study languages with only nat's, they feel quite disappointed.</p>

CC BY-SA 3.0
2011-11-22T09:49:29.477Z
To paraphrase Kronecker: God made the Axiom of Induction; all the rest is the work of man.
Jeffε
CC BY-SA 3.0
2014-03-26T00:04:17.200Z
@RichardCook: naturals do include zero in virtually all computer science presentations, including the textbooks referenced here (IIRC). See http://en.wikipedia.org/wiki/Natural_number#History_of_natural_numbers_and_the_status_of_zero
Blaisorblade
CC BY-SA 2.5
2010-12-13T20:53:01.737Z
I guess this is not a research level question, although an interesting one.
Raphael
CC BY-SA 2.5
2010-12-14T00:38:47.467Z
It's not, but it's a kind of big-picture question, which we do accept.
Suresh Venkat
CC BY-SA 2.5
2010-12-16T22:45:44.780Z
I'm wondering if in some way the set of non-negative integers might be even more fundamental than natural numbers due to the unique properties of the 0-value that does not exist in the latter. I would also suggest that this is more valid as the choice of fundamental numeric type for digital computers given the importance of 0.
Richard Cook
CC BY-SA 2.5
2010-12-17T00:00:11.310Z
I do not understand your **UPD**. Naturals are more fundamental than integers, and the answers give examples of why this is the case.
Radu GRIGore
CC BY-SA 2.5
2010-12-18T18:45:07.027Z
Re: UPD.  I'm not too sure why "people from industry" would be "disappointed". (I've spent my career in industry myself.)  Why should anyone expect that theory ought to be an obvious extension of what they are already familiar with? It is quite common that certain things common in industry, much like integer variables, are there more for "historical reasons" than for deep theoretical ones.
Marc Hamann
CC BY-SA 2.5
2010-12-30T14:45:36.307Z
Naturals are simpler. I am afraid that "fundamentality" is the right answer here. You are like complaining about gravity because you were hurt and disappointed when fell on the earth.
beroal
<pl.programming-languages><big-picture><type-theory>
Why naturals instead of integers?
Artem Pelenitsyn
# Why naturals instead of integers?

(Asked by: username_0 on 2010-12-13)

I'm interested in why natural numbers are so beloved by the authors of books on programming languages theory and type theory (e.g. J. Mitchell, Foundations for programming languages and B. Pierce, Types and Programming Languages). Description of the simply-typed lambda-calculus and in particular PCF programming language are usually based on Nat's and Bool's. For the people using and teaching general-purpose industrial PL's it is great deal more natural to treat integers instead of naturals. Can you mention some good reasons why PL theorist prefer nat's? Besides that it is a little less complicated. Are there any fundamental reasons or is it just an honour the tradition?

**UPD** For all those comments about “fundamentality” of naturals: I'm a quite aware about all those cool things, but I'd rather prefer to see an example when it is really vital to have those properties in type theory of PL's theory. E.g. widely mentioned induction. When we have any sort of logic (which simply typed LC is), like basic first-order logic, we do really use induction — but induction on derivation tree (which we also have in lambda).

My question basically comes from people from industry, who wants to gain some fundamental theory of programming languages. They used to have integers in their programs and without concrete arguments and applications to the theory being studied (type theory in our case) why to study languages with only nat's, they feel quite disappointed.

**Tags:** pl.programming-languages, big-picture, type-theory

> **Comments:**
> **username_3**: I guess this is not a research level question, although an interesting one.  
> **username_4**: It's not, but it's a kind of big-picture question, which we do accept.  
> **username_5**: I'm wondering if in some way the set of non-negative integers might be even more fundamental than natural numbers due to the unique properties of the 0-value that does not exist in the latter. I would also suggest that this is more valid as the choice of fundamental numeric type for digital computers given the importance of 0.  
> **username_6**: I do not understand your **UPD**. Naturals are more fundamental than integers, and the answers give examples of why this is the case.  
> **username_7**: Re: UPD.  I'm not too sure why "people from industry" would be "disappointed". (I've spent my career in industry myself.)  Why should anyone expect that theory ought to be an obvious extension of what they are already familiar with? It is quite common that certain things common in industry, much like integer variables, are there more for "historical reasons" than for deep theoretical ones.  
> **username_8**: Naturals are simpler. I am afraid that "fundamentality" is the right answer here. You are like complaining about gravity because you were hurt and disappointed when fell on the earth.  
> **username_1**: To paraphrase Kronecker: God made the Axiom of Induction; all the rest is the work of man.  
> **username_2**: @RichardCook: naturals do include zero in virtually all computer science presentations, including the textbooks referenced here (IIRC). See http://en.wikipedia.org/wiki/Natural_number#History_of_natural_numbers_and_the_status_of_zero  

---

## 6 answers

### Answer by username_17 on 2010-12-14. Score: 26 | Accepted answer

Short answer: the naturals are the first limit ordinals. Hence they play a central role in axiomatic set theory (eg, the axiom of infinity is the assertion they exist) and logic, and PL theorists tend to share foundational preoccupations with logicians. We want to have access to the principle of induction to prove total correctness, termination, and similar properties, and the naturals are an (er) natural choice of well-order.

I don't want to imply that finite-width binary integers are any less cool objects, though. They are representations of the p-adics, and permit us to use power series methods in number theory and combinatorics. This means that their significance becomes more visible in algorithmics than PL, since this is when we start caring more about complexity rather than termination.


---

### Answer by username_7 on 2010-12-13. Score: 22

Naturals are a much more fundamental concept than the integers.

Induction occurs over the naturals and the integers can be derived from the naturals with the simple addition of a unary inverse operator.

I would actual want to ask the reverse question: why did early programming language (and register machine) designers enshrine integers as the basic data type when they are so secondary and so easily derived from naturals?

I suspect it is just because there were some cool binary encodings that could handle integers elegantly. ;-)

Think how often you want to ignore the negative range of a programmatic integer, and consider the impulse to have an unsigned integer type to recover the lost bit.

> **Comments:**
> **username_9**: Another reason: if you want something like Church numerals, a negative integer would have to denote function inversion. So in that context integers would be more natural in a calculus of computably bijective functions.  
> **username_7**: @username_9: not sure which way you are arguing there.  But I think it is safe to say that the computably bijective functions are less fundamental than arbitrary computable functions most of the time. ;-)  
> **username_10**: There is no question that complex numbers, which are at the top of number hierarchy Natural Numbers -> Integers -> Rational Numbers -> Real Numbers -> Complex Numbers are more fundamental than the others, because they have "nicer" algebraic properties. They are everywhere in science, but are conspicuously absent in "foundations" of math. So the answer to what is more "fundamental" integers or naturals really depends whom you ask: algorithmist or algebraist.  
> **username_7**: Since this is a TCS site, I think we are safe in privileging the view of computer science. ;-)  Computationally, that hierarchy is progressive: each new entry is literally built upon the previous one.  Since "fundamental" usually refers to something at the base, I think the naturals end is the right one to confer that title upon.  

---

### Answer by username_3 on 2010-12-13. Score: 18

There exists a computable bijection between $\mathbb{N}$ and $\mathbb{Z}$. Therefore it is sufficient to reason about computability and the like only using natural numbers, all the time knowing that your results generalize to integers (and rational numbers, and all other recursively enumerable sets).

Reasoning only on naturals is convenient because you have induction and $\mathbb{N}$ is a well-founded set with the natural order $\leq$. The latter one is especially important since it can be instrumentalized in termination proofs. While you can define a well-founded order on $\mathbb{Z}$, it is less convenient because it does not match the usual order.


---

### Answer by username_11 on 2011-11-20. Score: 14

Yet another reason (related to the ones already given, but this answer does add new information) is that there is a very simple, quotient-free construction of the naturals, which comes along with a nice induction principle [as has already been said]. What has not been expanded upon is [how difficult](https://mathoverflow.net/questions/29090/direct-construction-of-the-integers) it is to come up with a quotient-free construction of the integers.

The more programming I do where I want high assurance, the more I need the naturals, and I find having only the integers pre-defined for me a real pain.

> **Comments:**
> **username_3**: There are languages which have a basic type for naturals, you know.  
> **username_11**: @username_3: I know.  But not the ones I otherwise like (namely Haskell and OCaml).  I am not quite ready to start 'programming' in Agda or Coq.  
> **username_12**: What is so bad about quotients?  
> **username_11**: Quotients are great in the semantics.  They are much, much harder to deal with in actual computations and in concrete representations.  There are countless papers on how to deal with them in Coq, Isabelle, Agda, (type theory in general), etc.  I just assumed it was folklore knowledge in all communities that quotients are just a pain to deal with 'in reality'.  
> **username_13**: I feel like this is the strongest answer of the bunch: Naturals are the simplest non-trivial inductive datatype. once you have given definition and proved simple properties for natural numbers, you've paved the way for more complex inductive data types, like lists or trees.  
> **username_14**: @username_13: I voted your comment up because I couldn't vote this answer up twice.  

---

### Answer by username_15 on 2012-03-21. Score: 7

*Are there any good reasons why PL theorists prefer naturals instead of integers?* There are some, but in a text book on programming language semantics, I think there is no technical reason why they need to. I can't think of any place other than dependent type systems, where induction on data is important in PL theory. Other text books by [Mike Gordon](http://books.google.co.uk/books?id=_QAnAAAAMAAJ), [David Schmidt](http://books.google.co.uk/books?id=bWMZAQAAIAAJ), [Bob Tennent](http://books.google.co.uk/books?id=K7N7QgAACAAJ) and [John Reynolds](http://books.google.co.uk/books?id=2OwlTC4SOccC) don't do it. (And, those books would probably be a lot more suitable for teaching people that care about general-purpose industrial PLs!)

So, there, you have the proof that it is *not* necessary. In fact, I would claim that a good PL theory text book should be *parametric* in the primitive types of the programming language, and it is misleading to suggest otherwise.


---

### Answer by username_16 on 2010-12-14. Score: 6

Naturals and bools and operations on them can be encoded in the pure lambda calculus in a straightforward manner, as so-called Church numerals (and Church bools, I guess). It is not clear how one would encode integers nicely, though it can obviously be done.

> **Comments:**
> **username_0**: I meant first of all typed lambda calculus. The course of the books I mentioned in top post is based on it. I guess untyped lambda not so vital in type theory and PL's theory nowadays (I may be wrong but that's what I see in those books.). Anyway thank you!  

---

