خوارزمية إكمال كنوت-بنديكس

الموسوعة الحرة

خوارزمية إكمال كنوت-بنديكس (نسبةً إلى دونالد كنوت وبيتر بنديكس [ 1 ] ) هي خوارزمية شبه قرار [ 2 ] [ 3 ] لتحويل مجموعة من المعادلات (على مستوى الحدود ) إلى نظام إعادة كتابة حدود متقاربة . عندما تنجح الخوارزمية، فإنها تحل فعليًا مسألة الكلمات للجبر المحدد .

تُعدّ خوارزمية بوخبيرغر لحساب قواعد غروبنر خوارزميةً مشابهةً جدًا. ورغم تطويرها بشكلٍ مستقل، إلا أنه يُمكن اعتبارها أيضًا تجسيدًا لخوارزمية كنوت-بنديكس في نظرية حلقات كثيرات الحدود .

مقدمة

بالنسبة لمجموعة المعادلات E ، فإن إغلاقها الاستنتاجي ( ⁎ ⟷ E ) هو مجموعة جميع المعادلات التي يمكن استنتاجها بتطبيق المعادلات من E بأي ترتيب. رسميًا، تُعتبر E علاقة ثنائية ، و( ⟶ E ) هو إغلاق إعادة كتابتها ، و( ⁎ ⟷ E ) هو إغلاق التكافؤ لـ( ⟶ E ). بالنسبة لمجموعة قواعد إعادة الكتابة R ، فإن إغلاقها الاستنتاجي ( ⁎ ⟶ R ∘ ⁎ ⟵ R ) هو مجموعة جميع المعادلات التي يمكن التحقق منها بتطبيق القواعد من R من اليسار إلى اليمين على كلا الطرفين حتى تصبح متساوية تمامًا. بشكل رسمي، يُنظر إلى R مرة أخرى على أنها علاقة ثنائية، و ( ⟶ R ) هي إغلاق إعادة الكتابة الخاص بها، و( ⟵ R ) هي عكسها ، و( ⁎⟶ R ∘ ⁎⟵ R ) هي تركيب العلاقة لإغلاقاتها المتعدية الانعكاسية ( ⁎⟶ R و⁎⟵ R ) .

على سبيل المثال، إذا كانت E = {1⋅ x = x , x −1 ⋅ x = 1, ( x ⋅ y )⋅ z = x ⋅( y ⋅ z )} هي بديهيات المجموعة ، فإن سلسلة الاشتقاق

a −1 ⋅( a ⋅ b ) ⁎ ⟷ E ( a −1 ⋅ a )⋅ b ⁎ ⟷ E 1⋅ b ⁎ ⟷ E b      

يوضح ذلك أن a −1 ⋅( a ⋅ b ) ⁎ ⟷ E b هو عنصر من الإغلاق الاستنتاجي لـ E. إذا كانت R = { 1⋅ x → x , x −1 ⋅ x → 1, ( x ⋅ y )⋅ z → x ⋅( y ⋅ z ) } هي نسخة "قاعدة إعادة كتابة" من E ، فإن سلاسل الاشتقاق

( a −1 ⋅ a )⋅ b * ⟶ R 1⋅ b * ⟶ R b و b * ⟵ R b            

أثبت أن ( a⁻¹ ⋅ a ) ⋅ b * ⟶ R ∘ * ⟵ Rb عنصر من عناصر الإغلاق الاستنتاجي لـ R. مع ذلك، لا توجد طريقة لاستنتاج a⁻¹ ⋅ ( a ⋅ b ) * ⟶ R ∘ * ⟵ Rb بنفس الطريقة المذكورة أعلاه، لأن تطبيق القاعدة ( x ⋅ y ) ⋅ z → x ⋅ ( y ⋅ z ) من اليمين إلى اليسار غير مسموح به.

تأخذ خوارزمية كنوت-بنديكس مجموعة E من المعادلات بين الحدود ، وترتيب اختزال (>) على مجموعة جميع الحدود، وتحاول بناء نظام إعادة كتابة حدود متقارب ومنتهٍ R له نفس الإغلاق الاستنتاجي لـ E. في حين أن إثبات النتائج من E غالبًا ما يتطلب حدسًا بشريًا، فإن إثبات النتائج من R لا يتطلب ذلك. لمزيد من التفاصيل، انظر Confluence (abstract rewriting)#Motivating examples ، الذي يقدم مثالًا على برهان من نظرية الزمر، تم إجراؤه باستخدام كل من E و R.

قواعد

بفرض وجود مجموعة E من المعادلات بين الحدود ، يمكن استخدام قواعد الاستدلال التالية لتحويلها إلى نظام إعادة كتابة حدود متقارب مكافئ (إن أمكن): [ 4 ] [ 5 ] وهي تستند إلى ترتيب اختزال (>) يحدده المستخدم على مجموعة جميع الحدود؛ ويتم رفعه إلى ترتيب مؤسس جيدًا (▻) على مجموعة قواعد إعادة الكتابة بتعريف ( s → t ) ▻ ( l → r ) إذا

يمسح‹ E ∪{ s = s } ، ر  ›⊢‹ E ، ر  ›
تأليف    ‹ E ، R ∪{ s → t }  ›    ⊢     ‹ E ، R ∪{ s → u }  ›    إذا كان t ⟶ R u
بسّط‹ E ∪{ s = t } ، ر  ›⊢‹ E ∪{ s = u } ، ر  ›إذا كان t ⟶ R u
شرق‹ E ∪{ s = t } ، ر  ›⊢‹ E ، R ∪{ s → t }  ›إذا كانت s > t
ينهار‹ E ، R ∪{ s → t }  ›⊢‹ E ∪{ u = t } ، ر  ›إذا كان s ⟶ R u بواسطة l → r مع ( s → t ) ▻ ( l → r )
استنتج‹ E ، ر  ›⊢‹ E ∪{ s = t } ، ر  ›إذا كان ( s , t ) زوجًا حرجًا من R

مثال

يحسب المثال التالي، المُستخلص من مُثبت نظرية E ، إكمال بديهيات المجموعة (الجمعية) كما ورد في كتاب كنوت وبنديكس (1970). يبدأ المثال بالمعادلات الثلاث الأولية للمجموعة (العنصر المحايد 0، العناصر المعكوسة، التجميعية)، باستخدام f(X,Y)X + Y و − i(X)X. تُشكل المعادلات العشر المميزة بنجمة نظام إعادة الكتابة المتقارب الناتج. "pm" اختصار لـ " paramodulation "، وهو يُنفذ عملية الاستنتاج . يُعد حساب الزوج الحرج مثالًا على paramodulation لبنود الوحدة المعادلة. "rw" هو إعادة الكتابة، حيث يُنفذ عمليات التركيب والدمج والتبسيط . يتم توجيه المعادلات ضمنيًا دون تسجيل.

رقمالجانب الأيسرالجانب الأيمنمصدر
1:*f(X,0)=Xinitial("GROUP.lop", at_line_9_column_1)
2:*f(X,i(X))=0initial("GROUP.lop", at_line_12_column_1)
3:*f(f(X,Y),Z)=f(X,f(Y,Z))initial("GROUP.lop", at_line_15_column_1)
5:f(X,Y)=f(X,f(0,Y))pm(3,1)
6:f(X,f(Y,i(f(X,Y))))=0pm(2,3)
7:f(0,Y)=f(X,f(i(X),Y))pm(3,2)
27:f(X,0)=f(0,i(i(X)))pm(7,2)
36:X=f(0,i(i(X)))rw(27,1)
46:f(X,Y)=f(X,i(i(Y)))pm(5,36)
52:*f(0,X)=Xrw(36,46)
60:*i(0)=0pm(2,52)
63:i(i(X))=f(0,X)pm(46,52)
64:*f(X,f(i(X),Y))=Yrw(7,52)
67:*i(i(X))=Xrw(63,52)
74:*f(i(X),X)=0pm(2,67)
79:f(0,Y)=f(i(X),f(X,Y))pm(3,74)
83:*Y=f(i(X),f(X,Y))rw(79,52)
134:f(i(X),0)=f(Y,i(f(X,Y)))pm(83,6)
151:i(X)=f(Y,i(f(X,Y)))rw(134,1)
165:*f(i(X),i(Y))=i(f(Y,X))pm(83,151)

انظر أيضًا إلى المسألة اللفظية (الرياضيات) لعرض آخر لهذا المثال.

أنظمة إعادة كتابة السلاسل في نظرية الزمر

تُعدّ أنظمة إعادة كتابة السلاسل حالةً مهمةً في نظرية الزمر الحاسوبية، حيث يمكن استخدامها لإعطاء تسمياتٍ معياريةٍ لعناصر أو مجموعاتٍ مشتركةٍ لزمرةٍ معروضةٍ بشكلٍ منتهٍ كحاصل ضربٍ للمولدات . وتُشكّل هذه الحالة الخاصة محور هذا القسم.

الدافع في نظرية الجماعة

تنصّ مبرهنة الزوج الحرج على أن نظام إعادة كتابة المصطلحات يكون متقاربًا محليًا (أو متقاربًا ضعيفًا) إذا وفقط إذا كانت جميع أزواجه الحرجة متقاربة. علاوة على ذلك، لدينا مبرهنة نيومان التي تنص على أنه إذا كان نظام إعادة الكتابة (المجرد) مُعَيِّرًا بقوة ومتقاربًا ضعيفًا، فإن نظام إعادة الكتابة يكون متقاربًا. لذا، إذا استطعنا إضافة قواعد إلى نظام إعادة كتابة المصطلحات لإجبار جميع الأزواج الحرجة على التقارب مع الحفاظ على خاصية التعيير القوي، فإن هذا سيجبر نظام إعادة الكتابة الناتج على أن يكون متقاربًا.

لنفترض مونيدًا معروضًا بشكل محدودم=⟨X|R⟩{\displaystyle M=\langle X\mid R\rangle }حيث X مجموعة منتهية من المولدات، وR مجموعة من العلاقات المحددة على X. ولتكن X * مجموعة جميع الكلمات في X (أي الزمرة الحرة المولدة بواسطة X). بما أن العلاقات R تولد علاقة تكافؤ على X*، يمكن اعتبار عناصر M فئات التكافؤ لـ X * تحت R. لكل فئة {w1 , w2 , ...}، يُستحسن اختيار ممثل قياسي wk . يُسمى هذا الممثل بالصيغة القانونية أو الطبيعية لكل كلمة wk في الفئة. إذا وُجدت طريقة حسابية لتحديد صيغتها الطبيعية wi لكل wk ، فإن مسألة الكلمات تُحل بسهولة. يسمح نظام إعادة الكتابة المتقاربة بالقيام بذلك تحديدًا.

على الرغم من إمكانية اختيار الشكل القياسي نظريًا بشكل عشوائي، إلا أن هذا النهج غير قابل للحساب عمومًا. (ضع في اعتبارك أن علاقة التكافؤ في لغة ما يمكن أن تُنتج عددًا لا نهائيًا من الفئات اللانهائية). إذا كانت اللغة مُرتبة ترتيبًا جيدًا ، فإن الترتيب < يُوفر طريقة متسقة لتعريف الممثلين الأدنى، ومع ذلك، قد يظل حساب هؤلاء الممثلين غير ممكن. على وجه الخصوص، إذا تم استخدام نظام إعادة كتابة لحساب الممثلين الأدنى، فيجب أن يتمتع الترتيب < أيضًا بالخاصية التالية:

A < B → XAY < XBY لجميع الكلمات A، B، X، Y

تُسمى هذه الخاصية بثبات الإزاحة . ويُطلق على الترتيب الذي يكون ثابتًا في الإزاحة وترتيبًا جيدًا اسم ترتيب الاختزال .

انطلاقًا من عرض المونويد، يُمكن تعريف نظام إعادة كتابة مُعطى بالعلاقات R. إذا كان A × B ينتمي إلى R، فإن A  <  B، وفي هذه الحالة B  →  A قاعدة في نظام إعادة الكتابة، وإلا فإن A  >  B و A  →  B. بما أن < ترتيب اختزال، يُمكن اختزال كلمة مُعطاة W إلى W > W₁ > ... > Wₙ، حيث Wₙ غير قابلة للاختزال في نظام إعادة الكتابة. مع ذلك، اعتمادًا على القواعد المُطبقة عند كل Wᵢ →  Wᵢ₊₁  ، يُمكن الحصول على اختزالين غير قابلين للاختزال Wₙ ≠  Wₘ  للكلمة W. ولكن، إذا تم تحويل نظام إعادة الكتابة المُعطى بالعلاقات إلى نظام إعادة كتابة مُتلاقٍ باستخدام خوارزمية كنوت-بنديكس، فإن جميع الاختزالات تضمن إنتاج نفس الكلمة غير القابلة للاختزال، أي الشكل الطبيعي لتلك الكلمة.

وصف الخوارزمية الخاصة بالوحدات الأحادية ذات العرض المحدود

لنفترض أننا تلقينا عرضًا تقديميًا⟨X|R⟩{\displaystyle \langle X\mid R\rangle }، أينX{\displaystyle X}هي مجموعة من المولدات وR{\displaystyle R}هي مجموعة من العلاقات التي تُشكّل نظام إعادة الكتابة. لنفترض كذلك أن لدينا ترتيبًا اختزاليًا<{\displaystyle <}من بين الكلمات التي تم توليدها بواسطةX{\displaystyle X}(على سبيل المثال، ترتيب الكلمات المختصرة ). لكل علاقةPأنا=سؤالأنا{\displaystyle P_{i}=Q_{i}}فيR{\displaystyle R}، يفترضسؤالأنا<Pأنا{\displaystyle Q_{i}<P_{i}}وهكذا نبدأ بمجموعة الاختزالاتPأنا→سؤالأنا{\displaystyle P_{i}\rightarrow Q_{i}}.

أولاً، إذا كانت هناك أي علاقةPأنا=سؤالأنا{\displaystyle P_{i}=Q_{i}}يمكن تقليلها، استبدالهاPأنا{\displaystyle P_{i}}وسؤالأنا{\displaystyle Q_{i}}مع التخفيضات.

بعد ذلك، نضيف المزيد من الاختزالات (أي قواعد إعادة الكتابة) لإزالة الاستثناءات المحتملة للتقارب. لنفترض أنPأنا{\displaystyle P_{i}}وPج{\displaystyle P_{j}}تداخل.

  1. الحالة 1: إما البادئة منPأنا{\displaystyle P_{i}}يساوي لاحقةPج{\displaystyle P_{j}}أو العكس. في الحالة الأولى، يمكننا أن نكتبPأنا=بج{\displaystyle P_{i}=BC}وPج=أب{\displaystyle P_{j}=AB}في الحالة الأخيرة،Pأنا=أب{\displaystyle P_{i}=AB}وPج=بج{\displaystyle P_{j}=BC}.
  2. الحالة الثانية: إماPأنا{\displaystyle P_{i}}محصور بالكامل في (محاط بـ) Pج{\displaystyle P_{j}}أو العكس. في الحالة الأولى، يمكننا أن نكتبPأنا=ب{\displaystyle P_{i}=B}وPج=أبج{\displaystyle P_{j}=ABC}في الحالة الأخيرة،Pأنا=أبج{\displaystyle P_{i}=ABC}وPج=ب{\displaystyle P_{j}=B}.

اختصر الكلمةأبج{\displaystyle ABC}استخدامPأنا{\displaystyle P_{i}}أولاً، ثم باستخدامPج{\displaystyle P_{j}}أولاً. اتصل بالنتائجر1،ر2{\displaystyle r_{1},r_{2}}، على التوالي. إذار1≠ر2{\displaystyle r_{1}\neq r_{2}}إذن، لدينا حالة قد يفشل فيها Confluence. لذا، أضف عملية الاختزال.الأعلىر1،ر2→مينر1،ر2{\displaystyle \max r_{1},r_{2}\rightarrow \min r_{1},r_{2}}لR{\displaystyle R}.

بعد إضافة قاعدة إلىR{\displaystyle R}قم بإزالة أي قواعد فيR{\displaystyle R}والتي قد يكون لها جوانب يسارية قابلة للاختزال (بعد التحقق مما إذا كانت هذه القواعد تحتوي على أزواج حرجة مع قواعد أخرى).

كرر الإجراء حتى يتم فحص جميع الجوانب اليسرى المتداخلة.

أمثلة

مثال ختامي

لننظر إلى المونويد:

⟨x،y|x3=y3=(xy)3=1⟩{\displaystyle \langle x,y\mid x^{3}=y^{3}=(xy)^{3}=1\rangle }.

نستخدم ترتيب shortlex . هذا أحادي لانهائي، ومع ذلك، فإن خوارزمية Knuth–Bendix قادرة على حل مشكلة الكلمات.

وبالتالي فإن تخفيضاتنا الثلاثة الأولى هي

لاحقة منx3{\displaystyle x^{3}}(أيx{\displaystyle x}) هو بادئة لـ(xy)3=xyxyxy{\displaystyle (xy)^{3}=xyxyxy}لذا فكر في الكلمةx3yxyxy{\displaystyle x^{3}yxyxy}بالاختزال باستخدام ( 1 )، نحصل علىyxyxy{\displaystyle yxyxy}وباستخدام المعادلة ( 3 ) في عملية التبسيط، نحصل علىx2{\displaystyle x^{2}}ومن ثم، نحصل علىyxyxy=x2{\displaystyle yxyxy=x^{2}}، مما يعطي قاعدة الاختزال

وبالمثل، باستخدامxyxyxy3{\displaystyle xyxyxy^{3}}وبالاختزال باستخدام ( 2 ) و( 3 )، نحصل علىxyxyx=y2{\displaystyle xyxyx=y^{2}}ومن ثم التخفيض

كلا هاتين القاعدتين أصبحتا قديمتين ( 3 )، لذلك نقوم بإزالتها.

بعد ذلك، فكر فيx3yxyx{\displaystyle x^{3}yxyx}عن طريق تداخل ( 1 ) و( 5 ). بالتبسيط نحصل علىyxyx=x2y2{\displaystyle yxyx=x^{2}y^{2}}لذلك نضيف القاعدة

بالنظر إلىxyxyx3{\displaystyle xyxyx^{3}}بدمج ( 1 ) و( 5 )، نحصل علىxyxy=y2x2{\displaystyle xyxy=y^{2}x^{2}}لذلك نضيف القاعدة

هذه القواعد القديمة ( 4 ) و( 5 )، لذلك نقوم بإزالتها.

والآن، لم يتبق لنا سوى نظام إعادة الكتابة

بفحص تداخل هذه القواعد، لم نجد أي حالات فشل محتملة في الالتقاء. لذلك، لدينا نظام إعادة كتابة متقارب، وتنتهي الخوارزمية بنجاح.

مثال غير منتهٍ

قد يؤثر ترتيب المولدات بشكل حاسم على ما إذا كان إكمال كنوت-بنديكس سينتهي أم لا. على سبيل المثال، لننظر إلى المجموعة الأبيلية الحرة من خلال عرض المونويد:

⟨x،y،x-1،y-1|xy=yx،xx-1=x-1x=yy-1=y-1y=1⟩.{\displaystyle \langle x,y,x^{-1},y^{-1}\,|\,xy=yx,xx^{-1}=x^{-1}x=yy^{-1}=y^{-1}y=1\rangle .}

إكمال كنوت-بنديكس فيما يتعلق بالترتيب المعجميx<x-1<y<y-1{\displaystyle x<x^{-1}<y<y^{-1}}ينتهي بنظام متقارب، مع الأخذ في الاعتبار الترتيب المعجمي الطوليx<y<x-1<y-1{\displaystyle x<y<x^{-1}<y^{-1}}لا تنتهي العملية لعدم وجود أنظمة متقاربة محدودة متوافقة مع هذا الترتيب الأخير. [ 6 ]

التعميمات

إذا لم تنجح خوارزمية كنوت-بنديكس، فإما أنها ستستمر في العمل إلى ما لا نهاية، مُنتجةً تقريبات متتالية لنظام كامل لا نهائي، أو ستفشل عند مواجهة معادلة غير قابلة للتوجيه (أي معادلة لا يمكن تحويلها إلى قاعدة إعادة كتابة). أما النسخة المُحسّنة منها، فلن تفشل عند مواجهة المعادلات غير القابلة للتوجيه، وستُنتج نظامًا متقاربًا أساسيًا ، مُوفرةً بذلك شبه خوارزمية لمسألة الكلمات. [ 7 ]

يُتيح مفهوم إعادة الكتابة المُسجلة، الذي نُوقش في ورقة هيوورث ووينسلي المذكورة أدناه، تسجيل عملية إعادة الكتابة أثناء سيرها. وهذا مفيد لحساب العلاقات بين المجموعات عند عرضها.

مراجع

  1. ↑ د. كنوت، "نشأة قواعد السمات"
  2. ↑ جاكوب ت. شوارتز؛ دومينيكو كانتوني؛ يوجينيو ج. أوموديو؛ مارتن ديفيس (2011). المنطق الحسابي ونظرية المجموعات: تطبيق المنطق الرسمي على التحليل . سبرينغر ساينس آند بيزنس ميديا. ص  200. ISBN 978-0-85729-808-9.
  3. ↑ هسيانغ، ج.؛ روسينوفيتش، م. (1987). "حول مسائل الكلمات في النظريات المعادلاتية" (ملف PDF) . الأوتوماتا واللغات والبرمجة . سلسلة محاضرات في علوم الحاسوب. المجلد 267. ص 54. doi : 10.1007/3-540-18088-5_6 . ISBN   978-3-540-18088-3.، ص 55
  4. ↑ باخماير، ل.؛ ديرشوفيتز، ن.؛ هسيانغ، ج. (يونيو 1986). "ترتيبات البراهين المعادلة". وقائع ندوة IEEE حول المنطق في علوم الحاسوب . ص 346-357 . 
  5. ↑ ن. ديرشوفيتز؛ ج.-ب. جوانو (1990). جان فان ليوين (محرر). أنظمة إعادة الكتابة . دليل علوم الحاسوب النظرية. المجلد ب. إلسيفير. الصفحات 243-320 .  هنا: القسم 8.1، صفحة 293
  6. ↑ ف. ديكرت؛ أ. ج. دنكان؛ أ. ج. مياسنيكوف (2011). "أنظمة إعادة الكتابة الجيوديسية والمجموعات المسبقة". في: أوليغ بوغوبولسكي؛ إينا بوماجين؛ أولغا خارلامبوفيتش؛ إنريك فينتورا (محررون). نظرية المجموعات التوافقية والهندسية: مؤتمرات دورتموند وأوتاوا-مونتريال . سبرينغر ساينس آند بيزنس ميديا. ص 62. ISBN  978-3-7643-9911-5.
  7. ↑ باخماير، ليو؛ ديرشوفيتز، ناحوم؛ بلايستيد، ديفيد أ. (1989). "الإكمال دون فشل" (ملف PDF) . تقنيات إعادة الكتابة : 1-30 . doi : 10.1016/B978-0-12-046371-8.50007-9 . تاريخ الاسترجاع: 24 ديسمبر 2021 .