# 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 (x$_n$) d'éléments de E telle qu'on ait x$_{n+1}$Rx$_n$ pour tout n.
Un ordre bien fondé (encore appelé ordre noethérien ou ordre artinien) 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 $\Box$ 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 > $\Box$ ou A ¤ B > C si A $\geq$ C ou B $\geq$ C.
* Sur l'ensemble des arbres binaires, on peut définir l'ordre bien fondé > suivant :
** A ¤ B > $\Box$,
** 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 ($\Box$ ¤ $\Box$) ¤ $\Box$ 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 n$^o$ 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.
Par passage au complémentaire, la condition de l'énoncé équivaut à l'implication
    pour toute partie X de E, si ∀ x ∈ E (R$^{−1}$[x]∩X = ∅ ⇒ x ∉ X) alors X = ∅
ou encore, à sa contraposée :
    pour toute partie non vide X de E, ∃ x ∈ X (R$^{−1}$[x]∩X = ∅),
qui exprime bien que 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.
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 D$_f$ = 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.
Définissons le prédicat rec(h) par : h est une fonction, de domaine D$_h$ ⊂ E, telle que pour tout z ∈ D$_h$, R$^{−1}$[z] ⊂ D$_h$ et h(z) = G(z, h$_{|R−1[z]}$), puis le prédicat F(x, y) par : ∃h (rec(h) et h(x) = y).
Par induction bien fondée, la classe F est fonctionnelle (ce qui prouve déjà, par extensionnalité, que l'éventuelle fonction f annoncée dans le théorème est unique), or son domaine est inclus dans l'ensemble E donc (d'après le schéma d'axiomes de remplacement) il existe une fonction f telle que F(x, y) ⇔ f(x) = y. De plus, par construction, rec(f) est satisfait.
Enfin, D$_f$ = E, à nouveau par induction bien fondée : pour tout x ∈ E tel que R$^{−1}$[x] ⊂ D$_f$, l'ensemble de couples h := f∪{(x, G(x, f$_{|R−1[x]}$))} satisfait rec(h) donc x ∈ D$_f$.
Ces deux théorèmes s'étendent aux classes$^,$, 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.