A Graded Modal Dependent Type Theory with Erasure, Formalized

إليك ملخص تقني مفصل لورقة البحث بعنوان "نظرية النوع المعتمد الموجهة المتدرجة مع المحو، مُصاغة برمجياً" (A Graded Modal Dependent Type Theory with Erasure, Formalized) من إعداد أندرياس آبل، نيلز أندرس دانييلسون، وأوسكار إريكسون.

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

تعد نظريات النوع المعتمد (مثل Agda وIdris) أدوات قوية للتحقق من صحة البرامج، ولكنها غالباً ما تتضمن حدوداً برهانية (proof terms) أو بيانات وصفية (metadata) لا علاقة لها بالتنفيذ الفعلي للبرنامج أثناء التشغيل. يجب على المترجمات إجراء عملية المحو (erasure) لإزالة هذه الحدود لتوليد كود فعال. ومع ذلك، فإن ضمان أن يكون المحو صحيحاً (أي أن إزالة هذه الأجزاء لا تغير سلوك البرنامج الملحوظ أو قيمته) أمر غير بديهي، خاصة في ظل وجود:

• البرامج المفتوحة (Open programs): البرامج التي تحتوي على متغيرات حرة تم تعليمها بأنها قابلة للمحو.
• السياقات غير المتسقة (Inconsistent contexts): السيناريوهات التي توجد فيها بديهيات أو أنواع مستحيلة (مثل النوع الفارغ $\bot$).
• بنى الأنواع المعقدة: الأنواع المعتمدة، عمليات الإلغاء الكبيرة (computing types from terms)، ومختلف الأنماط (modalities) مثل الخطية (linearity)، والأنواع التآلفية (affine types)، وتدفق المعلومات.

اعتمدت النهج السابقة غالباً على حجج تركيبية (syntactic arguments) أو بيئات مقيدة (مثل البرامج المغلقة فقط). وكان هناك نقص في إطار عمل موحد ومصاغ برمجياً بالكامل للتعامل مع صحة المحو للبرامج المفتوحة في نظرية نوع معتمدة عامة تحتوي على كون (universe) وعمليات إلغاء كبيرة.

2. المنهجية

يقدم المؤلفون نظرية نوع معتمدة موجهة متدرجة ($\lambda\Sigma\Pi\mathbb{N}^M$) معلمة بـ بنية نمطية (modality structure).

أ. الإطار النظري

• البنية النمطية (Modality Structure): تُعلم هذه النظرية بواسطة نصف زمرة مرتبة جزئياً $(M, +, \cdot, \wedge, nr, 0, 1)$. العناصر في $M$ (الدرجات/grades) تتبع استخدام المتغيرات.
  • العمليات: الجمع ($+$) يجمع الاستخدام للمكونات المتوازية؛ الضرب ($\cdot$) يضاعف الاستخدام؛ التقاطع ($\wedge$) يتعامل مع التفرع (أخذ تقاطع الاستخدام)؛ ودالة خاصة $nr$ تتعامل مع التكرار في الأعداد الطبيعية.
  • النماذج (Instances): يدعم الإطار تفسيرات متنوعة، بما في ذلك المحو (الدرجات $\{0, \omega\}$)، الأنواع الخطية/التآلفية، وشبكات تدفق المعلومات.
• فصل الأحكام (Separation of Judgments): يفصل المؤلفون بين حكم النوع ($\Gamma \vdash t : A$) وحكم الاستخدام ($\gamma \triangleright t$). يخصص حكم الاستخدام درجات للمتغيرات الحرة لضمان تتبع الموارد بشكل صحيح دون التداخل مع تساوي النظام النوعي الأساسي.
• النحو (Syntax): تتضمن اللغة أنواع $\Pi$، وأنواع $\Sigma$ الضعيفة والقوية، كوناً $\mathbb{U}$، أعداداً طبيعية $\mathbb{N}$، نوعاً فارغاً $\bot$، وأنواع الوحدة (unit types). كما تدعم عمليات الإلغاء الكبيرة (حساب الأنواع من الحدود).

ب. الصياغة البرمجية (Formalization)

• تمت صياغة النظرية بأكملها وميتا-نظريتها برمجياً بالكامل في لغة Agda (حوالي 110,000 سطر من الكود).
• تستخدم الصياغة البرمجية نحواً جيد التعيين (well-scoped syntax) وتستند إلى صياغة سابقة لتقرير قابلية قرار تحويل الأنواع (Abel et al., 2017).
• توظف علاقة منطقية من نوع كريبكي (Kripke logical relation) كآلية أساسية لإثبات الخصائص الميتا-نظرية.

ج. دراسة حالة المحو

• يعرّف المؤلفون نموذجاً محدداً للبنية النمطية لعملية المحو، حيث تعني الدرجة $0$"قابلة للمحو" والدرجة$\omega$ تعني "ذات صلة/مهمة".
• يعرّفون دالة استخراج ($\cdot^\bullet$) تترجم الحدود من اللغة المصدر إلى لغة $\lambda$-calculus غير محددة النوع (الهدف).
  • غير الصارمة (Call-by-Name): يتم استبدال الحدود الممحاة بحدود حلقة تكرارية ($\loop$) لضمان عدم تقييمها أبداً.
  • الصارمة (Call-by-Value): يتم استبدال الحدود الممحاة بقيمة وهمية ($\_$) لمنع التقييم.
• يثبتون صحة الاستخراج: إذا قام برنامج بحساب عدد طبيعي، فإن نسخته المستخرجة تحسب نفس العدد الطبيعي، حتى لو كان البرنامج مفتوحاً (يحتوي على متغيرات حرة)، بشرط أن يكون السياق متسقاً والمتغيرات معلمة بأنها قابلة للمحو.

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

1. نظرية النوع الموجهة المتدرجة العامة: نظرية نوع معتمدة موجهة متدرجة مصاغة برمجياً بالكامل، تستخدم الدرجات لتتبع استخدام كل من الحدود والأنواع. وهي أول صياغة برمجية كاملة للميتا-نظرية لنظرية نوع متدرجة تحتوي على كون وعمليات إلغاء كبيرة.
2. معالجة التكرار المنقحة: تقديم دالة $nr$ جديدة (بدلاً من عامل natrec-star السابق) للتعامل مع تعيين الدرجات لتكرار الأعداد الطبيعية. يسمح هذا بنموذج أكثر مرونة وصحة للخطية والمحو في التعريفات التكرارية.
3. استنتاج الاستخدام وقابلية القرار: خوارزمية قابلة للقرار لاستنتاج سياقات الاستخدام ($\gamma$) من الحدود، مما يثبت أن علاقة الاستخدام هي خوارزمية وتلبي خاصية المبدئية (الأن السياق المستنتج هو الأكثر تحديداً وصحة).
4. صحة المحو للبرامج المفتوحة: إثبات لصحة الاستخراج باستخدام علاقة منطقية مفهرسة بالأنواع. ومن المهم أن هذا ينطبق على البرامج المفتوحة طالما أن:
   • جميع المتغيرات الحرة في مواضع قابلة للمحو.
   • السياق متسق (لا توجد براهين لـ $\bot$).
   • المطابقة الممحاة (erased matches) على أنواع $\Sigma$ الضعيفة غير مسموح بها (لمنع الحدود العالقة/stuck).
5. التوسعات:
   • تنفيذ أنواع الوحدة الضعيفة والقوية مع قواعد الاستخدام المناسبة.
   • توسيع أنواع $\Sigma$ المتدرجة (المستوحاة من tensors المعتمدة لـ Atkey) مما يسمح بوجود حقول ممحاة في بنى البيانات، مدعومة بنظام تدرج "نمطي" (يميز بين الأنماط الممحاة/وقت التجميع والأنماط الموجودة/وقت التشغيل).

4. النتائج

تثبت الصياغة البرمجية الخصائص الميتا-نظرية التالية:

• اختزال الموضوع (Subject Reduction): درجات الاستخدام محفوظة تحت الاختزال ($\gamma \triangleright t$ و $t \to u \implies \gamma \triangleright u$).
• لمية الاستبدال (Substitution Lemma): تسلك سياقات الاستخدام سلوكاً خطياً تحت الاستبدال، مما يسمح بتركيب تحليل الاستخدام.
• التطبيع (Normalization): النظام يحقق التطبيع القوي.
• قابلية القرار (Decidability): تساوي التعريف والتحقق من النوع قابلان للقرار للجزء المعروض.
• صحة الاستخراج:
  • المبرهنة 6.9: لأي سياق متسق $\Delta$، إذا كان $\Delta \vdash t : \mathbb{N}$ و $0 \triangleright t$ (جميع المتغيرات قابلة للمحو)، فإن $t$ يختزل إلى رقم $n$، وشكله المستخرج $t^\bullet$ يختزل أيضاً إلى $n$.
  • هذا ينطبق على كل من دلالات الهدف غير الصارمة والصارمة.

5. الأهمية

• الصحة من خلال التصميم (Correctness by Construction): من خلال مكننة البراهين في Agda، أزال المؤلفون إمكانية حدوث أخطاء دقيقة في الميتا-نظرية (مثل فشل الاستبدال الذي وجده McBride في أعمال سابقة).
• الترجمة البرمجية العملية: يوفر هذا العمل أساساً صارماً لمترجمات اللغات ذات الأنواع المعتمدة (مثل Agda وIdris) لتمكينها من محو حدود البراهين والحجج غير الضرورية بأمان، مما يحسن أداء وقت التشغيل دون التضحية بضمانات الصحة.
• التعامل مع البرامج المفتوحة: على عكس العديد من الأعمال السابقة التي تضمن الصحة للبرامج المغلقة فقط، يدعم هذا الإطار البرامج المفتوحة ذات الافتراضات القابلة للمحو، وهو أمر ضروري للبرمجة النمطية والتحقق العملي.
• المرونة: تسمح البنية النمطية المعلمة بإعادة استخدام نفس الإطار النظري لتحليلات ثابتة مختلفة، بما في ذلك الخطية، والأنواع التآلفية، والتحكم في تدفق المعلومات، وليس فقط المحو.
• التعامل مع الحالات الحدية: تعالج الورقة صراحةً تعقيدات المطابقة الممحاة (Pattern matching على البيانات الممحاة) والسياقات غير المتسقة، مما يوفر حدوداً واضحة (مثل منع المطابقات الممحاة على أنواع $\Sigma$ الضعيفة في السياقات المفتوحة) حيث تضمن الصحة.

باختالام، تقدم هذه الورقة أساساً متيناً ومتحققاً آلياً لنظريات النوع الموجهة المتدرجة، مظهرةً أن الميزات المعقدة مثل المحو والخطية والأنواع المعتمدة يمكن أن تتعايش مع استخراج برامج صحيح وضمانات ميتا-نظرية قوية.