Discussion:Complétion de Knuth-Bendix

Procédure vs algorithme

Dans cet article la terminologie est fluctuante. Pierre de Lyon 24 août 2006 à 09:51 (CEST)

aide:catégories

Je précise ici mon commentaire de diff qui m'a échappé des mains, je voulais juste dire qu'ici (comme dans problème du mot), je me suis permis d'enlever des catégories-mères redondantes, suivant Aide:Catégorie/Syntaxe#Comment catégoriser une page lorsque la catégorie choisie existe déjà. Anne Bauval (d) 5 novembre 2010 à 19:02 (CET)

Le renommage est une erreur

Avant de renommer, il aurait fallu en parler dans la page de discussion. La procédure de Knuth-Bendix n'est pas un algorithme, car elle peut ne pas terminer. Si elle terminait toujours alors le problème du mot serait décidable. Je propose donc le renommage vers Procédure de Knuth-Bendix.--Pierre de Lyon (d) 6 novembre 2010 à 10:44 (CET)

Transfert d'un message reçu sur ma PdD + réponse Anne Bauval (d) 6 novembre 2010 à 11:02 (CET)

Vous avez déplacé Knuth-Bendix, vers algorithme de Knuth-Bendix. C'est une erreur car la procédure de Knuth-Bendix n'est pas un algorithme car le processus ne se termine pas forcément. --Pierre de Lyon (d) 6 novembre 2010 à 10:38 (CET)

Bonjour Pierre. À ma décharge :

Le titre initial comportait déjà le mot "algorithme", et mon renommage concernait la forme, pas le fond : remplacement de "Knuth-Bendix (algorithme)" par "Algorithme de Knuth-Bendix", suivant WP:CsT : "L’usage des parenthèses est strictement réservé aux cas d’homonymies."

L'article correspondant en anglais est en:Knuth–Bendix completion algorithm.

Je ne suis pas convaincue par ton argument, mais je ne suis pas experte comme toi, donc je rends mon tablier si d'autres spécialistes confirment.

Je ne suis pas spécialiste non plus, mais l'argument de Pierre Lescanne est confirmé par l'article « Algorithme ». Il peut effectuer un renommage en « Procédure de Knuth-Bendix » s'il pense ce titre plus adapté. Ambigraphe, le 11 novembre 2010 à 09:46 (CET)

Je suis d'accord que "algorithme" est impropre. Mais des gens l'appelent encore "Algorithme" (par exemple, le programme de l'option informatique de l'agrégation de mathématiques). J'ai mis les deux terminologies dans l'article. Il faudrait des sources pour les deux terminologies.--Fschwarzentruber (discuter) 15 mai 2016 à 21:35 (CEST)

Vocabulaire

Le mot "équation" n'est-il pas plus clair que "identité" ? 18 mai 2016 à 21:28 (CEST)

En français on parle d' identités remarquables et c'est bien de cela dont il s'agit. En revanche on parle de l'équation du second degré parce qu'elle contient des inconnues qu'il faut trouver. En fait une équation est une expression contenant une égalité entre deux termes avec des variables qu'il faut résoudre. Typiquement ce que l'on manipule dans un problème d'unification, ce sont des équations. En revanche, la complétion manipule des identités ou des égalités (à voir).--Pierre de Lyon (discuter) 26 mai 2016 à 07:23 (CEST)

Algorithme et règles

J'ai ajouté une procédure écrite en pseudo-code un peu naïve mais simple à comprendre. Puis j'ai enchaîné avec des règles. Il faut relire et polir. La partie sur les règles manque cruellement d'explications. C'est encore très cryptique. 18 mai 2016 à 23:02 (CEST) 18 mai 2016 à 23:10 (CEST)~~

Ce programme est tellement naïf qu'il est totalement inefficace. A chaque boucle il recalcule toutes les paires critiques et les normalise. Il ne faut pas faire croire que ce programme approxime même de loin une vraie complétion. Je suis vraiment favorable à sa suppression. Déjà Knuth explique si je me souviens bien que ce n'est pas ce qu'il faut faire. --Pierre de Lyon (discuter) 19 mai 2016 à 08:33 (CEST)

Bien sûr qu'il est tellement naïf. Mais il est tellement simple et pédagogique. Pour quelqu'un qui ne connaît la procédure de complétion (comme moi il y a 5 jours), c'est précisément cette procédure qui m'a permis de comprendre et certainement pas les règles. Arriver d'emblée sur des règles cryptiques, c'est vraiment trop technique (en plus, les règles modifient le système d'équations... donc modifie l'entrée, on y comprend plus rien). La procédure naïve est donnée dans le Baader et c'est pédagogique car le nombre de notions à connaître sont minimales : équations, systèmes de réécriture, ordre de réduction et paires critiques, système de réécriture qui termine et système confluent (et c'est déjà beaucoup !). Ensuite, si Knuth a dit que ce n'est pas ce qu'il faut faire, on peut rajouter une référence à la phrase à ajouter qui dit que l'algorithme est complétement inefficace.

=> Solution : J'ai renommé la section en "Procédure naïve". Comme tu dis, c'est important que personne ne croit que c'est ce qui est fait en vrai à cause de l'adjectif "naïf". J'ai étoffé le texte. Si le texte est assez précis, peut-être que le pseudo-code est inutile car il paraphrase trop le texte. Mais je sais que certaines personnes trouvent le pseudo-code plus clair. Donc je l'ai laissé. Par contre, dans une boîte, je trouve que c'est un bon compromis car ça met le pseudo-code en second plan.

=> avec cette idée de base (sans avoir des règles et tout un formalisme compliqué), on peut donner des EXEMPLES.

=> Ensuite, enchaîner par des règles qui modifient le système de réécriture ET le système d'équations, et "montrer la vraie vie" au lecteur une fois qu'il a une idée de ce que c'est, c'est technique mais pas trop. Pour la partie règles, il faut vraiment étoffer car c'est très très cryptique. Surtout la règle "Simplifier règle à gauche". Aussi, si après vous connaissez toutes les optimisations de cette procédure, je pense qu'il ne faut pas hésiter à compléter la page mais à mon avis, plutôt vers la fin.

Fschwarzentruber (discuter) 19 mai 2016 à 09:24 (CEST)

Je ne vais chipoter et je préfère laisser aussi d'autres s'exprimer, car je ne souhaite pas imposer mon avis qui est biaisé. D'autre part, ça n'est pas parce que c'est dans le All that que c'est forcément parfait. Je note que la version anglaise de Wikipédia n'a pas de pseudo-code et seulement des règles. Mais si cela permet à certains de mieux comprendre pourquoi pas? Mais ceux qui feront une implantation à partir de ce pseudo-code vont avoir des surprises, tant ce sera inefficace. --Pierre de Lyon (discuter) 19 mai 2016 à 13:54 (CEST)

C'est important de chipoter ǃ Je trouve la version anglaise très difficile pour un néophyte. Ensuite, j'ai bien rajouté dans l'article que c'est un algorithme NAÏF. Et implémenter un algorithme naïf est stupide. Aussi, j'ai gonflé un peu le texte donc le pseudo-code a vraiment moins d'intérêt. Effectivement, les autres contributeurs pourront trancher. Mon avis est très biaisé également. En tout cas, merci d'avoir bien signaler que cette "première" procédure est bien naïve.

Du coup, pour la suite de l'article ː

• Continuer à bien débattre avec les autres si on garde le pseudo-code (mais la section "Procédure naïve est importante pour moi)
• Continuer l'article sur des points plus spécialisés.

Bonne journée ǃ

--Fschwarzentruber (discuter) 19 mai 2016 à 13:59 (CEST)

Tâches restantes

Bonjour à tous, j'ai besoin de lister les tâches et j'ai vraiment besoin d'aide.

• Il faut expliquer mieux les règles. Ai-je bien raison quand je dis que les deux dernières règles (que j'ai séparé du tableau délibéremment) sont de l'optimisation. En tout cas, le "Terese" n'en parle pas. Le "all that" en parle. Si elles sont de l'optimisation. C'est bien de le dire. Il faut donc laisser le tableau bien séparé en deux pour que l'on voit bien que c'est "en plus" si on veut aller plus vite.
• Un exemple où ça boucle. Un exemple où ça termine. Est-ce que quelqu'un a un exemple NON LOURDINGUE ?
• Parler de la vraie vie et des implémentations. Pierre, est-ce que tu peux inscrire tes travaux autour du logiciel ORME et écrire un paragraphe dessus ? et d'autres logiciels encore si tu veux ? Et aussi pt autour des variantes ?
• Aussi si un spécialiste veut parler de la théorie des groupes et de réécriture de mots dans ce contexte (c'est fait dans l'article wikipedia anglais, donc pourquoi pas ?ǃ)
• Ensuite, il faut relire. Par exemple, il reste une phrase comme "Il existe une procédure de complétion améliorée qui n'échoue pas sur les identités non orientables" dans l'introduction. Je ne sais pas ce que c'est. Il n'y a pas de référence, pas de nom. Je ne sais pas de quoi ça parle.

On aura bientôt une page plutôt sympathique pour Knuth-Bendix ː)

PS ː aussi, l'outil http://cl-informatik.uibk.ac.at/software/kbcv/ est vraiment bien fait. C'est un peu austère mais c'est vraiment un bon début. Si vous avez d'autres outils, encore plus agréables, j'achète (fa̠çon de parler, bien sûr... jamais je ne débourserai un euro pour Knuth-Bendix) ː).

PS 2 ː le livre de R. Lalement donne une assez bonne introduction à Knuth-Bendix. Il sépare aussi les règles en deux paquets (les "basiques" puis l'optimisation). Je vais donc regarder cela. Il donne aussi une bonne traduction pour les noms des règles. --Fschwarzentruber (discuter) 19 mai 2016 à 23:36 (CEST)

Implémentations

Merci Pierre. Il n'existe pas "une" mais "des" variantes où il n'y a pas besoin de donner un ordre de réduction. Cependant, je préfère lorsqu'il y a des citations car cela permet de renvoyer le lecteur à des références. J'avais proposé ː . Je suis d'accord avec toi qu'il n'y a pas de raison d'en citer qu'une. Je pense par contre que le lecteur peut apprécier le fait d'en avoir plusieurs. Est-ce quelqu'un peut faire une liste raisonnable d'implémentation ? Pierre, c'est l'occasion peut-être de parler de ORME ? --Fschwarzentruber (discuter) 22 mai 2016 à 17:15 (CEST)

Titre de l'article

Je propose de renommer l'article en Complétion de Knuth-Bendix ou Complétion de Knuth et Bendix (à voir). Cela évitera les arguties entre « algorithme » ou « procédure ». Pour moi (et pour nombre de mes collègues), un algorithme est une procédure qui se termine, ce qui n'est évidemment pas le cas de la complétion.. --Pierre de Lyon (discuter) 25 mai 2016 à 11:33 (CEST)

Qui est Bendix ?

Une question, non scientifique, souvent posée est « Qui est et qu'est devenu Bendix? ». La réponse est là. Y répond-on dans l'article? --Pierre de Lyon (discuter) 25 mai 2016 à 11:44 (CEST)

Excellent ǃ Oui, on peut par exemple ajouter une section "Histoire" où on mentionne ça. On raconterait les diverses implémentations (pt du coup, supprimer la dernière section) et applications, etc.--Fschwarzentruber (discuter) 25 mai 2016 à 13:05 (CEST)

Nom français du rpo

J'ai toujours appelé en français le lpo ou lexicographic path ordering, l'« ordre lexicographique sur les les chemins ». D'où vient le terminologie « ordre chemin lexicographique » qui fait un peu bizarre ? --Pierre de Lyon (discuter) 26 mai 2016 à 07:45 (CEST)

Merci. J'ai modifié (j'avais mal traduit). PS ː rpo ? lpo ?--Fschwarzentruber (discuter) 26 mai 2016 à 08:06 (CEST)

Cà n'est qu'une proposition, en essayant de traduire ce que Dershowitz voulait dire quand il a créé le recursive path ordering. En fait, à vrai dire, je l'appelle le lpo. . --Pierre de Lyon (discuter) 27 mai 2016 à 08:21 (CEST)

La complétion réussit, échoue ou diverge

Le troisième cas est celui où la complétion diverge; elle en boucle pas. Elle ne peut pas boucler d'après le théorème de Huet. Dans mon cours j'utilise endomorphisme + associativité qui illustre sur le même exemple le trois cas. Je propose de le « recycler » ici. --Pierre de Lyon (discuter) 10 octobre 2017 à 21:19 (CEST)