Études-Mathématique/Règle d'induction
Contents
Question
Comment exprimer la règle d'induction ?
Étude
Forme actuelle de déduction
Une déduction a pour objet : les formules en conditions, la formule déduite.
Principe de l'induction
Le principe de base est d'enchaîner une suite de déduction, l'enchaînement étant paramétré par une chose ressemblant à une liste dite "index".
Liste index
On a deux options: l'index est une représentation ou non.
Habituellement on utiliser un index qui est une représentation. Si on utilisait une liste directe, cela interdirait d'utiliser cette déduction dans une hypothèse puisque alors on ne pourrait pas utiliser la représentation de liste pour avoir une liste directe.
Donc il faut utiliser une représentation de liste.
La règle
Variables
l,p,q
Conditions
- p(0l)
- pour tout x de l on a q x
- d est une déduction utilisant les variables globales "p,m,q,x" qui a pour condition "isList m", "p m" et "q x" et pour conclusion "p (m +le x)"
Conclusion
p l
La règle, sans q
À partir de la règle où l'on en lève la condition q, on peut déduire celle avec q: on remplace p y par "(si pour tout x de y, q x) alors p y"
Réponse
Voir l'étude.