1215 ورقة بحثية
تقدم هذه الورقة تقنية تجريد سببي قائمة على الخصائص لعمليات ماركوف لاتخاذ القرار الموزعة، والتي تستفيد من العلاقات السببية بين متغيرات الحالة لإنشاء نماذج مدمجة وقابلة للتوسع قادرة على حساب سياسات قريبة من المثالية والتعميم على الأنظمة واسعة النطاق.
تتقصى هذه الورقة العلاقة بين فئات استيعاب جاكوبس (Jacobs comprehension categories) وفئة فرعية من فئات استيعاب لوفير-إيرهارد (Lawvere-Ehrhard comprehension categories) من خلال توصيف الأخيرة عبر رتيبات (fibrations) مورفيزم النوع والحد، ومن ثم تقديم بناءات لفئات استيعاب حرة فوق الرتيبات وفئات استيعاب لوفير-إيرهارد حرة فوق فئات استيعاب جاكوبس.
تقدم هذه الورقة منطقاً خفيف الوزن شبيهًا بمنطق هوار (Hoare-like logic) مشتقًا من تمثيل هايزنبرغ لغوتسمان للتحقق بكفاءة من خصائص دوائر كليفورد، وتوسعه ليشمل الحوسبة الكمومية الشاملة عبر دمج بوابات T والحالات السحرية، مما يتيح تطبيقات مثل التصديق على التخلص من الكيوبتات، وفحوصات القابلية للانفصال، ووضع حدود دنيا لتعقيد بوابة T.
يقدم هذا البحث حساب "الاستدعاء بالسخافة" (call-by-silly) المتدهور الذي يجمع بشكل متماثل بين أسوأ جوانب الاستدعاء بالاسم والاستدعاء بالقيمة لإثبات أن التكافؤ السياقي للاستدعاء بالقيمة أعمى تجاه الكفاءة، مع توفير استراتيجية مقابلة، وآلة مجردة، ونظام أنواع متعددة محكم لإثبات أنه يحسب تسلسلات تقييم ذات طول أقصى.
تقدم هذه الورقة النظريات المونودية الطبقية بوصفها تعميماً للنظريات المونودية التي تتيح التكامل المخططاتي الدقيق لمستويات متعددة من التجريد ضمن إطار مخطط خيطي واحد، مما يقدم نهجاً جبرياً موحداً لنمذجة تدفق المعلومات عبر مجالات علمية متنوعة مثل الفيزياء الكمية، والكيمياء، وعلوم الحاسوب.
تقدم هذه الورقة حساباً مُحققاً بـ Lean 4 ونظاماً ثنائي المستويات يُسمى "hurdy-gurdy" يُمكّن النماذج اللغوية الكبيرة غير الموثوقة من توليد إجابات ذاتية التصديق وذات درجة دقة لأسئلة البرمجة، وذلك عبر تركيب مسارات ترجمة موثوقة ضمن رسم بياني متنامٍ من اللغات التي تم التحقق منها بشرياً.
تُظهر هذه الدراسة أنه بينما تستطيع النماذج اللغوية الكبيرة الرائدة توليد بيئات "دوكر" (Docker) متعددة الخدمات تعمل وظيفياً من مجرد مخرجات المستودعات، إلا أنها تخفق باستمرار في استنتاج مواصفات نية النشر الحرجة مثل السياسات الأمنية وتحسينات البناء، مما يستلزم نهجاً صريحاً قائماً على المواصفات لسد الفجوة بين الصحة الوظيفية والجاهزية للإنتاج.
تقدم هذه الورقة اثنين من أدوات الربط لمكتبة miniKanren، وهما `prune` و `defrel/bank` اللذان يتيحان التعداد من الأسفل إلى الأعلى مع إزالة التكرار الملاحظي والتخزين المؤقت لتحسين أداء التركيب البرمجي العلائقي على الأهداف العميقة بشكل كبير، مع اقتراح متغير مرجح لمعالجة الحالات التي يفشل فيها الترتيب المعياري للبحث بالعمق أولاً في إيجاد ممثلين مدمجين.
تقدم هذه الورقة صياغة رسمية بلغة Lean 4، تم التحقق منها بالكامل عبر النواة (kernel)، تثبت أن أي تغطية منتهية للأعداد الصحيحة بمقاييس فردية متمايزة أكبر من 1 يجب أن يكون لها مضاعف مشترك أصغر يتجاوز 10,000، مما يؤسس لاستبعاد موثق آلياً لمسألة إيردوس-سيلريدج الخاصة بالتغطية الفردية دون الاعتماد على أدوات حل حسابية غير متحقق منها.
تغلق هذه الورقة فجوة تحقق حرجة في حد كوشين-سبيكر الأدنى من خلال تقديم شهادات شجرة-حالة عقلانية دقيقة وفاحصين مستقلين (أحدهما بلغة بايثون والآخر مثبت رسميًا بلغة Lean 4) للتحقق آليًا من عدم القابلية للاندماج الهندسي لجميع الرسوم البيانية الـ 180 المتميزة في قاعدة بيانات الحجب المنشورة، مما يستبدل قرارات Z3 غير المتحقق منها بنظريات مدققة عبر النواة، بينما يكشف في الوقت نفسه عن عدة عيوب وتناقضات خفية في مسار الإثبات الأصلي ويعالجها.