Knuth-Bendix Completion Algorithm

The Knuth-Bendix completion algorithm attempts to transform a finite set of identities into a finitely terminating, confluent term rewriting system whose reductions preserve identity. This term rewriting system serves a decision procedure for validating identities.

As defined in universal algebra, identities are equalities of two terms: . Presumably, the values of the two terms are equal for all values of variables occurring in them. A reduction order is another input to the completion algorithm provided that every identity is viewed as two candidates for rewrite rules transforming the left-hand side into the right-hand side and vice versa.

The output term rewriting system is used to determine whether  is an identity or not in the following manner. If two distinct terms  and  have the same normal form, then  is an identity. Otherwise,  is not an identity. Term rewriting systems that are both finitely terminating and confluent enjoy the property of having unique normal forms for all expressions. The problem of deciding whether  is an identity is also known as the word problem.

Initially, this algorithm attempts to orient input identities according to the reduction order (if, then  becomes a rule). Then, it completes this initial set of rules with derived ones. The algorithm iteratively detects critical pairs, obtains their normal forms, and adds a new rule for every pair of the normal forms in accordance with the reduction order.

This algorithm may

1. Terminate with success and yield a finitely terminating, confluent set of rules,

2. Terminate with failure, or

3. Loop without terminating.

Note that Buchberger's algorithm for constructing Gröbner bases is very similar to the Knuth-Bendix completion algorithm.

---

REFERENCES

Baader, F. and Nipkow, T. Term Rewriting and All That. Cambridge, England: Cambridge University Press, 1999.

Knuth D. E. and Bendix P. B. "Simple Word Problems in Universal Algebra." In Computational Problems in Abstract Algebra (Proc. Conf., Oxford, 1967).

 Pergamon Press, pp. 263-297, 1970.Wolfram, S. A New Kind of Science. Champaign, IL: Wolfram Media, p. 1037, 2002.

اخر الاخبار

اخبار العتبة العباسية المقدسة

قسم صناعة الشبابيك يستعرض أعماله للمشاركين في البرنامج المركزي الأسبوعي

جامعة الكفيل تنظم حملة للتبرع بالدم للأطفال المصابين بالثلاسيميا والأورام السرطانية

قسم الشؤون الفكرية يصدر العدد 55 من مجلة العميد المحكمة

المجمع العلمي يجري اختبار القبول للمتقدمين إلى دورة ربيع القرآن في كربلاء

المزيد

الآخبار الصحية

كنز غذائي على طبقك.. ماذا تفعل السبانخ بجسمك؟

ما لا يتوقعه أحد.. "سر غذائي" في الجبن الدسم

لتحسين الهضم والنوم.. هذا أفضل وقت لتناول العشاء

10 طرق بسيطة وغير مألوفة لحرق المزيد من السعرات يوميا

المزيد

الآخبار التكنلوجية

سابقة بعالم الطيران.. طائرة تقرر الهبوط بنفسها بعد ظرف طارئ

"الإنفلونزا الخارقة" تكتسح دول العالم.. وتثير قلقا كبيرا

مرحلة ما قبل الأعراض.. دواء جديد يستهدف "شرارة" الزهايمر

إزالة ثاني أكسيد الكربون من الغلاف الجوي.. ما دور المحيطات والبحار؟

المزيد

مواضيع ذات صلة

Lemma

Proof

Zeno,s Paradoxes

Unexpected Hanging Paradox

Strange Loop

Sorites Paradox

Simpson,s Paradox

Russell,s Antinomy

Paradox

Newcomb,s Paradox

Missing Dollar Paradox

Line Point Picking