Pourquoi les naturels au lieu des entiers?

Je m'intéresse aux raisons pour lesquelles les nombres naturels sont si appréciés par les auteurs de livres sur la théorie des langages de programmation et la théorie des types (par exemple J. Mitchell, Foundations for Programming Languages ​​et B. Pierce, Types and Programming Languages). La description du lambda-calcul simplement tapé et en particulier du langage de programmation PCF est généralement basée sur Nat et Bool. Pour les personnes qui utilisent et enseignent des PL industriels à usage général, il est beaucoup plus naturel de traiter les entiers plutôt que les naturels. Pouvez-vous mentionner quelques bonnes raisons pour lesquelles le théoricien du PL préfère les nat? En plus c'est un peu moins compliqué. Y a-t-il des raisons fondamentales ou est-ce juste un honneur pour la tradition?

UPD Pour tous ces commentaires sur la «fondamentalité» des naturels: je suis très conscient de toutes ces choses cool, mais je préfère plutôt voir un exemple quand il est vraiment vital d'avoir ces propriétés dans la théorie des types de la théorie de PL. Par exemple, l'induction largement mentionnée. Lorsque nous avons une sorte de logique (qui est simplement de type LC), comme la logique de premier ordre de base, nous utilisons vraiment l'induction - mais l'induction sur l'arbre de dérivation (que nous avons également dans lambda).

Ma question vient essentiellement des gens de l'industrie, qui veulent acquérir une théorie fondamentale des langages de programmation. Ils avaient l'habitude d'avoir des entiers dans leurs programmes et sans arguments concrets et applications à la théorie étudiée (théorie des types dans notre cas) pourquoi étudier les langues avec seulement des nat, ils se sentent assez déçus.

Réponse courte: les naturels sont les premiers ordinaux limites. Par conséquent, ils jouent un rôle central dans la théorie des ensembles axiomatiques (par exemple, l'axiome de l'infini est l'affirmation qu'ils existent) et la logique, et les théoriciens PL ont tendance à partager les préoccupations fondamentales avec les logiciens. Nous voulons avoir accès au principe de l'induction pour prouver l'exactitude totale, la terminaison et les propriétés similaires, et les naturels sont un choix (plus) naturel de bon ordre.

Je ne veux pas impliquer que les entiers binaires de largeur finie sont des objets moins cool, cependant. Ce sont des représentations des p-adiques, et nous permettent d'utiliser des méthodes de séries de puissance en théorie des nombres et en combinatoire. Cela signifie que leur signification devient plus visible en algorithmique que PL, car c'est à ce moment que nous commençons à nous préoccuper davantage de la complexité plutôt que de la terminaison.

Les naturels sont un concept beaucoup plus fondamental que les entiers.

L'induction se produit sur les naturels et les entiers peuvent être dérivés des naturels avec la simple addition d'un opérateur inverse unaire.

Je voudrais en fait poser la question inverse: pourquoi les premiers concepteurs de langage de programmation (et de machine à registre) ont-ils consacré des entiers comme type de données de base alors qu'ils sont si secondaires et si facilement dérivés des naturels?

Je soupçonne que c'est simplement parce qu'il y avait des encodages binaires sympas qui pouvaient gérer les entiers avec élégance. ;-)

Pensez à la fréquence à laquelle vous souhaitez ignorer la plage négative d'un entier programmatique et considérez l'impulsion d'avoir un type entier non signé pour récupérer le bit perdu.

$\mathbb{N}$$\mathbb{Z}$

$\mathbb{N}$$\leq$$\mathbb{Z}$

Encore une autre raison (liée à celles déjà données, mais cette réponse ajoute de nouvelles informations) est qu'il existe une construction très simple et sans quotient des naturels, qui s'accompagne d'un joli principe d'induction [comme cela a déjà été dit] . Ce qui n'a pas été développé, c'est la difficulté de trouver une construction sans quotient des entiers.

Plus je fais de programmation là où je veux une assurance élevée, plus j'ai besoin de produits naturels et je trouve que le fait d'avoir uniquement les nombres entiers prédéfinis me fait vraiment mal.

Y a-t-il de bonnes raisons pour lesquelles les théoriciens du PL préfèrent les naturels au lieu des entiers? Il y en a, mais dans un manuel sur la sémantique des langages de programmation, je pense qu'il n'y a aucune raison technique pour qu'ils en aient besoin. Je ne peux penser à aucun autre endroit que les systèmes de type dépendants, où l'induction sur les données est importante dans la théorie PL. D'autres manuels de Mike Gordon , David Schmidt , Bob Tennent et John Reynolds ne le font pas. (Et, ces livres seraient probablement beaucoup plus appropriés pour enseigner aux gens qui se soucient des PL industriels à usage général!)

Alors là, vous avez la preuve que ce n'est pas nécessaire. En fait, je dirais qu'un bon livre de théorie de PL devrait être paramétrique dans les types primitifs du langage de programmation, et il est trompeur de suggérer le contraire.

Les naturels et les bools et les opérations sur ceux-ci peuvent être encodés dans le calcul lambda pur de manière simple, en tant que soi-disant chiffres de l'Église (et Church bools, je suppose). Il n'est pas clair comment on pourrait coder les entiers correctement, bien que cela puisse évidemment être fait.