Discussion:Relation bien fondée

J'ai appris le mot "noethérien" dans ce contexte, et depuis, qu'il a été introduit par Bourbaki. J'ai un doute quant à l'ordre de x_n, x_n+1 (de même que le sens de l'appartenance dans axiome de régularité), mais j'ai tendance à confondre droite et gauche. J'y reviendrai quand je serai plus frais. Je me souviens qu'il y a trois propriétés équivalentes (si DC est vérifié) pour la bonne fondation : la propriété que toute partie non vide contienne un élement sans antécédent dans l'ensemble (soit, dit autrement, la propriété qui apparaît dans la formulation de l'axiome de fondation), le fait qu'il n'y ait pas de suite infinie "décroissante" (et c'est cela qui motive ma première remarque), enfin le fait qu'on puisse faire de la récurrence (induction) transfinie "le long" de R (auquel se rattache une fonction de rang à valeurs dans les ordinaux). A mon avis, il serait plus harmonieux de prendre la même propriété de définition dans l'axiome de fondation et ici, et expliquer les deux autres, plus la fonction de rang. Enfin, cela devrait être écrit ailleurs mais j'y pense ici, ce serait peut-être bien de changer le titre de axiome de régularité en axiome de fondation ; on parle tant de régularité en mathématique ! D'ailleurs, Krivine dans son livre ne parle que de l'axiome de fondation et "régularité" n'apparaît pas dans son index. CD 21 jan 2005 à 23:40 (CET)

Et oui, la terminologie noethérienne due à Gérard Huet pour ce domaine, je crois, est contraire à la terminologie mathématique habituelle qui utilise artinienne dans ce cas. Pierre de Lyon 10 février 2006 à 21:57 (CET)

Si on considère la relation de réécriture il s'agit bien de "noethérien" au sens usuel en math. Il me semble que "bien fondé" est vraiment le vocabulaire usuel en théorie des ordres et que l'on peut renvoyer à l'article récemment créé conditions de chaîne dans l'intro pour les autres terminologies. Proz (d) 1 janvier 2012 à 20:51 (CET)

Récurrence

L'article semble indiquer qu'il faudrait passer par la notion (utile par ailleurs) de rang ordinal pour la récurrence, alors qu'il y a une propriété de récurrence en gros équivalente à celle sur le rang qui est conséquence directe de la définition. J'ai modifié l'intro, mais c'est à reprendre aussi dans l'article. Proz (d) 31 janvier 2012 à 11:22 (CET)

Usage en algorithmique

Ce paragraphe omet de définir "inférieur". C'est très problématique car de nombreuses relations d'ordre possibles entre des "éléments" donnent lieu à des suites infinies strictement décroissantes, par exemple les fractions 0.1, 0.01, 0.001, etc. ou les chaines de caractères "b", "ab", "aab", etc. Il est évident qu'un programme qui parcourt une telle suite ne se termine pas. — Le message qui précède, non signé, a été déposé par Ripounet (discuter), le 30 mars 2015 à 16:06

De quel paragraphe parlez-vous? Bien sûr nous savons qu'il y a en informatique et en mathématiques des ordres non bien fondés. Qu'est-ce que cela a de problématique et de surprenant? --Pierre de Lyon (discuter) 31 mars 2015 à 19:07 (CEST)

Du paragraphe "Usage en algorithmique". Sa première phrase est fausse. Ripounet (discuter)

En admettant que "antécédent" et "inférieur" soient équivalents, en quoi cette phrase est-elle fausse? --Pierre de Lyon (discuter) 1 avril 2015 à 21:56 (CEST)

Combien d'équivalences?

L'introduction de l'article parle de 2 conditions équivalentes mais en mentionne 3. — Le message qui précède, non signé, a été déposé par Bobouh (discuter (discuter), le 3 octobre 2015 à 09:38‎ contributions)

C'est corrigé maintenant. Merci de l'avoir signalé. --Pierre de Lyon (discuter) 4 octobre 2015 à 17:11 (CEST)

+

J'ai parcouru rapidement l'article. Il manque le plus important, la raison d'être de la notion :

1. $(\forall x\in X)\;[(\forall y\in X)\;[yRx\implies P(y)]\implies P(x)]\quad {\text{implies}}\quad (\forall x\in X)\,P(x).$
2. Il est intéressant (pratique) de dire que « ∀ f:E→ℕ, well_founded (fun x y : A => f x < f y).  »
3. Il me semble que « R est bien fondée ssi toute partie possède un "élément minimal" »
4. Enfin une conjecture /(FIXME: théorême ?) qui me semble fondamentale : is_finite A ↔ { R:A→A→Prop & well_founded R & well_founded (flip R) }
5. Par ailleurs The Coq Standard Library possède une librairie importante sur le sujet.

Dans Library Coq.Init.Wf :

 Inductive Acc (x: A) : Prop :=
     Acc_intro : (forall y:A, R y x -> Acc y) -> Acc x.

A relation is well-founded if every element is accessible

 Definition well_founded := forall a:A, Acc a.

Donc, il me semble essentielle de parler de ce prédicat d'accessibilité.   <STyx @ (en vadrouille)

Bonjour,

• ton point 1 est dans le premier des 2 théorèmes ;
• ton point 3 est le premier des 2 points de l'intro.
• Tes points 2, 4 et 5 sont écrits dans un (ou des) langage(s) que je ne connais pas. Peux-tu traduire stp ?
• Ton point 5 ressemble furieusement à ton point 1.

Anne (discuter) 24 juillet 2020 à 19:43 (CEST)

Baah ! y-a un problème réciproque de langage et vocabulaire, je trouve le langage (ensembliste) de l'article terriblement vieillot et difficilement déchiffrable ! (R-antécédents ? quesaco !)

• Acc: x est accessible ssi tout y tel que y R x est accessible.
• 4: A est fini ssi il possède une relation R telle que R et R' (R' x y:=R y x) soient bien fondées.   <STyx @ (en vadrouille) 24 juillet 2020 à 20:08 (CEST)