Encoding Peano Arithmetic in a Minimal Fragment of Separation Logic

यहाँ सोहेई इतो और माकोटो तात्सुता के शोध पत्र "Encoding Peano Arithmetic in a Minimal Fragment of Separation Logic" का विस्तृत तकनीकी सारांश दिया गया है।

1. समस्या विवरण (Problem Statement)

यह शोध पत्र सेपरेशन लॉजिक (Separation Logic - SL) में अंकगणित (arithmetic) के विस्तार के साथ निर्णयक्षमता (decidability) के मौलिक प्रश्न को संबोधित करता है। यद्यपि सेपरेशन लॉजिक का व्यापक रूप से हीप-हेरफेर करने वाले (heap-manipulating) प्रोग्रामों के सत्यापन के लिए उपयोग किया जाता है, लेकिन अंकगणितीय सिद्धांतों (जैसे प्रेज़रर अंकगणित) के साथ इसका संयोजन अक्सर यह मान लेता है कि यदि अंकगणितीय खंड (arithmetic fragment) निर्णय योग्य है, तो पूरा तर्क भी निर्णय योग्य रहेगा।

लेखक नंबरों के साथ सेपरेशन लॉजिक (SLN) के एक न्यूनतम खंड की जांच करते हैं, जिसे इस प्रकार परिभाषित किया गया है:

• स्थानिक घटक (Spatial Component): केवल सहज बोध वाला 'पॉइंट्स-टू' प्रेडिकेट ($t_1 \to t_2$), जो एक एकल मेमोरी सेल का प्रतिनिधित्व करता है।
• अंकगणितीय घटक (Arithmetic Component): केवल स्थिरांक $0$ और सक्सेसर (successor) फलन $s$।
• अपवर्जन (Exclusions): यह स्पष्ट रूप से सेपरेटिंग कॉंजंक्शन ($*$), मैजिक वैंड ($-\ast$), और मल्टी-फील्ड पॉइंट्स-टू प्रेडिकेट्स को बाहर करता है।

मुख्य समस्या इस अत्यंत कमजोर खंड की अभिव्यंजक शक्ति (expressive power) को निर्धारित करना है। विशेष रूप से, लेखक पूछते हैं: क्या यह न्यूनतम खंड पीआनो अंकगणित (Peano Arithmetic - PA) के अनिर्णनीय $\Pi^0_1$ सूत्रों को एनकोड कर सकता है?

2. कार्यप्रणाली (Methodology)

लेखक अनिर्णयता (undecidability) सिद्ध करने और जटिलता सीमाओं (complexity bounds) को स्थापित करने के लिए एक अनुवाद-आधारित दृष्टिकोण (translation-based approach) का उपयोग करते हैं। कार्यप्रणाली में तीन मुख्य तकनीकी स्तंभ शामिल हैं:

A. हीप-आधारित ऑपरेशन टेबल (Heap-Based Operation Tables)

मुख्य नवाचार अंकगणितीय ऑपरेशनों (योग, गुणन, और असमानता) को सीधे मेमोरी हीप की संरचना में एनकोड करना है। अंतर्निर्मित अंकगणितीय ऑपरेटरों के बजाय, यह तर्क लिंक्ड मेमोरी सेल्स के रूप में संग्रहीत ऑपरेशन टेबल्स का उपयोग करके उन्हें सिम्युलेट करता है।

• एनकोडिंग योजना (Encoding Scheme): हीप में प्रविष्टियाँ क्रमिक सेल के रूप में संग्रहीत होती हैं।
  • योग (Addition): इसे 0 के साथ टैग किया गया है। $x + y = z$ के लिए एक प्रविष्टि एड्रेस $a$ से शुरू होने वाले सेल के अनुक्रम के रूप में संग्रहीत की जाती है: $(0, x+3, y+3, z+3)$। ऑफसेट $+3$ टैग्स के साथ टकराव से बचने के लिए है।
  • गुणन (Multiplication): इसे 1 के साथ टैग किया गया है। प्रविष्टि: $(1, x+3, y+3, z+3)$।
  • असमानता (Inequality): इसे 2 के साथ टैग किया गया है। प्रविष्टि: $(2, x+3, y+3)$।
• निरंतरता बाधाएं (Consistency Constraints): एक विशिष्ट सूत्र $H$ ("टेबल हीप कंडीशन") बनाया जाता है ताकि यह सुनिश्चित किया जा सके कि यदि हीप में किसी ऑपरेशन के लिए प्रविष्टि है, तो बाद के सेल में इंडक्टिव परिभाषाओं (जैसे $s(x) + y = s(x+y)$) के आधार पर सही परिणाम होना चाहिए।

B. $\Pi^0_1$ सूत्रों का अनुवाद (Translation of $\Pi^0_1$ Formulas)

लेखक PA के बाउंडेड फॉर्मूला से SLN में एक अनुवाद $(\cdot)^\circ$ को परिभाषित करते हैं।

• सामान्य रूप (Normal Form): वे पहले PA सूत्रों को एक "सामान्य रूप" में परिवर्तित करते हैं जहाँ अंकगणितीय ऑपरेशन ($+, \times$) केवल $\exists(x = t + u)$ के रूप में अस्तित्ववादी क्वांटिफायर (existential quantifiers) के भीतर दिखाई देते हैं।
• अनुवाद तर्क (Translation Logic):
  • अंकगणितीय पदों को ऑपरेशन टेबल्स के संदर्भों द्वारा प्रतिस्थापित किया जाता है (उदाहरण के लिए, $x + y = z$ बन जाता है $\forall a ((a \to 0, [x], [y]) \to s^3(a) \to [z])$)।
  • सीमित हीप का प्रबंधन (Handling Finite Heaps): एक महत्वपूर्ण चुनौती यह है कि हीप परिमित (finite) होता है और इसमें बड़ी संख्याओं के लिए प्रविष्टियाँ नहीं हो सकती हैं। अनुवाद इसे निहितार्थ (implications) का उपयोग करके संभालता है: यदि हीप आवश्यक टेबल प्रविष्टि को रखने के लिए "बहुत छोटा" है, तो निहितार्थ रिक्त रूप से सत्य (vacuously true) होगा। यह सुनिश्चित करता है कि SLN में वैधता (जो सभी हीप्स के लिए सत्य होनी चाहिए) PA (मानक मॉडल) में वैधता के अनुरूप हो।
  • विशेष रूप से, बाउंडेड क्वांटिफायर $\exists x \le t$ के लिए, अनुवाद एक वियोजन (disjunction) शामिल करता है: या तो हीप सीमा की जाँच करने के लिए बहुत छोटा है (जिससे सूत्र सत्य हो जाता है), या हीप में सीमा को सत्यापित करने के लिए आवश्यक टेबल प्रविष्टियाँ मौजूद हैं।

C. जटिलता विश्लेषण (Complexity Analysis)

सटीक जटिलता वर्ग स्थापित करने के लिए, लेखक दो दिशाएँ सिद्ध करते हैं:

1. निचली सीमा ($\Pi^0_1$-hard): यह दिखाकर कि अनुवाद $\Pi^0_1$ सूत्रों के लिए वैधता को सुरक्षित रखता है।
2. ऊपरी सीमा ($\Pi^0_1$): SLN के लिए मॉडल-चेकिंग समस्या को निर्णय योग्य सिद्ध करके। वे दिखाते हैं कि पॉइंट्स-टू प्रेडिकेट में चर (variables) हीप के आकार द्वारा सीमित होते हैं, जिससे समस्या प्रेज़रर अंकगणित (जो सक्सेसर अंकगणित का एक उप-खंड है) के एक निर्णय योग्य खंड की जाँच करने में बदल जाती है।

3. मुख्य योगदान (Key Contributions)

1. न्यूनतम SLN की अनिर्णयता (Undecidability of Minimal SLN): यह शोध पत्र सिद्ध करता है कि SLN में वैधता अनिर्णणीय (undecidable) है। यह आश्चर्यजनक है क्योंकि इस खंड में केवल सबसे सरल स्थानिक प्रेडिकेट और सबसे कमजोर अंकगणित (केवल सक्सेसर) है, फिर भी यह $\Pi^0_1$ वाक्यों के लिए पूर्ण पीआनो अंकगणित (PA) को सिम्युलेट करने के लिए पर्याप्त शक्तिशाली है।
2. प्रतिनिधित्व प्रमेय (Representation Theorem): एक कठोर अनुवाद प्रदान किया गया है जो दिखाता है कि एक $\Pi^0_1$ सूत्र $A$, PA में मान्य है यदि और केवल यदि उसका अनुवाद $A^\circ$, SLN में मान्य है।
3. $\Pi^0_1$-पूर्णता ($\Pi^0_1$-Completeness): लेखक स्थापित करते हैं कि SLN के लिए वैधता समस्या $\Pi^0_1$-पूर्ण है। यह एक महत्वपूर्ण परिणाम है क्योंकि यह तर्क को सटीक रूप से अरिथमेटिक पदानुक्रम (arithmetical hierarchy) के भीतर स्थित करता है।
4. $\Sigma^0_1$ पर सीमा (Limitation on $\Sigma^0_1$): शोध पत्र प्रदर्शित करता है कि अनुवाद $\Sigma^0_1$ सूत्रों के लिए वैधता को सुरक्षित नहीं करता है। एक प्रति-उदाहरण ($\exists x (x + 0 \neq x)$) दिया गया है, जो दिखाता है कि जबकि यह PA में असत्य है, इसका अनुवाद SLN में मान्य है क्योंकि "छोटे" हीप आवश्यक टेबल प्रविष्टियों के अभाव के कारण आसानी से शर्त को संतुष्ट कर सकते हैं।
5. वैकल्पिक प्रमाण (Alternative Proof): एक वैकल्पिक अनिर्णयता प्रमाण भी प्रस्तुत किया गया है जो फाइनाइट मॉडल थ्योरी (ट्रैखटेनब्रॉट प्रमेय) के वैधता समस्या से रिडक्शन (reduction) के माध्यम से हीप में फाइनाइट स्ट्रक्चर को एनकोड करता है।

4. परिणाम (Results)

• मुख्य प्रमेय (Main Theorem): पीआनो अंकगणित में $\Pi^0_1$ सूत्रों की वैधता उनके SLN खंड में उनके अनुवादों की वैधता के समकक्ष है।
• उपप्रमेय (Corollary): SLN के लिए वैधता समस्या अनिर्णणीय है।
• जटिलता (Complexity): वैधता समस्या $\Pi^0_1$-पूर्ण है।
  • कठिनाई (Hardness): PA के एनकोडिंग से प्राप्त हुई।
  • सदस्यता (Membership): मॉडल-चेकिंग समस्या की निर्णयक्षमता से प्राप्त हुई (स्थानिक परमाणुओं में चर हीप आकार द्वारा सीमित हैं; शेष तर्क निर्णय योग्य सक्सेसर अंकगणित है)।

5. महत्व (Significance)

• सैद्धांतिक सीमाएँ (Theoretical Boundaries): ये परिणाम सेपरेशन लॉजिक के निर्णय योग्य और अनिर्णable खंडों के बीच की सीमा को पुनर्परिभाषित करते हैं। यह दिखाता है कि यहाँ तक कि सबसे बुनियादी अंकगणित (0 और सक्सेसर) जोड़ना भी, यदि तर्क हीप्स पर क्वांटिफिकेशन की अनुमति देता है, तो निर्णयक्षमता को तोड़ने के लिए पर्याप्त है।
• सत्यापन निहितार्थ (Verification Implications): प्रोग्राम सत्यापन के लिए, इसका अर्थ है कि नंबरों के साथ सेपरेशन लॉजिक के लिए स्वचालित तर्क उपकरण (automated reasoning tools) सावधान रहने चाहिए। भले ही स्थानिक भाग को सिंगल-सेल पॉइंटर्स तक सीमित किया गया हो, अंकगणित के साथ इसका संयोजन अनिर्णयता की ओर ले जा सकता है, जिससे व्यावहारिक उपकरणों के लिए ह्यूरिस्टिक्स या प्रतिबंधित खंडों (जैसे विशिष्ट इंडक्टिव परिभाषाओं के साथ सिम्बोलिक हीप्स) का उपयोग आवश्यक हो जाता है।
• अभिव्यंजक शक्ति (Expressive Power): यह शोध पत्र इस विचार को चुनौती देता है कि उच्च अभिव्यक्त क्षमता के लिए SL में सेपरेटिंग कॉंजंक्शन ($*$) आवश्यक है। यह दर्शाता है कि पॉइंट्स-टू प्रेडिकेट की "सहज बोध" प्रकृति (जो आंशिक हीप्स की अनुमति देती है) अंकगणितीय बाधाओं के साथ मिलकर जटिल अंकगणितीय तर्क को एनकोड करने के लिए पर्याप्त है।

संक्षेप में, इतो और तात्सुता यह प्रदर्शित करते हैं कि सेपरेशन लॉजिक में सिंटैक्टिक सरलता (syntactic simplicity) निर्णयक्षमता की गारंटी नहीं देती है। केवल एक स्थानिक परमाणु और बुनियादी अंकगणित वाला खंड, तार्किक प्रणालियों के निरंतरता और समाप्ति गुणों को एनकोड करने के लिए पर्याप्त है, जो वैधता समस्या को $\Pi^0_1$-पूर्णता के स्तर पर रखता है।