Termination Analysis of Linear-Constraint Programs

ملخص تقني: تحليل الإنهاء للبرامج ذات القيود الخطية

بيان المشكلة
يتناول هذا الاستقصاء مشكلة الإنهاء (termination problem) للبرامج ذات المتغيرات العددية (الأعداد الصحيحة، أو النسبية، أو الحقيقية) حيث تُعرَّف الانتقالات بواسطة قيود خطية. يكمن التحدي الجوهري في عدم القابلية للتقرير (undecidability) المتأصلة في مشكلة الإنهاء العامة لهذه الأنظمة. يستكشف البحث بشكل منهجي حدود القابلية للتقرير، وتعقيد المسائل الفرعية المحددة، والتقنيات الخوارزمية المستخدمة لإثبات الإنهاء أو عدم الإنهاء. يقتصر النطاق على البرامج ذات القيود الخطية، مستبعدًًا الحسابات غير الخطية، والاختيارات الاحتمالية، وأنظمة إعادة كتابة المصطلحات (term rewriting systems). يغطي التحليل ثلاثة نماذج برمجية رئيسية:

1. حلقات المسار الواحد الخطية ذات الشكل الأفيني (SLC): حلقات ذات مسار تحكم واحد وتحديثات أفينية ($x' = Ax + c$).
2. حلقات SLC العامة: حلقات ذات قيود خطية في الشروط (guards) والتحديثات، وقد تكون غير أفينية.
3. حلقات المسارات المتعددة (MLC) والرسوم البيانية لتدفق التحكم (CFGs): برامج تحتوي على منطق التفرع، وتُنمذج كأطقم من متعددات السطوح الانتقالية (transition polyhedra).

المنهجية والإطار العملي
ينظم البحث هذا المجال ضمن أربعة ركائز منهجية أساسية: نتائج القابلية للتقرير، دوال التصنيف (ranking functions)، ثوابت الانتقال (transition invariants)، وشواهد عدم الإنهاء (non-termination witnesses).

• تحليل القابلية للتقرير: يميز المؤلفون بين الإنهاء عبر نطاقات مختلفة ($\mathbb{R}, \mathbb{Q}, \mathbb{Z}$). وتتمثل التقنية الرئيسية في اختزال مشكلة الإنهاء إلى وجود نقاط "يحتمل عدم إنهائها" ضمن مجموعة شبه جبرية محدبة ($P_N$). بالنسبة لحلقات SLC الأفينية، يعتمد ذلك على التحليل الطيفي لمصفوفة التحديث (القيم والناقلات الذاتية)، ونظرية كرونيكر للتقريب الديوفانتي المتزامن، ونظرية التسطيح (Flatness Theorem) للشبكات الصحيحة.
• دوال التصنيف: يفصل الاستقصاء عملية تخليق الدوال التي تربط حالات البرنامج بنطاق جيد الترتيب (well-founded domain)، مما يضمن تناقصًا صارمًا مع كل انتقال.
  • دوال التصنيف الخطية (LRFs): دوال أفينية $\rho(x) = \vec{\lambda}x + \lambda_0$ تتناقص بمقدار 1 على الأقل. غالبًا ما يتم اختزال التخليق إلى البرمجة الخطية (LP) باستخدام لمة فاركاس (Farkas' Lemma).
  • دوال التصنيف الخطية اللكسيكوغرافية (LLRFs): هي عبارة عن صفوف من الدوال الخطية $\langle \rho_1, \dots, \rho_d \rangle$ تتناقص لكسيكوغرافياً. يستعرض البحث متغيرات محددة (BG-LLRFs, ADFG-LLRFs, BMS-LLRFs, M$\Phi$RFs) وخوارزميات تخليقها، والتي غالبًا ما تعتمد على استراتيجيات جشعة أو مناهج قائمة على القوالب باستخدام أدوات حل المعادلات (SMT solvers).
• ثوابت الانتقال: بديل لدوال التصنيف، باستخدام ثوابت الانتقال ذات الترتيب الجيد المنفصل (DTIs). هذا النهج، المتجذر في نظرية رامزي، يقسم إثبات الإنهاء إلى إثباتات فرعية لدورات مختلفة، ويشمل تقنيات مثل إنهاء تغيير الحجم (Size-Change Termination - SCT) وقيود الرتابة (Monotonicity Constraints).
• شواهد عدم الإنهاء: لإثبات أن البرنامج لا يتوقف، يناقش البحث المجموعات المتكررة (recurrent sets) (مجموعات الحالات التي يمكن للبرنامج من خلالها الدخول في حلقات لانهائية)، والمجموعات المتكررة الرتيبة للانتقالات، والحجج الهندسية لعدم الإنهاء (GNTAs)، والتي تصف التنفيذات اللانهائية ذات أنماط النمو الهندسي.

المساهمات والنتائج الرئيسية

1. قابلية التقرير لحلقات SLC الأفينية: يقدم البحث إطارًا موحدًا (بناءً على Hosseini et al., 2019) يثبت أن الإنهاء لحلقات SLC الأفينية هو قابل للتقرير عبر $\mathbb{R}$ و $\mathbb{Q}$ و $\mathbb{Z}$. تتضمن الإجراءات حساب مجموعة النقاط التي يحتمل عدم إنهائها والتحقق من وجود نقطة في النطاق المعني. التعقيد يكون أسيًا بالنسبة لحجم المدخلات.
2. نتائج عدم القابلية للتقرير:
   • إن الإنهاء لحلقات MLC العامة هو غير قابل للتقرير عبر $\mathbb{Z}, \mathbb{Q},$ و $\mathbb{R}$، حتى بالنسبة للحلقات الحتمية ذات عدد قليل من المسارات (قابلة للاختزال من الآلات العدادية/counter machines).
   • الإنهاء لحلقات SLC ذات المعاملات غير النسبية هو غير قابل للتقرير عبر الأعداد الصحيحة.
   • تظل قابلية تقرير الإنهاء لحلقات SLC العامة (ذات المعاملات النسبية) مشكلة مفتوحة كبرى.
3. تعقيد دوال التصنيف:
   • دوال LRFs: تحديد وجود LRF لحلقات SLC النسبية يقع ضمن فئة PTIME. بالنسبة لحلقات SLC الصحيحة، الأمر هو coNP-complete. أما بالنسبة لحلقات MLC و CFGs، فإن التعقيد يزداد بشكل كبير (PSPACE-hard للنسبية، و Ackermann-hard للصحيحة مع حالات ابتدائية).
   • دوال LLRFs: يقدم البحث تحليلًا شاملًا للتعقيد لمختلف متغيرات LLRF. على سبيل المثال، إيجاد BG-LLRF لحلقات MLC النسبية هو PTIME، بينما بالنسبة لحلقات MLC الصحيحة، يكون EXPTIME (أو coNP-complete اعتمادًا على المتغير المحدد والقيود).
4. تخليق عدم الإنهاء:
   • يفصل البحث خوارزميات لتخليق الحجج الهندسية لعدم الإنهاء (GNTAs) لحلقات SLC، وهي كاملة للحلقات الأفينية ذات القيم الذاتية الحقيقية غير السالبة.
   • يناقش المجموعات المتكررة الرتيبة وعلاقتها بفشل تخليق دوال التصنيف متعددة المراحل (multiphase ranking functions).
   • تشمل التقنيات الخاصة بالرسوم البيﺔ لتدفق التحكم (CFGs) تعداد حلقة اللاسو (lasso loop)، والثوابت شبه المستقرة (quasi-invariants)، وتسريع الحلقة (loop acceleration) (Frohn and Giesl)، والتي تسمح بإثبات عدم الإنهاء عن طريق تسريع تكرارات الحلقة إلى قيد معلمي (parameterized constraint).

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

يصرح المؤلفون صراحةً بأن الاستقصاء لا يغطي:

• تفاصيل التنفيذ في لغات البرمجة الواقعية.
• الحسابات غير الخطية، أو الاختيار الاحتمالي، أو إعادة كتابة المصطلحات.
• الحلول التجريبية أو الجزئية التي تفتقر إلى ضمانات الاكتمال النظرية.

المسائل المفتوحة
يختتم الاستقصاء بسرد 16 مسألة مفتوحة، مؤكدًا أن المجال لا يزال بعيدًا عن الاستقرار. تشمل الأسئلة الرئيسية المفتوحة ما يلي:

• قابلية تقرير الإنهاء لحلقات SLC العامة (النسبية/الصحيحة).
• قابلية تقرير الإنهاء لحلقات SLC الأفينية فيما يتعلق بحالات ابتدائية محددة (مرتبط بمسألة الإيجابية لمتتاليات التكرار الخطي).
• وجود خوارزميات كاملة لتخليق دوال M$\Phi$RF دون حدود للعمق.
• ما إذا كانت المجموعات المتكررة متعددة السطوح كافية لإثبات عدم الإنهاء لجميع حلقات SLC غير المنتهية.
• تعقيد إيجاد دوال LLRF ذات الحد الأدنى من العمق.

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