💻 computer science

Work-in-Progress: A Tactic for Pattern Matching in Autosubst

यह कार्य-प्रगति (work-in-progress) पत्र Autosubst के लिए एक स्वचालित पैटर्न मिलान टैक्टिक पेश करता है जो टाइपिंग नियमों, रिडक्शन संबंधों और गैर-अद्वितीय समाधानों को संभालने में इसकी वर्तमान सीमाओं को संबोधित करता है, जैसा कि POPLMark और POPLMark Reloaded चुनौतियों पर मूल्यांकनों के माध्यम से प्रदर्शित किया गया है।

मूल लेखक: Mathews George (Heriot-Watt University Edinburgh), Kathrin Stark (Heriot-Watt University Edinburgh)

प्रकाशित 2026-07-15

📖 6 मिनट में पढ़ें🧠 गहराई से पढ़ें

CC BY 4.0

मूल लेखक: Mathews George (Heriot-Watt University Edinburgh), Kathrin Stark (Heriot-Watt University Edinburgh)

मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। ✨ नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें

कल्पना कीजिए कि आप एक विशाल, जादुई पहेली को सुलझाने की कोशिश कर रहे हैं जहाँ हर टुकड़े पर एक छिपा हुआ लेबल लगा है। कंप्यूटर विज्ञान की दुनिया में, इन लेबलों को "डी ब्रुइन इंडिसेस" (De Bruijn indices) कहा जाता है। ये कोड में वेरिएबल्स (variables) को ट्रैक रखने का एक चतुर तरीका है, लेकिन ये काफी पेचीदा होते हैं। इन्हें संगीत वाली कुर्सियों (musical chairs) के खेल की तरह समझें जहाँ हर बार जब कोई कुर्सी पर बैठता है, तो कुर्सियाँ (वेरिएबल्स) अपने नाम बदल लेती हैं। यदि आप एक पहेली के टुकड़े (एक नियम) को एक छेद (एक लक्ष्य) से मिलाने की कोशिश करते हैं, तो वे अलग दिख सकते हैं, भले ही वे वास्तव में एक ही हों, बस उन्होंने अलग टोपी पहनी हो।

लंबे समय तक, Autosubst नामक एक उपकरण इस कहानी का नायक रहा है। यह एक सुपर-स्मार्ट रोबोट की तरह है जो तुरंत आपको बता सकता है कि दो पहेली के टुकड़े एक ही हैं या नहीं, भले ही उनके लेबल इधर-उधर घूम गए हों। यह इसे करने के लिए $\sigma$ -कैलकुलस ( $\sigma$ -calculus) नामक नियमों के एक सेट का उपयोग करता है ताकि टुकड़ों को सामान्य (normalize) किया जा सके और वे बिल्कुल एक जैसे दिखें। यदि आप केवल यह जांचना चाहते हैं कि दो चीजें समान हैं या नहीं, तो यह रोबोट एकदम सही है।

समस्या: "अप्लाई" (Apply) का जाल
हालाँकि, एक पेंच है। जब आप किसी नियम को लागू करने के लिए (जैसे कि वीडियो गेम में एक "अप्लाई" बटन का उपयोग करना) इन पहेली के टुकड़ों का उपयोग करने की कोशिश करते हैं, तो रोबोट अटक जाता है। यह यह बताने में बहुत अच्छा है कि "हाँ, ये बराबर हैं," लेकिन यह यह बताने में बहुत बुरा है कि "यहाँ इस नियम को इस विशिष्ट छेद में कैसे फिट किया जाए।"

क्यों? क्योंकि कभी-कभी, एक नियम कई तरीकों से एक छेद में फिट हो सकता है, और रोबोट को यह नहीं पता होता कि बिना मदद के कौन सा तरीका "सही" वाला है। अतीत में, मानव प्रोग्रामरों को भारी काम खुद करना पड़ता था। उन्हें अपने नियमों को अजीब, अप्रत्यक्ष तरीकों से फिर से लिखना पड़ता था या केवल रोबोट को काम करने के लिए गायब लेबल का अनुमान लगाना पड़ता था। यह एक चौकोर टुकड़े को गोल छेद में जबरदस्ती डालने की कोशिश करने जैसा था, जैसे कि आपने सही उपकरण खोजने के बजाय खुद ही टुकड़े को घिसकर आकार दिया हो।

नया विचार: एक स्मार्ट अनुमान लगाने की रणनीति
यह शोध पत्र एक नया टूल पेश करता है जिसे as_apply कहा जाता है। इसे एक नए, थोड़े अधिक साहसी रोबोटिक हाथ के रूप में सोचें जिसे उन पहेली के टुकड़ों को पकड़ने और उन्हें छेदों में धकेलने के लिए डिज़ाइन किया गया है, भले ही पहली नज़र में लेबल पूरी तरह से मेल न खाते हों।

पुराने, भरोसेमंद Autosubst नियमों का उपयोग करके टुकड़ों को साफ करने के बजाय, यह नया टैकटिक heuristics (जो कि पहले देखे गए पैटर्न के आधार पर शिक्षित अनुमान हैं) का उपयोग करता है। यह छेद को देखता है, नियम को देखता है, और कहता है, "मुझे यकीन है कि अगर मैं इन लेबल्स को थोड़ा सा शिफ्ट कर दूँ, तो वे फिट हो जाएंगे!"

यह कैसे काम करता है (जादुई ट्रिक)
प्रक्रिया दो चरणों में होती है:

तैयारी (Preparation): रोबोट पहले टुकड़ों को पुराने, भरोसेमंद Autosubst नियमों का उपयोग करके यथासंभव व्यवस्थित (tidy) बनाता है।
अनुमान लगाने का खेल (The Guessing Game): इसके बाद यह टुकड़ों को मिलाने की कोशिश करता है। यदि टुकड़े पूरी तरह से मेल नहीं खाते हैं, तो यह घबराता नहीं है। इसके बजाय, यह कुछ विशिष्ट ट्रिक्स आज़माता है:
- यह जाँचता है कि क्या बेमेल होना केवल एक साधारण "शिफ्ट" (जैसे वेरिएबल को एक स्थान ऊपर ले जाना) है।
- यह जाँचता है कि क्या गायब हिस्सा केवल एक "आइडेंटिटी" (कुछ न करना) है।
- यह उन सामान्य पैटर्न को खोजता है जो आमतौर पर इन पहेलियों में होते हैं।

यदि इनमें से कोई भी अनुमान काम करता है, तो यह गायब लेबल्स को भर देता है और आगे बढ़ जाता है। यदि यह विफल हो जाता है, तो यह पीछे हटता है (backtrack) है और दूसरा अनुमान आज़माता है।

शोध पत्र क्या कहता है (और क्या नहीं कहता)
लेखक बहुत सावधान हैं कि वे बहुत अधिक बढ़ा-चढ़ाकर दावा न करें। वे स्वीकार करते हैं कि यह कोई जादुई छड़ी नहीं है जो हर संभव पहेली को सुलझा देती है।

यह पूर्ण नहीं है: शोध पत्र स्पष्ट रूप से कहता है कि कभी-कभी, एक पहेली के कई समाधान हो सकते हैं, और यह रोबोट गलत विकल्प चुन सकता है। एक पेचीदा उदाहरण बनाया जा सकता है जहाँ रोबोट गलत अनुमान लगाता है, भले ही सही उत्तर मौजूद हो।
यह एक "कार्य-प्रगति" (Work-in-Progress) है: लेखक इस पद्धति को एक "कार्य-प्रगति" के रूप में वर्णित करते हैं। वे यह दावा नहीं कर रहे हैं कि उन्होंने मिलान करने के पूरे सिद्धांत को हमेशा के लिए हल कर दिया है।
परिणाम: उन्होंने इस नए टैकटिक का परीक्षण दो प्रसिद्ध, कठिन चुनौतियों पर किया जिन्हें POPLMark और POPLMark Reloaded कहा जाता है। ये प्रोग्रामिंग भाषाओं के बारे में प्रमाण देने वाले "ओलंपिक्स" की तरह हैं।
- POPLMark चुनौती (642 लाइन कोड) में, उन्होंने इस नए टैकटिक का 15 बार उपयोग किया।
- POPLMark Reloaded चुनौती (683 लाइन कोड) में, उन्होंने इसका 10 बार उपयोग किया।
- इन सभी मामलों में, टैकटिक ने सफलतापूर्वक लक्ष्य को हल किया।

निष्कर्ष
शोध पत्र सुझाव देता है कि हालांकि इस टैकटिक की सैद्धांतिक सीमाएँ हैं (यह बहुत अजीब, प्रतिकूल पहेलियों से भ्रमित हो सकता है), यह वास्तविक दुनिया में आश्चर्यजनक रूप से अच्छा काम करता है। यह प्रोग्रामरों को अपने नियमों को अजीब, अप्रत्यक्ष तरीकों में फिर से लिखने के बजाय उन्हें स्वाभाविक रूप से लिखने की अनुमति देता है।

लेखक आशावादी लेकिन सतर्क हैं। वे सुझाव देते हैं कि यह दृष्टिकोण कई व्यावहारिक मामलों में पुराने, बोझिल तरीके की जगह ले सकता है, लेकिन वे जानते हैं कि यह सुनिश्चित करने के लिए अभी भी काम करना बाकी है कि रोबोट कभी भी गलत समाधान न चुने। वे वर्तमान में यह पता लगाने पर काम कर रहे हैं कि कौन से प्रकार की पहेलियाँ यह रोबोट 100% निश्चितता के साथ हल कर सकता है, और किनमें अभी भी मानव द्वारा काम की दोबारा जाँच करने की आवश्यकता हो सकती है।

संक्षेप में: यह एक चतुर, सहायक नया टूल है जो पहेली के टुकड़ों को मिलाने के कठिन काम को बहुत आसान बना देता है, भले ही यह अभी बॉक्स में एकमात्र टूल बनने के लिए पूरी तरह तैयार न हो।

तकनीकी सारांश: Autosubst में पैटर्न मिलान के लिए एक रणनीति

समस्या विवरण
यह शोध पत्र Autosubst फ्रेमवर्क की एक विशिष्ट सीमा को संबोधित करता है, जो कि Rocq (पूर्व में Coq) प्रूफ़ असिस्टेंट के लिए एक कोड जनरेटर है और $\sigma$ -कैलकुलस के माध्यम से de Bruijn टर्म्स और प्रतिस्थापन (substitution) के बारें में तर्क को स्वचालित करता है। जबकि Autosubst asimpl टैक्टिक का उपयोग करके धारणा-मुक्त लक्ष्यों (assumption-free goals) के लिए समानता जाँच को सफलतापूर्वक स्वचालित करता है, यह तब विफल हो जाता है जब उपयोगकर्ता मानक टैक्टिक्स जैसे apply या eapply के माध्यम से किसी लक्ष्य पर धारणाओं (जैसे टाइपिंग नियम या लेम्मा) को लागू करने का प्रयास करते हैं।

इन परिदृश्यों में, उपयोगकर्ता को $\sigma$ -तुल्यता (equivalence) के सापेक्ष एक लक्ष्य को धारणा के साथ सुसंगत (unify) करना होता है। हालाँकि, Autosubst का स्वचालन धारणाओं के विरुद्ध मिलान करने के लिए डिज़ाइन नहीं किया गया है। फलस्वरूप, उपयोगकर्ताओं को कठिन वर्कअराउंड (workarounds) अपनाने के लिए मजबूर होना पड़ता है, जैसे कि:

नियमों को अप्रत्यक्ष रूपों में तैयार करना (प्रत्यक्ष प्रतिस्थापन पदों के बजाय ताज़ा मेटा-वेरिएबल्स का उपयोग करना)।
लक्ष्य और धारणा के बीच के अंतर को पाटने के लिए सहायक लेम्मा (auxiliary lemmas) पेश करना।
प्रमाणों के दौरान लक्ष्यों को मैन्युअल रूप से रूपांतरित करना या अस्तित्व संबंधी चरों (existential variables) को स्पष्ट रूप से इंस्टैंशिएट करना।

मुख्य कठिनाई यह है कि $\sigma$ -मिलान ( $\sigma$ -तुल्यता तक मिलान) अद्वितीय नहीं है; एक एकल मिलान समस्या कई समाधान दे सकती है, जिनमें से सभी संदर्भ के पूर्ववृत्तों (premises) को संतुष्ट नहीं करते हैं। इसके अलावा, पूर्ण $\lambda\sigma$ -कैलकुलस के लिए सेकंड-ऑर्डर मिलान अनिर्णायक (undecidable) है, और $\beta$ -रिडक्शन के बिना भी, समाधान अनिवार्य रूप से अद्वितीय नहीं होते हैं।

कार्यप्रणाली (Methodology)
लेखक एक कार्य-प्रगति (work-in-progress) हीयुरिस्टिक टैक्टिक as_apply का प्रस्ताव करते हैं, जिसे $\sigma$ -तुल्यता के सापेक्ष पैटर्न मिलान को स्वचालित करने के लिए Rocq की Ltac भाषा में कार्यान्वित किया गया है। यह टैक्टिक दो प्राथमिक चरणों में कार्य करता है:

प्रीप्रोसेसिंग (Preprocessing):
- लक्ष्य और लक्षित धारणा दोनों को मौजूदा asimpl टैक्टिक का उपयोग करके $\sigma$ -कैलकुलस के संबंध में सामान्यीकृत (normalize) किया जाता है।
- धारणा में क्वांटिफाइड वेरिएबल्स को अस्तित्व संबंधी चरों (evariables) से बदल दिया जाता है।
- धारणा के पूर्ववृत्तों को उन उप-लक्ष्यों (subgoals) में परिवर्तित किया जाता है जिन्हें मिलान चरण के बाद हल किया जाना है।
- टैक्टिक substify और renamify का उपयोग करके स्पष्ट रीनेमिंग ऑपरेशन्स (जैसे $s\langle\xi\rangle$ ) और इंस्टैंशिएशन ऑपरेशन्स ( $s[\xi]$ ) के बीच रूपांतरण को संभालता है।
मिलान चरण (Matching Phase):
- टैक्टिक लक्ष्य पदों और इंस्टैंशिएटेड धारणा पदों के बीच मिलान समीकरणों का एक सेट $M = \{s_i =_\sigma t_i\}$ बनाता है।
- यह समीकरणों को बाएँ से दाएँ एक आंशिक प्रक्रिया, $\sigma_{min}$ , का उपयोग करके संसाधित करता है, जो $\sigma_{min}$ खंड (इंस्टैंशिएशन और कंपोजिशनलिटी को चित्रित करने वाले $\sigma$ -नियमों का एक उपसमुच्चय) के सापेक्ष मिलान करने का प्रयास करता है।
- हीयुरिस्टिक्स (Heuristics): यदि $\sigma_{min}$ $σ_{min}$ मिलान खोजने में विफल रहता है, तो टैक्टिक औपचारिक विकास के सामान्य पैटर्न को पकड़ने वाले हीयुरिस्टिक्स के एक सेट को लागू करता है। इनमें शामिल हैं:
  - $s[t \cdot \sigma] =_\sigma ?s[t \cdot id]$ के रूप में समीकरणों को संभालना, जिसमें अज्ञात को एक लिफ्टेड सब्स्टीट्यूशन ( $?s \mapsto s[\Uparrow\sigma]$ ) के साथ इंस्टैंशिएट किया जाता है।
  - पहचान (identity) सब्स्टीट्यूशन या विशिष्ट वेरिएबल स्ट्रक्चर से जुड़े मामलों को संभालना।
- सब्स्टीट्यूशन लागू करने के बाद, टैक्टिक धारणा को पुन: सामान्यीकृत (re-normalize) करता है। सफलता तब निर्धारित होती है जब लक्ष्य और धारणा सिंटैक्टिक रूप से समान हो जाते हैं।

इस टैक्टिक को Autosubst कंपाइलर द्वारा समर्थित पूर्ण इनपुट भाषा के लिए सामान्यीकृत किया गया है, जिसमें कई परस्पर इंडक्टिव सॉर्ट्स (mutually inductive sorts), वेक्टर सब्स्टीट्यूशंस और फर्स्ट-क्लास रीनेमिंग्स शामिल हैं।

प्रमुख योगदान

as_apply का परिचय: एक हीयुरिस्टिक टैक्टिक जो Autosubst-आधारित विकासों में apply/eapply को बदलने के लिए डिज़ाइन किया गया है, जो धारणाओं की उपस्थिति में $\sigma$ -तुल्यता के सापेक्ष मिलान को सक्षम बनाता है।
सामान्यीकरण (Generalization): जटिल बाइंडर्स और रीनेमिंग ऑपरेशन्स सहित Autosubst द्वारा समर्थित पूर्ण सिंटैक्स को कवर करने के लिए मिलान तर्क का विस्तार।
अनुभवजन्य मूल्यांकन (Empirical Evaluation): मानक बेंचमार्क, विशेष रूप से POPLMark और POPLMark Reloaded चुनौतियों पर टैक्टिक का अनुप्रयोग।

परिणाम
लेखकों ने POPLMark (642 पंक्तियाँ) और POPLMark Reloaded (683 पंक्तियाँ) चुनौतियों पर as_apply का मूल्यांकन किया।

उपयोग की आवृत्ति: POPLMark B समाधान में टैक्टिक का उपयोग 15 बार और POPLMark Reloaded समाधान में 10 बार किया गया।
प्रभावशीलता: सभी परीक्षण किए गए मामलों में, as_apply ने इच्छित लक्ष्यों को सफलतापूर्वक हल किया।
सरलीकरण: टैक्टिक के उपयोग ने अप्रत्यक्ष नियम फॉर्मुलेशन, सहायक लेम्मा और मैन्युअल लक्ष्य रूपांतरण की आवश्यकता को समाप्त कर दिया जो पिछले समाधानों की विशेषता थी।
सीमाएँ: लेखक स्वीकार करते हैं कि as_apply $\sigma$ -पूर्ण (complete) नहीं है और न ही यह एक ड décider (decider) है। क्योंकि $\sigma$ -मिलान के कई समाधान हो सकते हैं, टैक्टिक की हीयुरिस्टिक प्रकृति का अर्थ है कि यह सैद्धांतिक रूप से एक गलत समाधान चुन सकता है जब एक सही समाधान मौजूद हो, हालांकि केस स्टडीज में ऐसे कोई विफलताएं नहीं देखी गईं।

महत्व और दावे
शोध पत्र का दावा है कि जबकि $\sigma$ -मिलान की सैद्धांतिक समस्या स्वाभाविक रूप से कठिन है (गैर-अद्वितीय समाधान, पूर्ण $\lambda\sigma$ में अनिर्णायकता), एक व्यावहारिक, हीयुरिस्टिक दृष्टिकोण वास्तव में उच्च स्तर का स्वचालन प्राप्त कर सकता है। इसका महत्व उपयोगकर्ता के मैनुअल बोझ को कम करने में है जो de Bruijn सिंटैक्स के साथ काम कर रहे हैं, जिससे उन्हें अपने प्रमाण इंजन की सीमाओं के अनुरूप अप्रत्यक्ष रूपों के बजाय अपने प्रत्यक्ष, प्राकृतिक रूपों में टाइपिंग नियम और लेम्मा को घोषित करने की अनुमति मिलती है।

लेखक अपने वर्तमान कार्य के बारे में विनम्र हैं, इसे "कार्य-प्रगति" (Work-in-Progress) के रूप में लेबल करते हैं। वे नोट करते हैं कि वर्तमान टैक्टिक हीयुरिस्टिक्स पर निर्भर करता है क्योंकि अनंत या कई समाधानों की संभावना बनी रहती है। भविष्य के कार्य का लक्ष्य सबसे बड़े $\sigma'$ खंड की पहचान करना है जिसके लिए एक विशिष्टता मानदंड (uniqueness criterion) लागू होता है, जिससे संभावित रूप से प्रमाणित गारंटी के साथ एक मिलान टैक्टिक विकसित हो सके।

इसी तरह के और पेपर