L'ordre des déclarations dans un type inductif est-il important?

9

Je me demandais si l'ordre des déclarations de type inductif pouvait avoir de l'importance.

Par exemple, dans Coq, vous pouvez définir Natsoit par:

Inductive Nat :=
  | O : Nat
  | S : Nat -> Nat.

ou

Inductive Nat :=
  | S : Nat -> Nat
  | O : Nat.

Cela changera peut-être l'ordre des paramètres dans l'éliminateur généré automatiquement, mais ce n'est pas un gros problème.

Je me demande s'il est possible d'écrire une déclaration comme

Inductive typewhereordermatters :=
  | cons1 : type1
  | cons2 : type2.

où type2est un type dépendant, selon cons1? (et dans ce cas, écrire les déclarations dans l'autre ordre n'aurait aucun sens, car type2se référer à cons1ce qui n'existe pas encore).

lo.logic type-theory coq dependent-type Guillaume Brunerie
la source

Réponses:

10

  1. L'ordre n'a pas d'importance. Je ne peux pas penser à un cas où cela se produirait. Comme Andrej Bauer le fait remarquer dans un commentaire, si vous changez l'ordre, le résultat est canoniquement isomorphe à l'original .

  2. Un cas ne peut pas dépendre d'un autre cas. Les éléments de la somme représentent un choix, il n'a donc pas de sens que le choix fait dépend d'un choix qui n'est pas fait.

Dave Clarke
la source
2
Vous pouvez être plus précis sur votre premier point. L'ordre n'a pas d'importance. Si vous changez l'ordre, le résultat est canoniquement isomorphe à l'original.
Andrej Bauer
2
@Dave: Merci! Je posais cette question à cause de (la théorie hautement expérimentale des) types inductifs supérieurs, où ce phénomène semble se produire , et je voulais savoir si cela peut également être le cas avec les types inductifs réguliers.
Guillaume Brunerie
1
@Guillaume: Je ne sais pas quel phénomène vous pointez avec le lien. Les différentes clauses constructeur d'une définition de type de données ne peuvent pas dépendre les unes des autres, qu'il s'agisse ou non d'un type de données d'ordre supérieur. Peut-être pensez-vous aux enregistrements dépendants (qui sont utilisés sur le lien et qui sont disponibles dans Agda et Coq )?
Noam Zeilberger
1
@Noam: Dans l'exemple du type inductif supérieur circle, le type du loopconstructeur dépend du baseconstructeur.
Guillaume Brunerie
2
@Guillaume: Je vois maintenant (ils introduisent une syntaxe expérimentale), je ne sais pas comment j'ai raté ça.
Noam Zeilberger
6

La commande est-elle importante dans la façon dont vous demandez? Non.

Mais l'ordre est-il complètement hors de propos pour le fonctionnement de l'assistant de preuve? Encore une fois, non. En Matita, un assistant de preuve très semblable à Coq, l'ordre dans lequel les constructeurs sont écrits dans une définition inductive ne soit pour le contrôle de type, en particulier lorsque le type de vérification d' une expression de correspondance.

Matita doit d'abord vérifier que tous les constructeurs sont mis en correspondance dans le corps du match. Pour ce faire, il parcourt les constructeurs dans l'ordre dans lequel ils sont déclarés. Ensuite, il s'agit de taper l'expression de correspondance appropriée, ce qui se produit dans l'ordre inverse, en vérifiant d'abord la casse pour le dernier constructeur déclaré. Ce type est ensuite effectué et utilisé pour vérifier les autres cas.

Cela apparaît très souvent lors de l'écriture d'une expression de correspondance importante. Vous souhaitez d'abord remplir les cas faciles, en laissant les cas plus difficiles sous un caractère générique, en vérifiant périodiquement ce que vous avez écrit pour vous assurer que cela a du sens. Parfois, Matita n'est pas en mesure de déduire le type de l'expression de correspondance incomplète, mais le fera très volontiers si vous remplissez le cas du dernier constructeur défini dans le type inductif.

Je suppose, bien que je ne sois pas certain, que Coq fasse quelque chose de similaire.

Dominic Mulligan
la source