A Bitopological Approach to Finite Reduction and Bounded Exact-Value Certificates for Fitting's Finite Heyting-valued Modal Logic

ملخص تقني: نهج ثنائي الطوبولوجيا للاختزال المحدود وشهادات القيم الدقيقة المحدودة لمنطق فيتينج للمنطق الموجه ذي القيم الهييتينغية المحدودة

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

تتناول الورقة مشكلة الاختزال في الحالة المحدودة (finite-state reduction) واستخراج المثال المضاد (counterexample extraction) ضمن منطق فيتينج (Fitting's logic) ذي القيم الهييتينغية المحدودة. في هذا المنطق، تأخذ الصيغ قيم حقيقة في جبر هيتينغ (Heyting algebra) محدود وثابت $L$ بدلاً من جبر بولياني ثنائي. يتم تفسير مؤثر الضرورة $\Box$ كتقاطع (infimum) لقيم الحقيقة عبر الحالات المتاحة في نموذج كريبكي.

التحدي الجوهري مزدوج:

1. اختزال الحالة: بالنظر إلى نموذج كريبكي محدود $M = (W, R, V)$ ومفردات قضائية محدودة $\Sigma$، كيف يمكن بناء نموذج مختزل يحافظ على القيمة الدقيقة لكل صيغة في $\Sigma$؟ بخلاف التحقق من الصحة الكلاسيكي (classical model checking) حيث يهم فقط الصلاحية (قيمة الحقيقة 1)، يتطلب التحقق متعدد القيم الحفاظ على القيم المتوسطة (مثل عدم اليقين أو الحقيقة الجزئية).
2. بناء الشهادة: بالنسبة لصيغة محددة $\phi$ وحالة $x$ تفشل فيها $\phi$ (أي أن $J\phi K_M(x) \neq 1$)، هل يمكن بناء مثال مضاد محدود وشجري الحجم، بحيث يكون حجمه محدوداً بشكل مستقل عن فضاء حالات النموذج الأصلي، ومعتمداً فقط على الجبر $L$ وبنية $\phi$؟

غالباً ما تركز الطرق الموجودة، مثل الترشيح (filtration) أو تنقية التقسيم (partition refinement)، على الصلاحية البوليانية أو لا تستخدم صراحةً الثنائية ثنائية الطوبولوجيا لتوصيف الحد الأدنى من الاختزال للحفاظ على القيمة الدقيقة.

2. المنهجية

يستخدم المؤلفون تمثيلاً ثنائي الطوبولوجيا علاقتيّ (relational bitopological representation) مستمداً من نظرية الثنائية للجبرات الموجهة ذات القيم الجبرية. تسير المنهجية في مرحلتين رئيسيتين:

أ. التمثيل ثنائي الطوبولوجيا والثنائية
تستخدم الورقة الثنائية بين فئة جبرات $L$-ML (الجبرات الموجهة فوق جبر هيتينغ محدود) وفئة الفضاءات البوليانية المزدوجة العلاقتية ($PRBS_L$).

• الفضاء المزدوج: للفبر $A$، الفضاء المزدوج هو مجموعة التشاكلات $X_A = \text{Hom}_{VAL}(A, L)$ المزودة بطوبولوجيتين ($\tau_1, \tau_2$) وعلاقة ثنائية نموذجية $R_A$.
• العلاقة النموذجية: تُعرف العلاقة $R_A$ بحيث أن $h R_A k$ إذا وفقط إذا كان $h(\Box a) \leq k(a)$ لجميع العناصر $a \in A$. تلتقط هذه العلاقة دلالات المنطق الموجه في الفضاء المزدوج.
• مبرهنة التمثيل: تثبت الورقة أن فئة جبرات $L$-ML متكافئة ثنائياً مع $PRBS_L$، مما يضمن أن العمليات الجبرية تقابل الهياكل الطوبولوجية والعلاقية.

ب. الاختزال المحدود عبر التكافؤ الرصدي
بالنظر إلى نموذج محدود $M$ ومفردات $\Sigma$، يعرّف المؤلفون جبر الملاحظة الموجه $A^\Sigma_M$ الناتج عن التقييمات الذرية $V(p)$ لـ $p \in \Sigma$.

• دالة التقييم: يتم تعريف دالة $\eta^\Sigma_M: W \to X_{A^\Sigma_M}$ بـ $\eta^\Sigma_M(x)(f) = f(x)$.
• التكافؤ الرصدي: حالتان $x, y$ متكافئتان ($x \equiv^\Sigma_M y$) إذا أعطتا نفس قيمة الحقيقة لكل صيغة في الجبر الناتج.
• بناء خارج القسمة: يتم بناء النموذج المختزل كخارج قسمة $W / \equiv^\Sigma_M$. يثبت المؤلفون أن خارج القسمة هذا متماثل مع الصورة المحدودة $X^\Sigma_M = \eta^\Sigma_M[W]$ داخل الثنائي ثنائي الطوبولوجيا. ومن المهم إثبات أن علاقة الانتقال في النموذج المختزل هي قيد للعلاقة المزدوجة النموذجية $R_{A^\Sigma_M}$.

ج. بناء شهادة محدودة الحجم
لمعالجة استخراج المثال المضاد، يستخدم المؤلفون الارتفاع المحدود $h(L)$ لجبر هيتينغ $L$.

• ضغط التقاطع: تثبت لمة (lemma) أن تقاطع أي مجموعة جزئية $S \subseteq L$ يمكن الحفاظ عليه بواسطة مجموعة جزئية $S_0 \subseteq S$ حيث $|S_0| \leq h(L) - 1$.
• بناء الشجرة: بالنسبة لصيغة $\phi$ بعمق موجه $d$ وحالة $x$، يتم بناء نموذج شجري $C(M, x, \phi)$. عند كل عقدة، يتم الاحتفاظ فقط بعدد محدود من التوابع (تحديداً تلك اللازمة للحفاظ على التقاطع لكل صيغة جزئية من نوع $\Box$).
• حدود الحجم: يتم تحديد عامل التفرع بـ $(h(L) - 1) \times m_\Box(\phi)$، حيث $m_\Box(\phi)$ هو عدد الصيغ الجزئية الموجهة المتميزة. الحجم الإجمالي مستقل عن حجم النموذج الأصلي.

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

1. تماثل خارج قسمة الملاحظة والصورة المزدوجة
النتيجة النظرية الأساسية هي أن خارج قسمة الملاحظة لنموذج "فيتينغ" محدود متماثل مع الصورة المحدودة للنموذج في الثنائي ثنائي الطوبولوجيا لجبر الملاحظة الناتج عنه.

• الحفاظ على القيمة الدقيقة: يحافظ الاختزال على القيمة الدقيقة لكل صيغة في $\Sigma$، وليس فقط الصلاحية. لأي $\phi \in \text{Form}(\Sigma)$ وحالة $x$، فإن $J\phi K_{M^{red}}([x]) = J\phi K_M(x)$.
• الحد الأدنى: خارج القسمة هو الأدنى بين جميع الاختزالات المتسامية التي تمر من خلالها جميع الملاحظات المولدة. إذا كانت أي دالة متسامية أخرى $h: W \to Y$ تحافظ على القيم الدقيقة لجميع الصيغ في $\Sigma$، فإن $|W/\equiv^\Sigma_M| \leq |Y|$.

2. شهادات القيم الدقيقة المحدودة
تنشئ الورقة شهادة شجرية محدودة الحجم $C(M, x, \phi)$ لأي صيغة $\phi$ وحالة $x$.

• المحدودية: عمق الشجرة محدود بالعمق الموجه لـ $\phi$، والتفرع محدود بـ $(h(L)-1)m_\Box(\phi)$.
• استخراج المثال المضاد: إذا كان $J\phi K_M(x) \neq 1$، فإن الشهادة (واختزالها الرصدي اللاحق) توفر مثالاً مضاداً نقطياً محدوداً يحافظ على قيمة الفشل الدقيقة. يعتمد حجم هذا المثال المضاد فقط على $L$ وبنية $\phi$، وليس على حجم $M$.

3. إجراء البناء المحدود
توضح الورقة إجراءً فعالاً ومحدوداً لحساب النموذج المختزل عبر توليد جبر الملاحظة بشكل تكراري وتجميع الحالات ذات نواقل التقييم المتطابقة.

4. الأهمية والادعاءات

تدعي الورقة أهميتها في المجالات التالية، مع الحفاظ على نطاق متواضع مقارنة بمشكلات التحقق الأوسع:

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

تختتم الورقة بالإشارة إلى أنه بينما يعتمد حجة ضغط التقاطع على الارتفاع المحدود لـ $L$، فإن توسيع هذه النتائج لتشمل النماذج الكولاجية الضبابية (fuzzy coalgebraic models) ذات الارتفاع اللانهائي يظل مسألة مفتوحة.