Unifying Semantic Path Order and Weighted Path Order

المشكلة
تُعد ترتيبات المسار الدلالي الرتيبة (MSPOs) وترتيبات المسار الموزونة (WPOs) ترتيبات اختزال قوية ومستقرة تُستخدم لإثبات إنهاء أنظمة إعادة الكتابة الطرفية (TRSs). وبينما كلاهما فعال، فقد تم التعامل معهما تاريخيًا كنهجين متميزين. أظهرت الأعمال السابقة أن WPOs هي حالات خاصة من MSPOs، ولكن لم يتم صياغة إطار عمل موحد يعامل MSPOs كحالات من WPO معمّم، مع الحفاظ على الخصائص المرغوبة لكل منهما، بشكل كامل. علاوة على ذلك، تعاني البناءات الحالية من صعوبة في تحقيق الإجمال الأرضي (ground totality) - وهو أمر بالغ الأهمية في إثبات النظريات - وفي نفس الوقت تحقيق آليات مقارنة فعالة عبر مختلف السياقات الجبرية وتوجهات الأسبقية (precedence-based settings).

المنهجية
يقترح المؤلفون توحيد هذه الترتيبات من خلال تقديم "ترتيب المسار الموزون المعمم" (GWPO) ونظيره الرتيب "ترتيب المسار الموزون المعمم الرتيب" (MGWPO).

1. البنية التأسيسية: يُبنى جوهر الترتيب الموحد على "ثلاثيات الاختزال" (reduction triples) $(\geq, \succeq, \succ)$، والتي أُدخلت أصلاً لـ MSPOs. تتكون ثلاثية الاختزال من ترتيب مسبق لإعادة الكتابة $\geq$، وزوج ترتيب مستقر $(\succeq, \succ)$ حيث يكون $\succ$ رتيبًا (well-founded)، وشرط تناغم يربط بين الترتيب المسبق وزوج الترتيب.
2. تعريف GWPO: يتم تعريف GWPO ($>_G$) باستخدام زوجين من العلاقات، $(\succeq_A, \succ_A)$ و $(\succeq_B, \succ_B)$. يكون المصطلح $s$ أكبر من $t$ إذا كان:
   • $s \succ_A t$، أو
   • $s \succeq_A t$ وتحقق شروط تكرارية محددة تتعلق بالكلمات الفرعية والمقارنات المعجمية، مع إمكانية استخدام الزوج الثاني $(\succeq_B, \succ_B)$ لمزيد من المقارنة.
3. الرتابة: لضمان أن الترتيب مغلق تحت السياقات (وهو متطلب لترتيبات الاختزال)، يتم تعريف MGWPO ($>_{MG}$) كتقاطع $\geq_A \cap \geq_B \cap >_G$.
4. أزواج الاختزال: يتم توسيع الإطار ليشمل "أزواج الاختزال" $(\geq, >)$ التي تتضمن "حالات جزئية" ($\pi$). يسمح هذا بمعالجة أكثر مرونة لمعاملات الدوال، مما يعمم نهج WPO القياسي.
5. منطق التوحيد:
   • WPO كـ MGWPO: يُظهر أن WPO القياسي هو حالة من MGWPO حيث يتم استقراء الثلاثية $A$ من جبر بسيط ضعيف، والثلاثية $B$ مستمدة من أسبقية (precedence).
   • MSPO كـ MGWPO: يُظهر أن MSPO هو حالة من MGWPO حيث تكون الثلاثية $A$ تافهة والثلاثية $B$ تقابل ثلاثية الاختزال الخاصة بـ MSPO. وعلى العكس من ذلك، يثبت المؤلفون أن أي MGWPO يمكن تمثيله كـ MSPO عن طريق بناء تركيب معجمي محدد للثلاثيات الأساسية.

المساهمات الرئيسية

• التعميم: يقدم البحث GWPOs و MGWPOs، موضحًا أن كل من MSPOs و WPOs هي حالات محددة من هذا الإطار المعمم.
• الإجمال الأرضي (Ground Totality): يحدد المؤلفون أن بينما تدعم WPOs الإجمال الأرضي بشكل طبيعي (مقارنة أي مصطلحين أرضيين متميزين)، فإن MSPOs لا تفعل ذلك. يسمح إطار MGWPO ببناء ترتيبات اختزال "إجمالية أرضيًا"، والتي يمكنها توجيه المعادلات (مثل combinators S و K) التي كان من الصعب التعامل معها باستخدام البناءات الحالية.
• التحسين: يوفر الترتيب الموحد تحسينًا للمقارنة؛ فإذا تم اكتشاف انخفاض صارم عبر المكون الأول ($\succ_A$)، تنتهي المقارنة فورًا دون فحوصات تكرارية. وهذا يحاكي كفاءة ترتيب كنوت-بينديكس (KBO) بدلاً من ترتيب المسار المعجمي (LPO).
• تحسين التعقيد: من خلال فرض خاصية "الكلمة الفرعية" (subterm property) على الترتيب الصارم $\succ_A$، يستنتج المؤلفون إجراءً لتقرير مقارنات MGWPO في زمن خطي بالنسبة لحجم المصطلحات (مقاسًا بعدد مقارنات العلاقات الأساسية)، مما يحسن من التعقيد الزمني الذي عادة ما يكون تربيعيًا في تعريفات شبيهة بـ LPO.
• توحيد أزواج الاختزال: يوسع البحث هذه النتائج لتشمل أزواج الاختزال ذات الحالات الجزئية، مُثبتًا إمكانية توحيد MGWPOs و MSPOs في هذا السياق أيضًا، بشرط استيفاء شروط بسيطة محددة.

النتائج
قام المؤلفون بتنفيذ نموذج أولي لأداة إنهاء تعتمد على طريقة أزواج التبعية باستخدام أزواج الاختزال المقترحة. أُجري التقييم على 1,528 نظامًا طرفيًا نهائيًا (finite TRSs) من قاعدة بيانات مشكلات الإنهاء (TPDB) مع حد زمني قدره دقيقة واحدة.

• الأداء: أثبت تكوين GWPO إنهاء 591 نظامًا، بينما أثبت تكوين SPO (الترتيب المساري الدلالي) 595 نظامًا، مقارنة بـ 486 لنظام WPO القياسي.
• المقارنة: حلت التكوينات مجموعات مختلفة من المشكلات. كان تكوين SPO قادرًا على حل المشكلات التي لا يكون فيها المكون الجبري "بسيطًا ضعيفًا" فيما يتعلق بالحالة الجزئية، وهو شرط مطلوب لـ GWPO.
• حالة الفن (State-of-the-Art): يشير المؤلفون إلى أنه بينما تثبت أساليبهم حالات إنهاء أكثر من WPO القياسي، فإن كل مشكلة حلتها أداتهم قد حلتها أيضًا أدوات مثل AProVE أو NaTT. وبناءً على ذلك، لا يدعي المؤلفون حل مشكلات جديدة كانت غير قابلة للحل سابقًا، بل استعرضوا التوحيد النظري ومكاسب الكفاءة المحددة لمنهجهم.

الأهمية
يدعي البحث أهميته بشكل أساسي في التوحيد النظري لفئتين رئيسيتين من ترتيبات الاختزال. ومن خلال إثبات أن MSPOs هي حالات من GWPOs (والعكس بالعكس)، يوفر هذا العمل إطارًا واحدًا يرث الخصائص المرغوبة من كليهما:

1. يتيح بناء ترتيبات إجمالية أرضيًا، وهي ميزة حاسمة لطرق حساب التفوق (superposition calculus)، والتي لم تكن متاحة بشكل طبيعي لـ MSPOs.
2. يقدم آلية لتحسين المقارنة عبر تجنب الفحوصات التكرارية عند العثور على انخفاض صارم في المكون الجبري الأساسي، مما قد يؤدي إلى تعقيد زمني خطي في سياقات معينة.
3. يوضح العلاقة بين التفسيرات الجبرية والترتيبات القائمة على الأسبقية، متتبعًا هذه الروابط إلى ملاحظات سابقة تتعلق بترتيب كنوت-بينديكس والترتيبات المسارية الدلالية.

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