Pourquoi les naturels au lieu des entiers?

28

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.

Artem Pelenitsyn
la source
Je suppose que ce n'est pas une question de niveau de recherche, bien que intéressante.
Raphael
4
Ce n'est pas le cas, mais c'est une sorte de question d'ensemble que nous acceptons.
Suresh Venkat
1
Je me demande si en quelque sorte l'ensemble des entiers non négatifs pourrait être encore plus fondamental que les nombres naturels en raison des propriétés uniques de la valeur 0 qui n'existe pas dans ce dernier. Je suggérerais également que cela est plus valable comme choix du type numérique fondamental pour les ordinateurs numériques étant donné l'importance de 0.
Richard Cook
Je ne comprends pas votre UPD . Les naturels sont plus fondamentaux que les entiers, et les réponses donnent des exemples de la raison pour laquelle c'est le cas.
Radu GRIGore
Re: UPD. Je ne sais pas trop pourquoi les "gens de l'industrie" seraient "déçus". (J'ai moi-même passé ma carrière dans l'industrie.) Pourquoi devrait-on s'attendre à ce que la théorie soit une extension évidente de ce qu'elle connaît déjà? Il est assez courant que certaines choses courantes dans l'industrie, tout comme les variables entières, existent davantage pour des "raisons historiques" que pour des raisons théoriques profondes.
Marc Hamann

Réponses:

24

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.

Neel Krishnaswami
la source
20

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.

Marc Hamann
la source
5
Une autre raison: si vous voulez quelque chose comme des chiffres d'église, un entier négatif devrait dénoter l'inversion de fonction. Ainsi, dans ce contexte, les entiers seraient plus naturels dans un calcul de fonctions bijectivement calculables.
Par Vognsen
@Per Vognsen: vous ne savez pas de quelle manière vous vous disputez. Mais je pense qu'il est sûr de dire que les fonctions bijectivement calculables sont moins fondamentales que les fonctions calculables arbitraires la plupart du temps. ;-)
Marc Hamann
Il ne fait aucun doute que les nombres complexes, qui sont au sommet de la hiérarchie des nombres Nombres naturels -> Entiers -> Nombres rationnels -> Nombres réels -> Nombres complexes sont plus fondamentaux que les autres, car ils ont des propriétés algébriques "plus belles". Ils sont partout dans la science, mais sont visiblement absents dans les "fondements" des mathématiques. Donc, la réponse à ce qui est des entiers ou des naturels plus "fondamentaux" dépend vraiment de qui vous demandez: algorithmiste ou algébrique.
Tegiri Nenashi
Comme il s'agit d'un site TCS, je pense que nous pouvons privilégier la vue de l'informatique en toute sécurité. ;-) Sur le plan du calcul, cette hiérarchie est progressive: chaque nouvelle entrée est littéralement construite sur la précédente. Étant donné que "fondamental" se réfère généralement à quelque chose à la base, je pense que la fin naturelle est la bonne pour conférer ce titre.
Marc Hamann
17

NZ

NZ

Raphael
la source
11

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.

Jacques Carette
la source
Il y a des langues qui ont un type de base pour les naturels, vous savez.
Raphael
@Raphael: Je sais. Mais pas ceux que j'aime autrement (à savoir Haskell et OCaml). Je ne suis pas tout à fait prêt à commencer la «programmation» dans Agda ou Coq.
Jacques Carette
Qu'est-ce qui est si mauvais avec les quotients?
David Harris
3
Les quotients sont excellents dans la sémantique. Ils sont beaucoup, beaucoup plus difficiles à gérer dans les calculs réels et dans les représentations concrètes. Il existe d'innombrables articles sur la façon de les traiter dans Coq, Isabelle, Agda (théorie des types en général), etc.
Jacques Carette
2
J'ai l'impression que c'est la réponse la plus forte du groupe: les produits naturels sont le type de données inductif non trivial le plus simple. une fois que vous avez donné une définition et prouvé des propriétés simples pour les nombres naturels, vous avez ouvert la voie à des types de données inductifs plus complexes, comme des listes ou des arbres.
cody
7

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.

Uday Reddy
la source
6

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.

Dave Clarke
la source
Je voulais d'abord dire le calcul lambda tapé. Le cours des livres que j'ai mentionnés dans le post supérieur est basé sur cela. Je suppose que le lambda non typé n'est pas si vital dans la théorie des types et la théorie de PL de nos jours (je me trompe peut-être, mais c'est ce que je vois dans ces livres). En tout cas merci!
Artem Pelenitsyn