Constructing (Co)inductive Types via Large Sizes

إليك ملخص تقني مفصل للورقة البحثية بعنوان "بناء الأنواع الاستقرائية (الاستقرائية المشتركة) عبر الأحجام الكبيرة" (Constructing (Co)inductive Types via Large Sizes) للباحثين باستيان لاركر، دانييل أوتن، وبينو فان دير بيرغ.

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

تعتمد مساعدات الإثبات (مثل Agda وLean وRocq) على نظرية النوع المعتمد لضمان الاتساق والقابلية للتقرير. أحد المتطلبات الحاسمة هو أن تكون جميع الدوال العودية (recursive functions) كلية (terminating) وجميع الدوال الاستقرائية المشتركة (corecursive functions) منتجة (productive).

• القيود الحالية: تعتمد معظم الأنظمة على التحقق النحوي (syntactic checks) لفرض الكلية (مثل الاستقراء الهيكلي أو تغير الحجم). هذه التحققات غالبًا ما تكون مقيدة، وغير نمطية، وحساسة لإعادة هيكلة الكود (refactoring).
• الأنواع ذات الأحجام (Sized Types): يعد "النوع القائم على الحجم" بديلاً يعتمد على الأنواع، حيث يستخدم "الأحجام" (الترتيبات الأصلية/ordinals) لتوصيف الأنواع، مما يسمح بإثبات التوقف عبر الاستقراء جيد التأسيس على الحجم.
• عدم اتساق Agda: تنفذ Agda الأنواع ذات الأحجام، لكنها تقدم أكبر حجم ($\infty$) لتعريف النوع الاستقرائي/الاستقرائي المشترك الكامل كتقريب له عند $\infty$. يؤدي هذا إلى عدم اتساق منطقي: حيث يثبت النظام أن $\infty < \infty$، مما ينتهك خاصية عدم الانعكاس في الترتيبات الجيدة الصارمة.
• العمل النظري السابق: كانت المحاولات السابقة لإصلاح ذلك باستخدام المكممات البارامترية (الوجودي $\exists$ للاستقرائي، والشمولي $\forall$ للاستقرائي المشترك) محدودة. وتحديداً، لم تستطع بناء سوى الأنواع الاستقرائية محدودة التفرع لأن نوع الحجم كان يُفسر كأرقام طبيعية ($\mathbb{N}$)، والتي تفتقر إلى الترتيبات الأصلية الحدية (limit ordinals) اللازمة للهياكل غير محدودة التفرع.

الهدف: بناء نظرية أنواع متسقة تدعم جميع (الاستقرائية والمشتركة) الأنواع (بما في ذلك الأنواع غير محدودة التفرع) باستخدام الأنواع ذات الأحجام والمكممات البارامترية، دون الاعتماد على "أكبر حجم" غير متسق.

2. المنهجية

يقوم المؤلفون بتوسيع نظرية مارتن-لوف للأنواع (MLTT) بميزات محددة لتحقيق هذا البناء وإثبات اتساقه عبر نموذج التحقق (realizability model).

أ. نظرية الأنواع الموسعة

تتضمن النظرية ميزات MLTT القياسية (الأكوان، $\Sigma$، $\Pi$، أنواع الهوية) بالإضافة إلى:

1. نوع للأحجام (Size):
   • مزود بصفر ($0$) وخلف ($ \uparrow i$).
   • مرتب بترتيب مسبق ($\leq$) مشفر كقضية بسيطة (mere proposition).
   • بشكل حاسم: Size هو نوع كبير (ليس في الكون $U$)، ولكن التكميم عليه يمكن أن ينتج أنواعاً صغيرة.
2. المكممات البارامترية:
   • المكمم الوجودي $\exists i. A(i)$: يمثل اتحاد التقريبات. العناصر هي أزواج $\langle s, a \rangle$، لكن الحجم $s$ مجرد (لا يمكن مطابقة النمط عليه). التخلص (elimination) مقيد بالأنواع الصغيرة.
   • المكمم الشمولي $\forall i. A(i)$: يمثل تقاطع التقريبات. تعمل الدوال بشكل موحد على أي حجم.
   • بديهيات البارامترية (Parametricity Axioms): تتضمن النظرية بديهيات تنص على أن هذه المكممات تتبادل مع منشئات الأنواع (على سبيل المثال، $\Pi x:A. \exists i. B(x,i) \simeq \exists i. \Pi x:A. \exists j < i. B(x,j)$). هذا يجسد فكرة أن الأحجام تُعامل بشكل موحد.
3. الاستقراء جيد التأسيس (fix):
   • عامل نقطة ثابتة (fixpoint operator) يسمح بالتعريف عبر الاستقراء على الأحجام: $fix\ f : \forall i. A(i)$ بشرط أن يكون $f : \forall i. ((\forall j < i. A(j)) \to A(i))$.
   • قاعدة $\beta$ هي قضية (propositional) وليست تعريفية (definitional) للحفاظ على قابلية تقرير نوع البيانات.

ب. بناء (الأنواع) الاستقرائية والمشتركة

يقوم المؤلفون بترميز (الأنواع) الاستقرائية والمشتركة كجبرات أولية (initial algebras) ومعادلات نهائية (final coalgebras) للدوال متعددة الحدود (polynomial endofunctors) ($F$).

1. التقريبات الترتيبية: يقومون بتعريف دوال مرتبطة بالحجم $F[\exists -]$ و $F[\forall -]$. باستخدام عامل fix ، يبنون الجبرات الأولية ($\mu_3 F$) والمعادلات النهائية ($\nu_2 F$) لهذه الدوال المرتبطة بالحجم. تمثل هذه الأنواع المقطوعة عند حجم معين.
2. الأنواع الكاملة عبر التكميم:
   • الأنواع الاستقرائية: تُعرف كـ $\mu F := \exists i. (\mu_3 F) i$. المكمم الوجودي يجمع كل العناصر المحدودة بحجم ما.
   • الأنواع الاستقرائية المشتركة: تُعرف كـ $\nu F := \forall i. (\nu_2 F) i$. المكمم الشمولي يضمن أن العناصر قابلة للملاحظة عند أي عمق.
3. التعامل مع الأنواع غير محدودة التفرع: الابتكار الرئيسي هو إظهار أن الدوال متعددة الحدود تتبادل ضعيفاً مع المكمم الوجودي. يتطلب هذا وجود ترتيبات أصلية حدية (suprema لمتتاليات الأحجام)، وهو أمر مستحيل إذا كانت الأحجام مجرد أرقام طبيعية $\mathbb{N}$.

ج. إثبات الاتساق: نموذج التحقق (Realizability Model)

لإثبات اتساق النظرية، يبني المؤلفون نموذج تحقق يعتمد على الطبقة الفعالة (Effective Topos) لهيلاند.

• تفسير الأنواع:
  • الأنواع الصغيرة: تُفسر كعلاقات تكافؤ جزئية (PERs) على الأعداد الطبيعية (بيانات قابلة للحوسبة).
  • الأنواع الكبيرة: تُفسر كـ "تجميعات" (Assemblies) (مجموعات مع علاقات حوسبية).
• تفسير Size:
  • نوع Size يُفسر كـ $\nabla \omega_1$، حيث $\omega_1$ هي الترتيب الأصلي الأول غير القابل للعد (مجموعة كل الترتيبات الأصلية القابلة للعد).
  • يتم إعطاؤه علاقة تحقق "كاملة"، مما يعني أن المورفيزمات يجب أن تعامل جميع الأحجام بشكل موحد (البارامترية).
• التحقق:
  • نظرًا لأن $\omega_1$ يحتوي على ترتيبات أصلية حدية، فإن النموذج يثبت بديهيات البارترامتري (البارامترية) المطلوبة للأنواع غير محدودة التفرع.
  • النموذج يثبت عدم القدرة على التنبؤ (Impredicativity) (التكميم فوق الأنواع الكبيرة ينتج أنواعاً صغيرة) ووحدة أدلة الهوية (UIP)، رغم أن النحو لا يفترض ذلك. وهذا يثبت أن النحو متوافق مع النظريات الأقوى (مثل نظرية النوع الهندسي - HoTT) دون أن يكون مقيداً بها.

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

1. البناء العام للأنواع الاستقرائية والمشتركة: على عكس النهجات البارامترية السابقة المقتصرة على الأنواع محدودة التفرع، يبني هذا العمل جميع الأنواع الاستقرائية والمشتركة، بما في ذلك غير محدودة التفرع (مثل ترتيبات بروير، ونماذج نظرية المجموعات البنائية).
2. حل عدم اتساق Agda: من خلال استبدال "أكبر حجم" ($\infty$) غير المتسق بمكممات بارامترية فوق نوع كبير من الأحجام، يقدم المؤلفون بديلاً متسقاً للتطبيق الحالي في Agda.
3. المكممات البارامترية كآلية: يوضح المؤلفون أن تجسيد البارامترية داخلياً عبر $\exists$ و $\forall$ فوق الأحجام يفرض بفعالية التجريد اللازم لمنع السلوك غير المنتهي وعدم الاتساق المنطقي.
4. نموذج تحقق قوي: يوفر بناء نموذج حيث يُفسر Size كـ $\omega_1$ تبريراً دلالياً (semantic) صارماً للنظرية، مما يثبت أن بديهيات البارامترية متسقة.

4. النتائج

• السلامة النظرية: تثبت الورقة أن الجبر الأولي والمعادلة النهائية لأي دالة متعددة الحدود موجودان داخل النظرية الموسعة.
• الاتساق: يؤكد نموذج التحقق أن النظرية متسقة. ويظهر أن بديهيات المكممات البارامترية تتحقق عندما تُفسر الأحجام كترتيب أصلي غير قابل للعد.
• التوافق: لا تعتمد البناءات على UIP أو عدم القدرة على التنبؤ (impredicativity) في النحو، مما يجعل النتائج متوافقة مع نظرية النوع الهندسي (HoTT)، رغم أن النموذج يحقق هذه الخصائص.

5. الأهمية والعمل المستقبلي

• الأثر على مساعدات الإثبات: يقدم هذا العمل مساراً لتنفيذ الأنواع ذات الأحجام في مساعدات الإثبات (مثل Agda) دون عدم الاتساق الحالي الناتج عن حجم $\infty$. هذا يسمح بتحقق من التوقف أكثر نمطية وتكوينية.
• السلوك الحسابي: يقر المؤلفون أنه بينما النظرية متسقة، فإن النحو الحالي يفتقر إلى السلوك الحسابي لبديهيات البارامترية (فهي بديهيات وليست قواعد اختزال). العمل المستقبلي يحتاج إلى ربط هذا بالبارامترية الداخلية (مثل أنواع الجسر أو نظرية النوع التكعيبية) لضمان القابلية للتقرير والكانونية (canonicity) في الممارسة العملية.
• قابلية تقرير عدم التساوي: يشير النموذج إلى أن عدم التساوي في الأحجام ليس قابلاً للتقرير بشكل عام (بسبب القيم العليا/suprema). يقترح المؤلفون نهجاً هجيناً (عدم تساوي تعريفي مقابل قضائي) للتطبيق العملي.
• التعميم: يمكن تعميم النموذج ليشمل جبرات تركيبية جزئية أخرى أو دمجه مع التأثيرات (effects) والوحدانية (univalence).

باختصار، تنجح الورقة في سد الفجوة بين الحاجة النظرية للأنواع ذات الأحجام البارامترية والمتطلب العملي للاتساق، مما يتيح بناء أنواع استقرائية ومشتركة معقدة في إطار نظري سليم.