Impredicativity in Linear Dependent Type Theory

ملخص تقني: عدم التقرير (Impredicativity) في نظرية الأنواع الخطية المعتمدة

1. بيان المشكلة

تتناول الورقة فجوة جوهرية في دلالات نظريات الأنواع تحت البنيوية (substructural type theories): وهي دمج عدم التقرير (impredicativity) ضمن نظرية الأنواع الخطية المعتمدة (LDTT).

بينما تعتمد النظريات العليا من الرتب (مثل حساب الإنشاءات - Calculus of Constructions) على عدم التقرير — وهو القدرة على تعريف نوع عبر التكميم فوق كون (universe) يتضمن النوع نفسه — للوصه إلى قدرة تعبيرية عالية، فإن معظم النماذج الحالية لنظرية الأنواع الخطية تواجه صعوبة في استيعاب هذه الميزة. يُعد عدم التقرير أمراً ضرورياً لـ الترميزات متعددة الأشكال (polymorphic encodings) (على سبيل المثال، ترميز الأنواع الاستقرائية مثل القوائم كدوال)، ولكن الأنظمة الخطية القياسية غالباً ما تفتقر إلى البنية الفئوية (categorical structure) اللازمة لدعم هذه الترميزات مع الحفاظ على الاتساق والقدرة على إثبات مبادئ الاستقراء.

2. المنهجية

يستخدم المؤلفون دلالات التحقيق (realizability semantics) لبناء نموذج لـ LDTT. يتبع البناء الخطوات التقنية التالية:

• البنية التأسيسية: يبدأ المؤلفون بـ جبر تركيبي خطي (Linear Combinatory Algebra - LCA)، وهو بنية تطبيقية مزودة بعملية أحادية ($!$) ومجموعات محددة من الـ combinators ($B, I, C, W, K, D, \delta, F$) التي تحقق بديهيات المنطق الخطي.
• الإطار الفئوي: يستخدمون فئات الاستيعاب الخطية (Linear Comprehension Categories). هذا الإطار يوسع فئات الاستيعاب القياسية (المستخدمة لنمذجة نظرية الأنواع المعتمدة) من خلال دمج "فيبريشن" (fibrations) متميزين: أحدهما للأنواع القرطسية (cartesian types - حدسية) والآخر للأنواع الخطية (linear types - تحت بنيوية).
• الارتباط الخطي-غير الخطي (Linear-Non-Linear Adjunction): لربط الجانبين، يقومون بتنفيذ ارتباط متناظر ($L \dashv M$) بين الفيبريشنات الخطية والقرطسية. وهذا يسمح بتفسير "النماذج" (modalities) التي تحول الحدود الخطية إلى حدود قرطسية.
• بناء الكون (Universe Construction): يبنون كوناً من نوع "تارسكي" غير مقرر (Tarski-style universe $U$) باستخدام مفهوم المجموعات المتواضعة (modest sets) وعلاقات التكافؤ الجزئية (Partial Equivalence Relations - PERs). ومن خلال الاستفادة من التكافؤ بين المجموعات المتواضعة والـ PERs، يثبتون أن الكون مغلق تحت كل من الضربات المعتمدة القرطسية الكبيرة والضربات المعتمدة الخطية الكبيرة.
• الصياغة الرسمية: تم صياغة البناء بأكمله رسمياً في مساعد الإثبات Rocq (المعروف سابقاً بـ Coq) باستخدام مكتبة UniMath، مما يضمن الدقة الرياضية للإنشاءات الفئوية.

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

• نموذج جديد لـ LDTT: بناء نموذج دلالات التحقيق الذي يجمع بنجاح بين الخطية وعدم التقرير.
• الكون ثنائي فك التشفير (Dual-Decoding Universe): تقديم كون $U$ يحتوي على عمليتي فك تشفير: $El^C$ (رسم الخرائط من الأكواد إلى الأنواع القرطسية) و $El^L$ (رسم الخرائط من الأكواد إلى الأنواع الخطية).
• قواعد نظرية الأنواع الجديدة: تقترح الورقة وتبرر عدة قواعد لم تكن مألوفة سابقاً في LDTT، بما في ذلك:
  • المُتساويات (Equalizers) على الجانب الخطي.
  • التضمن (Injectivity) للنموذج $M$ (لضمان أمان الدالة/المنظر).
  • الاستعلاء الوظيفي (Function Extensionality) للدوال المعتمدة الخطية.
• ترميزات غير مقررة منقحة: طريقة للانتقال من "الجبرات ضعيفة الأولية" إلى "الجبرات الأولية" في سياق خطي.

4. النتائج

• الاتساق: يثبت النموذج أن عدم التقرير يتسق مع قواعد LDTT.
• بناء الجبر الأولي: كدراسة حالة، يستخدم المؤلفون الكون غير المقرر لترميز نوع القوائم فوق نوع خطي.
• حل مشكلة الاستقراء: غالباً ما تفشل الترميزات غير المقررة القياسية في تلبية مبادئ الاستقراء المطلوبة. يطبق المؤلفون تقنية تنقية (مستوحاة من أعمال Awodey و Frey و Speight) باستخدام المُتساويات لبناء نوع فرعي من القائمة المُرمزة. ويثبتون أن هذا النوع المنقى هو بالفعل الجبر الأولي، محققاً كلاً من مبدأ التكرار وخصائص الوحدانية/الاستقراء الضرورية.

5. الأهمية

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

من خلال إثبات إمكانية ترميز الأنواع الاستقرائية (مثل القوائم) خطياً مع استعادة مبادئ الاستقراء الكاملة لها، تمهد الورقة الطريق للغات برمجة الكم الأكثر تعبيراً، وأنظمة أنواع الجلسات (session-typed systems)، وأدوات التحقق الصوري المتقدمة التي تعمل تحت قيود تحت بنيوية.