2025-11-10T02:31:47.007663

CoLF Logic Programming as Infinitary Proof Exploration

Chen, Pfenning
Logical Frameworks such as Automath [de Bruijn, 1968] or LF [Harper et al., 1993] were originally conceived as metalanguages for the specification of foundationally uncommitted deductive systems, yielding generic proof checkers. Their high level of abstraction was soon exploited to also express algorithms over deductive systems such as theorem provers, type-checkers, evaluators, compilers, proof transformers, etc. in the paradigm of computation-as-proof-construction. This has been realized in languages such as $λ$-Prolog [Miller et al., 1991] or Elf [Pfenning, 1991] based on backward chaining, and LolliMon [Lopez et al., 2005] or Celf [Schack-Nielsen and Schuermann, 2008], which integrated forward chaining. None of these early frameworks supported the direct expression of infinitary objects or proofs, which are available in the recently developed CoLF$^ω$ [Chen, 2023]. In this work-in-progress report, we sketch an approach to computation-as-proof-construction over the first-order fragment of CoLF$^ω$ (called CoLF$^ω_1$ ) that already includes infinitary objects and proofs. A key idea is the interpretation of logic variables as communication channels and computation as concurrent message-passing. This is realized in a concrete compiler from CoLF$^ω_1$ to Sax, a proof-theoretically inspired parallel programming language based on the proof-reduction in the semi-axiomatic sequent calculus [DeYoung et al., 2020].
academic

برمجة منطق CoLF كاستكشاف إثبات لا نهائي

المعلومات الأساسية

  • معرّف الورقة: 2510.12302
  • العنوان: CoLF Logic Programming as Infinitary Proof Exploration
  • المؤلفون: Zhibo Chen (جامعة كارنيجي ميلون)، Frank Pfenning (جامعة كارنيجي ميلون)
  • التصنيف: cs.LO (المنطق في علوم الحاسوب)
  • المؤتمر المنشور فيه: LFMTP 2025 (ورشة العمل الدولية للأطر المنطقية واللغات الوصفية: النظرية والممارسة)
  • رابط الورقة: https://arxiv.org/abs/2510.12302

الملخص

تستكشف هذه الورقة طريقة لتنفيذ "الحساب كبناء إثبات" على القطاع من الدرجة الأولى من CoLF^ω (CoLF^ω_1)، وهو قطاع يحتوي بالفعل على كائنات وإثباتات لا نهائية. الفكرة الأساسية هي تفسير المتغيرات المنطقية كقنوات اتصال وتفسير الحساب كنقل رسائل متزامن. يتم تجسيد هذه الفكرة من خلال تطبيق مترجم ملموس يترجم CoLF^ω_1 إلى Sax—لغة برمجة متوازية مستوحاة من نظرية الإثبات تعتمد على اختزال الإثبات في حساب التسلسل شبه البديهي.

الخلفية البحثية والدافع

خلفية المشكلة

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

الدافع البحثي

  1. دعم الحساب اللا نهائي: الحاجة إلى دلالات ديناميكية قادرة على حساب المخرجات بشكل متزايد من المدخلات، مشابهة للمحولات بين التدفقات
  2. تجنب التراجع: ضمان ثابت من خلال فحوصات النمط والفرادة أن كل مدخل فريد له إثبات واحد على الأكثر
  3. المعالجة المتوازية: الاستفادة من الاتصال بين المتغيرات المشتركة لتحقيق التوازي و-بين المقدمات المتعددة

المساهمات الأساسية

  1. اقتراح لغة برمجة منطقية CoLF^ω_1: تدعم الإثباتات ذات تمثيل الحدود اللا نهائية، بناء الإثبات بدون تراجع، تقييم المقدمات المتوازية باستخدام المتغيرات المنطقية المشتركة للاتصال
  2. نموذج حساب مبتكر: تفسير المتغيرات المنطقية كقنوات اتصال وتفسير الحساب كنقل رسائل متزامن
  3. تطبيق مترجم: تطبيق مترجم ملموس من CoLF^ω_1 إلى Sax
  4. نظام أمثلة غني: يتضمن تطبيقات معالجة التدفقات وسلسلة فيبوناتشي والعمليات المتكاملة وغيرها من العلاقات المعقدة

شرح الطريقة

تعريف المهمة

تبحث هذه الورقة عن كيفية تنفيذ البرمجة المنطقية في إطار منطقي يدعم الكائنات اللا نهائية، والمهمة المحددة هي:

  • المدخل: مواصفات برنامج CoLF^ω_1
  • المخرج: الهياكل اللا نهائية (مثل التدفقات) المحسوبة من خلال نقل الرسائل المتزامن
  • القيود: بدون تراجع، دعم الحساب المتوازي، ضمان الفرادة

البنية التقنية الأساسية

1. نظام أنواع البيانات

conat: cotype.          % نوع الأعداد الطبيعية المشتركة
z: conat.               % منشئ الصفر
s: conat -> conat.      % منشئ الخليفة

stream: cotype.         % نوع التدفق
cons: conat -> stream -> stream.  % منشئ التدفق

2. تعريف العلاقات وإعلان النمط

add: conat -> conat -> conat -> cotype. %mode add + + -.
add_z : add z A A.
add_s : add A B C -> add (s A) B (s C).

3. دلالات الحساب

يتم تعريف سلوك البرنامج من خلال العمليات التالية:

  • عمليات القناة: يتم التعامل مع كل معامل كقناة اتصال، ويحدد إعلان النمط قنوات الإدخال (+) أو الإخراج (-)
  • عمليات القراءة والكتابة: يمكن للبرنامج قراءة القيم من قنوات الإدخال وكتابة القيم إلى قنوات الإخراج
  • إعادة توجيه القناة: إعادة توجيه قناة الإدخال مباشرة إلى قناة الإخراج
  • الإنشاء المتوازي: تخصيص قنوات جديدة وإنشاء عمليات جديدة

نقاط الابتكار التقني

1. ضمان عدم التراجع

يتم ضمان عدم التراجع من خلال فحص فرادة ثابت يضمن أن هناك إجراء واحد على الأكثر في كل نقطة برنامج، مما يلغي الحاجة إلى التراجع في البرمجة المنطقية التقليدية.

2. نموذج التنفيذ المتزامن

mult_s : mult A B C -> add B C D -> mult (s A) B D.

في تعريف الضرب أعلاه، يمكن تقييم المقدمتين mult A B C و add B C D بشكل متوازي، مع الاتصال من خلال المتغير المشترك C.

3. الحساب المتزايد

يدعم التقييم الكسول، عندما يتم الكشف عن المخرجات D تدريجياً، لا تحتاج الخطوات B الأولى إلى تقييم mult A B C لأن C تبقى دون تغيير.

إعداد التجارب

حالات الاختبار

تتحقق الورقة من فعالية الطريقة من خلال عدة أمثلة ملموسة:

  1. عمليات التدفق الأساسية:
    • repeat n: تدفق يكرر الرقم n بلا نهاية
    • up n: تدفق متزايد يبدأ من n
  2. العلاقات المعقدة:
    • إضافة الأعداد الطبيعية المشتركة
    • الإضافة النقطية للتدفقات
    • توليد سلسلة فيبوناتشي
  3. العمليات المتقدمة:
    • العمليات المتكاملة (المجاميع التراكمية)
    • توليد تدفقات الأعداد الزوجية

تفاصيل التطبيق

  • يولد المترجم كود Sax من كود مصدر CoLF^ω_1
  • التقييم يتوقف بعد الوصول إلى عمق محدد مسبقاً
  • يدعم نقل الرسائل بين العمليات المتزامنة

نتائج التجارب

النتائج الرئيسية

1. توليد التدفق الأساسي

up z نتيجة التنفيذ:
(cons z
(cons (s z)
(cons (s (s z))
(cons (s (s (s z)))
(cons (s (s (s (s z)))) ...)))))

2. معالجة الكائنات اللا نهائية

omega : conat = s omega.
main : stream = repeat omega.

النتيجة:
(cons (s (s (s (s ...))))
(cons (s (s (s ...)))
(cons (s (s ...))
(cons (s ...)
(cons ...)))))

3. التحقق من الحسابات المعقدة

سلسلة فيبوناتشي:

(cons z
(cons (s z)
(cons (s z)
(cons (s (s z))
(cons (s (s (s z)))
(cons (s (s (s (s (s z)))))
(cons (s (s (s (s (s (s (s (s z)))))))) ...)))))))

نتيجة العملية المتكاملة:

(cons z
(cons (s z)
(cons (s (s (s z)))
(cons (s (s (s (s (s (s z))))))
(cons (s (s (s (s (s (s (s (s (s (s z)))))))))) ...)))))

النتائج التجريبية

  1. التحقق من التوازي: يمكن فعلاً تنفيذ المقدمات المتعددة بشكل متوازي، مع اتصال فعال من خلال المتغيرات المشتركة
  2. معالجة الهياكل اللا نهائية: نجح في معالجة التعريفات العودية اللا نهائية، مثل ω = s ω
  3. الحساب المتزايد: التحقق من فعالية التقييم الكسول والمخرجات المتزايدة

الأعمال ذات الصلة

الأطر المنطقية التقليدية

  • سلسلة LF: إطار LF من Harper وآخرين، يدعم فحص الإثبات الأساسي
  • λ-Prolog/Elf: الحساب كبناء إثبات بناءً على الربط العكسي
  • LolliMon/Celf: أطر متكاملة مع الربط الأمامي

مزايا هذه الورقة مقارنة بالأعمال ذات الصلة

  1. دعم اللا نهاية: أول دعم مباشر للكائنات والإثباتات اللا نهائية في إطار منطقي
  2. نموذج متزامن: نموذج حساب متزامن مبتكر لنقل الرسائل
  3. بدون تراجع: القضاء على الحاجة إلى التراجع من خلال التحليل الثابت

الخلاصة والنقاش

الاستنتاجات الرئيسية

  1. تم تنفيذ لغة برمجة منطقية CoLF^ω_1 تدعم الكائنات اللا نهائية بنجاح
  2. التحقق من جدوى تفسير المتغيرات المنطقية كقنوات اتصال
  3. إثبات فعالية نموذج نقل الرسائل المتزامن في البرمجة المنطقية

القيود

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

الاتجاهات المستقبلية

  1. التوسع إلى CoLF^ω الكامل: دعم الحدود من الدرجة الأعلى وعناصر النوع المعتمد
  2. الاستقراء المختلط والاستقراء المشترك: دعم مزيج من أنواع الاستقراء والاستقراء المشترك
  3. الدلالات الرسمية: توفير وصف رسمي كامل لعملية الترجمة

التقييم المتعمق

المزايا

  1. قوة الابتكار النظري: أول إدخال للكائنات اللا نهائية في إطار البرمجة المنطقية، ذو قيمة نظرية مهمة
  2. اكتمال التطبيق: توفير مسار كامل من النظرية إلى التطبيق، بما في ذلك تطبيق المترجم
  3. أمثلة غنية: عرض واضح لفعالية الطريقة من خلال عدة أمثلة ملموسة
  4. نموذج متزامن جديد: دمج عضوي للبرمجة المنطقية مع الحساب المتزامن

أوجه القصور

  1. التحليل النظري غير كافٍ: كتقرير تقدم، يفتقر إلى التعريف الرسمي للدلالات وإثباتات الصحة
  2. نقص تحليل الأداء: لا توجد معايير الأداء أو تحليل التعقيد
  3. قيود نطاق التطبيق: الإصدار الحالي محدود الميزات، لا يزال بعيداً عن التطبيق العملي

التأثير

  1. المساهمة الأكاديمية: إدخال اتجاه بحثي جديد في مجال البرمجة المنطقية
  2. القيمة العملية: توفير نموذج برمجة جديد لمعالجة الهياكل البيانية اللا نهائية
  3. قابلية التكرار: توفير تطبيق ملموس لتسهيل التحقق والتوسع

السيناريوهات المناسبة

  1. أنظمة معالجة التدفقات: مناسبة للتطبيقات التي تتعامل مع تدفقات البيانات اللا نهائية
  2. الحساب الرمزي: الحسابات التي تحتاج إلى التعامل مع الكائنات الرياضية اللا نهائية
  3. نمذجة الأنظمة المتزامنة: يمكن استخدامها لنمذجة والتحقق من سلوك الأنظمة المتزامنة

المراجع

تستشهد الورقة بالأدبيات المهمة في مجالات الأطر المنطقية ونظرية الإثبات والحساب المتوازي، بما في ذلك:

  • نظام Automath لـ de Bruijn
  • إطار LF لـ Harper وآخرين
  • λ-Prolog لـ Miller وآخرين
  • حساب التسلسل شبه البديهي لـ DeYoung وآخرين

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