Static Analysis of Recursive SHACL

ملخص تقني: التحليل الساكن لـ SHACL العودي (Recursive SHACL)

بيان المشكلة
تتناول الورقة البحثية التعقيد الحسابي لخدمات التحليل الساكن لوثائق SHACL العودية. وبينما تمت دراسة التحقق من صحة SHACL (التحقق مما إذا كان الرسم البياني للبيانات يتوافق مع وثيقة ما) تحت دلالات مختلفة، فإن مشكلة الاستلزام (أو الاحتواء) — أي تقرير ما إذا كانت جميع الرسوم البيانية التي تحقق وثيقة SHACL واحدة ($S_1$) تحقق بالضرورة وثيقة أخرى ($S_2$) — لا تزال غير مستكشفة إلى حد كبير بالنسبة للقيود العودية. وخلافًا للأعمال السابقة التي ركزت فقط على استلزام تعبيرات الأشكال، تدرس هذه الدراسة وثائق كاملة تتكون من تعريفات أشكال عودية وأهداف. ويتقصى المؤلفون هذه المشكلة تحت ثلاث دلالات بارزة: النموذج المدعوم (supported model)، والنموذج المستقر (stable model)، والدلالات جيدة التأسيس (well-founded semantics).

المنهجية
يستخدم المؤلفون نهجًا اختزاليًا، حيث يترجمون وثائق SHACL إلى أنظمة منطقية صورية للاستفادة من نتائج القابلية للتقرير والتعقيد الموجودة.

1. تحليل الدلالات: تثبت الورقة أولاً سلوك SHACL تحت دلالات النموذج المدعوم والنموذج المستقر. وتوضح أنه تحت هذه الدلالات، تكون مشكلة الاستلزام غير قابلة للتقرير (undecidable)، حتى عند قصر تعبيرات الأشكال على الجزء المقابل لمنطق الوصف $\mathcal{ALCIO}$. وقد تم إثبات ذلك عبر الاختزال من مشكلة البلاط (tiling problem) غير القابلة للتقرير، وذلك باستخدام قدرة هذه الدلالات على دعم تعيينات كلية متعددة (أو التحقق "الجريء" - brave validation) لترميز هياكل الشبكة.
2. الترجمة إلى حساب $\mu$-الهجين (Hybrid $\mu$-calculus): بالنسبة لـ الدلالات جيدة التأسيس، والتي تنتج تعييناً فريداً للشكل لأي رسم بياني معطى، طور المؤلفون ترجمة جديدة لوثائق SHACL إلى حساب $\mu$-الهجين الكامل.
   • تستخدم الترجمة دالتين عوديتين متبادلتين، $tr^+$ و $tr^-$، لترجمة الحروف الشكلية الموجبة والسالبة، على التوالي.
   • ومن الأهمية بمكان أن هذه الترجمة تلتقط الدلالات جيدة التأسيس باستخدام صيغة ذات تبادل محدود (limited alternation) لمؤثرات النقطة الثابتة. وتحديداً، تأخذ الصيغة الناتجة الشكل $\mu X. \phi(X)$، حيث يمكن أن تحتوي $\phi$ على صيغ فرعية من الشكل $\nu Y. \psi(X, Y)$، ولكن لا توجد نقاط ثابتة متداخلة داخل النقاط الثابتة الكبرى.
   • وهذا يؤسس رابطاً نظرياً جديداً بين النماذج جيدة التأسيس ومنطق النقطة الثابتة الموجه (fixed-point modal logic).
3. إجراء قرار قائم على الأوتوماتا (Automata-Based Decision Procedure): لتجنب التضخم الأسي المتأصل في ترجمة وثيقة SHACL إلى صيغة واحدة ضخمة من حساب $\mu$-الهجين، قام المؤلفون بتكييف إجراء قرار قائم على الأوتوماتا. لقد استخدموا أوتوماتا الشجرة الزوجية المتبادلة (Two-Way Alternating Parity Tree Automata - 2ATA). وبدلاً من بناء أوتوماتا ذات حالات تقابل جميع الصيغ الفرعية للصيغة المترجمة، استخدموا دوال الترجمة نفسها كدالة انتقال. وهذا يسمح لإجراء القرار بالعمل في وقت محكوم بدالة أسية واحدة من حجم المدخلات الأصلي، بدلاً من حجم الصيغة المترجمة.

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

• عدم القابلية للتقرير تحت الدلالات المدعومة/المستقرة: تثبت الورقة أن استلزام الشكل لـ $\mathcal{ALCIO}$ SHACL غير قابل للتقرير تحت كل من دلالات النموذج المدعوم ودلالات النموذج المستقر. وينطبق هذا حتى على القيود الطبقية (stratified constraints) تحت دلالات النموذج المدعوم.
• القابلية للتقرير تحت الدلالات جيدة التأسيس: في المقابل، تثبت الورقة أن مشكلة الاستلزام لـ SHACL العودية قابلة للتقرير تحت الدلالات جيدة التأسيس.
• حدود التعقيد:
  • قابلية إرضاء الشكل (Shape Satisfiability): تقرير قابلية إرضاء الشكل بالنسبة للقيود لـ $\mathcal{ALCIO}$ SHACL تحت الدلالات جيدة التأسيس هو EXPTIME-complete.
  • قابلية إرضاء الوثيقة (Document Satisfiability): تقرير قابلية إرضاء الوثيقة لـ $\mathcal{ALCIO}$ SHACL تحت الدلالات جيدة التأسيس هو أيضاً EXPTIME-complete.
  • استلزام الوثيقة (Document Implication): تقرير استلزام الوثيقة لـ $\mathcal{ALCIO}$ SHACL تحت الدلالات جيدة التأسيس هو EXPTIME-complete.
  • النماذج المحدودة: تثبت الورقة أن $\mathcal{ALCO}$ SHACL يمتلك خاصية النموذج المحدود تحت الدلالات جيدة التأسيس، بينما لا يمتلكها $\mathcal{ALCI}$ SHACL. ومع ذلك، تظل قابلية الإرضاء والاستلزام المحدودين قابلين للتقرير لـ $\mathcal{ALCIO}$، بحدود عليا تبلغ 3-EXPTIME و 2-EXPTIME على التوالي، والمستمدة من قابلية الإرضاء المحدودة لمنطق النقطة الثابتة المحروس (guarded fixed-point logic).
• الجدة النظرية: تكشف الترجمة أن الدلالات جيدة التأسيس يمكن التقاطها بواسطة حساب $\mu$-الهجين الكامل مع التبادل المحدود، وهو ارتباط لم يتم إثباته سابقاً لهذا السياق الخاص بالبرمجة المنطقية.

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

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