28
$\begingroup$

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.

|cite|improve this question|||||
$\endgroup$
  • $\begingroup$ I guess this is not a research level question, although an interesting one. $\endgroup$ – Raphael Dec 13 '10 at 20:53
  • 4
    $\begingroup$ It's not, but it's a kind of big-picture question, which we do accept. $\endgroup$ – Suresh Venkat Dec 14 '10 at 0:38
  • 1
    $\begingroup$ 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. $\endgroup$ – Richard Cook Dec 16 '10 at 22:45
  • $\begingroup$ I do not understand your UPD. Naturals are more fundamental than integers, and the answers give examples of why this is the case. $\endgroup$ – Radu GRIGore Dec 17 '10 at 0:00
  • $\begingroup$ 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. $\endgroup$ – Marc Hamann Dec 18 '10 at 18:45
24
$\begingroup$

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.

|cite|improve this answer|||||
$\endgroup$
20
$\begingroup$

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.

|cite|improve this answer|||||
$\endgroup$
  • 5
    $\begingroup$ 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. $\endgroup$ – Per Vognsen Dec 14 '10 at 0:57
  • $\begingroup$ @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. ;-) $\endgroup$ – Marc Hamann Dec 18 '10 at 18:51
  • $\begingroup$ 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. $\endgroup$ – Tegiri Nenashi Jan 13 '11 at 0:53
  • $\begingroup$ 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. $\endgroup$ – Marc Hamann Jan 13 '11 at 13:46
17
$\begingroup$

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.

|cite|improve this answer|||||
$\endgroup$
11
$\begingroup$

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

|cite|improve this answer|||||
$\endgroup$
  • $\begingroup$ There are languages which have a basic type for naturals, you know. $\endgroup$ – Raphael Nov 20 '11 at 17:24
  • $\begingroup$ @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. $\endgroup$ – Jacques Carette Nov 20 '11 at 17:31
  • $\begingroup$ What is so bad about quotients? $\endgroup$ – David Harris Nov 20 '11 at 22:28
  • 3
    $\begingroup$ 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'. $\endgroup$ – Jacques Carette Nov 21 '11 at 1:49
  • 2
    $\begingroup$ 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. $\endgroup$ – cody Mar 20 '12 at 13:43
7
$\begingroup$

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, David Schmidt, Bob Tennent and John Reynolds 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.

|cite|improve this answer|||||
$\endgroup$
6
$\begingroup$

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.

|cite|improve this answer|||||
$\endgroup$
  • $\begingroup$ 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! $\endgroup$ – Artem Pelenitsyn Dec 14 '10 at 8:17

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.