The Computability Path Order for Beta-Eta-Normal Higher-Order Rewriting (Full Version)

तकनीकी सारांश: बीटा-एटा-सामान्य उच्च-क्रम पुनर्लेखन (Beta-Eta-Normal Higher-Order Rewriting) के लिए कंप्यूटबिलिटी पाथ ऑर्डर

समस्या विवरण
उच्च-क्रम पुनर्लेखन (Higher-order rewriting) विभिन्न औपचारिकताओं को समाहित करता है, जिनमें विशेष रूप से "साधारण" उच्च-क्रम पुनर्लेखन (जो सिंथैक्टिक मिलान का उपयोग करता है और $\beta$-रिडक्शन को एक पुनर्लेखन नियम के रूप में मानता है) और "सामान्य" उच्च-क्रम पुनर्लेखन (जो $\beta\eta$ के सापेक्ष मिलान का उपयोग करता है और $\beta\eta$-सामान्य रूपों में पदों पर विचार करता है) शामिल हैं। जबकि साधारण उच्च-क्रम पुनर्लेखन के लिए शक्तिशाली समाप्ति विधियाँ (termination methods) जैसे कि कंप्यूटबिलिटी पाथ ऑर्डर (CPO) मौजूद हैं, $\beta\eta$-सामान्य उच्च-क्रम पुनर्लेखन (विशेष रूप से निपकॉव (Nipkow) की शैली में उच्च-क्रम पुनर्लेखन प्रणालियों - HRSs) के अनुकूल बनाना महत्वपूर्ण चुनौतियाँ प्रस्तुत करता है।

HRSs के लिए मौजूदा विधियाँ, जैसे कि NHORPO (Normal Higher-Order Recursive Path Order), अक्सर "न्यूट्रलाइजेशन" (neutralization) नामक एक रूपांतरण तकनीक पर निर्भर करती हैं, जिसका उपयोग वहां किया जाता है जहाँ मूल क्रम विफल हो जाता है। हालाँकि, न्यूट्रलाइजेशन स्वचालन (automation) को जटिल बना देता है। इसके अतिरिक्त, मानक पाथ ऑर्डर सामान्य पुनर्लेखन के साथ संघर्ष करते हैं क्योंकि $\beta\eta$ के अनुकूल सुस्थापित क्रम (well-founded orders) पारंपरिक अर्थों में मॉनोटोनिक (monotone) या स्थिर (stable) नहीं होते हैं। उदाहरण के लिए, यदि कोई क्रम $\beta\eta$ के अनुकूल है और संदर्भों (contexts) के तहत बंद है, तो यह $c > c$ जैसी विरोधाभासी स्थितियाँ उत्पन्न कर सकता है, जो सुस्थापितता (well-foundedness) का उल्लंघन करती है।

कार्यप्रणाली
लेखक कंप्यूटबिलिटी पाथ ऑर्डर (CPO), जिसे मूल रूप से साधारण उच्च-क्रम पुनर्लेखन के लिए परिभाषित किया गया था, को $\beta\eta$-सामान्य उच्च-क्रम पुनर्लेखन के परिवेश में उठाने (lifting) का प्रस्ताव करते हैं। परिणामी क्रम को $\beta\eta$-सामान्य कंप्यूटबिलिटी पाथ ऑर्डर (NCPO) कहा जाता है।

कार्यप्रणाली निम्नलिखित मुख्य घटकों पर आधारित है:

1. रिडक्शन ऑर्डर पेयर (Reduction Order Pair): जुआनोड और रूबियो (Jouannaud and Rubio) के दृष्टिकोण का अनुसरण करते हुए, लेखक एक रिडक्शन ऑर्डर को एक जोड़े $(>, \sqsupset)$ के रूप में परिभाषित करते हैं, जहाँ $>$ प्राथमिक क्रम (NCPO) है और $\sqsupset$ एक "साधारण" संस्करण (CPO) है। यह जोड़ा $\beta\eta$-सामान्य स्थिरता ($\beta\eta$-normal stability) को संतुष्ट करता है: यदि $s > t$, तो सभी प्रतिस्थापन $\sigma$ के लिए $s\sigma\downarrow \sqsupset^+ t\sigma\downarrow$ होता है, जहाँ $\downarrow$ $\beta\eta$-सामान्यकरण (normalization) को दर्शाता है। यह साधारण CPO घटक की सुस्थापितता और मॉनोटोनिसिटी पर समाप्ति के प्रमाण को सक्षम बनाता है।
2. गैर-बहुमुखी पद (Nonversatile Terms): एक महत्वपूर्ण तकनीकी नवाचार गैर-बहुमुखी पदों पर ऑर्डर के अनुप्रयोग का प्रतिबंध है। एक पद गैर-बहुमुखी है यदि प्रतिस्थापन और उसके बाद का $\beta\eta$-सामान्यकरण केवल उसके उचित उप-पदों (proper subterms) को प्रभावित करता है। लेखक पिछले कार्य की तुलना में गैर-बहुविषयीता के लिए एक बेहतर पर्याप्त स्थिति (Lemma 1) प्रदान करते हैं, जो स्थिरता को सिद्ध करने के लिए आवश्यक है।
3. CPO से विस्तार (Extensions from CPO): NCPO, मूल CPO से दो प्रमुख विस्तारों को शामिल करता है:
   • सुलभ उप-पद (Accessible Subterms): ये सुलभ उप-पद विशिष्ट प्रकार स्थितियों (धनात्मक/ऋणात्मक बेस टाइप पोजीशन) द्वारा निर्धारित मामलों में पुनरावर्ती तुलनाओं को बाईपास करने की अनुमति देते हैं।
   • लघु प्रतीक (Small Symbols): यह सुविधा कुछ फलन प्रतीकों को "लघु" (small) मानने की अनुमति देती है, जिससे उन प्रणालियों के लिए समाप्ति प्रमाण संभव होता है जहाँ मानक पुनरावर्ती पाथ ऑर्डर विफल हो जाते हैं (जैसे, लिस्ट प्रोसेसिंग फंक्शन्स)।
4. नियम सेट (Rule Set): ऑर्डर को फलन प्रतीकों (बड़े और छोटे), अनुप्रयोगों (applications), और एब्स्ट्रैक्शन (abstractions) को संभालने वाले नियमों के एक समूह (चित्र 1) के माध्यम से प्रेरणिक रूप से (inductively) परिभाषित किया गया है। विशेष रूप से, $\beta$ और $\eta$ रिडक्शन को ओरिएंट करने के नियम हटा दिए गए हैं, क्योंकि ऑर्डर सीधे सामान्य रूपों पर कार्य करता है। सुलभ उप-पदों के संदर्भ में $\eta$-एक्सपेंशन से जुड़े विशिष्ट मामलों को संभालने के लिए एक नया नियम, $\langle \lambda\triangleright\eta \rangle$, पेश किया गया है।

मुख्य योगदान

• NCPO की परिभाषा: यह शोध पत्र NCPO को औपचारिक रूप से परिभाषित करता है, जो $\beta\eta$-सामान्य उच्च-क्रम पुनर्लेखन के लिए विशेष रूप से डिज़ाइन किया गया पहला कंप्यूटबिलिटी पाथ ऑर्डर है जो सुलभ उप-पदों और लघु प्रतीकों को एकीकृत करता है।
• शुद्धता प्रमाण (Correctness Proof): लेखक सिद्ध करते हैं कि जोड़ा $(>_\tau, \sqsupset_\tau)$ एक वैध $\beta\eta$-सामान्य उच्च-क्रम रिडक्शन ऑर्डर (प्रमेय 2) बनाता है, जिससे इसके अनुकूल किसी भी HRS के लिए समाप्ति सुनिश्चित होती है।
• बेहतर गैर-बहुविषयीता स्थिति: यह शोध पत्र गैर-बहुविषयीता के लिए एक परिष्कृत पर्याप्त स्थिति प्रदान करता है, जो NHORPO के आधारभूत कार्य की तुलना में अधिक सशक्त है।
• SAT/SMT के माध्यम से स्वचालन: लेखक तर्क देते हैं कि NCPO, न्यूट्रलाइजेशन वाले NHORPO की तुलना में स्वचालन के लिए अधिक उपयुक्त है। जबकि न्यूट्रलाइजेशन के लिए प्रतीकात्मक मापदंडों पर निर्भर जटिल सिंथैक्टिक विश्लेषण की आवश्यकता होती है (जो SMT एन्कोडिंग को कठिन बनाता है), NCPO के पैरामीटर (precedence, type orders, status) अधिक सीधे तौर पर एनकोड किए जा सकते हैं।

परिणाम
लेखकों ने Haskell में NCPO का एक प्रोटोटाइप लागू किया है, जिसमें SMT-LIB 2 प्रारूप में समाप्ति समस्याओं को SMT-LIB 2 प्रारूप में एनकोड करने और Z3 सॉल्वर का उपयोग करके उन्हें हल करने के लिए Hasmtlib पैकेज का उपयोग किया गया है। प्रयोगात्मक परिणाम (तालिका 1) NCPO की तुलना NHORPO (न्यूट्रलाइजेशन के साथ और बिना) तथा WANDA और CSI$^{ho}$ में HORPO कार्यान्वयन से करते हैं।

• NHORPO पर श्रेष्ठता: NCPO उन कई प्रणालियों के लिए समाप्ति सिद्ध करने में सफल रहता है जहाँ NHORPO (न्यूट्रलाइजेशन के साथ भी) विफल रहता है। विशेष रूप से:
  • उदाहरण 8 (लिस्ट इंक्रीमेंटिंग): NCPO 'लघु प्रतीकों' का उपयोग करके समाप्ति सिद्ध करता है, जो NHORPO में अनुपस्थित विशेषता है।
  • उदाहरण 7 (नेगेशन नॉर्मल फॉर्म्स): NCPO 'सुलभ उप-पदों' का उपयोग करके समाप्ति सिद्ध करता है, जबकि न्यूट्रलाइजेशन के साथ NHORPO तुलना में बहुमुखी पदों को संभालने में असमर्थ होने के कारण विफल रहता है।
• अतुलनीय शक्ति (Incomparable Power): अध्ययन उन मामलों (जैसे, neutr.p) की पहचान करता है जहाँ न्यूट्रलाइजेशन के साथ NHORPO सफल होता है लेकिन NCPO विफल हो जाता है, जो दर्शाता है कि दोनों दृष्टिकोणों की शक्ति अतुलनीय है।
• दक्षता (Efficiency): NCPO के मापदंडों की खोज को गणनात्मक रूप से कुशल दिखाया गया है, जो अक्सर NHORPO खोजों के समान समय लेती है, जबकि न्यूट्रलाइजेशन मापदंडों की खोज की जटिलता अत्यधिक बढ़ सकती है।

महत्व और दावे
शोध पत्र दावा करता है कि NCPO, NHORPO और न्यूट्रलाइजेशन के संयोजन का एक शक्तिशाली और हल्का विकल्प प्रदान करता है। लेखक इस बात पर जोर देते हैं कि हालांकि न्यूट्रलाइजेशन के साथ NHORPO एक मजबूत प्रतिस्पर्धी है, लेकिन न्यूट्रलाइजेशन तकनीक को स्वचालित करने की जटिलता NCPO को सामान्य उच्च-क्रम पुनर्लेखन में स्वचालित समाप्ति सिद्ध करने के लिए अधिक व्यावहारिक विकल्प बनाती है।

लेखक विनम्रतापूर्वक नोट करते हैं कि NCPO की ट्रांजिटिविटी (transitivity) अभी भी एक खुला प्रश्न है, क्योंकि $\beta$-रिडक्शन का समावेश मूल प्लेन ऑर्डर में CPO और NHORPO के लिए गैर-ट्रांजिटिविटी को न्यायसंगत बनाता है, लेकिन NCPO के विशिष्ट गुणों के लिए आगे की जांच की आवश्यकता है। इसके अतिरिक्त, वे सुझाव देते हैं कि NCPO को सामान्य उच्च-क्रम पुनर्लेखन के लिए डिपेंडेंसी पेयर तकनीकों में एकीकृत करना एक तार्किक अगला कदम है। शोध पत्र पिछले साहित्य में पाई गई त्रुटियों, जैसे कि NHORPO द्वारा कुछ उदाहरणों को हल करने के संबंध में गलत दावों से बचने के लिए उच्च-क्रम समाप्ति विधियों के औपचारिकीकरण की आवश्यकता पर प्रकाश डालते हुए समाप्त होता है।