Induction structurelle

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.