Induction structurelle

Les informations figurant dans cet article ou cette section doivent être reliées aux sources mentionnées dans les sections « Bibliographie », « Sources » ou « Liens externes » (décembre 2017).

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.

Cette section doit être déjargonisée (août 2023). Le texte doit être remanié en utilisant un vocabulaire plus directement compréhensible. Discutez des points à améliorer en page de discussion.

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 ω {\displaystyle \omega } , 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.

Les fonctions définies par récurrence structurelle généralisent les fonctions définies par récurrence sur les entiers.

Les listes sont définies comme étant

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

La fonction l e n g t h : l i s t e s → N {\displaystyle length:listes\to \mathbb {N} } qui définit la longueur d'une liste par induction :

• l e n g t h ( [] ) ↦ 0 {\displaystyle length({\texttt {[]}})\mapsto 0}
• l e n g t h ( a :: ℓ ) ↦ 1 + l e n g t h ( ℓ ) {\displaystyle length(a::\ell )\mapsto 1+length(\ell )} .

La fonction c o n c a t : l i s t e s × l i s t e s → l i s t e s {\displaystyle concat:listes\times listes\to listes} qui concatène deux listes ℓ 1 {\displaystyle \ell _{1}} et ℓ 2 {\displaystyle \ell _{2}}

• c o n c a t ( [] , ℓ 2 ) ↦ ℓ 2 {\displaystyle concat({\texttt {[]}},\ell _{2})\mapsto \ell _{2}}
• c o n c a t ( a :: ℓ 1 , ℓ 2 ) ↦ a :: ( c o n c a t ( ℓ 1 , ℓ 2 ) ) {\displaystyle concat(a::\ell 1,\ell 2)\mapsto a::(concat(\ell 1,\ell 2))}

On peut démontrer la proposition suivante :

∀ ℓ 1 ℓ 2 , l e n g t h ( c o n c a t ( ℓ 1 , ℓ 2 ) ) = l e n g t h ( ℓ 1 ) + l e n g t h ( ℓ 2 ) {\displaystyle \forall \ell _{1}\ell _{2},\;length(concat(\ell _{1},\ell _{2}))=length(\ell _{1})+length(\ell _{2})}

On procède par induction sur ℓ 1 {\displaystyle \ell _{1}} après avoir introduit ℓ 2 {\displaystyle \ell _{2}}

Cas de base ( ℓ 1 = [] {\displaystyle \ell _{1}={\texttt {[]}}} )

l e n g t h ( c o n c a t ( [] , ℓ 2 ) ) = l e n g t h ( ℓ 2 ) = 0 + l e n g t h ( ℓ 2 ) = l e n g t h ( [] ) + l e n g t h ( ℓ 2 ) {\displaystyle length(concat({\texttt {[]}},\ell _{2}))=length(\ell _{2})=0+length(\ell _{2})=length({\texttt {[]}})+length(\ell _{2})}

Cas inductif ( ℓ 1 = a :: ℓ 1 ′ {\displaystyle \ell _{1}=a::\ell _{1}'} )

On cherche à monter que l e n g t h ( c o n c a t ( ℓ 1 , ℓ 2 ) ) = l e n g t h ( ℓ 1 ) + l e n g t h ( ℓ 2 ) {\displaystyle length(concat(\ell _{1},\ell _{2}))=length(\ell _{1})+length(\ell _{2})}

On dispose de l'hypothèse d'induction suivante l e n g t h ( c o n c a t ( ℓ 1 ′ , ℓ 2 ) ) = l e n g t h ( ℓ 1 ′ ) + l e n g t h ( ℓ 2 ) {\displaystyle length(concat(\ell _{1}',\ell _{2}))=length(\ell _{1}')+length(\ell _{2})}

Donc 1 + l e n g t h ( c o n c a t ( ℓ 1 ′ , ℓ 2 ) ) = 1 + l e n g t h ( ℓ 1 ′ ) + l e n g t h ( ℓ 2 ) {\displaystyle 1+length(concat(\ell _{1}',\ell _{2}))=1+length(\ell _{1}')+length(\ell _{2})}

Donc l e n g t h ( a :: c o n c a t ( ℓ 1 ′ , ℓ 2 ) ) = l e n g t h ( a :: ℓ 1 ′ ) + l e n g t h ( ℓ 2 ) {\displaystyle length(a::concat(\ell _{1}',\ell _{2}))=length(a::\ell _{1}')+length(\ell _{2})} , par définition de l e n g t h {\displaystyle length}

Donc l e n g t h ( c o n c a t ( a :: ℓ 1 ′ , ℓ 2 ) ) = l e n g t h ( a :: ℓ 1 ′ ) + l e n g t h ( ℓ 2 ) {\displaystyle length(concat(a::\ell _{1}',\ell _{2}))=length(a::\ell _{1}')+length(\ell _{2})} , par définition de c o n c a t {\displaystyle concat}

Donc l e n g t h ( c o n c a t ( ℓ 1 , ℓ 2 ) ) = l e n g t h ( ℓ 1 ) + l e n g t h ( ℓ 2 ) {\displaystyle length(concat(\ell _{1},\ell _{2}))=length(\ell _{1})+length(\ell _{2})} , par définition de ℓ 1 {\displaystyle \ell _{1}}

Considérons les arbres binaires définis ainsi :

• ◻ {\displaystyle \Box } pour l'arbre vide,
• B 1 {\displaystyle _{1}} ∙ {\displaystyle \bullet } B 2 {\displaystyle _{2}} pour un arbre non vide ayant pour sous-arbre gauche B 1 {\displaystyle _{1}} et pour sous-arbre droit B 2 {\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 1 {\displaystyle _{1}} ∙ {\displaystyle \bullet } B 2 {\displaystyle _{2}} ) = taille(B 1 {\displaystyle _{1}} ) + taille(B 2 {\displaystyle _{2}} ) + 1

Sur N {\displaystyle \mathbb {N} } , le premier principe d'induction, permet, en montrant une propriété sur un cas de base et la conservation de cette propriété de manière héréditaire, de montrer la propriété pour tous les entiers naturels si le cas de base est n 0 = 0 {\displaystyle n_{0}=0} .

( B n 0 {\displaystyle B_{n_{0}}} ) s'appelle l'étape de base de l'induction, elle affirme que P ( n 0 ) {\displaystyle P(n_{0})} est vrai.

( H n 0 {\displaystyle H_{n_{0}}} ) s'appelle l'étape héréditaire ou inductive, elle affirme pour tout n ⩾ n 0 {\displaystyle n\geqslant n_{0}} que si P ( n ) {\displaystyle P(n)} est vrai alors P ( n + 1 ) {\displaystyle P(n+1)} est vrai aussi^[1].

Lorsque l'on a des cas plus complexes, que l'on ait besoin d'utiliser P ( n 0 ) , P ( n 0 + 1 ) , … P ( n ) {\displaystyle P(n_{0}),P(n_{0}+1),\dots P(n)} pour montrer P ( n + 1 ) {\displaystyle P(n+1)} , il est plus pratique d'utiliser le second principe d'induction.

L'étape de base est cachée dans Γ n 0 {\displaystyle \Gamma _{n_{0}}} .

Sur N {\displaystyle \mathbb {N} } , les deux principes d'induction sont équivalents, mais seul le deuxième principe d'induction se généralise à des ensembles ordonnés plus généraux^[1].

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

La définition par induction structurelle d'une fonction g {\displaystyle g} s'écrit pour chaque constructeur f i {\displaystyle 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 ) {\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ù E i {\displaystyle E_{i}} est une expression qui dépend de i'. On remarque que si f i {\displaystyle 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 ) {\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 f i {\displaystyle f_{i}}

P ( x 1 ) . . . P ( x a i ) P ( f i ( x 1 , . . . , x a 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 à un flux de trucs.

Les système, langages et logiciels supportant à des degrés divers cette fonctionnalité sont nombreux.

Cette section est vide, insuffisamment détaillée ou incomplète. Votre aide est la bienvenue ! Comment faire ?

Un assistant de preuve est un logiciel permettant l'écriture et la vérification de preuves mathématiques. L'induction structurelle étant une technique de preuve très utilisée, les assistants de preuves supportent souvent l'écriture de telles preuves.

Rocq permet l'écriture de types inductifs qui représentent les ensembles inductifs. Rocq va alors générer automatiquement un principe d'induction associé à ce type.

On commence par définir l'ensemble inductif où l'on retrouve les deux façons de construire un objet de type liste, la liste vide et la concaténation d'un élément et d'une liste.

Inductive list {A : Type} :=
    | nil
    | cons (head : A) (tail : list).

On définit deux notations afin que notre code se rapproche de l'écriture de l'exemple :

Notation "[]" := (nil).
Notation "head :: tail" := (cons head tail).

On définit les fonctions length et concat

Fixpoint length {A : Type} (l : @list A) : nat :=
    match l with
    | [] => 0
    | head :: tail => 1 + length tail
    end.|lang=Rocq

Fixpoint concat {A : Type} (l1 : @list A) (l2 : @list A) : @list A :=
    match l1 with
    | [] => l2
    | head :: tail => head :: (concat tail l2)
    end.

Enfin, on peut formaliser la preuve que la taille de la liste issue de la concaténation est bien la somme des tailles des listes en entrée.

Goal forall (A : Type) (l1 l2: @list A), 
        length (concat l1 l2) = length l1 + length l2.
Proof. intros A l1 l2.  
    induction l1 as [{{!}} a l1 IHl1].
    + simpl. reflexivity.
    + simpl. f_equal.
      apply IHl1.
Qed.

Le cas de base de l'induction se montre bien en utilisation la réflexivité de l'égalité après avoir évalué concat sur l1 vide.

Le cas inductif se montre bien principalement en utilisant l'hypothèse d'induction IHl1.

Pour chaque ensemble inductif, définition Inductive ma_def en rocq, un principe d'induction enregistré dans la variable ma_def_ind. On peut l'afficher à l'aide de la commande Check list_ind. pour les listes de l'exemple précédent.

list_ind : forall (A : Type) (P : list -> Prop),
    P [] ->
    (forall (head : A) (tail : list), P tail -> P (head :: tail)) ->
        forall l : list, P l

On retrouve bien une propriété proche du premier principe d'induction, pour toute propriété P {\displaystyle P} , si la propriété est vérifiée sur la liste vide [] {\displaystyle {\texttt {[]}}} (cas de base), et que sachant qu'elle est vérifiée pour une liste, elle l'est encore si on lui rajoute un élément (cas inductif), alors, elle est vérifiée pour toute liste.

On peut alors se demander si le principe d'induction généré par Rocq est admis en axiome ou s'il est lui-même prouvé par l'assistant de preuve. On est dans le second cas, Rocq génère une preuve du principe d'induction.

Cette génération est un exemple d'application de la correspondance de Curry-Howard. En effet, pour prouver le principe d'induction, on va exhiber une fonction récursive terminant et ayant pour type le principe d'induction.

Pour les listes, on cherche à exhiber la fonction prenant une propriété P {\displaystyle P} sur les listes, la preuve P n i l {\displaystyle Pnil} que P {\displaystyle P} est vérifiée sur la liste vide, la preuve P c o n s {\displaystyle Pcons} du cas inductif et une liste quelconque ℓ {\displaystyle \ell } et doit renvoyer la preuve que P {\displaystyle P} est vérifiée sur ℓ {\displaystyle \ell } .

Si l'on peut exhiber une telle fonction, alors, il est suffisant de disposer de P n i l {\displaystyle Pnil} et P c o n s {\displaystyle Pcons} , les preuves du cas de base et du cas inductif, afin de pouvoir prouver la propriété P {\displaystyle P} sur toutes les listes. En effet, on a simplement à appliquer cette fonction.

Voici la fonction générée pour le principe d'induction des listes :

fun (A : Type)
    (P : list -> Prop)
    (Pnil : P [])
    (Pcons : forall (head : A) (tail : list), P tail -> P (head :: tail)) 
=> fix F (l : list) : P l :=
    match l with
    | [] => Pnil
    | head :: tail => Pcons head tail (F tail)
    end

Ici la fonction récursive F {\displaystyle F} termine immédiatement, le variant étant la taille de la liste ℓ {\displaystyle \ell } .

• (en) John E. Hopcroft, Rajeev Motwani et Jeffrey D. Ullman, Introduction to Automata Theory, Languages, and Computation, Reading Mass, Addison-Wesley, 2001, 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, n^o 1,‎ février 1968, p. 41–48 (DOI 10.1093/comjnl/12.1.41, lire en ligne)
• Niklaus Wirth, Algorithms and Data Structures, Prentice Hall, 1985 (lire en ligne)
• Horst Reichel, Structural induction on partial algebras, Akademie-Verlag, 1984
• Jason Filippou, « Structural Induction », 7 mai 2016
• 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 ensembles abstraits avec, comme domaines, des structures adaptées).

• Forme de Backus-Naur
• Type récursif
• Définition par récurrence
• Ordre bien fondé
• Raisonnement par récurrence
• Récurrence transfinie
• Terme (logique)

• Portail de la programmation informatique
• Portail de la logique
• Portail des mathématiques
• Portail de l'informatique théorique