Induction structurale

L'induction structurale est une méthode de démonstration utilisée en logique mathématique (par exemple, dans la démonstration du théorème de Łoś' ), en informatique , en théorie des graphes et dans d'autres domaines mathématiques. Elle généralise l' induction mathématique sur les nombres naturels et peut être étendue à toute induction noethérienne . La récursion structurale est une méthode de récursion qui entretient avec l'induction structurale la même relation que la récursion ordinaire avec l' induction mathématique ordinaire .

L'induction structurale permet de démontrer qu'une proposition pour tout définie récursivement , comme les formules , les listes ou les arbres . Un ordre partiel bien fondé est défini sur ces structures (« sous-formule » pour les formules, « sous-liste » pour les listes et « sous-arbre » pour les arbres). La démonstration par induction structurale prouve que la proposition est vraie pour toutes les structures minimales et que, si elle est vraie pour les sous-structures immédiates d'une structure induction bien fondée , qui affirme que ces deux conditions suffisent pour que la proposition soit vraie pour tout

Un arbre généalogique est une structure de données bien connue, qui présente les parents, grands-parents, etc. d'une personne, aussi loin que l'on puisse les connaître (voir l'illustration pour un exemple). Il est défini de manière récursive :

• Dans le cas le plus simple, un arbre généalogique ne montre qu'une seule personne (si l'on ne sait rien de ses parents) ;
• Alternativement, un arbre généalogique montre une personne et, reliés par des branches, les deux sous-arbres généalogiques de ses parents (en utilisant, par souci de concision, l'hypothèse simplificatrice selon laquelle si l'un d'eux est connu, les deux le sont).

À titre d’exemple, la propriété « Un arbre généalogique s’étendant sur