Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Concept
Induction structurelle
Résumé
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 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.
Les système, langages et logiciels supportant à des degrés divers cette fonctionnalité sont nombreux.
L'un des plus puissants est le calcul des constructions inductives (CIC) et son logiciel Coq.
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 ( 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 , 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.
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.