A Classical Linear $λ$-Calculus based on Contraposition

ملخص تقني: حساب $\lambda$-خطي كلاسيكي قائم على التناقض العكسي (Contraposition)

بيان المشكلة
يتناول البحث تحدي التوفيق بين التناظرات الكلاسيكية للمنطق الخطي (Linear Logic - LL) والصياغة الحسابية لحساب $\lambda$. في حين يُظهر المنطق الخيري تناظرات قوية (مثل التناظر بين القواعد اليسارية واليمينية، ونفي النفي الذي يعود للأصل $\neg\neg A = A$)، فإن عروض الاستنباط الطبيعي القياسية غالبًا ما تفشل في الحفاظ على هذه التناظرات مع الحفاظ على خصائص حسابية جيدة مثل التوافق (confluence) والتقارب القوي (strong normalization). تنقسم الأنظمة الحالية عادةً إلى فئتين:

1. الأجزاء الحدسية: الأنظمة مثل ILL أو DILL التي تقيد المنطق بالاستنتاجات أحادية الجانب، مما يؤدي لفقدان التناظرات الكلاسيكية والقدرة على نمذجة بعض البراهين.
2. الأنظمة القائمة على التسلسل (Sequent-based): الأنظمة المشتقة من حساب التسلسل (مثل شبكات البراهين proof-nets أو حسابات العمليات) التي تحافظ على التناظرات ولكنها تعامل البراهين كعمليات متوازية بدلاً من برامج وظيفية، مما يجعلها أقل ملاءمة لنماذج البرمجة الوظيفية.

على وجه التحديد، يشير المؤلفون إلى أنه في المنطق الكلاسيكي، يعد إثبات قضية $A$ كأطروحة مكافئاً لنفيها كفرضية. وفي سياق المنطق الخطي، يعني هذا أن $A \multimap B$ و $B^\perp \multimap A^\perp$ يجب أن يتشاركا نفس البراهين. ومع ذلك، فإن حسابات $\lambda$ الكلاسيكية (مثل $\lambda\mu$ لباريجوت) هي توافقية ولكنها غير متناظرة (النفي ليس نفيًا عكسيًا)، بينما الأنظمة المتناظرة (مثل بارانيرا وبرياردي) تفتقر غالبًا إلى التوافق. يسعى البحث إلى تقديم نظام استنباط طبيعي أحادي الاستنتاج للمنطق الخطي الأسي المتعدد (MELL) يحافظ على التناظرات الكلاسيكية ويتمتع بخصائص لغات البرمجة الوظيفية القياسية.

المنهجية
يقترح المؤلفون تعييناً جديداً للمصطلحات (term assignment) لـ MELL، يُطلق عليه اسم حساب $\lambda$MELL، وهو قائم على نموذج "ال propositions-as-types". وتعتمد المنهجية الأساسية على:

1. الأساس المنطقي: انطلاقاً من الجزء الحدسي للمنطق الخطي المتعدد (MLL)، يقدم المؤلفون قاعدة "مودوس تولينز الخطية" (linear modus tollens). وبينما تسمح قاعدة حذف الاستلزام الخطي القياسية (modus ponens) باستنتاج $B$ من $A \multimap B$ و $A$، فإن القاعدة الجديدة تسم تسمح باستنتاج $A^\perp$ من $A \multimap B$ و $B^\perp$. هذا الإضافة تستعيد المنطق الخطي الكلاسيكي (MLL).
2. العملية المبتكرة: التعويض العكسي (Contra-Substitution): لتوفير تفسير حسابي لقاعدة "مودوس تولينز"، عرّف المؤلفون عملية جديدة تسمى التعويض العكسي، ويرمز لها بـ $t\{a \backslash s\}$.
   • الحدس: إذا كان التعويض القياسي $t\{a := s\}$ يستبدل ظهوراً فريداً للمتغير $a$ في $t$ بـ $s$، فإن التعويض العكسي "يمسك" بالظهور الفريد لـ $a$ في $t$ و"يسحب" منه، مما يجعل المصطلح $t$ ينقلب "للداخل والخارج" (مثل الجورب) قبل استبدال $a$ بـ $s$.
   • الآلية: تُعرَّف هذه العملية عبر الاستقراء الهيكلي على المصطلحات الخطية. على سبيل المثال، إذا كان $t = \langle u, a \rangle$ و $s : A \multimap B^\perp$، فإن $\langle u, a \rangle\{a \backslash s\}$ ينتج عنه $s \bullet u : B^\perp$.
3. بناء الحساب: يتضمن الحساب عمليات خطية قياسية (tensor، الاستلزام الخطي، lambda abstraction) جنباً إلى جنب مع التطبيق العكسي (contra-application) الجديد ($t \blacktriangledown s$)، والذي يقابل حذف "مودوس تولينز". بالنسبة لـ MELL، يتم توسيع الحساب ليشمل الأدوات الأسية ($!$ و $?$) والوحدات، مما يتطلب تعريفاً دقيقاً للخطية وعلاقة تكافؤ هيكلية.
4. التكافؤ الهيكلي: لضمان التوافق في وجود الأدوات الأسية ومسارات الاختزال المعقدة، عرّف المؤلفون تكافؤاً هيكلياً ($\equiv$) يعمل كـ "تماثل ثنائي قوي" (strong bisimulation) بالنسبة للاختزال المسبق. يتضمن هذا التكافؤ بديهيات لنشر المزالات (eliminators) والتعامل مع الوحدات (مثلاً $t[\star := s] \equiv s[\star := t]$ للمصطلحات من النوع 1).

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

1. حساب $\lambda$MELL: عرض استنباط طبيعي أحادي الجانب لـ MELL حيث تُنمذج البراهين كمصطلحات وظيفية. وهو يقدم بنية التطبيق العكسي وعملية التعويض العكسي.
2. الضبط والتمام (Soundness and Completeness): يثبت المؤلفون أن الحساب مضبوط وتام بالنسبة لـ MELL. وتحديداً، يمكن قراءة أي تسلسل MELL صالح كحكم نوعي في $\lambda$MELL عبر اختيار أي صيغة كأطروحة ونفي الصيغ الأخرى كفرضيات.
3. الخصائص الميتا-نظرية: يحقق الحساب الخصائص القياسية للغة برمجة موجهة بالأنواع:
   • اختزال الموضوع (Subject Reduction): الاختزال يحافظ على النوع.
   • التوافق (Confluence): علاقة الاختزال توافقية (باعتبار التكافؤ الهيكلي).
   • التقارب القوي (Strong Normalization): كل تسلسل اختزال ينتهي.
4. ترميز الأنظمة الكلاسيكية: يوضح البحث كيف يمكن ترميز العديد من تعيينات المصطلحات المعروفة للمنطق الكلاسيكي في $\lambda$MELL، بما في ذلك:
   • حساب $\lambda\mu$ لباريجوت (عبر ترجمتي T و Q).
   • حساب $\lambda\mu\tilde{\mu}$ لكوريين وهيربيل.
   • $\mu$DCLL لهاسيغاوا.

النتائج
النتائج الأساسية هي براهين الخصائص الميتا-نظرية. أثبت المؤلفون التقارب القوي باستخدام تقنية "مرشحي القابلية للاختزال" (reducibility candidates)، عبر تعريف مجموعات من المصطلحات المرتبطة بكل نوع. تم إثبات التوافق عبر "قانون نيومان" من خلال إثبات التوافق المحلي، والذي يعتمد على كون التكافؤ الهيكلي يعمل كتماثل ثنائي قوي للاختزال المسبق. كما يقدم البحث براهين إنشائية لتمام الحساب، موضحاً كيفية استعادة المصطلحات من اشتقاقات MLL الخالية من القطع (cut-free).

الأهمية
يزعم البحث أهميته من خلال تقديم تفسير "وظيفي" للمنطق الخطي الكلاسيكي يحافظ على تناظراته المتأصلة دون اللجوء إلى حسابات العمليات أو الاستنباط الطبيعي متعدد الجوانب. من خلال تقديم "التعويض العكسي"، يوفر المؤلفون آلية للتعامل مع المبدأ الكلاسيكي للتناقض العكسي حسابياً ضمن إطار أحادي الجانب. يمهد هذا العمل الطريق للغات البرمجة الوظيفية الخطية ومساعدي البراهين الذين يمكنهم دعم الاستدلال الكلاسيكي وحساسية الموارد بشكل أصيل. يشير المؤلفون إلى أن توسيع النهج ليشمل الروابط الجمعية (additive connectives) أمر غير بسيط بسبب الاعتماد على الخطية للتعويض العكسي، إلا أن النظام الحالي يتعامل بنجاح مع الأجزاء الضربيه (multiplicative) والأسية (exponential). يجسد هذا العمل الفجوة بين تناظر حساب التسلسل والطبيعة الوظيفية لحسابات $\lambda$.