Induction structurelle
![Si ce bandeau n'est plus pertinent, retirez-le. Cliquez ici pour en savoir plus.](http://upload.wikimedia.org/wikipedia/commons/thumb/3/38/Info_Simple.svg/12px-Info_Simple.svg.png)
![](http://upload.wikimedia.org/wikipedia/commons/thumb/a/a1/2017-fr.wp-orange-source.svg/45px-2017-fr.wp-orange-source.svg.png)
Certaines informations figurant dans cet article ou cette section devraient être mieux reliées aux sources mentionnées dans les sections « Bibliographie », « Sources » ou « Liens externes » ().
Vous pouvez améliorer la vérifiabilité en associant ces informations à des références à l'aide d'appels de notes.
En mathématiques et davantage en informatique, la définition récursive ou induction structurelle est un procédé de définition conjointe d'un type (classe ou ensemble) et d'objets (éléments) qui le compose au moyen de règles de construction (constructeurs) qui agencent ou structurent ces objets.
L'on peut ainsi définir des nombres, des listes, des arbres, des relations, et plus généralement, toute structure mathématique (langage, système, …). En permettant par le même principe de définir un prédicat total[pas clair] i.e. qui est défini partout, l'induction structurelle est aussi une méthode de démonstration d'une propriété sur une structure.
Outils mathématiques et informatiques
Les système, langages et logiciels supportant à des degrés divers cette fonctionnalité sont nombreux.
![](http://upload.wikimedia.org/wikipedia/commons/thumb/8/87/Fairytale_warning.png/17px-Fairytale_warning.png)
L'un des plus puissants est le calcul des constructions inductives (CIC) et son logiciel Coq.
![](http://upload.wikimedia.org/wikipedia/commons/thumb/8/87/Fairytale_warning.png/17px-Fairytale_warning.png)
Caractéristiques
![](http://upload.wikimedia.org/wikipedia/commons/thumb/b/bf/Circle-icons-easel.svg/17px-Circle-icons-easel.svg.png)
La définition récursives se distingue de la "macro" et de la définition algébrique en cela qu'elle est la seule créatrice d'objets. La « macro » n'est qu'un raccourci de langage (i.e., une notation), alors que la définition algébrique « quotiente » ou contraint et restreint un type préexistant ((en) carier) au moyen d'axiomes. En revanche, la définition inductive engendre ex nihilo ses objets. Les règles de construction sont donc procréatrice.
Ainsi contrairement à l'axiome, les règles de construction d'une récurrence bien fondée ne peuvent créer l'incohérence.
De plus, tout objet appartient à une génération. Dans le cas le plus général, cette génération est un entier ou un ordinal. Le nombre de générations peut donc être , fini … nulle (types vide) ou ne pas être.
La validité de l'induction découle du caractère bijectif du procédé de procréation :
- injectivité : à construction différente, objet différent ;
- surjectivité : tout objet a une construction.
L'induction structurelle est une généralisation de la récurrence traditionnelle.
Exemples
Les fonctions définies par récurrence structurelle généralisent les fonctions définies par récurrence sur les entiers.
Les listes
Les listes sont définies comme étant
- soit la liste vide [ ],
- soit la liste obtenue par la mise en tête d'une liste d'un élément a, ce qui donne a : .
La fonction length qui définit la longueur d'une liste se définit par induction structurelle :
- length ([ ]) = 0
- length (a : ) = 1 + length ().
La fonction concat qui concatène deux listes et
- concat ([ ], ) =
- concat (a : , ) = a : (concat(, ))
On peut démontrer par induction structurelle la proposition suivante :
- length(concat()) = length() + length().
Première étape
- length(concat([ ], )) = length() = 0 + length() = length([ ]) + length()
Deuxième étape La démonstration utilise l'hypothèse d'induction structurelle
- length(concat(a : , )) = length(a : concat(, )) = 1 + length(concat(, ))
- = (par hypothèse d'induction structurelle) 1+ length() + length() = length(a:) + length()
Les arbres binaires
Considérons les arbres binaires définis ainsi :
- pour l'arbre vide,
- B B pour un arbre non vide ayant pour sous-arbre gauche B et pour sous-arbre droit B.
On peut définir la fonction taille (le nombre de nœuds internes de l'arbre binaire) :
- taille() = 0
- taille(B B) = taille(B) + taille(B) + 1
Principes
Considérons une structure définie par des constructeurs d'arité . Les constructeurs d'arité 0 sont des constantes.
Définition par induction structurelle
La définition par induction structurelle d'une fonction s'écrit pour chaque constructeur
où est une expression qui dépend de i'. On remarque que si est une constante, la définition est celle d'un cas de base:
Raisonnement par induction structurelle
Le schéma de démonstration qu'une propriété P est valide sur toute une structure se présente sous la forme d'une règle d'inférence pour chaque constructeur
Il faut donc faire une démonstration d'« hérédité » pour chaque constructeur.
Le cas des entiers naturels
Le cas des entiers naturels est celui où il y a deux constructeurs: 0 d'arité 0 (donc une constante) et succ (autrement dit +1) d'arité 1. La récurrence traditionnelle se réduit donc à une récurrence structurelle sur ces deux constructeurs.
La coinduction
Grossièrement la coinduction étend l'induction en offrant la possibilité d'omettre les éléments initiaux (le jardin d'éden).
Par exemple, omettre la liste vide, transforme la liste en flux ((en) stream). : Un flux de trucs est un truc qui s'ajoute à flux de trucs.
Bibliographie
- (en) John E. Hopcroft, Rajeev Motwani et Jeffrey D. Ullman, Introduction to Automata Theory, Languages, and Computation, Reading Mass, Addison-Wesley, , 2nd éd., 521 p. (ISBN 0-201-44124-1)
- (en) R.M. Burstall, « Proving Properties of Programs by Structural Induction », The Computer Journal, vol. 12, no 1, , p. 41–48 (DOI 10.1093/comjnl/12.1.41, lire en ligne)
- Niklaus Wirth, Algorithms and Data Structures, Prentice Hall, (lire en ligne)
- Horst Reichel, Structural induction on partial algebras, Akademie-Verlag,
- Jason Filippou, « Structural Induction »,
- Rozsa Peter, Über die Verallgemeinerung der Theorie der rekursiven Funktionen für abstrakte Mengen geeigneter Struktur als Definitionsbereiche, Symposium International, Varsovie () (Sur la généralisation de la théorie des fonctions récursives à des ensembles abstraits avec, comme domaines, des structures adaptées).
Voir aussi
- Forme de Backus-Naur
- Type récursif
- Définition par récurrence
- Ordre bien fondé
- Raisonnement par récurrence
- Récurrence transfinie
- Terme (logique)
v · m Types de données | |
---|---|
Non interprétée | |
Numérique |
|
Texte brut |
|
Pointeur |
|
Composite (en) |
|
Autres |
|
Articles liés |
|
Portail de la programmation informatique
Portail de la logique
Portail des mathématiques
Portail de l'informatique théorique