Mechanized Undecidability of Higher-order beta-Matching (Extended Version)

ملخص تقني: عدم قابلية التقرير الميكانيكية للمطابقة من الرتب العليا في نظام بيتا ($\beta$-matching)

بيان المشكلة
تتناول الورقة البحثية مسألة القرار الخاصة بالمطابقة من الرتب العليا لـ $\beta$ (higher-order $\beta$-matching) ضمن حساب $\lambda$ البسيط النوع (simply typed $\lambda$-calculus). بالنظر إلى حدين من حدود $\lambda$ بسيطة النوع، $F$ و $N$، حيث لا يحتوي $N$ على متغيرات حرة، تسأل المسألة عما إذا كان هناك حد $M$ بحيث يكون التطبيق $F M$ مكافئاً لـ $N$ بموجب $\beta$ ($\beta$-equivalent). وبينما تم إثبات عدم قابلية التقرير لتوحيد $\beta$ من الرتب العليا (higher-order $\beta$-unification) بواسطة هويه (Huet) في السبعينيات، ظلت مسألة تقرير $\beta$-matching مفتوحة حتى أثبتت لودر (Loader) عدم قابليتها للتقرير في عام 203. اعتمد برهان لودر على اختزال لمتغير من تعريف $\lambda$ ($\lambda$-definability)، باستخدام آليات معقدة لصياغة قيود تحدد دوال منتهية عشوائية.

المنهجية
يقدم المؤلف برهاناً جديداً لعدم قابلية التقرير يختلف عن نهج لودر من خلال تجنب تعريف $\lambda$ تماماً. بدلاً من ذلك، يقوم البرهان بترميز شكل مقيد من إعادة كتابة السلاسل (string rewriting)، وتحديداً المسألة $0^+ \Rightarrow^* 1^+$ ضمن أنظمة سي مي-ثوي (semi-Thue systems) بسيطة، مباشرة في عملية $\beta$-matching من الرتب العليا.

تتقدم المنهجية عبر الخطوات التالية:

1. نقطة البداية: يبدأ الاختزال من المسألة غير القابلة للتقرير $0^+ \Rightarrow^* 1^+$، والتي تسأل عما إذا كان يمكن تحويل تسلسل غير فارغ من الأصفار ($0$s) إلى تسلسل غير فارغ من الآحاد ($1$s) باستخدام مجموعة من قواعد إعادة الكتابة من الشكل$ab \Rightarrow cd$. هذه المسألة معروفة بالفعل بأنها غير قابلة للتقرير وميكانيكية في مكتبة "روك" (Coq) لإثباتات عدم قابلية التقرير.
2. استراتيجية الترميز: يقوم المؤلف ببناء حدود $\lambda$ بسيطة النوع لمحاكاة عملية إعادة الكتابة. يلتقط الترميز جانبين رئيسيين:
   • توسيع الكلمة والتهيئة: يتم بناء الحدود لتمثيل توسيع كلمة طولها $n$ وتهيئتها بالأصفار ($0$s).
   • خطوات إعادة الكتابة: تمثل الحدود تطبيق قواعد إعادة الكتابة في مواقع محددة داخل الكلمة.
3. القيود النحوية والدلالية: لضمان أن الحل في حدود $\lambda$ يمثل عملية إعادة الكتابة بأمانة دون حلول "مرتجلة" (على سبيل المثال، حدود تتجاهل الوسائط أو تبني نتائج عشوائية)، يستخدم المؤلف قيود نوع محددة وتحققات تكافؤ $\beta$.
   • القيود النحوية: من خلال استخدام متغير حر $u$ وحد الهوية $I$ في سياقات محددة (مستوحاة من دويك وأورزين - Dowek and Urzyczyn)، يقيد المؤلف شكل الحلول المحتملة لتكون "جيدة التكوين". هذا يمنع الحلول التي تُدخل تجريدات $\lambda$ غير ضرورية أو تتجاهل الوسائط المقدمة.
   • القيود الدلالية: يعرّف المؤلف مجموعة من الحدود المحددة النوع ($G_\star, G_0, G_{ab \Rightarrow cd}$) التي تعمل كمفسرات لقواعد إعادة الكتابة. تُستخدم هذه الحدود في قيود تكافؤ $\beta$ للتحقق من أن الحل المرشح يحاكي بشكل صحيح الانتقال من تسلسل من الأصفار إلى تسلسل من الآحاد.
4. الميكانيكية: تم تكييف البرهان بالكامل ميكانيكياً في مساعد الإثبات روك (Rocq Prover) (المعروف سابقاً باسم Coq). البرهان خالٍ من البديهيات (axiom-free) ويمتد لحوالي 4,000 سطر من الكود، مغطياً تعريف حساب $\lambda$ بسيط النوع، ومنطق الاختزال، ونتيجة عدم قابلية التقرير النهائية.

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

• اختزال جديد: توفر الورقة اختزالاً جديداً من المسألة $0^+ \Rightarrow^* 1^+$ إلى $\beta$-matching من الرتب العليا. هذا يتجاوز الآليات المعقدة لتعريف $\lambda$ المستخدمة في البراهين السابقة.
• التحقق المبسط: نظراً لبساطة أنظمة سي مي-ثوي الأساسية والطبيعة المهيكلة للترميز، يُقال إن البرهان أبسط في التحقق منه بالتفصيل الكامل مقارنة بنهجي لودر أو جولي (Joly).
• البناء الموحد: يحدد النهج بناءً موحداً يثبت عدم قابلية التقرير لثلاث مسائل ذات صلة: $\beta$-matching من الرتب العليا، وإشغال النوع التقاطعي (intersection type inhabitation)، وتعريف $\lambda$ ($\lambda$-definability). تربط الورقة صراحةً بين بناء $\beta$-matching وتفسيرات نظرية النموذج المنتهي المستخدمة في براهين إشغال النوع التقاطعي.
• الاختزال المعتمد: ينتج العمل اختزالاً معتمداً من نوع "واحد لواحد" (many-one reduction) من مسألة التوقف (Halting Problem) إلى $\beta$-matching من الرتب العليا، حيث أن عدم قابلية التقرير للمسألة الأصلية (إعادة الكتابة) معتمدة بالفعل في مثبت "روك".

النتائج

• مبرهنة: $\beta$-matching من الرتب العليا غير قابل للتقرير.
• رتبة عدم قابلية التقرير: يوضح الاختزال المصنوع عدم قابلية التقرير عند رتبة النوع 6. وهذا يتوافق مع نتيجة لودر التي تفيد بأن $\beta$-matching غير قابل للتقرير عند الرتبة 6. وتشير الورقة إلى أنه بينما افترض لودر أن الرتبة 5 قد تكون كافية، فإن لا تقنية لودر ولا النهج الحالي ينطبقان عند الرتبة 5، مما يترك قابلية التقرير عند الرتبة 5 كمسألة مفتوحة.
• الميكانيكية: تم إدراج البرهان بنجاح في مكتبة "روك" الحالية لإثباتات عدم قابلية التقرير، مما يضمن خلو النتيجة من الغموض الذي غالباً ما يشوب البراهين اليدوية.

الأهمية
تزعم الورقة أهميتها بشكل أساسي من خلال الميكانيكية والتبسيط لبرهان عدم قابلية التقرير. من خلال نقل نقطة البداية من تعريف $\lambda$ إلى مسألة مقيدة لإعادة كتابة السلاسل، يحقق المؤلف برهاناً أكثر ملاءمة للتحقق الرسمي. يكمل هذا العمل النتائج الميكانيكية الموجودة حول توحيد $\beta$ من الرتب العليا. علاوة على ذلك، يسلط النهج الضوء على وجود صلة هيكلية عميقة بين $\beta$-matching من الرتب العليا، وإشغال النوع التقاطعي، وتعريف $\lambda$، مما يشير إلى أن هذه المسائل تشترك في آلية أساسية واحدة لعدم قابلية التقرير متجذرة في محاكاة خصائص نظرية النموذج المنتهي عبر حدود $\lambda$. يؤكد المؤلف أن البرهان تم تطويره تفاعلياً مع مساعد الإثبات، بالاعتماد على التحليل الشامل للحالات لضمان الصحة، وبالتالي تقليل خطر الخطأ البشري في البناء المنطقي المعقد.