💻 computer science

Type Theory With Erasure

تقدم هذه الورقة صياغة بنيوية لنظرية النوع مع المحو بوصفها نظرية جبرية معممة من الدرجة الثانية (SOGAT) تميز بين البيانات ذات الصلة بوقت التشغيل والبيانات غير ذات الصلة عبر تمييز طوري، مؤسسةً نماذجها الدلالية، وتحفظيتها على نظرية مارتن-لوف للأنواع، وصحتها لاستخراج الكود إلى حساب لامدا غير النمطي.

المؤلفون الأصليون: Constantine Theocharis, Edwin Brady

نُشر 2026-05-04

📖 4 دقيقة قراءة☕ قراءة في استراحة قهوة

CC BY 4.0

المؤلفون الأصليون: Constantine Theocharis, Edwin Brady

البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل

تخيل أنك طاهٍ يقوم بإعداد مأدبة ضخمة ومعقدة. لديك كتاب وصفات (وهو نظرية الأنواع - Type Theory) يخبرك بالضبط كيفية إعداد كل طبق. بعض المكونات في الوصفة ضرورية للمذاق النهائي (مثل الملح أو البروتين الرئيسي)، بينما البعض الآخر هو مجرد مرجع لك أثناء عملية الطهي (مثل العلامة التجارية المحددة للوعاء، أو ملاحظة تقول "حرك بلطف").

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

هذه الورقة البحثية، "نظرية الأنواع مع المحو" (Type Theory With Erasure)، من تأليف كونستانتين ثيوتشاريس وإدوين برادي، تقترح طريقة أكثر نظافة وتنظيمًا لكتاب الوصفات بحيث يعرف الكمبيوتر بالضبط ما الذي سيبقيه وما الذي سيرميه قبل أن يبدأ حتى في الطهي.

إليك تفصيل فكرتهم باستخدام تشبيهات بسيطة:

1. الوضعان: "ملاحظات الطاهي" مقابل "الوجبة"

قدم المؤلفون قاعدة بسيطة: كل معلومة في الكود يتم وسمها بأحد ملصقين:

وقت التشغيل (الوجبة): هي البيانات التي يجب أن تظل موجودة حتى النهاية. إنها الطعام الفعلي الذي يأكله الزبون.
الممحو (الملاحظات): هي بيانات تُستخدم فقط لإثبات صحة الوصفة، ولكن يتم التخلص منها قبل تقديم الوجبة.

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

2. المفتاح السحري: "التمييز بين المراحل"

الابتكار الجوهل هو مفهوم "التمييز بين المراحل" (Phase Distinction). تخيل مفتاحًا سحريًا في المطبخ يسمى #.

عندما يكون المفتاح في وضع الإيقاف (OFF)، فأنت في "مرحلة الإنشاء". يمكنك رؤية كل شيء: الملاحظات، المكونات، والأدوات.
عندما يكون المفتاح في وضع التشغيل (ON)، فأنت في "مرحلة التقديم". تختفي الملاحظات سحريًا.

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

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

### 3. المكونات "الشبحية"

في هذا النظام، يمكنك الحصول على "مكونات شبحية".

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

4. "المترجم العالمي" (النموذج)

لم يكتفِ المؤلفون بكتابة قاعدة فحسب؛ بل بنوا "مترجمًا" رياضيًا لإثبات نجاحها.

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

5. لماذا يهم هذا (التطبيق "اللعبة")

بنى المؤلفون نموذجًا أوليًا صغيرًا يعمل (مُنشئ "لعبة" - toy elaborator) لإظهار أن هذا ليس مجرد نظرية.

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

الملخص

فكر في هذه الورقة البحثية كأنها ابتكار نوع جديد من كتب الوصفات حيث يمكن للمؤلف تحديد "غير قابل للأكل" بوضوح على التعليمات.

الطريقة القديمة: يتعين على الكمبيوتر تخمين أي التعليمات "غير قابلة للأكل"، وغالبًا ما يرتكب أخطاءً أو يقوم بعمل إضافي.
الطريقة الجديدة: يحدد المؤلف ذلك بوضوح. يتبع الكمبيوتر القواعد، ويرمي التعليمات "غير القابلة للأكل"، ويقدم وجبة مثالية وخفيفة الوزن.

تثبت الورقة أن هذا النظام سليم رياضيًا، ويتعامل مع الأنواع المعقدة، ويمكن تنفيذه في برمجيات حقيقية لجعل البرامج أسرع وأكثر موثوقية.

إليك ملخص تقني مفصل لورقة البحث "Type Theory With Erasure" (نظرية النوع مع المحو) للباحثين كونستانتين ثيوتشاريس وإدوين برادي.

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

في لغات البرمجة ذات الأنواع المعتمدة (مثل Agda وIdris وRocq)، تعتمد الأنواع غالبًا على القيم. وهذا يخلق غموضًا جوهريًا: ما هي الأجزاء من البرنامج ذات الصلة حسابيًا عند وقت التشغيل (runtime)، وما الذي يمكن محوه بأمان أثناء عملية التجميع (compilation)؟

النهج الحالي: تعتمد الحلول الحالية غالبًا على النظرية النوعية الكمية (QTT)، التي تستخدم نصف زمرة كمية (على سبيل المثال، $\{0 < \omega\}$ ) لتتبع استخدام المتغيرات. ورغم فعاليتها، إلا أن QTT تفرض تعقيدات تتعلق بالقيود الهيكلية والخطية. وتستخدم مقاربات أخرى "أنواعًا شبحية" (ghost sorts) أو تحليلًا شاملًا للبرنامج يعتمد على الاستدلال، وهي طرق قد تكون هشة وغير متوقعة في الأنواع المعتمدة المعقدة.
الفجوة: هناك حاجة إلى صياغة هيكلية، ونمطية، وخالية من الاختزال لعملية المحو، تتكامل بسلاسة مع الميتا-نظرية للأنواع القياسية، وتدعم استخراج الكود (code extraction)، وتوفر أساسًا دلاليًا واضحًا دون الاعتماد على دلالات كمية معقدة.

2. المنهجية

يقترح المؤلفون نسخة هيكلية من نظرية النوع مع المحو مصاغة كـ نظرية جبرية معممة من الدرجة الثانية (SOGAT).

التمييز الطوري الاصطناعي (Synthetic Phase Distinction): بدلًا من استخدام نصف الزمر الكمية، صاغ المؤلفون المحو كـ تمييز طوري باستخدام قضية اصطناعية، يُرمز لها بـ # (علامة المحو).
- يعتبر السياق $\Gamma$ "محوًا" إذا كان يحتوي على القضية $\#$ (أي $\# \in \Gamma$ ).
- هذا يخلق تمييزًا بين وضع وقت التشغيل ( $\omega$ ) والوضع الممحو ($0$).
- من المهم ملاحظة أن $\#$ هي قضية ليس لها قيمة حقيقة؛ لا يمكن بناؤها أو تفريغها بشكل تعسفي. إنها تعمل كعلامة تسمح بتحويل المصطلحات بين الأوضاع.
آلية الإكراه (Coercion Mechanism): تقدم النظرية نوعين من الإكراه:
- المحو ( $\#$ ): إذا كان المصطلح $a$ من النوع $A$ في سياق ممتد بـ $\#$ ، فيمكن إكراهه إلى مصطلح ممحو ( $\# a : 0: A$ ).
- **الرفع ( $\$ $):** إذا كان المصطلح$ a $ممحيًا، فيمكن رفعه إلى مصطلح وقت تشغيل تحت افتراض$ # $($ \ $a : \omega: A$ ).
- هذان الإكراهان هما معكوسان متبادلان حتى التساوي التعريفي، مما يضمن أن المصطلحات الممحاة لا تعتمد على بيانات وقت التشغيل.
صياغة SOGAT النمطية: تُعرَّف النظرية كـ SOGAT تمتد من نظرية مارتن-لوف للأنواع (MLTT). يسمح هذا للمؤلفين بالاستفادة من الميتا-نظرية الموجودة لـ SOGAT، بما في ذلك الدلالات الفانكتورية (functorial semantics) وبناء النماذج عبر فئات "الأصناف مع العائلات" (Categories with Families - CwFs).

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

أ. الصياغة النظرية

تعريف SOGAT: تُعرف الورقة TT0 (نظرية النوع مع المحو) كـ SOGAT. وهي تتضمن الأنواع ( $Ty$ )، والمصطلحات ( $Tm$ ) المفهرسة بالأوضاع $\{0, \omega\}$ ، وعلامة المحو ( $\#$ ).
الجزئية الممحاة المشتقة: من المساهمات الهامة أن النظرية لا تحتاج إلى تعريف نسخ ممحاة لكل مكون مصطلح بشكل صريح (مثل $\Pi_0, \Sigma_0$ ). نظرًا لوجود تماثل بين السياقات التي تحتوي على $\#$ والسياقات التي لا تحتوي عليها، فإن الجزء الممحى بالكامل يُشتق تلقائيًا من الجزء الخاص بوقت التشغيل.
الأنواع الاستقرائية: يدعم الإطار الأنواع الاستقرائية حيث يمكن وسم وسائط محددة (مثل الفهارس) بأنها ممحية. كما يتعامل مع الأنواع الاستقرائية "الغريبة" (exotic) حيث قد توجد البنائات نفسها فقط في الوضع الممحى.

ب. النماذج الدلالية

نموذج Fam(Set): يبني المؤلفون نموذجًا قياسيًا في فئة عائلات المجموعات ($Fam(Set)$).
- في هذا النموذج، يكون الكائن عبارة عن زوج $(X_0, X_1)$ حيث تمثل $X_0$ البيانات الممحاة و $X_1$ تمثل بيانات وقت التشغيل.
- تُفسر علامة المحو $\#$ كـ "قضية ضئيلة" (tiny proposition) (كائن $\phi$ يجعل الأس لـ $\phi$ يعزل المكون الأساسي).
- يتوسع هذا النموذج إلى أي توبوس غروثينديك (Grothendieck topos) مجهز بقضية ضئيلة.
الأكوان المسحوقة (Squashed Universes): للتعامل مع الأكوان في السياق الممحى، قدم المؤلفون "الأكوان المسحوقة" ( $\sqrt{\phi}U$ ). هذه الأكوان هي كائنات $\phi$ -modal تحتفظ بهيكل الأكوان القياسية ولكنها تحقق شرط أن أليافها (fibers) قابلة للانكماش (contractible)، مما يسمح بوجودها في السياقات الممحاة دون حمل بيانات وقت التشغيل.

ج. استخراج الكود وصحته

استخراج لغة لامدا غير المحددة: يبني المؤلفون نموذجًا يستخرج برامج TT0 إلى لغة لامدا غير المحددة.
- المصطلحات في وقت التشغيل ترتبط بمصطلحات لامدا.
- المصطلحات الممحاة ترتبط بالكائن النهائي (terminal object) (أي تختفي فعليًا).
- السياقات التي تحتوي على متغيرات ممحية تكون متماثلة مع السياقات التي لا تحتوي عليها.
اللصق (Gluing) والعلاقات المنطقية: لإثبات الصحة، يستخدم المؤلفون تقنية "اللصق" (gluing) لبناء علاقة منطقية بين نموذج استخراج الكود ونموذج المجموعة القياسي.
- مبرهنة 27 (عدم التداخل): تثبت أن كل دالة ممحية هي دالة ثابتة في وقت التشغيل. إذا كانت الدالة تأخذ وسيطًا ممحيًا، فإن مخرجها لا يمكن أن يعتمد على ذلك الوسيط في وقت التشغيل.
- مبرهنة 25 و26: تثبت "الكانونية" (canonicity) وأن الكود المستخرج يتتبع التفسير الدلالي.

د. التنفيذ

المُلبِغ (Elaborator): تم تنفيذ مُلبِغ تجريبي في لغة Agda. يأخذ لغة عالية المستوى (تشبه Idris/Agda مع وسمات 0 و @0) ويقوم بتلبيغها إلى جوهر SOGAT.
توحيد الأنماط (Pattern Unification): يوضح المؤلفون أنه نظرًا لأن الجوهر هيكلي، يمكن إعادة استخدام خوارزميات توحيد الأنماط القياسية دون الحاجة إلى فحوصات كمية معقدة أو آليات تعميم خاصة للمتغيرات الميتاتغيرة (metavariables) الممحاة، مما يحل المشكلات الموجودة في الأنظمة الحالية مثل Agda وIdris 2.

4. النتائج

الحفاظ (Conservativity): ثبت أن النظرية محافظة على MLTT. إضافة المحو لا تزيد من القدرة الإثباتية لنظرية النوع؛ فأي مبرهنة يمكن إثباتها في TT0 يمكن إثباتها في MLTT القياسية.
الاستقلال: ثبت أن البيانات الممحاة مستقلة عن بيانات وقت التشغيل. المصطلح الممحى في سياق $\Gamma$ يتوافق بشكل فريد مع مصطلح ممحى في السياق "المصفر" $0\Gamma$ (حيث يتم ضبط جميع الأوضاع على 0).
صحة الاستخراج: يؤكد إثبات اللصق أن عملية الاستخراج تحافظ على السلوك الحسابي وتمحو البيانات غير الضرورية بشكل صحيح، مما يضمن أن الكود الناتج آمن وفعال.

5. الأهمية

الوضوح الهيكلي: من خلال الانتقة من نصف الزمر الكمية إلى تمييز طوري اصطناعي، توفر الورقة أساسًا أنظف وأكثر نمطية للمحو. إنها تفصل بين مفهوم المحو وآلية تتبع الموارد.
توجيه التنفيذ: يسهل النهج الهيكلي تنفيذ الملبغات (elaborators) وفاحصات الأنواع. فهو يلغي الحاجة إلى فحوصات الكمية العشوائية أثناء التوحيد، مما قد يحل الأخطاء في الأنظمة الحالية مثل Idris 2 وAgda.
الأساس الدلالي: يربط استخدام توبوسات غروثينديك والقضايا الضئيلة عملية المحو بالمنطق الفئوي الأوسع، مما يسمح باستخدام "حساب تايت الاصطناعي" (Synthetic Tait Computability) في البراهين الميتا-نظرية.
التوسعات المستقبلية: تم تصميم الإطار ليكون قابلًا للتوسيع، مما يدعم العمل المستقبلي المحتمل على أنواع وقت التشغيل، والتمييز الطوري المتعدد (للبرمجة المرحلية/Metaprogramming)، والتكامل مع نظرية النوع التكعيبية (Cubical Type Theory).

باختصار، تقدم هذه الورقة نهجًا صارمًا وهيكليًا وذا أساس دلالي لنظرية النوع مع المحو، حيث تقدم ضمانات نظرية (الحفاظ، عدم التداخل) وفوائد عملية لتنفيذ المترجمات واستخراج الكود.