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.

اخر الاخبار

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

قسم الإعلام يشارك في الاجتماع التحضيري لمناقشة الخطة الإعلامية لزيارة عاشوراء

بحضور متوليها الشرعي.. العتبة العباسية المقدسة تواصل إقامة المجالس الحسينية لإحياء شهر المحرم

قسم الشؤون الفكرية يطلق برنامجه التبليغي في أكثر من 20 دولة إفريقية

شعبتا الخطابة النسوية والتوجيه الديني تواصلان إقامة المجالس الحسينية في مرقد أبي الفضل العباس (عليه السلام)

المزيد

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

دراسة تكشف علاقة خطيرة بين عمر الأم وصحة مولودها

دراسة تحذر.. اضطراب نوم بسيط قد يسبب الموت المبكر ؟

الاستحمام بالماء الساخن.. راحة مؤقتة وأضرار دائمة للبشرة

ماذا يحدث للجسم عند تخطي وجبة الإفطار؟

المزيد

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

كيف تساعد الصيانة الوقائية في الحفاظ على كفاءة التكييف في سيارتك ؟

في ظاهرة غريبة حيرت العلماء.. كوكبنا قد يسجل أقصر يوم في التاريخ هذا الصيف!

السد الصيني العملاق يعيق دوران الأرض ويغيّر شكلها ؟

السعودية تطلق 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