Relation bien fondée
En mathématiques, une relation bien fondée (encore appelée relation noethérienne ou relation artinienne) est une relation binaire vérifiant l'une des deux conditions suivantes, équivalentes d'après l'axiome du choix dépendant (une version faible de l'axiome du choix) :
- pour toute partie non vide X de E, il existe un élément x de X n'ayant aucun R-antécédent dans X (un R-antécédent de x dans X est un élément y de X vérifiant yRx) ;
- condition de chaîne descendante : il n'existe pas de suite infinie (xn) d'éléments de E telle qu'on ait xn+1Rxn pour tout n.
Un ordre bien fondé (encore appelé ordre noethérien ou ordre artinien[1]) est une relation d'ordre dont l'ordre strict associé est une relation bien fondée.
Toute relation bien fondée est strictement acyclique, c'est-à-dire que sa clôture transitive est un ordre strict. Une relation R est bien fondée si sa clôture transitive l'est, ou encore si R est antiréflexive et si sa clôture réflexive transitive est un ordre bien fondé.
Exemples
Nombres
- Sur l'ensemble N des entiers naturels, la relation R définie par x R y ⇔ y = x + 1 est bien fondée. Sa clôture transitive est l'ordre strict usuel <, et l'ordre usuel ≤ est un ordre total bien fondé, c'est-à-dire un bon ordre.
- Sur N×N, l'ordre produit est bien fondé (mais non total).
- Sur l'ensemble Z des entiers relatifs, la relation R définie par x R y ⇔ y = x + 1 n'est pas bien fondée comme l'atteste cette suite de nombres relatifs qui ne respectent pas la condition de chaîne descendante : ...< -6 < -5 < -4 < -3 < -2 < -1 < 0. Sa clôture transitive qui est l'ordre strict usuel < ne l'est pas non plus.
Chaînes de caractères
- Sur l'ensemble des chaînes de caractères, l'ordre strict « est préfixe strict de » est bien fondé.
- Sur l'ensemble des chaînes de caractères, l'ordre lexicographique n'est pas bien fondé. Par exemple, voici un exemple d'une suite de chaînes de caractères qui ne respectent pas la condition de chaîne descendante : ... < aaaaab < aaaab < aaab < aab < ab
Arbres binaires finis
- Sur l'ensemble des arbres binaires finis, construits à partir de l'arbre vide et de l'enracinement ¤ (c'est-à-dire qu'à partir de deux arbres A et B on forme l'arbre A ¤ B), l'ordre strict « est un sous-arbre strict de » est un ordre bien fondé. Il se signifie ainsi : A ¤ B > ou A ¤ B > C si A C ou B C.
- Sur l'ensemble des arbres binaires, on peut définir l'ordre bien fondé > suivant :
- A ¤ B > ,
- ou A ¤ B > C ¤ D parce que
- A > C et A ¤ B > D,
- ou A = C et B > D
- Dans le dernier ordre, l'arbre ( ¤ ) ¤ a une infinité d'arbres plus petits que lui.
Théorie des ensembles
L'axiome de fondation affirme que la relation d'appartenance est bien fondée ; mais on peut avoir une théorie des ensembles équicohérente avec l'axiome d'anti-fondation.
Propriétés
La bonne fondation est préservée par pullback, c'est-à-dire que pour toute application ρ : E → F et toute relation bien fondée S sur F, la relation T sur E définie par xTy ⇔ ρ(x)Sρ(y) est bien fondée.
Récurrence noethérienne ou bien fondée
On notera R−1[x] l'ensemble des R-antécédents de x.
Le théorème suivant (dans la théorie des ensembles de Zermelo) offre à la fois une troisième définition équivalente de la bonne fondation et une généralisation du principe de démonstration par induction transfinie (sur un bon ordre ou sur un ordinal), qui elle-même étend l'axiome de Peano no 5 ou le principe de récurrence (correspondant à l'ordre usuel sur les entiers naturels) :
Théorème (bonne fondation et induction bien fondée) — Une relation R sur un ensemble E est bien fondée si et seulement si, pour qu'une partie de E soit égale à E tout entier, il suffit qu'elle contienne chaque élément dont elle contient tous les R-antécédents.
Formellement[2] : R est bien fondée si et seulement si, pour toute partie P de E,De même, un second théorème (dans la théorie des ensembles de Zermelo-Fraenkel, donc avec remplacement) généralise le principe de définition par récurrence d'une suite et plus généralement, de définition d'une fonction par récursion transfinie :
Théorème (fonction définie par récursion bien fondée) — Soient R une relation bien fondée sur un ensemble E et G une classe fonctionnelle partout définie. Alors, il existe une fonction f et une seule (au sens : un seul graphe de fonction), de domaine Df = E, telle que pour tout x ∈ E, f(x) = G(x, f|R−1[x]), où f|P désigne la restriction de f à P.
Ces deux théorèmes s'étendent aux classes[3],[4], comme leurs homologues dans le cas particulier de la récurrence transfinie. Plus précisément : on peut remplacer, dans ces deux énoncés, les ensembles E, R et f par des classes (relationnelle pour R et fonctionnelle pour f), sous réserve que pour tout ensemble x, la classe R−1[x] soit un ensemble (dans le cas de la récurrence transfinie, il est inutile d'ajouter cette hypothèse car ∈−1[x] = x).
Fonction rang
Dans un ensemble E muni d'une relation bien fondée R, chaque élément x admet un rang ρ(x), qui est un nombre ordinal. La fonction rang est définie sur E par récursion bien fondée par :
- ρ(x) = ∪ { α + 1 | α ∈ im(ρ|R−1[x]) } = ∪ { ρ(y) + 1 | y R x }
(l'union d'un ensemble d'ordinaux est un ordinal). Ainsi, le rang de x est le plus petit ordinal strictement supérieur aux rangs des antécédents de x.
La longueur de la relation R, souvent notée |R|, est le plus petit ordinal contenant tous les ρ(x).
L'induction et la récursion bien fondées (voir supra) s'appliquent à R, mais il est parfois plus commode de les appliquer au pullback par ρ de l'ordre strict sur l'ordinal |R|, c'est-à-dire à la relation T définie par : xTy ⇔ ρ(x) < ρ(y).
La fonction rang permet d'organiser de manière évidente E en une hiérarchie, très utilisée en théorie des ensembles avec pour R la relation d'appartenance (cf. « Rang d'un ensemble »).
Usage en algorithmique
Un cas particulier de la récurrence bien fondée est la récurrence structurelle. Un algorithme, lorsqu'il construit une suite d'éléments en assurant qu'un élément construit est strictement inférieur à son prédécesseur, assure aussi sa terminaison, dès que l'ordre strict est bien fondé.
Les structures utilisées en algorithmique (types construits) étant souvent des ordres stricts bien fondés, on dispose ainsi d'une méthode très générale pour prouver la terminaison d'un programme informatique.
Notes et références
- Jean-Pierre Ramis, André Warusfel et al., Mathématiques Tout-en-un pour la Licence : Niveau L1, Dunod, , 2e éd. (lire en ligne), p. 38.
- (en) Kees Doets, From Logic to Logic Programming, MIT Press, (lire en ligne), p. 7.
- (en) András Hajnal et Peter Hamburger, Set Theory, Cambridge University Press, (lire en ligne), p. 202 et 280.
- (en) Michael Holz, Karsten Steffens et Edmund Weitz, Introduction to Cardinal Arithmetic, Birkhäuser, (lire en ligne), p. 20-23.
Articles connexes
- Arbre (mathématiques)
- Méthode de descente infinie
- Bel ordre et lemme de Higman
- Terminaison d'un système de réécriture
- ∈-induction (en)
- Noethérien
- Portail de la logique
- Portail des mathématiques