Multi-clocked Guarded Recursion Beyond {\omega}

ملخص تقني: التكرار المحروس متعدد الساعات لما وراء $\omega$

بيان المشكلة
توفر نظريات النوع ذات التكرار المحروس متعدد الساعات (مثل نظرية النوع الموقوتة، CloTT) إطار عمل مرن للبرمجة باستخدام الأنواع التعاونية (coinductive types) وبناء نماذج دلالية للغات البرمجة التي تتميز بتركيبات متقدمة مثل عدم الحتمية (non-determinism) والاختيار الاحتمالي (probabilistic choice). وبينما تم نمذجة هذه النظريات بنجاح باستخدام "المجموعات المسبقة" (presheaves) فوق "توبوس الأشجار" (المفهرسة بـ $\omega$)، ومؤخراً باستخدام "المجموعات المكعبة" (cubical sets)، لا تزال هناك فجوة في ربط هذه النتائج بـ "العالم الحقيقي" لنظرية المجموعات القياسية.

على وجه التحديد، غالباً ما تفشل تفسيرات نظرية المجموعات القياسية في الحفاظ على تبادلية التكميم عبر الساعات مع دوال معينة (مثل دالة القوة المحدودة $P_f$ ودالة التوزيع المحدودة $D_f$) ومع التكميم الوجودي. في "توبوس الأشجار"، لا يتم دائماً "تصدير" (externalize) التكميم الوجودي إلى الوجود في المجموعات، كما أن الدوال مثل $P_f$ و $D_f$ لا تتبادل مع التكميم عبر الساعات في النموذج القياسي. بناءً على ذلك، تُفسر النتائج المثبتة في "نظرية النوع المكعبة الموقوتة" (Clocked Cubical Type Theory) حالياً كعبارات حول "المونادات" (monads) على مجموعات $hsets$داخل النموذج المكعب، مما يترك صحتها في فئة المجموعات القياسية ($\mathbf{Set}$) غير مؤكدة.

المنهجية
يبحث هذا البحث في كيفية توسيع نموذج "المجموعات المسبقة الامتدادية" لـ "التكرار المحروس متعدد الساعات" ليشمل أعداداً ترتيبية أعلى ($\rho > \omega$) لاستعادة خصائص التبادلية اللازمة. تتضمن المنهجية ما يلي:

1. توسيع النموذج: تعميم نموذج المجموعات المسبقة لـ CloTT (الذي وضعه Mannaa وآخرون لـ $\rho = \omega$) ليكون مفهرساً بواسطة أي عدد ترتيبي حدي منتظم $\rho$. يتم بناء النموذج في فئة المجموعات المسبقة فوق فئة من "أجسام الزمن" $T_\rho$، حيث تكون الأجسام أزواجاً من مجموعات الساعات المحدودة والخرائط إلى $\rho$.
2. التحليل الدلالي للتبادلية: يحلل البحث الشروط التي يتشارك فيها التكميم الكلي عبر الساعات ($\forall \kappa$) مع:
   • الدوال الناتجة عن النظريات الجبرية (تحديداً المونادات مثل $P_f$ و $D_f$).
   • التكميم الوجودي ($\exists$).
3. الشروط السنتكتيكية والدلالية:
   • بالنسبة للدوال: يثبت البحث أن الدالة $F$ تتبادل مع النهايات المفهرسة بـ $\rho^{op}$ (وبالتالي مع التكميم عبر الساعات) إذا كانت $F$ هي $\kappa$-accessible، وتحافظ على التقاطعات $\kappa$-small، وتحافظ على "الصور العكسية" (pullbacks) للمدخلات أحادية (monomorphisms)، بشرط أن يحتوي $\rho$ على عدد ترتيبي ببطاقة (cardinality) تساوي $\kappa$.
   • بالنسبة للنظريات الجبرية: تم تحديد شرط سنتكتيكي (نحوي): يجب ألا تحتوي النظريات الجبرية على "معادلات الإسقاط" (drop equations) (وهي المعادلات حيث تختلف مجموعة المتغيرات الحرة في كلا الطرفين). يضمن هذا أن الموناد الناتج يحقق الشروط الدلالية المذكورة أعلاه.
   • بالنسبة للتكميم الوجودي: يثبت البحث أن $\forall \kappa$ يتبادل مع $\exists$ فوق نوع $X$ إذا كانت ألياف (fibers) $X$ تمتلك بطاقة أصغر تماماً من العدد الترتيبي المفهرس $\rho$. كما يتناول البحث حالات التكميم الوجودي "الفريد جوهرياً"، حيث يكون الشاهد (witness) فريداً حتى عدد محدد من خطوات التأخير.

المساهمات والنتائج الرئيسية

• الحفظية فوق المجموعة (Conservativity over Set): يصرح البحث صراحةً ويثبت حفظية نموذج "نظرية النوع الموقوتة" فوق النموذج المجموعاتي القياسي لنظرية النوع. وهذا يعني أن أي عبارة يمكن التعبير عنها في اللغة الداخلية لـ $\mathbf{Set}$ والتي يمكن إثباتها في CloTT، هي أيضاً صحيحة في $\mathbf{Set}$.
• تبادلية المونادات: يقدم البحث شروطاً دلالية ومعياراً سنتكتيكياً (غياب معادلات الإسقاط) للمونادات الناتجة عن النظريات الجبرية لكي تتبادل مع التكميم عبر الساعات. هذا يثبت صلاحية استخدام $P_f$ و $D_f$ في النموذج المجموعاتي، بشرط أن يكون العدد الترتيبي المفهرس $\rho$ كبيراً بما يكفي (على سبيل المثال $\omega_1$ للعمليات القابلة للعد).
• تبادلية التكميم الوجودي: يوضح البحث أنه من خلال اختيار عدد ترتيبي حدي منتظم كافٍ ($\rho$ مثل $\omega_1$ أو أعلى)، فإن التكميم الكلي عبر الساعات يتبادل مع التكميم الوجودي فوق مجموعات ذات بطاقة أقل من $\rho$. هذا يحل مشكلة تصدير البراهين الوجودية من "توبوس الأشجار" إلى $\mathbf{Set}$.
• تفسير الأعمال السابقة: يظهر البحث أن التطبيقات التي تم صياغتها سابقاً في "نظرية النوع المكعبة الموقوتة" — وتحديداً:
  • النمذجة الكوجبرية (Coalgebraic modeling) للأنظمة غير الحتمية والاحتمالية.
  • الاستدلال على التشابه الضعيف (weak bisimilarity) والقوانين التوزيعية بين المونادات.
  • براهين التكافؤ السياقي لـ Probabilistic FPC.
    — يمكن تفسيرها في النموذج المجموعاتي المفهرس بواسطة عدد ترتيبي كافٍ. وهذا يثبت صحة هذه النتائج تحت تفسيرها المجموعاتي القياسي.

الأهمية
يزعم البحث أنه من خلال تغيير العدد الترتيبي المفهرس للنموذج، يمكن سد الفجوة بين المنطق الداخلي للـ "الاستدعاء الذاتي المحروس" (guarded recursion) (الذي يتعامل مع الإنتاجية والتعاونية بأناقة) وبين العالم الخارجي لنظرية المجموعات القياسية.

تكمن الأهمية الأساسية في أن هذا يسمح بالتحقق من النتائج المثبتة باستخدام آليات "نظرية النوع المكعبة الموقوتة" في نظرية المجموعات القياسية دون الاعتماد على الخصائص المحددة للمجموعات المكعبة. يشير هذا إلى أن الأساس الدلالي لصياغة التطبيقات التي تتضمن عدم الحتمية، والاحتمالية، والمحمولات التعاونية (coinductive predicates) يمكن تأسيسه في مساعدات الإثبات التي لا تعتمد على النظرية المكعبة، بشرط أن يستخدم النموذج الأساسي عدداً ترتيبياً مفهرساً كبيراً بما يكفي. يشير البحث إلى أنه بينما الميتا-نظرية (metatheory) المستخدمة لهذه البراهين هي نظرية المجموعات الكلاسيكية، فإن النتائج توفر تبريراً مجموعاتياً صارماً لصحة ترميزات الأنواع التعاونية التي تتضمن أنواع الاستقراء المقسمة (quotient inductive types) والتكميم الوجودي.