Scoped MSO, Register Automata, and Expressions: Equivalence over Data Words

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

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

في نظرية اللغات الكلاسيكية فوق الأبجديات المحدودة، تُوصَف اللغات المنتظمة بشكل متكافئ بواسطة الأوتوماتا المحدودة، والتعبيرات المنتظمة، ومنطق الدرجة الأولى المونادي (MSO). ومع ذلك، ينهار هذا التكافؤ بالنسبة لـ كلمات البيانات (متتاليات فوق $\Sigma \times A$، حيث $A$ هو نطاق بيانات لانهائي مثل $\mathbb{N}$ أو $\mathbb{Q}$).

• الفجوة: المنطقيات الموجودة لكلمات البيانات إما أنها ضعيفة جداً بحيث لا تستطيع استيعاب القوة الكاملة للأوتوماتا المسجلة، أو قوية جداً (مما يؤدي إلى عدم القابلية للتقرير). وتحديداً، فإن منطق MSO القياسي الممتد مع تساوي البيانات يسمح بترميز آلات تورينج، مما يجعل مسألة القابلية للتحقق (satisfiability) غير قابلة للتقرير.
• التحدي: تُعد NRAg هي المعيار المرجعي الأساسي للغات البيانات، لكنها تفتقر إلى توصيف منطقي طبيعي. علاوة على ذلك، تسمح NRAg بـ "التخمين" (إدخال قيم بيانات جديدة ليست موجودة في المدخلات)، مما يعقد التعريفات المنطقية التي تعتمد عادةً على القيم الموجودة في بنية المدخلات.

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

يقدم المؤلف صياغتين جديدتين لسد الفجوة: المنطق المحدود النطاق (Scoped MSO) (منطق) والتعبيرات المنتظمة للبيانات (DRE).

أ. المنطق المحدود النطاق ($MSOS$)

تعرف الورقة نسخة مقيدة من MSO مصممة خصيصاً لقدرات الأوتوماتا المسجلة.

• نمط القطعة ($\mathcal{X}\phi$): عامل مبتكر يقوم بتقييم صيغة $\phi$ على جميع الفترات المتصلة (القطع) المحددة بواسطة مجموعة من نقاط القطع $X$. يسمح هذا للمنطق بالتفكير في "الفترات الحية" لقيم السجلات دون التكميم العالمي.
• القيود النحوية (صحة التكوين): لمنع عدم القابلية للتقرير، يفرض المنطق قيداً صارماً على صيغ البيانات الذرية $R(x)$: يمكن أن تحتوي على متغير متداخل واحد على الأكثر (متغير مرتبط بمكمم داخل نفي أو نطاق). هذا يمنع المقارنات العشوائية للبيانات بين المواضع المختلفة التي تتجاوز الذاكرة المحدودة للأوتوماتا المسجلة.
• النطاق: ثبت أن المنطق يكافئ NRAg بشرط أن يدعم نطاق البيانات إلغاء التخمين القوي.

ب. التعبيرات المنتظمة للبيانات (DRE)

تقترح الورقة حساب تعبيرات بسيط يحاكي بنية التعبيرات المنتظمة الكلاسيكية ولكنه يتكيف مع قيود البيانات.

• المناطق الخالية من المكممات: الوحدات البنائية الذرية ليست كلمات مفردة بل "مناطق" (مجموعات من الكلمات التي تشترك في نفس النوع الخالي من المكممات).
• الارتباط الانكماشي $k$ ($\cdot_k$): عامل ارتباط معلمي. على عكس الارتباط القياسي، يتطلب $K \cdot_k L$ تداخلاً بطول $k$ بين نهاية الكلمة في $K$ وبداية الكلمة في $L$. يمثل هذا المعامل $k$ عدد السجلات، وهو ما ينمذج الواجهة المحدودة التي يتم من خلالها نقل قيم البيانات بين مكونات الأوتوماتا.
• $k$-Star: عامل تكرار متكيف مع الارتباط الانكماشي هذا.

ج. مبرهنة التكافؤ

النتيجة المركزية هي إرساء التكافؤ التالي لأي أبجدية محدودة $\Sigma$ وذرات $A$ (حيث تدعم $A$ إلغاء التخمين القوي):
$$\text{NRAg}[\Sigma, A] \equiv \text{DRE}[\Sigma, A] \equiv MSOS[<, \Sigma, A]$$

3. النتائج التقنية والبراهين

• إلغاء التخمين القوي: تصيغ الورقة الشرط حيث يمكن تحويل NRAg ذات "التخمين القوي" (تخمين قيم لا تظهر أبداً في المدخلات) إلى أوتوماتا مكافئة تقوم فقط بـ "التخمين الضعيف" (تخمين القيم التي تظهر بالفعل في المدخلات). تنطبق هذه الخاصية على النطاقات القياسية مثل ذرات التساوي ($\mathbb{N}, =$) وذرات الترتيب الكثيف ($\mathbb{Q}, <$).
• من الأوتوماتا إلى التعبيرات: يتضمن البرهان فصل التحكم المحدود (الانتقالات) عن اتساق البيانات. يتم وصف تدفق التحكم بواسطة تعبير منتظم كلاسيكي، بينما يتم ترميز قيود البيانات في كتل محلية بطول $2k+1$ تمثل حالات السجل قبل وأثناء وبعد الانتقال.
• من التعبيرات إلى الأوتوماتا: يستخدم البناء الارتباط الانكماشي $k$ لمحاكاة آلية "التخمين وإعادة التشغيل". تخمن الأوتوماتا التداخل بطول $k$ (الواجهة)، وتخزنه في السجلات، ثم تعيد تشغيله للتحقق من الاتساق بين الجزئين المتصلين.
• من المنطق إلى الأوتوماتا: يتضمن الترجمة من $MSOS$ إلى NRAg "فك" نمط النطاق. يتم التعامل مع المتغيرات العليا بواسطة مسارات مساعدة تحمل قيم الشهود. يتم تجميع المنطق في صيغة اختبار محلي (تتحقق فقط من المواضع الحالية) فوق أبجدية موسعة، والتي يتم التعرف عليها بعد ذلك بواسطة أوتوماتا ذات 0 سجل، ثم تُسقط مرة أخرى على الأبجدية الأصلية.
• من الأوتوماتا إلى المنطق: يستخدم الاتجاه العكسي "الفترات الحية" لقيم السجلات. يخمن المنطق هيكل التشغيل (تسلسل الانتقالات) ويستخدم نمط $\mathcal{X}$ لاختيار مواضع الشهود بشكل متكرر لقيم السجلات ضمن فتراتها الحية. يسمح "التنافر المتبادل" للفترات التشغيلية (الفترات المكونة من أزواج النطاقات الحية للسجلات) للمنطق باختيار الشهود بشكل مستقل دون انتهاك شرط صحة التكوين.

4. الأهمية والآثار

1. استعادة المتانة: نجح هذا العمل في توسيع "مبرهنة كليين" الكلاسيكية (الأوتوماتا $\leftrightarrow$ التعبيرات $\leftrightarrow$ المنطق) إلى مجال كلمات البيانات، مما يوفر إطاراً نظرياً موحداً.
2. القابلية للتقرير: من خلال توصيف NRAg عبر $MSOS$، تشير الورقة إلى أن مسألة القابلية للتحقق لـ $MSOS$ قابلة للتقرير إذا وفقط إذا كانت مسألة الفراغ لـ NRAg قابلة للتقرير. وبما أن مسألة الفراغ لـ NRAg قابلة للتقرير للذرات القياسية، فإن هذا يوفر جزءاً منطقياً قابلاً للتقرير لكلمات البيانات.
3. أداة للمسائل المفتوحة: يوفر الصياغة المنطقية مجموعة أدوات جديدة لمعالجة المسائل المفتوحة في نظرية لغات البيانات. على سبيل المثال، قد توفر رؤى حول تخمين كولكومبيت المتعلق بقابلية الفصل بين لغات NRAg المنفصلة بواسطة الأوتوماتا المسجلة غير الغامضة.
4. التوسعات: تظهر الورقة أن الإطار يمتد إلى الكلمات اللانهائية ($\omega$-words) مع قبول Büchi ويمكن تكييفه مع الفئات الفرعية مثل الأوتوماتا المسجلة الحتمية (بدون تخمين) عن طريق تعديل مكممات النطاق.

باختاً، تقدم الورقة نظرية وصفية دقيقة للأوتوماتا المسجلة، وتثبت أنه مع القيود النحوية الصحيحة (Scoped MSO) والعمليات الهيكلية ($k$-contracting concatenation)، يمكن استيعاب القوة التعبيرية للأوتوماتا المسجلة بالكامل بواسطة كل من المنطق والتعبيرات، مما يحاكي أناقة نظرية اللغات المنتظمة الكلاسيكية.