Mechanized Undecidability of Higher-order beta-Matching (Extended Version)

तकनीकी सारांश: उच्च-क्रम बीटा-मैचिंग की यांत्रिक अनिश्चितता (Mechanized Undecidability of Higher-Order Beta-Matching)

समस्या विवरण (Problem Statement)
यह शोध पत्र सरल रूप से टाइप किए गए $\lambda$-कैलकुलस (simply typed $\lambda$-calculus) के भीतर उच्च-क्रम $\beta$-मैचिंग (higher-order $\beta$-matching) की निर्णय समस्या (decision problem) को संबोधित करता है। दिए गए दो सरल रूप से टाइप किए गए $\lambda$-पदों (terms), $F$ और $N$ के लिए, जहाँ $N$ में कोई मुक्त चर (free variables) नहीं हैं, समस्या यह पूछती है कि क्या ऐसा एक पद $M$ मौजूद है कि अनुप्रयोग (application) $F M$, $N$ के $\beta$-तुल्य ( $\beta$-equivalent) हो। जबकि ह्युएट (Huet) द्वारा 1970 के दशक में उच्च-क्रम $\beta$-यूनिफिकेशन (higher-order $\beta$-unification) की अनिश्चितता स्थापित की गई थी, $\beta$-मैचिंग की निर्णय क्षमता (decidability) लोडर (Loader) द्वारा 2003 में तब तक खुली रही जब तक उन्होंने इसे सिद्ध नहीं किया। लोडर का प्रमाण $\lambda$-परिभाषनीयता ( $\lambda$-definability) के एक संस्करण से रिडक्शन (reduction) पर आधारित था, जिसमें मनमाने परिमित फलनों (arbitrary finite functions) को निर्दिष्ट करने वाले बाधाओं (constraints) को तैयार करने के लिए जटिल तंत्र का उपयोग किया गया था।

कार्यप्रणाली (Methodology)
लेखक एक नवीन अनिश्चितता प्रमाण प्रस्तुत करते हैं जो $\lambda$-परिभाषनीयता के दृष्टिकोण से भिन्न है और $\lambda$-परिभाषनीयता को पूरी तरह से टाल देता है। इसके बजाय, प्रमाण एक प्रतिबंधित स्ट्रिंग रीराइटिंग (string rewriting) के रूप, विशेष रूप से सरल सेमी-थ्यू सिस्टम (semi-Thue systems) के भीतर समस्या $0^+ \Rightarrow^* 1^+$ को सीधे उच्च-क्रम $\beta$-मैचिंग में एनकोड करता है।

कार्यप्रणाली निम्नलिखित चरणों के माध्यम से आगे बढ़ती है:

1. प्रारंभिक बिंदु (Starting Point): रिडक्शन की शुरुआत अनिश्चित समस्या $0^+ \Rightarrow^* 1^+$ से होती है, जो यह पूछती है कि क्या $0$के एक गैर-रिक्त अनुक्रम को$ab \Rightarrow cd$ के रूप में पुनर्गठन नियमों (rewrite rules) के एक सेट का उपयोग करके $1$ के एक गैर-रिक्त अनुक्रम में परिवर्तित किया जा सकता है। यह समस्या पहले से ही अनिश्चित ज्ञात है और 'कोक अनडिसाइडेबिलिटी प्रूफ लाइब्रेरी' (Coq Library of Undecidability Proofs) में मशीनीकृत (mechanized) है।
2. एन्कोडिंग रणनीति (Encoding Strategy): लेखक पुनर्गठन प्रक्रिया का अनुकरण करने के लिए सरल रूप से टाइप किए गए $\lambda$-पदों का निर्माण करते हैं। एन्कोडिंग दो मुख्य पहलुओं को कैप्चर करती है:
   • शब्द विस्तार और इनिशियलाइजेशन (Word Expansion and Initialization): पदों का निर्माण लंबाई $n$ के एक प्रारंभिक शब्द के विस्तार और उसके $0$s के साथ इनिशियलाइजेशन को दर्शाने के लिए किया जाता है।
   • पुनर्गठन चरण (Rewriting Steps): पद शब्द के भीतर विशिष्ट स्थितियों पर पुनर्गठन नियमों के अनुप्रयोग का प्रतिनिधित्व करते हैं।
3. सिंटैक्टिक और सिमेंटिक बाधाएं (Syntylactic and Semantic Constraints): यह सुनिश्चित करने के लिए कि $\lambda$-पद समाधान पुनर्गठन प्रक्रिया का निष्ठापूर्वक प्रतिनिधित्व करता है और "एड हॉक" (ad hoc) समाधानों (जैसे, तर्क को अनदेखा करने वाले या मनमाने ढंग से परिणाम बनाने वाले पद) को रोकता है, लेखक विशिष्ट टाइपिंग बाधाओं और $\beta$-तुल्यता जाँचों का उपयोग करते हैं।
   • सिंटैक्टिक बाधाएं (Syntactic Constraints): डौवेक (Dowek) और उरज़सिन (Urzyczyn) से प्रेरित होकर, एक मुक्त चर $u$ और पहचान पद $I$ का विशिष्ट संदर्भों में उपयोग करके, लेखक संभावित समाधानों के आकार को "सुव्यवस्थित" (well-formed) पदों तक सीमित करते हैं। यह अनावश्यक $\lambda$-एब्स्ट्रैक्शन पेश करने वाले या प्रदान किए गए तर्कों को अनदेखा करने वाले समाधानों को रोकता है।
   • सिमेंटिक बाधाएं (Semantic Constraints): लेखक टाइप किए गए पदों ($G_\star, G_0, G_{ab \Rightarrow cd}$) का एक सेट परिभाषित करते हैं जो पुनर्गठन नियमों के लिए इंटरप्रेटर (interpreters) के रूप में कार्य करते हैं। इन पदों का उपयोग यह सत्यापित करने के लिए $\beta$-तुल्यता बाधाओं में किया जाता है कि एक उम्मीदवार समाधान $0$s के अनुक्रम से$1$s के अनुक्रम में संक्रमण का सही ढंग से अनुकरण करता है।
4. मैकेनाइजेशन (Mechanization): संपूर्ण प्रमाण को रॉक प्रोवर (Rocq Prover) (पूर्व में कोक/Coq) में मशीनीकृत किया गया है। यह मशीनीकरण स्वयंसिद्ध-मुक्त (axiom-free) है और लगभग 4,000 पंक्तियों के कोड को कवर करता है, जिसमें सरल रूप से टाइप किए गए $\lambda$-कैलकुलस, रिडक्शन लॉजिक और अंतिम अनिश्चितता परिणाम की परिभाषा शामिल है।

प्रमुख योगदान (Key Contributions)

• नवीन रिडक्शन (Novel Reduction): यह शोध पत्र उच्च-क्रम $\beta$-मैचिंग में समस्या $0^+ \Rightarrow^* 1^+$ से एक नया रिडक्शन प्रदान करता है। यह $\lambda$-परिभाषनीयता के उपयोग वाले पिछले प्रमाणों के जटिल तंत्र को दरकिनार करता है।
• सरलीकृत सत्यापन (Simplified Verification): सरल सेमी-थ्यू सिस्टम की सरलता और एन्कोडिंग की संरचित प्रकृति के कारण, यह तर्क दिया गया है कि यह प्रमाण लोडर या जोली (Joly) के दृष्टिकोण की तुलना में पूर्ण विवरण में सत्यापित करने के लिए सरल है।
• समान निर्माण (Uniform Construction): यह दृष्टिकोण एक समान निर्माण की पहचान करता है जो तीन संबंधित समस्याओं की अनिश्चितता को प्रदर्शित करता है: उच्च-क्रम $\beta$-मैचिंग, इंटरसेक्शन टाइप इनहैबिटेशन (intersection type inhabitation), और $\lambda$-परिभाषनीयता। शोध पत्र स्पष्ट रूप से $\beta$-मैचिंग निर्माण को इंटरसेक्शन टाइप इनहैबिटेशन प्रमाणों में उपयोग किए जाने वाले फाइनाइट मॉडल थ्योरी व्याख्याओं से जोड़ता है।
• प्रमाणित रिडक्शन (Certified Reduction): यह कार्य हैल्टिंग प्रॉब्लम (Halting Problem) से उच्च-क्रम $\beta$-मैचिंग तक एक प्रमाणित 'मेनी-वन रिडक्शन' (many-one reduction) प्रदान करता है, क्योंकि शुरुआती पुनर्गठन समस्या की अनिश्चितता पहले से ही रॉक प्रोवर में प्रमाणित है।

परिणाम (Results)

• प्रमेय (Theorem): उच्च-क्रम $\beta$-मैचिंग अनिश्चित (undecidable) है।
• अनिश्चितता का क्रम (Order of Undecidability): निर्मित रिडक्शन टाइप ऑर्डर 6 पर अनिश्चितता को प्रदर्शित करता है। यह लोडर के इस परिणाम के अनुरूप है कि $\beta$-मैचिंग ऑर्डर 6 पर अनिश्चित है। शोध पत्र नोट करता है कि जबकि लोडर ने अनुमान लगाया था कि ऑर्डर 5 पर्याप्त हो सकता है, न तो लोडर की तकनीक और न ही वर्तमान दृष्टिकोण ऑर्डर 5 पर लागू होता है, जिससे ऑर्डर 5 की निर्णय क्षमता एक खुला प्रश्न बनी हुई है।
• मैकेनाइजेशन (Mechanization): प्रमाण को सफलतापूर्वक मौजूदा 'कोक अनडिसाइडेबिलिटी प्रूफ लाइब्रेरी' में योगदान दिया गया है, जो यह सुनिश्चित करता है कि परिणाम अक्सर मैनुअल प्रमाणों में मौजूद अस्पष्टताओं से मुक्त है।

महत्व (Significance)
यह शोध पत्र मुख्य रूप से अनिश्चितता प्रमाण के मैकेनाइजेशन और सरलीकरण के माध्यम से अपना महत्व दावा करता है। $\lambda$-परिभाषनीयता से शुरू होकर एक प्रतिबंधित स्ट्रिंग रीराइटिंग समस्या की ओर शिफ्ट होकर, लेखक एक ऐसा प्रमाण प्राप्त करते हैं जो पूर्ण औपचारिक सत्यापन (formal verification) के लिए अधिक अनुकूल है। यह कार्य उच्च-क्रम $\beta$-यूनिफिकेशन पर मौजूदा मशीनीकृत परिणामों का पूरक है। इसके अतिरिक्त, यह दृष्टिकोण उच्च-क्रम $\beta$-मैचिंग, इंटरसेक्शन टाइप इनहैबिटेशन और $\lambda$-परिभाषनीयता के बीच एक गहरा संरचनात्मक संबंध उजागर करता है, जो यह सुझाव देता है कि ये समस्याएं एक सामान्य अंतर्निहित तंत्र साझा करती हैं जो $\lambda$-पदों के माध्यम से फाइनाइट मॉडल थ्योरी गुणों के अनुकरण में निहित है। लेखक इस बात पर जोर देते हैं कि प्रमाण का विकास प्रमाण सहायक (proof assistant) के साथ संवादात्मक रूप से किया गया था, जो जटिल तार्किक निर्माण में मानवीय त्रुटि के जोखिम को कम करने के लिए व्यापक केस विश्लेषण (case analysis) पर निर्भर करता है।