Well-Scoped Locally Nameless Representation of Syntax

ملخص تقني: التمثيل المحلي اللاسمي جيد النطاق لبنية النحو (Syntax)

بيان المشكلة
عند صياغة اللغات التي تحتوي على بنى ربط (مثل حساب $\lambda$ أو أنظمة النوع)، في مبرهنات تفاعلية تعتمد على نظرية النوع التابع (مثل Agda أو Lean أو Rocq)، يبرز تحدٍ مركزي يتمثل في إدارة متغيرات الربط وتكافؤ $\alpha$. وقد ثبت أن نهج "الأسماء المحلية" (locally nameless) — الذي يمثل المتغيرات الحرة كأسماء صريحة والمتغيرات المربوطة كفهارس de Bruijn — يحقق معايير PoplMark من حيث انخفاض البنية التحتية، والشفافية، وسهولة الدخول. ومع ذلك، تعاني تمثيلات "الأسماء المحلية" القياسية من خلل حرج: وهو أن التعريف الاستقرائي للمصطلحات يسمح بوجود فهارس "هائمة" (indices) (فهارس تتجاوز النطاق الحالي). ولضمان الصحة، يجب تقييد المجال بمجموعة فرعية من المصطلحات "المحلية المغلقة". وهذا يستلزم إثباتات يدوية متكررة بأن العمليات (مثل التعويض) تحافظ على الإغلاق المحلي، مما يخلق عبئاً كبيراً ومصدراً للأخطاء المحتملة في التطويرات الرسمية.

المنهجية
يقترح البحث نسخة "جيدة النطاق" (well-scoped) من تمثيل الأسماء المحلية، والتي تستفيد من نظام النوع التابع في Agda لفرض الإغلاق المحلي جوهرياً، بدلاً من كونه محمولاً (predicate) منفصلاً.

1. الأنواع الاستقرائية المفهرسة: بدلاً من نوع واحد للمصطلحات، يعرّف المكتبة عائلة من الأنواع Trm[n] المفهرسة بعدد طبيعي $n$. المصطلح من النوع n-term هو مصطلح تكون جميع فهارس de Bruijn فيه مستمدة من النوع المنتهي Fin n (الأعداد الطبيعية الأقل من $n$).
2. المصطلحات المحلية المغلقة كـ 0-مصطلحات: في هذا الإطار، تقابل "المصطلحات المحلية المغلقة" (تلك التي لا تحتوي على فهارس هائمة) تماماً Trm[0]. أما المصطلحات التي تحتوي على متغيرات حرة فتُمثل كـ Trm[n] حيث يمثل $n$ عدد المتغيرات الحرة في النطاق.
3. البارامترية بواسطة تواقيع الربط: المكتبة عامة، وتعتمد في بارامتراتها على توقيع ربط من نمط Plotkin. يسمح هذا بتعريف المعاملات، وعدد حالات (arities) كل منها، وعدد الأسماء المربوطة في كل موضع وسيط.
4. العمليات عبر الأنواع التابعة:
   • إضعاف النطاق (Scope Weakening): دالة Trm[m] -> Trm[n] (حيث $m \le n$) تقوم بحقن الفهارس، وتتعامل مع الإزاحة المطلوبة عند الانتقال إلى نطاق أكبر.
   • التجسيد (Concretion/Opening): استبدال فهرس $i$ في مصطلح من النوع (1+n) بمصطلح من النوع 0 لإنتاج مصطلح من النوع n. يتضمن ذلك إزاحة الفهارس الأكبر من $i$ للأسفل بمقدار واحد.
   • التجريد (Abstraction/Closing): استبدال اسم حر في مصطلح من النوع n بفهرس لإنتاج مصطلح من النوع (1+n). يتضمن ذلك إزاحة الفهارس للأعلى.
   • التعويض (Substitution): مُعرَّف بنيوياً. وبما أن دالة التعويض تسند الأسماء إلى مصطلحات من النوع 0 (Trm)، فإن شرط "الإغلاق المحلي" يُفرض تلقائياً بواسطة نظام النوع. التعويض على n-term ينتج n-term آخر.

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

• مكتبة WSLN: مكتبة Agda عامة تنفذ مصطلحات الأسماء المحلية جيدة النطاق. توفر المكتبة البنية التحتية لتعريف النحو، والعمليات (الإضعاف، التعويض، التجريد، التجسيد)، ومبادئ الاستدلال لأي لغة محددة بتوقيع ربط من نمط Plotkin.
• إثبات الكفاية الرسمي: يقدم البحث إثباتاً صارماً يؤسس علاقة تقابل (bijection) بين:
  1. نوع المصطلحات Trm[0] جيدة النطاق محلياً.
  2. فئات تكافؤ $\alpha$ للمصطلحات "الاسمية" (المصطلحات التي تستخدم أسماء صريحة لكل من المتغيرات الحرة والمربوطة).
     هذا التقابل يوضح أن التمثيل جيد النطاق يلتقط بشكل صحيح دلالات التعويض المتجنب للاقتناص (capture-avoiding substitution) وتكافؤ $\alpha$.
• إزالة إثباتات الإغلاق المحلي: من خلال ترميز قيود النطاق في مؤشرات النوع، يتم القضاء على الحاجة إلى محمولات "الإغلاق المحلي" الصريحة وما يرتبط بها من التزامات إثبات (مثل إثبات أن التعويض يحافظ على الإغلاق المحلي). تصبح هذه الخصائص نتائج مباشرة لقواعد النوع.
• التعامل مع الجِدّة (Freshness): تدمج المكتبة تقنيات اسمية (nominal techniques)، باستخدام مجموعة من الذرات (atoms) "غير قابلة للنفاذ نهائياً" (فائقة النهاية) من الأعداد الطبيعية لتوليد أسماء جديدة عبر التكميم ناقص الوفاء (cofinite quantification)، مما يضمن التعامل مع شروط الجِدّة بشكل منهجي.

النتائج
يتحقق البحث من النهج من خلال ثلاثة أمثلة متميزة تم تنفيذها في Agda:

1. حساب $\pi$ ($\pi$-Calculus): يوضح قابلية تطبيق المكتبة خارج نطاق حساب $\lambda$، حيث يتعامل مع تعبيرات العمليات وأسماء القنوات. ويسلط الضوء على أنه بينما تتعامل المكتبة مع بنية الربط، فإن التحقق من النوع لصحة التكوين (مثل ضمان استخدام القنوات حيث يُتوقع ذلك) يظل حكماً منفصلاً يحدده المستخدم.
2. نظرية النوع لـ مارتن-لوف (MLTT): يوضح كيف تسهل المكتبة تعريف قواعد النوع. ويقارن بين قواعد "الوجود-الجديد" (التي تتطلب افتراضات صريحة للجِدّة) وقواعد "التكميم ناقص الوفاء" (حيث تكون الجِدّة ضمنية)، مبيناً أن التمثيل جيد النطاق يدعم النوع الأخير، مما يؤدي إلى صياغات أكثر نظافة وشفافية.
3. نظام غودل T (Normalization by Evaluation): تطوير جوهري يثبت قابلية قرار تحويل $\beta\eta$. يوضح هذا المثال كيف يبسط التمثيل جيد النطاق دلالات التجريد والتعامل مع الجِدّة في البناءات الدلالية المعقدة (presheaves ذات قيم Setoid)، متجنباً الحاجة إلى كائنات دلالية مدعومة نهائياً.

الأهمية والادعاءات
يزعم البحث أن تمثيل الأسماء المحلية جيد النطاق يقدم حلاً "مباشراً" وقوياً لمشكلة "الفهارس الهائمة" الموجودة في مقاربات الأسماء المحلية التقليدية. تكمن أهميته الأساسية في نقل عبء ضمان صحة النطاق من المستخدم (عبر الإثباتات اليدوية) إلى مدقق النوع الخاص بمبرهن النظريات (عبر الأنواع التابعة).

يؤكد المؤلفون أن هذا النهج يحافظ على الشفافية المطلوبة في معايير PopMark: حيث تحاكي التعريفات الرسمية الاصطلاحات غير الرسمية عن كثب، ويتم احتواء "يوغا الفهارس" (التلاعب بفهارس de Bruijn) داخل عمليات المكتبة. ورغم أن التنفيذ يتطلب تعاملاً دقيقاً مع الأعداد المحدودة (Fin n) وإزاحة الفهارس، إلا أن المكتبة تجعل هذا التعقيد بارامترياً، مما يسمح للمستخدمين بتعريف اللغات وإثبات الخصائص دون إدارة ميكانيكا النطاق منخفضة المستوى. يشير البحث بتواضع إلى أنه بينما تعتبر تواقيع الربط الحالية غير مرتبة وتنمذج نطاقات ربط بسيطة، فإن النهج قوي بما يكفي للتعامل مع أنظمة نوع معقدة وإثباتات دلالية، كما هو موضح في تطوير النظام T.