Définitions constructives standard d'entiers, de rationnels et de réels?

Les nombres naturels sont définis par induction comme (en utilisant la syntaxe Coq comme exemple)

Inductive nat: Set :=
| O: nat
| S: nat -> nat.

Existe-t-il un moyen standard de définir les entiers (et peut-être d'autres ensembles comme les rationnels et les réels) de manière constructive?

Il existe plusieurs façons de définir une structure mathématique, selon les propriétés que vous considérez comme la définition. Entre les caractérisations équivalentes, celle que vous prenez pour la définition et celle que vous prenez pour une autre caractérisation n'est pas importante.

En mathématiques constructives, il est préférable de choisir une définition qui facilite le raisonnement constructif. Pour les nombres naturels, la forme de base du raisonnement est l'induction, ce qui rend la définition traditionnelle zéro ou successeur tout à fait appropriée. D'autres ensembles de nombres n'ont pas une telle préférence.

Lorsque l'on raisonne sur des quotients, dans des contextes non constructifs, il est courant de dire «choisir un membre de la classe d'équivalence». Dans un cadre constructif, il est nécessaire de décrire comment choisir un membre. Cela facilite l'utilisation de définitions qui construisent un objet pour chaque membre du type, plutôt que de construire des classes d'équivalence.

Par exemple, pour définir , un mathématicien pourrait être content d'assimiler les différences de nombres naturels: Bien que cela ait un sens ordonné (pas de "ceci ou cela"), pour un raisonnement constructif, c'est plus simple si l'égalité des objets coïncide avec l'égalité des représentations , nous pouvons donc définir les entiers relatifs comme un nombre naturel ou le négatif d'un nombre naturel moins un:$\mathbb{Z}$

Inductive Z1 :=
  | Nonnegative : nat -> Z1   (* ⟦Nonnegative x⟧ = ⟦x⟧ *)
  | Negative : nat -> Z1.     (* ⟦Negative x⟧ = -⟦x⟧-1 *)

Cependant, cette définition est étrangement asymétrique, ce qui peut rendre préférable d'admettre deux représentations différentes pour zéro:

Inductive Z2 :=
  | Nonnegative : nat -> Z2   (* ⟦Nonnegative x⟧ = ⟦x⟧ *)
  | Nonpositive : nat -> Z2.  (* ⟦Nonpostitive x⟧ = -⟦x⟧ *)

Ou nous pouvons construire les entiers relatifs sans utiliser les naturels comme bloc de construction:

Inductive Pos3 :=
  | I : Pos3                  (* ⟦I⟧ = 1 *)
  | S3 : Pos3 -> Pos3         (* ⟦S3 x⟧ = ⟦x⟧+1 *)
Inductive Z3 :=
  | N3 : Pos3 -> Z3           (* ⟦N3 x⟧ = -⟦x⟧ *)
  | O3 : Z3                   (* ⟦O3⟧ = 0 *)
  | P3 : Pos3 -> Z3           (* ⟦P3 x⟧ = ⟦x⟧ *)

Les utilisations de la bibliothèque standard Coq encore une autre définition: il construit des nombres entiers positifs de leur notation est la base 2, comme le chiffre 1 suivi d'une séquence de chiffres 0 ou 1. On construit alors Zcomme Z3à partir de Pos3ci - dessus. Cette définition a également une représentation unique pour chaque entier. Le choix d'utiliser la notation binaire n'est pas pour un raisonnement plus facile, mais pour produire un code plus efficace lorsque les programmes sont extraits des preuves.

La facilité de raisonnement est une motivation pour choisir une définition, mais ce n'est jamais un facteur insurmontable. Si une construction facilite une preuve particulière, on peut utiliser cette définition dans cette preuve particulière, et prouver que la construction est équivalente à l'autre construction qui a été choisie comme définition à l'origine.

$\mathbb{N}$Q$\mathbb{N} \times \mathbb{N}^*$=?=Q

Les nombres réels sont une toute autre marmite de poisson car ils ne sont pas constructibles. Il est impossible de définir les nombres réels comme un type inductif (tous les types inductifs sont dénombrables). Au lieu de cela, toute définition des nombres réels doit être axiomatique, c'est-à-dire non constructive. Il est possible de construire des sous-ensembles dénombrables des nombres réels; la façon de le faire dépend du sous-ensemble que vous souhaitez construire.

La réponse de Gilles est bonne, sauf pour le paragraphe sur les nombres réels, qui est complètement faux, sauf pour le fait que les nombres réels sont bien une autre marmite de poisson. Étant donné que ce type de désinformation semble être assez répandu, je voudrais enregistrer ici une réfutation détaillée.

Il n'est pas vrai que tous les types inductifs soient dénombrables. Par exemple, le type inductif

Inductive cow := 
   | nose : cow
   | horn : (nat -> cow) -> cow.

n'est pas dénombrable, car étant donné toute séquence que c : nat -> cownous pouvons former horn cqui n'est pas dans la séquence par le bien-fondé du bétail. Si vous voulez une déclaration correcte de la forme "tous les types inductifs sont dénombrables", vous devez limiter sévèrement les constructions autorisées.

Les nombres réels ne peuvent pas être facilement construits comme un type inductif, sauf que dans la théorie du type homotopique, ils peuvent être construits comme un type inductif-inductif supérieur , voir le chapitre 11 du livre HoTT . On pourrait dire que c'est de la triche.

Il y a un certain nombre de constructives définitions et constructions des réaux, contrairement à ce que Gilles. Ils peuvent être largement divisés en deux classes:

1. Constructions de type Cauchy dans lesquelles les réels sont vus comme un achèvement métrique des nombres rationnels. Ce type de construction nécessite souvent des quotients, même si l'on peut s'en tirer avec une définition coiunductive, selon la façon dont on traite l'égalité. Une construction naïve nécessite généralement un choix dénombrable également, mais Fred Richman a donné une procédure d'achèvement qui fonctionne de manière constructive sans choix, voir ses nombres réels et autres achèvements .

2. $\lambda$$\Sigma$

Du côté de l'implémentation, nous avons diverses formalisations constructives de réels (mais pas celle de la bibliothèque standard Coq qui est tout simplement horrible), par exemple Robbert Krebbers et Bas Spitters's Computer certifiés efficaces réels exacts dans Coq .

Pour une implémentation réelle de nombres réels exacts , je vous montre l' iRRAM de Norbert Müller .

$\mathbb{N} \to \mathbb{N}$