Completeness of Synthesis under Realizability Assumptions using Superposition

ملخص تقني: اكتمال التركيب تحت فرضيات القابلية للتحقق باستخدام التراكب (Superposition)

بيان المشكلة
تتناول الورقة مشكلة التركيب الآلي للبرامج، وتحديداً مهمة اشتقاق برنامج خالٍ من التكرار (recursion-free) من مواصفات منطقية من الدرجة الأولى. يكمن التحدي الجوهري في وجود "رموز غير قابلة للحساب" (uncomputable symbols) ضمن المواصفات. هذه الرموز، والتي قد تشمل محمولات (predicates) محددة من قبل المستخدم أو دالات سكولم (Skolem functions) التي يتم إدخالها أثناء البحث عن البرهان، لا يمكن أن تظهر في البرنامج النهائي المُركَّب. يجب بناء البرنامج المُركَّب حصرياً من "رموز قابلة للحساب" (مثل الحساب القياسي، والدالات المعرفة من قبل المستخدم)، بينما قد تخلط المواصفات بين الرموز القابلة وغير القابلة للحساب.

قدم العمل السابق لـ Hozzová وآخرون [14] إطار عمل يعتمد على التشبع باستخدام حساب التراكب (superposition calculus) لحل هذه المشكلة. وبينما ثبت أن ذلك النهج سليم (أي أن أي برنامج مشتق هو برنامج صحيح)، إلا أن مسألة اكتماله ظلت سؤالاً مفتوحاً. وتحديداً، لم يكن من الواضح ما إذا كان الحساب قادراً على ضمان إيجاد حل إذا كان موجوداً بالفعل (فرضية القابلية للتحقق/realizability assumption). تحدد الورقة سيناريوهات محددة يفشل فيها حساب [14] في اشتقاق حل حتى عندما يكون البرنامج القابل للحساب موجوداً، ويرجع ذلك أساساً إلى القيود في كيفية التعامل مع ترتيب المصطلحات (term orderings)، ودوال الاختيار (selection functions)، والتفاعل بين المصطلحات القابلة وغير القابلة للحساب.

المنهجية: حساب SUPRA
يقترح المؤلفون حساباً مطوراً يسمى SUPRA (التراكب مع فرضيات القابلية للتحقق) لمعالجة عدم اكتمال إطار العمل السابق. تتضمن منهجية العمل ثلاثة تعديلات تقنية على نهج التراكب القياسي:

1. الترتيبات والانتخاب المجزأ (Partitioned Orderings and Selection):
   تُدخل الورقة "ترتيب تبسيط مجزأ". في هذا الترتيب، يكون أي مصطلح غير قابل للحساب أرضي (ground uncomputable term) أكبر تماماً من أي مصطلح قابل للحساب أرضي. وبناءً على ذلك، يتم تقييد دالة الاختيار لتختار دائماً جميع المصطلحات القصوى (maximal literals) في الجملة (clause). وهذا يضمن أن الاستدلالات التي تتضمن مصطلحات غير قابلة للحساب (الأكبر حجماً) تُعطى الأولوية على تلك التي تتضمن مصطلحات قابلة للحساب فقط، مما يمنع الحساب من التعثر في اشتقاقات حيث تعيق القيود غير القابلة للحساب حل الفروع القابلة للحساب.

2. قاعدة التجريد (Abs):
   للتعامل مع الحالات التي تحتوي فيها المعادلات غير القابلة للحساب على مصطلحات فرعية قابلة للحساب تحتاج إلى معالجة قبل معالجة المصطلح غير القابل للحساب، أدخل المؤلفون قاعدة استدلال مساعدة تسمى Abs. تقوم هذه القاعدة بتجريد المصطلحات الفرعية القابلة للحساب داخل المصطلحات غير القابلة للحساب عبر استبدالها بمتغيرات جديدة وإضافة قيود عدم المساواة (على سبيل المثال، تحويل $s[k] \approx t$ إلى $s[x] \approx t \land x \neq k$). تعمل هذه الآلية على فصل الاستدلال حول الرموز غير القابلة للحساب عن الرموز القابلة، مما يسمح للحساب بمعالجة المصطلحات غير القابلة للحساب دون انتهاك قيد القابلية للحساب الخاص بحد الإجابة (answer term).

3. قواعد استدلال منقحة:
   يستخدم الحساب نوعين من قواعد التراكب:

• SupC: يُدخل مُنشئ ite (إذا-إذن-وإلا) في حد الإجابة عند التفرع بناءً على مصطلح مساواة.
• SupU: يوحد حدود الإجابة من المقدمات مباشرة، متجنباً إضافة قيود قد تؤدي إلى شروط غير قابلة للحساب.
  كما يستبدل الحساب "الموحدات القابلة للحساب" (computable unifiers) المستخدمة في [14] بـ "الموحدات الأكثر عمومية" (MGUs) القياسية، معتمداً على الترتيب المجزأ وقاعدة Abs لضمان بقاء حدود الإجابة الناتجة قابلة للحساب.

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

• تحديد عدم الاكتمال: توضح الورقة عبر أمثلة مضادة (مثل سيناريو جدولة ورشة عمل وسيناريو معالجة الثوابت) أن حساب [14] ليس كاملاً تحت فرضيات القابلية للتحقق؛ حيث يفشل في إيجاد الحلول عندما يمنع اختيار المصطلحات أو ترتيبها الاستدلالات الضرورية على الرموز غير القابلة للحساب.
• إطار عمل SUPRA: يعرف المؤلفون حساب SUPRA، الذي يتضمن الترتيب المجزأ، وقاعدة Abs، وقيود الاختيار المحددة.
• إثبات السلامة (Soundness Proof): تثبت الورقة أن SUPRA سليم فيما يتعلق بدلالات جمل الإجابة، مما يضمن أن أي برنامج مشتق هو حل صالح لمواصفات التركيب.
• إثبات الاكتمال (Completeness Proof): المساهمة النظرية الرئيسية هي إثبات أن SUPRA كامل تحت فرضية القابل القابلية للتحقق. يوضح المؤلفون أنه إذا وجد برنامج قابل للحساب يحقق المواصفات، فإن حساب SUPRA (عند استخدامه بشكل شامل مع قاعدة Abs) سيضمن اشتقاق حل. يبني الإثبات نموذجاً للمجموعة المشبعة من الجمل، ويوضح أنه إذا لم يتم اشتقاق حل، فسيحدث تناقض فيما يتعلق بقابلية إشباع المواصفات المنفية.

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

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

باختصار، تقوم الورقة بتنقيح حساب التراكب للتركيب عبر إدخال ترتيب مجزأ وآلية تجريد، وتثبت أن هذه التعديلات كافية لضمان الاكتمال لتركيب البرامج الخالية من التكرار في وجود رموز غير قابلة للحساب.