Towards Weak Stratification for Logics of Definitions

ملخص تقني: نحو التدرج الضعيف لمنطق التعريفات

بيان المشكلة
منطق التعريفات هو عائلة من المنطقات المستخدمة لترميز والاستدلال على الأحكام المحددة بواسطة قواعد الاستنتاج، حيث ترتبط المحمولات الذرية بصيغ منطقية قد تعتمد على المحمول نفسه. ولحل مشكلة الدور (circularity) المتأصلة في مثل هذه التعريفات، تفرض النهج القياسية "شرط التدرج" (stratification condition)، مما يضمن عدم ظهور المحمول بشكل سلبي (إلى يسار الاستلزام) في متن تعريفه الخاص. يعمل هذا الشرط فعلياً على معاملة التعريفات كعوامل نقطة ثابتة رتيبة (monotone fixed-point operators).

ومع ذلك، فإن العديد من المواصفات المفيدة، لا سيما تلك المتعلقة بالعلاقات المنطقية (logical relations) لإثبات خصائص لغات البرمجة، تتطلب تعريفات يظهر فيها المحمول بشكل سلبي. في المنطق $\mathcal{G}$، الذي يقوم عليه مساعد الإثبات Abella، لا يُسمح بمثل هذه التعريفات. وبينما قدم Tiu [19] سابقاً منطقاً يسمى $\mathcal{LD}$ خفف شرط التدرج إلى "التدرج الضعيف" (weak stratification) (السماح بالظهور السلبي بشرط أن يكون مستوى الرأس أكبر تماماً من مستوى الظهور السلبي)، إلا أن $\mathcal{LD}$ كان مقتصرًا على جزء جوهري فقط. فقد افتقر إلى دعم "كمّ $\nabla$" (nabla quantifier) الضروري للاستدلال على الأسماء والجدة (freshness) عبر الثوابت الاسمية، وإلى التعريفات الاستقرائية العامة بما يتجاوز استقراء الأعداد الطبيعية. التحدي الذي يعالجه هذا العمل هو توسيع منطق التعريفات ليشمل التدرج الضعيف مع الحفاظ على الاتساق في وجود $\nabla$ والتعريفات الاستقرائية العامة.

المنهجية
يعرف البحث منطقاً جديداً، $\mathcal{LD}\mu\nabla$، يوسع $\mathcal{LD}$ الخاص بـ Tiu عبر إضافة التكميم $\nabla$ والتعريفات الاستقرائية العامة. تسير المنهجية عبر ثلاث مراحل رئيسية:

1. بناء وصياغة $\mathcal{LD}\mu\nabla$:
   صيغ المنطق كامتداد لحساب متتاليات الرتبة الأولى مع مجموعة من التعريفات $\mathcal{D}$ ومجموعة من التعريفات الاستقرائية $\mathcal{I}$.

• التدرج الضعيف: تكون مجموعة التعريفات $\mathcal{D}$ متدرجة ضعيفاً إذا كان لكل عبارة $H \triangleq_X B$ وتعويض تجذيري (grounding substitution) $\rho$، فإن $\text{lvl}(H\rho) \ge \text{lvl}(B\rho)$. ومن الأهمية بمكان أن هذا يسمح بالظهور السلبي للمحمول المعرف إذا كان مستوى الرأس أكبر تماماً من مستوى الظهور السلبي.
• التدرج الصارم للاستقراء: يفرض البحث شرطاً أكثر صرامة على التعريفات الاستقرائية $\mathcal{I}$: يجب أن تكون متدرجة "صارماً" (أي أن مستوى المحمول الذري الأرضي يجب أن يكون مستقلاً عن وسائطه). هذا القيد ضروري لمنع عدم الاتساق عند الجمع بين الاستقراء والتدرج الضعيف.
• كم $\nabla$: يدمج المنطق كم $\nabla$ للتعامل مع الثوابت الاسمية والجدة، مع التمييز بين الحالات العامة والخاصة للأسماء.

2. المنطق الأرضي والتفسير:
   لإثبات الاتساق، يبني المؤلفون نسخة أرضية من المنطق، $\mathcal{LD}\mu\nabla_\infty$، حيث تكون جميع الصيغ أرضية (لا توجد متغيرات ذاتية/eigenvariables).

• لمية التجذير (Grounding Lemma): خطوة تقنية رئيسية هي إثبات أن أي اشتقاق في $\mathcal{LD}\mu\nabla$ يمكن تفسيره كاشتقاق في $\mathcal{LD}\mu\nabla_\infty$ عبر تعويض تجذيري. وهذا يختزل مشكلة اتساق المنطق الكامل إلى اتساق المنطق الأرضي.
• القواعد اللانهائية: في $\mathcal{LD}\mu\nabla_\infty$، تُستبدل قواعد $\forall R$ و $\exists L$ القياسية بقواعد لانهائية تكمم على جميع الحدود الأرضية، كما يتم توسيع قاعدة $\mu L$ للاستقراء لتشمل جميع الحالات الأرضية.

3. حذف القطع (Cut Elimination):
   جوهر إثبات الاتساق هو حذف قاعدة القطع (تحديداً قاعدة multicut) في $\mathcal{LD}\mu\nabla_\infty$.

• علاقة الاختزال: تم تعريف علاقة اختزال على الاشتقاقات، تحدد كيفية دفع القطوع إلى الأعلى أو حذفها.
• القابلية للاختزال: اتباعاً لتقنية Tait-Martin-Löf التي كيّفها McDowell و Miller، يعرّف المؤلفون مفهوماً لـ "القابلية للاختزال" (reducibility) (والقابلية للانتظام/normalizability) للاشتقاقات. ويثبتون أن كل اشتقاق في $\mathcal{LD}\mu\nabla_\infty$ هو اشتقاق قابل للاختزال.
• معالجة الحالة الاستقرائية: جانب حاسم في الإثبات هو التعامل مع التفاعل بين التدرج الضعيف والاستقراء. يوضح المؤلفون أنه بينما يكفي التدرج الضعيف للتعريفات العامة، فإن التعريفات الاستقرائية يجب أن تظل متدرجة صارماً. ويقدم المؤلفون مثالاً مضاداً (القسم 3.3) يوضح أن السماح بالتدرج الضعيف للتعريفات الاستقرائية يؤدي إلى عدم الاتساق.

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

• تعريف $\mathcal{LD}\mu\nabla$: يحدد البحث رسمياً منطقاً يجمع بين التدرج الضعيف، وتكميم $\nabla$، والتعريفات الاستقرائية العامة.
• إثبات الاتساق: المساهمة الرئيسية هي إثبات أن $\mathcal{LD}\mu\nabla$ متسق. ويتحقق ذلك من خلال إثبات حذف القطع للمنطق الأرضي $\mathcal{LD}\mu\nabla_\infty$ وإرساء تفسير تجذيري.
• قيود التدرج: يوضح العمل الحدود بين التعريفات المسموح بها وغير المسموح بها. فهو يظهر أنه بينما يكفي التدرج الضعيف للتعريفات العامة (مما يتيح العلاقات المنطقية)، فإن التعريفات الاستقرائية تتطلب تدرجاً صارماً للحفاظ على الاتساق.
• المثال المضاد: يقدم البحث مثالاً مضاداً محدداً يوضح أن تخفيف شرط التدرج للتعريفات الاستقرائية يؤدي إلى عدم اتساق منطقي، مما يبرر القيد المفروض على $\mathcal{I}$.

النتائج

• الاتساق: ثبت أن المنطق $\mathcal{LD}\mu\nabla$ متسق. وبناءً على ذلك، يقبل المنطق $\mathcal{LD}\mu\nabla_\infty$ اشتقاقات خالية من القطع لجميع المتتاليات المثبتة.
• خصائص الانعكاس (Inversion Properties): يثبت البحث خصائص ميتا-نظرية لـ $\mathcal{LD}\mu\nabla_\infty$، بما في ذلك انعكاسية قواعد الإدخال المختلفة (مثل $\wedge R$، $\vee L$، $\nabla R$) والانعكاسية الجزئية المحددة لـ $\vee R$، $\exists R$، وقواعد التعريف ($\Delta R$) عندما يكون السياق فارغاً. هذه الخصائص حاسمة لإجراءات البحث عن البراهين.
• القيود: تم إثبات نظرية حذف القطع فقط للمنطق الأرضي $\mathcal{LD}\mu\nabla_\infty$. ويشير البحث إلى أن توسيع هذه النتيجة لتشمل المنطق الكامل $\mathcal{LD}\mu\nabla$ (مع المتغيرات الذاتية) يظل تحدياً مفتوحاً.

الأهمية
تكمن أهمية هذا العمل في قدرته على توسيع إمكانيات مساعد الإثبات Abella. يعتمد Abella على المنطق $\mathcal{G}$، الذي يقيد حالياً التعريفات بأن تكون متدرجة صارماً. ومن خلال تبرير تضمين التعريفات المتدرجة ضعيفاً، يمهد هذا البحث الطريق لتمكين Abella أصلياً من دعم "العلاقات المنطقية"، وهي تقنية أساسية لإثبات الخصائص الدلالية للغات البرمجة (مثل سلامة النوع وصحة المترجم).

يضع هذا العمل كخطوة تأسيسية نحو توسيع أوسع لـ $\mathcal{G}$. وبينما يتعامل النتيجة الحالية مع التدرج الضعيف مع $\nabla$ والاستقراء، يشير المؤلفون إلى أن التبرير الكامل لـ Abella سيتطلب توسعات إضافية لتشمل الاستقراء المشترك (co-induction) والتجريد الاسمي (nominal abstraction). كما يسلط العمل الضوء على ضرورة الحفاظ على التدرج الصارم للتعريفات الاستقرائية، وهو قيد يمنع حالات عدم الاتساق التي قد تنشأ من خلط التدرج الضعيف مع الاستقراء.