Towards Weak Stratification for Logics of Definitions

तकनीकी सारांश: परिभाषाओं के तर्क (Logics of Definitions) के लिए कमजोर स्तरीकरण (Weak Stratification) की ओर

समस्या विवरण
परिभाषाओं का तर्क (logic of definitions) तर्कों (logics) का एक परिवार है जिसका उपयोग उन निर्णयों को एनकोड और तर्क देने के लिए किया जाता है जो अनुमान नियमों (inference rules) द्वारा निर्दिष्ट होते हैं, जहाँ परमाणु विधेय (atomic predicates) उन तार्किक सूत्रों से जुड़े होते हैं जो स्वयं विधेय पर निर्भर हो सकते हैं। इस प्रकार की परिभाषाओं में निहित स्पष्ट चक्राकारता (circularity) को हल करने के लिए, मानक दृष्टिकोण एक स्तरीकरण स्थिति (stratification condition) लागू करते हैं, जो यह सुनिश्चित करती है कि एक विधेय अपनी ही परिभाषा के शरीर में नकारात्मक रूप से (इम्प्लिकेशन के बाईं ओर) प्रकट न हो। यह स्थिति परिभाषाओं को एक मोनोटोनिक फिक्स्ड-पॉइंट ऑपरेटर के रूप में मानती है।

हालाँकि, कई उपयोगी विनिर्देश, विशेष रूप से प्रोग्रामिंग भाषाओं के गुणों को सिद्ध करने के लिए लॉजिकल रिलेशंस (logical relations) में शामिल, ऐसे विनिर्देशों की आवश्यकता होती है जहाँ विधेय नकारात्मक रूप से प्रकट होता है। तर्क $\mathcal{G}$ में, जो Abella प्रूफ असिस्टेंट का आधार है, ऐसी परिभाषाओं की अनुमति नहीं है। जबकि Tiu [19] ने पहले $\mathcal{LD}$ नामक एक तर्क पेश किया था जिसने स्तरीकरण की स्थिति को कमजोर स्तरीकरण (weak stratification) तक शिथिल कर दिया (नकारात्मक उपस्थिति की अनुमति देता है यदि हेड का स्तर नकारात्मक उपस्थिति के स्तर से अधिक हो), $\mathcal{LD}$ एक कोर फ्रैगमेंट तक सीमित था। इसमें नाबला क्वांटिफायर ($\nabla$) का समर्थन नहीं था, जो नाम (names) और ताज़गी (freshness) के संबंध में तर्क देने के लिए आवश्यक है, और सामान्य इंडक्टिव डेफिनिशन्स (inductive definitions) का भी अभाव था। इस कार्य द्वारा संबोधित चुनौती $\mathcal{LD}\mu\nabla$ के साथ मिलकर कमजोर स्तरीकरण को शामिल करना है, जबकि $\nabla$ और सामान्य इंडक्टिव डेफिनिशन्स की उपस्थिति में निरंतरता (consistency) बनाए रखना है।

कार्यप्रणाली (Methodology)
यह शोध पत्र एक नया तर्क, $\mathcal{LD}\mu\nabla$ परिभाषित करता है, जो $\nabla$ क्वांटिफिकेशन और सामान्य इंडक्टिव डेफिनिशन्स के साथ Tiu के $\mathcal{LD}$ का विस्तार करता है। कार्यप्रणाली तीन मुख्य चरणों में आगे बढ़ती है:

1. $\mathcal{LD}\mu\nabla$ का सिंटैक्स और सिमेंटिक्स:
   इस तर्क को डेफिनिशन के एक सेट $\mathcal{D}$ और इंडक्टिव डेफिनिशन्स के एक सेट $\mathcal{I}$ के साथ फर्स्ट-ऑर्डर सीक्वेंट कैलकुलस के विस्तार के रूप में तैयार किया गया है।

   • कमजोर स्तरीकरण (Weak Stratification): एक डेफिनिशन सेट $\mathcal{D}$ तब कमजोर रूप से स्तरीकृत होता है यदि प्रत्येक क्लॉज $H \triangleq_X B$ और ग्राउंडिंग सब्स्टीट्यूशन $\rho$ के लिए, $\text{lvl}(H\rho) \ge \text{lvl}(B\rho)$ हो। महत्वपूर्ण रूप से, यह नकारात्मक उपस्थितियों की अनुमति देता है यदि हेड का स्तर नकारात्मक उपस्थिति के स्तर से अधिक हो।
   • इंडक्शन के लिए सख्त स्तरीकरण (Strict Stratification for Induction): यह शोध पत्र इंडक्टिव डेफिनिशन्स $\mathcal{I}$ पर एक सख्त स्थिति लागू करता है: उन्हें सख्त रूप से स्तरीकृत होना चाहिए (एक ग्राउंड एटॉमिक प्रेडिकेट का स्तर उसके तर्कों से स्वतंत्र होना चाहिए)। इंडक्शन को कमजोर स्तरीकरण के साथ मिलाने से होने वाली विसंगति को रोकने के लिए यह प्रतिबंध आवश्यक है।
   • नाबला क्वांटिफायर ($\nabla$): तर्क नामों के जेनेरिक और विशिष्ट उदाहरणों के बीच अंतर करने के लिए, नॉमिनल कांस्टेंट और ताज़गी को संभालने के लिए $\nabla$ क्वांटिफायर को शामिल करता है।

2. ग्राउंड लॉजिक और व्याख्या (Ground Logic and Interpretation):
   निरंतरता सिद्ध करने के लिए, लेखक तर्क का एक ग्राउंड संस्करण, $\mathcal{LD}\mu\nabla_\infty$ निर्मित करते हैं, जहाँ सभी सूत्र ग्राउंड हैं (कोई आइगनवेरिएबल नहीं)।

   • ग्राउंडिंग लेम्मा (Grounding Lemma): एक प्रमुख तकनीकी चरण यह सिद्ध करना है कि $\mathcal{LD}\mu\nabla$ में किसी भी डेरिवेशन की व्याख्या एक ग्राउंडिंग सब्स्टीट्यूशन के माध्यम से $\mathcal{LD}\mu\nabla_\infty$ में एक डेरिवेशन के रूप में की जा सकती है। यह पूर्ण तर्क की निरंतरता समस्या को ग्राउंड लॉजिक की निरंतरता में बदल देता है।
   • अनंत नियम (Infinitary Rules): $\mathcal{LD}\mu\nabla_\infty$ में, मानक $\forall R$ और $\exists L$ नियमों को इन्फिनिटरी नियमों द्वारा प्रतिस्थापित किया जाता है जो सभी ग्राउंड टर्म्स पर क्वांटिफाई करते हैं, और इंडक्शन के लिए $\mu L$ नियम को भी सभी ग्राउंड इंस्टेंस को कवर करने के लिए विस्तारित किया जाता है।

3. कट एलिमिनेशन (Cut Elimination):
   निरंतरता प्रमाण का मुख्य हिस्सा $\mathcal{LD}\mu\nabla_\infty$ में कट नियम (विशेष रूप से मल्टीकट नियम) का उन्मूलन है।

   • रिडक्शन रिलेशन (Reduction Relation): एक रिडक्शन रिलेशन को डेरिवेशंस पर परिभाषित किया गया है, जो यह निर्दिष्ट करता है कि कट्स को कैसे ऊपर की ओर धकेला जा सकता है या हटाया जा सकता है।
   • रिड्यूसिबिलिटी (Reducibility): टैट-मार्टिन-लोफ तकनीक (Tait-Martin-Löf technique) का अनुसरण करते हुए, जिसे मैकडॉवेल और मिलर द्वारा अनुकूलित किया गया है, लेखक डेरिवेशंस के लिए रिड्यूसिबिलिटी (और नॉर्मलाइज़ेबिलिटी) की अवधारणा को परिभाषित करते हैं। वे सिद्ध करते हैं कि $\mathcal{LD}\mu\nabla_\infty$ में प्रत्येक डेरिवेशन रिड्यूसिबल है।
   • इंडक्टिव केस हैंडलिंग: प्रमाण का एक महत्वपूर्ण पहलू कमजोर स्तरीकरण और इंडक्शन के बीच की अंतःक्रिया को संभालना है। लेखक दिखाते हैं कि जबकि कमजोर स्तरीकरण सामान्य डेफिनिशन्स के लिए पर्याप्त है, इंडक्टिव डेफिनिशन्स को निरंतरता बनाए रखने के लिए सख्त रूप से स्तरीकृत रहना चाहिए। वे एक काउंटरएग्जांपल (सेक्शन 3.3) प्रदान करते हैं जो यह दर्शाता है कि इंडक्टिव डेफिनिशन्स के लिए कमजोर स्तरीकरण की अनुमति देने से तार्किक विसंगति उत्पन्न होती है।

मुख्य योगदान

• $\mathcal{LD}\mu\nabla$ की परिभाषा: यह शोध पत्र एक ऐसे तर्क को औपचारिक रूप से परिभाषित करता है जो कमजोर स्तरीकरण, नाबला क्वांटिफिकेशन और सामान्य इंडक्टिव डेफिनिशन्स को जोड़ता है।
• निरंतरता प्रमाण: प्राथमिक योगदान यह है कि $\mathcal{LD}\mu\nabla$ निरंतर है। यह $\mathcal{LD}\mu\nabla_\infty$ के लिए कट एलिमिनेशन सिद्ध करके और एक ग्राउंडिंग व्याख्या स्थापित करके प्राप्त किया गया है।
• स्तरीकरण बाधाएं (Stratification Constraints): यह कार्य अनुमत और अनुपयुक्त डेफिनिशन्स के बीच की सीमा को स्पष्ट करता है। यह प्रदर्शित करता है कि जबकि कमजोर स्तरीकरण सामान्य डेफिनिशन्स के लिए पर्याप्त है (लॉजिकल रिलेशंस को सक्षम बनाता है), इंडक्टिव डेफिनिशन्स को निरंतरता बनाए रखने के लिए सख्त स्तरीकरण की आवश्यकता होती है।
• काउंटरएग्जांपल: यह शोध पत्र एक विशिष्ट काउंटरएग् एग्जांपल प्रदान करता है जो दिखाता है कि इंडक्टिव डेफिनिशन्स के लिए स्तरीकरण की स्थिति को शिथिल करने से तार्किक विसंगति उत्पन्न होती है, जो $\mathcal{I}$ पर लगाए गए प्रतिबंध को न्यायसंगत ठहराता है।

परिणाम

• निरंतरता (Consistency): $\mathcal{LD}\mu\nabla$ को निरंतर सिद्ध किया गया है। फलस्वरूप, $\mathcal{LD}\mu\nabla_\infty$ सभी सिद्ध किए जा सकने वाले सीक्वेंट्स के लिए कट-फ्री डेरिवेशंस स्वीकार करता है।
• इनवर्जन गुण (Inversion Properties): यह शोध पत्र $\mathcal{LD}\mu\nabla_\infty$ के लिए मेटा-थ्योरिटिक गुणों को स्थापित करता है, जिसमें विभिन्न इंट्रोडक्शन नियमों (जैसे $\wedge R$, $\vee L$, $\nabla R$) की इनवर्टीबिलिटी और खाली संदर्भ (empty context) होने पर $\vee R$, $\exists R$, और डेफिनिशन नियमों ($\Delta R$) के लिए विशिष्ट आंशिक इनवर्टीबिलिटी शामिल है। ये गुण प्रूफ सर्च प्रक्रियाओं के लिए महत्वपूर्ण हैं।
• सीमाएँ: कट एलिमिनेशन प्रमेय केवल ग्राउंड लॉजिक $\mathcal{LD}\mu\nabla_\infty$ के लिए स्थापित किया गया है। शोध पत्र नोट करता है कि इस परिणाम को पूर्ण तर्क $\mathcal{LD}\mu\nabla$ (आइगनवेरिएबल्स के साथ) तक विस्तारित करना एक खुला प्रश्न बना हुआ है।

महत्व
इस कार्य का महत्व Abella प्रूफ असिस्टेंट की क्षमताओं को विस्तारित करने की इसकी क्षमता में निहित है। Abella $\mathcal{G}$ तर्क पर आधारित है, जो वर्तमान में डेफिनिशन्स को सख्त रूप से स्तरीकृत रहने के लिए प्रतिबंधित करता है। कमजोर रूप से स्तरीकृत डेफिनिशन्स को शामिल करने को न्यायसंगत बनाकर, यह शोध Abella को लॉजिकल रिलेशंस को नेटिवली सपोर्ट करने का मार्ग प्रशस्त करता है, जो प्रोग्रामिंग भाषाओं (जैसे टाइप सेफ्टी और कंपाइलर शुद्धता) के गुणों को सिद्ध करने के लिए एक मौलिक तकनीक है।

यह शोध पत्र $\mathcal{G}$ के एक व्यापक विस्तार की दिशा में एक आधारभूत कदम के रूप में इस कार्य को प्रस्तुत करता है। जबकि वर्तमान परिणाम $\nabla$ और इंडक्शन के साथ कमजोर स्तरीकरण को संभालता है, लेखक नोट करते हैं कि $\mathcal{G}$ के पूर्ण औचित्य के लिए को-इंडक्शन (co-induction) और नॉमिनल एब्स्ट्रैक्शन (nominal abstraction) को शामिल करने वाले और विस्तार की आवश्यकता होगी। यह कार्य यह भी रेखांकित करता है कि इंडक्टिव डेफिनिशन्स के लिए सख्त स्तरीकरण को बनाए रखना आवश्यक है, एक ऐसा प्रतिबंध जो उन विसंगतियों को रोकता है जो कमजोर स्तरीकरण को इंडक्शन के साथ मिलाने से उत्पन्न हो सकती थीं।