ملخص تقني: المنطق الديناميكي القضاياي يمتلك خاصية استكمال كرايغ

1. المشكلة

تتناول الورقة السؤال المفتوح طويل الأمد حول ما إذا كان المنطق الديناميكي القضاياي (PDL) يمتلك خاصية استكمال كرايغ (Craig Interpolation Property - CIP). تنص خاصية CIP على أنه لأي استلزام صحيح $\phi \to \psi$، يوجد مستكمل $\theta$ بحيث يكون $\phi \to \theta$ و $\theta \to \psi$ صحيحين، ويحتوي $\theta$ فقط على الحروف القضاياية والبرامج الذرية المشتركة بين كل من $\phi$ و $\psi$.

وعلى الرغم من أن PDL هو منطق جهوي (modal logic) مدروس جيداً وله نتائج مثبتة في قابلية التقرير (decidability) والاكتمال (completeness)، إلا أن وضع الاستكمال الخاص به ظل غير واضح لعقود. تحتوي الأدبيات على ثلاث محاولات سابقة لإثبات الاستكمال:

1. ليفانت (1981): ادعى وجود برهان، لكن كراخت (1999) فنده لأسباب غير صحيحة، رغم أن ثغرة حقيقية في برهان ليفانت لا تزال قائمة.
2. بورزيكوفسكي (1988): أطروحة ماجستير (Diplomarbeit) ادعت وجود برهان، ولم تحظَ باهتمام كبير وتم استبعادها من قبل البعض باعتبارها غير قابلة للتحقق.
3. كوالسكي (2002): ادعى وجود برهان، تم تفنيده وسحبه رسمياً في عام 2004.

تنشأ الصعوبة لأن PDL هو منطق نقطة ثابت جهوية (modal fixpoint logic) بسبب عامل التكرار ($*$). وبينما تم إثبات الاستكمال لمنطق $\mu$-calculus الكامل وللجزء الخالي من التناوب فيه باستخدام أنظمة البراهين الدورية، فإن القيود المحددة لـ PDL تجعل من الصعب ضمان أن الحلول لمعادلات النقطة الثابتة التي توصف المستكملات يمكن التعبير عنها داخل PDL نفسه، بدلاً من الحاجة إلى القدرة التعبيرية الكاملة لـ $\mu$-calculus.

2. المنهجية

يقدم المؤلفون برهاناً بنائياً يعتمد على نظام جدول (tableau) دوري وتكييف لطريقة مايهارا (Maehara's method).

2.1. نظام جدول دوري لـ PDL

يعرف المؤلفون نظام جدول جديد لـ PDL يعمل على المتتاليات المنقسمة (split sequents) (أزواج من مجموعات الصيغ). وتشمل الميزات الرئيسية:

• الاستدلال المحلي مقابل الجهوي: يميز النظام بين القواعد المحلية (الاستدلال القضاياي وفك البرامج داخل حالة واحدة) والقواعد الجهوية (الانتقال بين الحالات في نموذج كريبكي).
• آلية الفك (Unfolding Mechanism): بدلاً من قواعد الاختزال القياسية لكل باني برنامج، يستخدم النظام آلية "تحميل" (loading). يتم فك الصيغ من شكل $[\alpha]\psi$ (حيث $\alpha$ غير ذرية) إلى مجموعة محدودة من المتتاليات بناءً على "ملفات تعريف الاختبار" (test profiles). هذه المجموعة، ويرمز لها بـ $\text{unfold}_\square(\alpha, \psi)$، تمثل انفصال جميع مسارات التنفيذ الممكنة لـ $\alpha$ حيث تنجح اختبارات معينة أو تفشل.
• التعامل مع التكرار: لمنع الفك المحلي اللانهائي لصيغ مثل $[\alpha^*]\psi$، يقوم النظام بإزالة التكرارات المعاد توليدها أثناء عملية الفك. ويعتمد هذا على ملاحظة أن $[\alpha^*]\psi$ هي نقطة ثابتة عظمى.
• البراهين الدورية: يسمح النظام بـ "التكرارات" (عقد لها نفس العلامات لأسلافها).
  • تكرارات المسار المحمل (Loaded-path repeats): تكرار حيث يتكون المسار من السلف (الرفيق) إلى العقدة الحالية بالكامل من عقد محملة. تُعامل هذه كأوراق "ناجحة" (مما يشير إلى حلقة تحقق الصيغة).
  • التكرارات الحرة (Free repeats): تكرار حيث يحتوي المسار على عقد غير محملة. تُعامل هذه كأوراق "غير ناجحة"، مما يشير إلى نموذج مضاد محتمل.
• الإنهاء: يضمن النظام النهاية من خلال فرض أن جميع التكرارات الحرة وتكرارات المسار المحملة هي أوراق، ومن خلال استخدام إغلاق فيشر-لادرنر (Fischer-Ladner closure) لحصر مجموعة الصيغ.

2.2. الاستكمال عبر الجداول شبه الجداول (Quasi-Tableaux) ومعادلات النقطة الثابتة

لتكوين المستكمل، يكيف المؤلفون طريقة مايهارا مع الإعداد الدوري:

• العناقيد (Clusters): يُنظر إلى الجدول كرسوم بيانية ذات حواف خلفية من التكرارات إلى الرفاق. المكونات المتصلة بقوة (SCCs) لهذا الرسم البياني تسمى "عناقيد".
• الجداول شبه الجداول (Quasi-Tableaux): بالنسبة لعنقود مناسب (SCC غير أحادي)، يعرف المؤلفون "جدولاً شبه جدول". يُستخدم هذا الهيكل لإعداد نظام معادلات يصف المستكمل.
• المستكملات الأولية (Pre-interpolants): تعتمد الطريقة على تعريف "مستكملات أولية" للعقد في الجدول شبه الجدول عبر الاستقراء من الورقة إلى الجذر.
  • عند عقد الخروج (الأوراق التي ليست جزءاً من العنقود)، يكون المستكمل الأولي هو مستكمل عقدة الخروج (بافتراض وجوده بالاستقراء).
  • عند أوراق التكرار، يكون المستكمل الأولي هو متغير قضاياي داخلي $q_x$.
  • عند عقد الرفيق، يُعرف المستكمل الأولي كحل لمعادلة نقطة ثابتة. تحديداً، إذا كان للرفيق $x$ طفل $y$ بمستكمل أولي $\iota_y \equiv \bigwedge_i [\alpha_i]q_x \wedge \bigwedge_j [\beta_j]q_{z_j} \wedge \psi$، فإن المستمل الأولي لـ $x$ يُعرف بـ $\iota_x := [(\bigcup_i \alpha_i)^*](\bigwedge_j [\beta_j]q_{z_j} \wedge \psi)$.
• الحل في PDL: الرؤية الحاسمة هي أن هذا البناء المحدد يضمن أن حلول معادلات النقطة الثابتة تظل ضمن لغة PDL. إن استخدام عامل التكرار $*$ في تعريف $\iota_x$ يحل فعلياً المعادلة $\iota_x \equiv \iota_y\langle q_x \mapsto \iota_x \rangle$ داخل PDL.
• المستكمل النهائي: يتم الحصول على المستكمل لجذر العنقود عن طريق استبدال المتغيرات الداخلية في المستكمل الأولي للجذر بصيغ المنطقة المقابلة (انفصال الجوانب اليسرى للمتتاليات المنقسمة).

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

• إثبات CIP لـ PDL: تثبت الورقة أن PDL يمتلك خاصية استكمال كرايغ.
• قابلية تعريف بيث (Beth Definability): كاستنتاج، تثبت الورقة أن PDL يمتلك خاصية تعريف بيث (بما أن CIP تؤدي إلى تعريف بيث في وجود مبرهنة الاستنتاج).
• خوارزمية بنائية: البرهان بنائي. يقدم المؤلفون خوارزمية واضحة لحساب المستكملات من جدول مغلق.
• التحقق الرسمي: قام المؤلفون بتوثيق البرهان جزئياً في المثبت التفاعلي Lean 4. حتى وقت كتابة الورقة، تم التحقق من نظريات الصحة والاكتمال، بالإضافة إلى العديد من اللمات الداعمة.
• التنفيذ: يتوفر تنفيذ بلغة Haskell لنظام الجدول وبناء المستكمل، متاح عبر واجهة ويب.

4. الأهمية والادعاءات

تدعي الورقة حل لغز في الأدبيات يتعلق بوضع استكمال PDL، حيث تقدم أول برهان تم التحقق منه يتجاوز الثغرات في المحاولات السابقة.

• حل المشكلات التاريخية: يعالج المؤلفون صراحةً تاريخ المحاولات الفاشلة، مشيرين إلى أن نهجهم يبني على الأفكار الأساسية لبورزيكوفسكي (1988) ولكنه يصيغ معالجة البراهين الدورية وبناء المستكملات داخل لغة PDL بشكل صارم.
• الجدة المنهجية: تسلط الورقة الضوء على أنه بينما تعد طريقة مايهارا معيارية للبرهان غير الدوري، فإن تطبيقها على البراهين الدورية (منطق النقطة الثابتة) يتطلب حل معادلات النقطة الثابتة. يوضح المؤلفون أنه بالنسبة لـ PDL، يمكن التعبير عن هذه الحلول باستخدام عامل التكرار الخاص بالمنطق، وهي نتيجة غير بديهية تميز PDL عن أجزاء أخرى قد تتطلب حلولها $\mu$-calculus كاملاً.
• الأسئلة المفتوحة: يشير المؤلفون بتواضع إلى أن طريقتهم تعتمد على وجود برامج الاختبار ($\tau?$). وبالتالي، يظل سؤال مفتوحاً حول ما إذا كان الجزء الخالي من الاختبارات لـ PDL يمتلك الاستكمال، حيث ينتج بناؤهم عموماً مستكملات تحتوي على اختبارات حتى عندما تكون المدخلات خالية من الاختبارات. كما يتركون مفتوحاً توسيع طريقتهم إلى متغيرات أخرى من PDL (مثل تلك التي تحتوي على معكوس أو تقاطع) وتداعيات ذلك على جبر كليين مع الاختبارات (KAT).

باختالاف، تقدم الورقة برهاناً بنائياً نهائياً لاستكمال كرايغ لـ PDL باستخدام نظام جدول دوري جديد وتقنية متخصصة لحل النقطة الثابتة للمستكمل، مدعومة بتنفيذ بلغة Haskell وتحقق رسمي جزئي في Lean.