Decidability Results for Fragments of First-Order Logic via a Symbolic Model Property

तकनीकी सारांश: एक प्रतीकात्मक मॉडल गुण के माध्यम से प्रथम-क्रम तर्क (First-Order Logic) के खंडों के लिए निर्णयता (Decidability) परिणाम

समस्या विवरण

प्रथम-क्रम तर्क (FOL) अनबाउंडेड डोमेन वाले सिस्टम के सत्यापन (verification) की शर्तों को निर्दिष्ट करने के लिए एक शक्तिशाली औपचारिकता है, जैसे कि लिंक्ड लिस्ट या ट्री-आकार की डेटा संरचनाओं से संबंधित मामले। हालाँकि, FOL सामान्यतः अनिर्णयकारी (undecidable) है। जबकि 'फाइनाइट मॉडल प्रॉपर्टी' (जहाँ प्रत्येक संतृप्त सूत्र का एक परिमित मॉडल होता है) निर्णयता को निहित करती है, कई उपयोगी FOL खंड इस गुण को प्राप्त नहीं करते हैं; वे केवल अनंत मॉडल ही स्वीकार कर सकते हैं। फलस्वरूप, FOL पर आधारित सत्यापन उपकरण अमान्य सूत्रों के लिए प्रति-मॉडल (counter-models) खोजने में विफल हो सकते हैं, जिससे उपयोगकर्ताओं को कार्रवाई योग्य फीडबैक नहीं मिल पाता।

मौजूदा निर्णयकारी खंड, जैसे कि स्ट्रैटिफाइड फॉर्मूला (SF) खंड (जो EPR का एक मल्टी-सॉर्ट वेरिएंट है), क्वांटिफायर-अल्टरनेशन ग्राफ पर सख्त अचक्रीयता (acyclicity) बाधाओं को लागू करते हैं ताकि एक फाइनाइट मॉडल प्रॉपर्टी सुनिश्चित की जा सके। ये बाधाएं जटिल प्रणालियों के मॉडलिंग के लिए अक्सर बहुत अधिक प्रतिबंधात्मक होती हैं, जिसके लिए विशिष्टताओं को अनुकूलित करने हेतु महत्वपूर्ण उपयोगकर्ता प्रयास की आवश्यकता होती है। यह शोध पत्र उन FOL खंडों के लिए निर्णयता स्थापित करने की चुनौती को संबोधित करता है जो फाइनाइट मॉडल प्रॉपर्टी का आनंद नहीं लेते हैं, विशेष रूप से वे जो एक विशिष्ट सॉर्ट पर क्वांटिफियर-अल्टरनेशन ग्राफ में स्व-चक्र (self-cycles) की अनुमति देते हैं, बशर्ते कि कुछ क्रम-सिद्धांत संबंधी (order-theoretic) प्रतिबंधों को पूरा किया गया हो।

कार्यप्रणाली

लेखक प्रतीकात्मक संरचनाओं (symbolic structures) का एक सामान्यीकरण प्रस्तावित करते हैं, जिसे मूल रूप से [15] में लीनियर इंटीजर अरिथमेटिक (LIA) का उपयोग करके पेश किया गया था, इसे किसी भी बेस थ्योरी (base theory) के लिए जो एक मानक मॉडल को स्वीकार करती है, विस्तारित किया गया है।

1. सामान्यीकृत प्रतीकात्मक संरचनाएँ

एक प्रतीकात्मक संरचना एक संभावित अनंत प्रथम-क्रम संरचना का एक परिमित प्रतिनिधित्व है। इसमें शामिल हैं:

• नोड्स (Nodes): एक बेस थ्योरी $T$ के डोमेन के उपसमुच्चयों का प्रतिनिधित्व करने वाले नोड्स का एक परिमित सेट।
• बाउंड फॉर्मूला (Bound Formulas): प्रत्येक नोड एक $T$ की भाषा में एक सूत्र से जुड़ा होता है जो उस सेट को परिभाषित करता है जिसका वह प्रतिनिधित्व करता है।
• प्रतीकात्मक व्याख्याएँ (Symbolic Interpretations): स्थिरांकों (constants), फलनों (functions) और संबंधों (relations) की व्याख्याओं को $T$ के टर्म्स और फॉर्मूलों का उपयोग करके प्रतीकात्मक रूप से परिभाषित किया जाता है।

प्रतीकात्मक संरचनाओं का मुख्य गुण यह है कि मॉडल चेकिंग (यह निर्धारित करना कि क्या एक संरचना एक सूत्र को संतुष्ट करती है) बेस थ्योरी $T$ में एक सूत्र की वैधता (validity) में बदल जाती है। यदि $T$ निर्णयकारी है, तो प्रतीकात्मक संरचनाओं के लिए मॉडल चेकिंग निर्णयकारी होती है।

2. प्रतीकात्मक मॉडल गुण (The Symbolic Model Property)

यह शोध पत्र FOL के विशिष्ट खंडों के लिए एक प्रतीकात्मक मॉडल गुण स्थापित करता है। एक खंड इस गुण को तब प्राप्त करता है जब उसके प्रत्येक संतृप्त सूत्र का एक निर्णयकारी बेस थ्योरी पर एक संतुष्ट करने वाली प्रतीकात्मक संरचना होती है। चूंकि ऐसी संरचनाओं के लिए मॉडल चेकिंग निर्णयकारी है, इसलिए इस गुण का अस्तित्व खंड की संतृप्ति (satisfiability) समस्या की निर्णयता को निहित करता है।

3. ऑर्डर्ड सेल्फ-साइकिल (OSC) परिवार

लेखक ऑर्डर्ड सेल्फ-साइकिल (OSC) नामक खंडों का एक परिवार परिभाषित करते हैं, जो एक विशिष्ट सॉर्ट $s_\infty$ पर एक सख्त क्रम संबंध $\prec$ के अभिलेखन (axiomatization) द्वारा पैरामीट्रिक है।

• SF का विश्राम (Relaxation of SF): OSC, स्ट्रैटिफाइड फॉर्मूला खंड की अचक्रीयता आवश्यकता को शिथिल करके इसे विस्तारित करता है। यह $s_\infty$ सॉर्ट पर स्व-लूप (self-loops) पेश करने के लिए फंक्शन सिम्बल्स की अनुमति देता है, बशर्ते कि क्वांटिफायर-अल्टरनेशन ग्राफ में अन्य कोई चक्र न हो।
• बेस थ्योरीज: शोध पत्र दो प्राथमिक बेस थ्योरीज का उपयोग करता है:
  • लीनियर इंटीजर अरिथमेटिक (LIA): टोटल ऑर्डर्स के लिए उपयोग किया जाता है।
  • डिसाइडेबल थ्योरी ऑफ स्ट्रिंग्स (STR): प्रीफिक्स ऑर्डर्स के लिए उपयोग किया जाता है।

4. प्रमाण निर्माण (Proof Construction)

निर्णयता प्रमाण एक जेनेरिक "प्रूफ रेसिपी" का पालन करते हैं जो किसी सूत्र $\phi$ के किसी भी मॉडल $M$ से एक प्रतीकात्मक मॉडल $S$ का निर्माण करता है। निर्माण में शामिल हैं:

1. विभाजन (Partitioning): $M$ के डोमेन को उन एटमिक फॉर्मूलों (atoms) के आधार पर इक्विवेलेंस क्लासेस में विभाजित करना जिन्हें वे संतुष्ट करते हैं। ये क्लासेस प्रतीकात्मक संरचना के नोड्स बन जाते हैं।
2. व्याख्या (Interpretation): स्थिरांकों, यूनरी संबंधों और क्रम $\prec$ की व्याख्याओं को $M$ में संतुष्ट किए गए एटम्स को "अवलोकन" (observe) करने के लिए परिभाषित करना।
3. मिक्स्ड ऑर्डर एटम्स को संभालना: मुख्य कठिनाई मिक्स्ड ऑर्डर एटम्स (जैसे, $f(x) \prec g(x)$) और क्रम के सिद्धांतों $\alpha$ को संतुष्ट करने में निहित है। इसे बेस थ्योरी के भीतर विशिष्ट आंतरिक आकृतियों (summary nodes) और फंक्शन टर्म्स को परिभाषित करके प्राप्त किया जाता है।
   • टोटल ऑर्डर्स (tot) के लिए, समरी नोड्स को द्विदिश अनंत रेखाओं (पूर्णांकों) के रूप में मॉडल किया जाता है, जो टर्म ऑर्डरिंग के "यूनिवर्सल फाइनाइट एंबेडेबिलिटी" की अनुमति देता है।
   • प्रीफिक्स ऑर्डर्स (pref) के लिए, समरी नोड्स को "यूनिवर्सल ट्रीज़" (विशिष्ट ब्रांचिंग फैक्टर्स के साथ द्विदिश अनंत ट्रीज़) के रूप में मॉडल किया जाता है, ताकि प्रीफिक्स ऑर्डर्स की नॉन-लीनियर प्रकृति को समायोजित किया जा सके।

मुख्य योगदान

1. प्रतीकात्मक संरचनाओं की सामान्य परिभाषा: यह शोध पत्र किसी भी बेस थ्योरी (जिसमें स्टैंडर्ड मॉडल हो) पर प्रतीकात्मक संरचनाओं की एक पैरामेट्रिक परिभाषा प्रदान करता है, जो LIA तक सीमित पिछले कार्यों का सामान्यीकरण करता है।
2. OSC परिवार का परिचय: यह ऑर्डर्ड सेल्फ-साइकिल (OSC) परिवार के खंडों को परिभाषित करता है, जो एक विशिष्ट क्रम के सिद्धांतों के तहत स्ट्रैटिफाइड फॉर्मूला को विस्तारित करता है।
3. नए निर्णयता परिणाम: लेखक OSC परिवार के भीतर कई नए खंडों के लिए निर्णयता सिद्ध करते हैं, विशेष रूप से:
   • OSC[pref]: स्ट्रिंग थ्योरी का उपयोग करते हुए प्रीफिक्स-ऑर्डर्ड सेल्फ-साइकिल। यह खंड अचक्रीय ट्री-आकार की डेटा संरचनाओं और शेयरिंग वाले लिंक्ड लिस्ट में रीचेबिलिटी को मॉडल करता है।
   • सक्सेसर/प्रीडेसेसर वाले वेरिएंट: टोटल/प्रीफिक्स ऑर्डर्स को उत्तराधिकारियों (successors - prosucc) या पूर्ववर्तियों (predecessors - regpred) के अस्तित्व की गारंटी देने वाले सिद्धांतों के साथ संयोजित करने वाले खंड।
4. जेनेरिक प्रूफ फ्रेमवर्क: एक एकीकृत प्रमाण तकनीक प्रस्तुत की गई है जो इन खंडों के लिए प्रतीकात्मक मॉडल का निर्माण करती है, यह प्रदर्शित करते हुए कि संतृप्ति (satisfiability) संबंधित निर्णयकारी बेस थ्योरीज (LIA या STR) में फॉर्मूलों की वैधता में बदल जाती है।
5. कार्यान्वयन: ओपन-सोर्स FEST लाइब्रेरी का विस्तार करते हुए एक प्रूफ-ऑफ-कॉन्सेप्ट टूल बनाया गया है जो स्ट्रिंग थ्योरी पर मॉडल चेकिंग सहित जेनेरिक प्रतीकात्मक संरचनाओं का समर्थन करता है।

परिणाम

शोध पत्र यह स्थापित करता है कि निम्नलिखित खंडों के लिए संतृप्ति समस्या निर्णयकारी है (जहाँ $\alpha$ क्रम का सिद्धांत है):

• $\alpha \in \{ \text{tot}, \text{tot} \land \text{prosucc}, \text{tot} \land \text{regpred}, \text{pref}, \text{pref} \land \text{prosucc}, \text{pref} \land \text{regpred} \}$.

tot के लिए परिणाम पूर्व कार्य [15] को दोहराता है, जबकि pref और इसके वेरिएंट के परिणाम नए हैं। OSC[pref] की निर्णयता विशेष रूप से महत्वपूर्ण है क्योंकि यह उन संरचनाओं को संभालता है जो फाइनाइट मॉडल प्रॉपर्टी का आनंद नहीं लेती हैं लेकिन जिन्हें स्ट्रिंग थ्योरी का उपयोग करके प्रतीकात्मक रूप से दर्शाया जा सकता है।

महत्व और दावे

यह शोध पत्र दावा करता है कि यह कार्य निर्णयता के प्रति एक नया दृष्टिकोण प्रदान करता है जो फाइनाइट मॉडल प्रॉपर्टी से आगे जाता है। प्रतीकात्मक संरचनाओं का उपयोग करके, यह उन सिस्टम के सत्यापन को सक्षम बनाता है जो फाइनाइट काउंटर-मॉडेल्स की कमी के कारण पहले कठिन थे।

• सैद्धांतिक प्रभाव: यह फाइनाइट मॉडल प्रॉपर्टी और अनंत मॉडल प्रतिनिधित्व के बीच के अंतर को पाटता है, यह दिखाते हुए कि निर्णयता प्राप्त की जा सकती है भले ही अनंत मॉडल आवश्यक हों, बशर्ते उन्हें एक निर्णयकारी बेस थ्योरी द्वारा कैप्चर किया जा सके।
• व्यावहारिक प्रासंगिकता: OSC[pref] खंड सीधे ट्री-आकार की डेटा संरचनाओं और शेयरिंग वाले लिंक्ड लिस्ट से जुड़े सामान्य सत्यापन परिदृश्यों को संबोधित करता है, जिन्हें सख्ती से स्ट्रैटिफाइड खंडों में मॉडल करना कठिन है।
• सामान्यता: फ्रेमवर्क को अन्य बेस थ्योरीज और क्रम संबंधों के लिए विस्तार योग्य बनाने के लिए डिज़ाइन किया गया है, जो और अधिक निर्णयकारी खंडों की खोज के लिए एक मार्ग सुझाता है।

लेखक उल्लेख करते हैं कि हालांकि निर्णय प्रक्रिया संतृप्ति को बेस थ्योरी में फॉर्मूलों की वैधता में बदल देती है (जो स्ट्रिंग थ्योरीज के लिए नॉन-एलिमेंट्री हो सकती है), प्राथमिक योगदान निर्णयता की स्थापना और सत्यापन विफल होने पर प्रतीकात्मक प्रति-मॉडल (symbolic counter-models) उत्पन्न करने की क्षमता है। कार्यान्वयन इस दृष्टिकोण की व्यवहार्यता के लिए एक प्रूफ-ऑफ-कॉन्सेप्ट के रूप में कार्य करता है।