Induction structurelle

Les listes sont définies comme étant

• soit la liste vide [ ],
• soit la liste obtenue par la mise en tête d'une liste ${\displaystyle \ell }$ d'un élément a, ce qui donne a : ${\displaystyle \ell }$.

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

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

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

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

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

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

Première étape

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

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

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

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

Considérons les arbres binaires définis ainsi :

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

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

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

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

• ${\displaystyle 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ù ${\displaystyle E_{i}}$ est une expression qui dépend de i'. On remarque que si ${\displaystyle f_{i}}$ est une constante, la définition est celle d'un cas de base:

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

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

${\displaystyle {\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 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.

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.