Induction structurelle

L'induction structurelle ou récurrence structurelle est une méthode de définition d'une fonction ou d'une propriété sur une structure, c'est-à-dire sur des objets (mathématiques ou informatiques) structurées comme, par exemple, les listes, les arbres ou les arbres binaires, mais qui, plus généralement, s'utilise sur toute structure mathématique ayant une définition récursive. En permettant par le même principe de définir un prédicat total 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.

L'induction structurelle est à la fois une généralisation de la récurrence traditionnelle et un cas particulier de la récurrence bien fondée.

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 $\ell$ d'un élément a, ce qui donne a : $\ell$.

La fonction length qui définit la longueur d'une liste se définit par induction structurelle :

• length ([ ]) = 0
• length (a : $\ell$) = 1 + length ($\ell$).

La fonction concat qui concatène deux listes $\ell _{1}$ et $\ell _{2}$

• concat ([ ], $\ell _{2}$) = $\ell _{2}$
• concat (a : $\ell _{1}$, $\ell _{2}$) = a : (concat($\ell _{1}$, $\ell _{2}$)

On peut démontrer par induction structurelle la proposition suivante :

length(concat($\ell _{1},\ell _{2}$)) = length$\ell _{1}$ + length($\ell _{2}$).

Première étape

length(concat([ ], $\ell _{2}$)) = length($\ell _{2}$) = 0 + length($\ell _{2}$) = length([ ]) + length($\ell _{2}$)

Deuxième étape La démonstration utilise l'hypothèse d'induction structurelle

length(concat(a : $\ell _{1}$, $\ell _{2}$)) = length(a : concat($\ell _{1}$, $\ell _{2}$)) = 1 + length(concat($\ell _{1}$, $\ell _{2}$))

= (par hypothèse d'induction structurelle) 1+ length($\ell _{1}$) + length($\ell _{2}$) = length(a:$\ell _{1}$) + length($\ell _{2}$)

Les arbres binaires

Considérons les arbres binaires définis ainsi :

• $\Box$ pour l'arbre vide,
• B$_{1}$ $\bullet$ B$_{2}$ pour un arbre non vide ayant pour sous-arbre gauche B$_{1}$ et pour sous-arbre droit B$_{2}$.

On peut définir la fonction taille (le nombre de nœuds internes de l'arbre binaire) :

• taille($\Box$) = 0
• taille(B$_{1}$ $\bullet$ B$_{2}$) = taille(B$_{1}$) + taille(B$_{2}$) + 1

Principes

Considérons une structure définie par des constructeurs $f_{1},...,f_{n}$ d'arité $a_{1},...,a_{n}$. Les constructeurs d'arité 0 sont des constantes.

Définition par induction structurelle

La définition par induction structurelle d'une fonction $g$ s'écrit pour chaque constructeur $f_{i}$

• $g(f_{i}(x_{1},..x_{a_{i}}),y_{1},...y_{n})=E_{i}(g(x_{1}),...,g(x_{a_{i}}),y_{1},...,y_{n})$

où $E_{i}$ est une expression qui dépend de i'. On remarque que si $f_{i}$ est une constante, la définition est celle d'un cas de base:

• $g(f_{i},y_{1},...y_{n})=E_{i}(y_{1},...,y_{n})$

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 $f_{i}$

${\frac {P(x_{1})...P(x_{a_{i}})}{P(f_{i}(x_{1},...,x_{a_{i}}))}}$

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.

Bibliographie

• (en) John E. Hopcroft, Rajeev Motwani et Jeffrey D. Ullman, Introduction to Automata Theory, Languages, and Computation, Reading Mass, 2nd, 2001 (ISBN 0-201-44124-1)
• R.M. Burstall, « Proving Properties of Programs by Structural Induction », The Computer Journal, vol. 12,‎ 1969, p. 41–48 (DOI 10.1093/comjnl/12.1.41)
• Niklaus Wirth Algorithms and Data Structures Prentice Hall (1985)
• Rozsa Peter, Über die Verallgemeinerung der Theorie der rekursiven Funktionen für abstrakte Mengen geeigneter Struktur als Definitionsbereiche, Symposium International, Varsovie septembre (1959) (Sur la généralisation de la théorie des fonctions récursives à des quantités abstraites avec comme domaines des structures adaptées).

Voir aussi

• Définition par récurrence
• Ordre bien fondé
• Raisonnement par récurrence
• Récurrence transfinie
• Terme (logique)