Discussion:Paire critique

Uniformisation des notations

Il faudrait uniformiser les notations entre Réécriture (informatique) et cet article. --Pierre de Lyon (discuter) 15 mai 2016 à 00:08 (CEST)

Merci pour tes reformulations dans l'article.

• Qui dit "se contracte en" pour "se réécrit en une étape" ? Je ne trouve pas de référence. As-tu une référence en français sous la main ?
• Pour l'uniformisation, on peut attendre que cela mûrisse. Je trouve les notations de l'article "réécriture" difficile à lire. Au lieu de r --> r', je préfère G --> D où g --> d, plus claires.
• Sinon, j'ai conscience que mes dessins ne sont pas forcément très très clairs mais je voulais éviter des notations trop lourdes.

Bonne soirée. --Fschwarzentruber (discuter) 15 mai 2016 à 20:47 (CEST)

Dans mes cours, je suivais l'habitude du lambda-calcul qui utilise "contraction" dans ce sens. En fait Dershowitz et Jouannaud utilisent "rewrite" pour une étape et "réductibilité" ou "dérivation" pour →*. De toute façon, on peut pas éviter les dessins, sinon ça devient incompréhensible. --Pierre de Lyon (discuter) 15 mai 2016 à 23:08 (CEST)

OK. Je ne suis pas un grand spécialiste de la réécriture. C'est moi qui avait écrit "t se réécrit en t1 en une étape". C'est plus clair mais plus long. Je ne sais pas si c'est bien d'utiliser le vocabulaire du lambda-calcul ici. Peut-être que oui. Mais pour moi, "rewrite" ("se réécrit en") est vague. On ne sait pas si c'est en une étape ou plusieurs. Et "se réécrit en une étape" c'est peut-être trop long... mais pas tant que cela. Compromis ː peut-être préciser dans la note en bas de page que l'on utiliser le vocabulaire du lambda-calcul ? (même si j'aurai préféré garder le vocabulaire propre à la réécriture je pense). On peut attendre que d'autres personnes réagissent car ce n'est pas urgent dans le sens où je trouve que l'article est compréhensible. En tout cas, merci. --Fschwarzentruber (discuter) 16 mai 2016 à 13:32 (CEST)

Le lambda-calcul est de la réécriture, mais ça n'est pas de la réécriture du premier ordre. Y a-t-il un vocabulaire propre à la réécriture du premier ordre. Soi c'est celui de Dershowitz et Jouannaud, me semble-t-il. --Pierre de Lyon (discuter) 16 mai 2016 à 21:57 (CEST)

Algorithme pour la confluence locale

Je vais sans doute prochainement ajouter un exemple où l'algorithme répond "oui" et un exemple où l'algorithme répond "non". Avez-vous des exemples jolis (et simples) ? --Fschwarzentruber (discuter) 16 mai 2016 à 14:39 (CEST)

Je suis en train de rédiger dans ma page de brouillon une section d'introduction à cet article où je développe un exemple, celui de l'axiomatique faible des groupes. Ça peut servir. --Pierre de Lyon (discuter) 16 mai 2016 à 21:40 (CEST)

Intéressant. Merci, super. ː) D'ailleurs, c'est pas plutôt pour la complétion de Knuth-Bendix ? --Fschwarzentruber (discuter) 16 mai 2016 à 23:33 (CEST)

Merci pour le super! . Oui je m'en rends bien compte, mais comment introduire les paires critiques sans parler de la complétion de Knuth-Bendix, qui demeure leur principale application et la raison pour laquelle le concept a été créé?

Je ne suis pas assez spécialiste pour avoir assez de recul. Mais mon avis est le suivant ː

• l'article "Paire critique" est un article "définition". L'objectif est dire ce que c'est avec un historique (donc parler de la complétion de Knuth-Bendix avec un renvoi vers l'article "complétion de Knuth-Bendix" c'est bien). Aussi vérifier la confluence locale c'est plus simple à comprendre que la complétion de Knuth-Bendix.
• L'article "complétion de Knuth-Bendix" décrit ce qu'est la procédure de complétion de Knuth-Bendix. Donc comme l'exemple que tu écris me semble plus parler de la complétion que des paires critiques, je le vois mieux là-bas.

Après... wikipedia est modifiable. Donc il n'y a pas de choix irréversibles. On fait, on essaie. De toute façon, personnellement, je dois me cultiver sur tous ces sujets. A bientôt. --Fschwarzentruber (discuter) 17 mai 2016 à 11:03 (CEST)

Il n'y a pas de concept d'« article définition » dans un encyclopédie. En effet, les lecteurs peuvent arriver sur un article par toutes sortes de chemins (non déteminisme « je m'en moque » ou confluence ), notamment en googlant. Cependant peut-être que dans le futur, quelqu'un déplacera cette section d'introduction intuitive vers la complétion KB et l'article paire critique reverra vers cette introduction. Mais pour l'instant, comme tu le dis, laissons en l'état et progressons. Ceci dit tes dessins sont très jolis. --Pierre de Lyon (discuter) 17 mai 2016 à 12:46 (CEST)