Qu'est-ce que l'induction-induction?

11

Qu'est-ce que l' induction-induction ?

Les ressources que j'ai trouvées sont:

Les deux premières références sont trop brèves pour moi et les deux dernières sont trop techniques. Quelqu'un peut-il l'expliquer en termes simples? Ce serait mieux s'il y avait du code Agda.

盛安安
la source
Il y a du code Agda dans votre quatrième citation.
Gilles 'SO- arrête d'être méchant'
Bien sûr, mais il serait très difficile de lire cette énorme quantité de code. Et (je suppose) super facile rien qu'en voyant 1 ou 2 exemples.
盛安安

Réponses:

13

Supplément 2016-10-03: J'ai mélangé induction-induction et induction-récursion (pas la première fois que je fais ça!). Mes excuses pour le désordre. J'ai mis à jour la réponse pour couvrir les deux.

Je trouve les explications dans l'article de Forsberg & Setzer Une axiomatisation finie des définitions inductives-inductives éclairantes.

Induction-récursivité

Une définition inductive-récursive est une définition dans laquelle nous définissons simultanément un type et une famille de types de manière spéciale:UNEB:UNEType

  1. UNE est défini comme un type inductif.
  2. B est défini par récurrence sur .UNE
  3. Fondamentalement, la définition de peut utiliser .UNEB

Sans la troisième condition, nous pourrions d' abord définir puis séparément .UNEB

Voici un exemple de bébé. Définissez inductive pour avoir les constructeurs suivants:UNE

  • une:UNE
  • :(X:UNEB(X))UNE

La famille de types est définie parB

  • B(une)=bool
  • B((X,F))=nunet .

Alors, qu'est-ce que dans ? Tout d'abord, nous avons un élément À cause de cela, il existe un type qui est défini comme étant . Par conséquent, nous pouvons former deux nouveaux éléments et dans . Nous avons maintenant , nous pouvons donc également former pour chaque les éléments et On peut continuer comme ça . La prochaine étape sera que depuis UNE

une:UNE.
B(une)bool
(une,Funelse)
(une,true)
UNEB((a,false))=B((a,true))=natn:nat
((a,false),n):A
((a,true),n):A
B(((a,true),n))=nat
il y a pour chaque l'élément et l'élément Nous pouvons continuer. Un peu de réflexion révèle que est plus ou moins deux copies de listes de nombres naturels, partageant une liste vide commune. Je vais le laisser comme un exercice pour comprendre pourquoi.m:nat
(((a,true),n),m):A
(((une,Funelse),n),m):UNE
UNE

Induction-induction

Une définition inductive-inductive définit également un type et simultanément une famille de types :UNEB:UNEType

  1. UNE est défini par induction
  2. BA est défini par induction, et il peut faire référence àUNE
  3. Crucialement, peut se référer à .UNEB

Il est important de comprendre la différence entre l'induction-récurrence et l'induction-induction. Dans induction récursion nous définissons en fournissant des équations de la forme où est un constructeur pour . Dans une définition inductif-inductif nous définissons en fournissant des constructeurs pour former les éléments de .B

B(c())=
c()UNEBB

Reformulons notre exemple précédent en induction-induction. Nous avons d'abord le tpye inductif :UNE

  • une:UNE
  • :(X:UNEB(X))UNE

La famille de types est définie par les constructeurs suivants:B

  • Tru:B(une)
  • Funel:B(une)
  • si et alorsX:UNEy:B(X)Zer:B((X,y))
  • si et et alors .X:UNEy:B(X)z:B((x,y))Suc(z):B((x,y))

Comme vous pouvez le voir, nous avons donné des règles pour générer les éléments de qui reviennent à dire que est (isomophique pour) les booléens, et est (isomorphe pour) les nombres naturels .BB(a)B((x,y))

Andrej Bauer
la source
pourquoi diable quelqu'un définir ce type de données D:
盛安安
7
Afin d'enseigner ce qu'est un type inductif-inductif. Je pourrais vous donner un exemple réel, à savoir un univers type, mais ce serait déroutant.
Andrej Bauer
3
@AndrejBauer Cela ressemble plus à une récurrence-induction pour moi. L'induction-induction est lorsque la famille de types est définie comme un type inductif .
gallais
2
Oups, vous avez absolument raison. Je le réparerai.
Andrej Bauer du
Le domaine de censé être un type Sigma au lieu d'un type Pi?
Dan Christensen