💻 computer science

Towards an HRS Category in TermCOMP

यह शोध पत्र यह सिद्ध करके कि उच्च-क्रम बेंचमार्क के एक विशिष्ट सिंटैक्टिक उपवर्ग के लिए निपको के HRSs और एक बीटा-प्रथम रणनीति के तहत रीराइटिंग (rewriting) एक समान हैं, TermCOMP में एक नए HRS उपश्रेणी के लिए एक औपचारिक आधार स्थापित करता है, जिससे अधिक उपकरणों को टर्मिनेशन विश्लेषण में प्रतिस्पर्धा करने में सक्षम बनाया जा सके।

मूल लेखक: Johannes Niederhauser, Aart Middeldorp

प्रकाशित 2026-06-25

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

CC BY 4.0

मूल लेखक: Johannes Niederhauser, Aart Middeldorp

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

कल्पना कीजिए कि आप TermCOMP नामक एक विशाल अंतर्राष्ट्रीय कुकिंग प्रतियोगिता आयोजित कर रहे हैं। इस प्रतियोगिता का लक्ष्य यह देखना है कि कौन सा कंप्यूटर प्रोग्राम (या "शेफ") यह सिद्ध करने में सबसे बेहतर है कि व्यंजनों के निर्देशों का एक विशिष्ट सेट अंततः खाना बनाना बंद कर देगा और एक अंतिम व्यंजन तैयार करेगा, न कि अनिश्चित काल तक चलाने (stirring) के अनंत लूप में फंसा रहेगा।

वर्षों से, इस प्रतियोगिता में "हाई-ऑर्डर कुकिंग" के लिए एक विशिष्ट श्रेणी रही है। हालाँकि, एक समस्या थी: शेफ अलग-अलग भाषाओं और अलग-अलग नियमों का उपयोग कर रहे थे कि सामग्रियों को कैसे मिलाया जाए। कुछ शेफ नियम सेट A (जिसे AFSs कहा जाता है) का पालन कर रहे थे, जबकि अन्य नियम सेट B (जिसे HRSs कहा जाता है, जो निपकोव के कार्य पर आधारित है) का पालन करना चाहते थे। क्योंकि नियम बहुत अलग थे, शेफ वास्तव में एक-दूसरे के खिलाफ निष्पक्ष रूप से प्रतिस्पर्धा नहीं कर सकते थे। यह एक ऐसा मामला था जैसे किसी ऐसे शेफ की तुलना करना जो केवल व्हिस्क (whisk) का उपयोग करता है, बनाम एक ऐसे शेफ की जो केवल ब्लेंडर का उपयोग करता है। वे दोनों भोजन बना रहे हैं, लेकिन उनकी कार्यप्रणाली बहुत अलग है।

समस्या: दो अलग-अलग भाषाएँ

कंप्यूटर विज्ञान की दुनिया में, ये "व्यंजन" प्रतीकों को फिर से लिखने के गणितीय नियम हैं।

नियम सेट A (AFSs) एक सख्त रसोई की तरह है जहाँ आप सामग्रियों को तभी बदल सकते हैं जब वे बिल्कुल मेल खाती हों। यदि रेसिपी कहती है "मैदा डालें," तो आप "मैदा और दूध का मिश्रण" तब तक नहीं डाल सकते जब तक कि आप इसे स्पष्ट रूप से न लिख दें।
नियम सेट B (HRSs) अधिक लचीला है। यह "बीटा-रिडक्शन" (beta-reduction) की अनुमति देता है, जो एक जटिल निर्देश को स्वचालित रूप से सरल बनाने जैसा है। यदि रेसिपी कहती है "X और Y को मिलाने का परिणाम लें," तो HRSs आपको तुरंत मिश्रण करने और परिणाम का उपयोग करने की अनुमति देते हैं, जबकि नियम सेट A आपको अंत तक प्रतीक्षा करने के लिए मजबूर कर सकता है।

इस शोध पत्र के लेखक, जोहान्स निडरहाउसर और आर्ट मिडल्डोर्फ, एक ऐसा समान मैदान बनाना चाहते थे जहाँ नियम सेट B का उपयोग करने वाले शेफ, नियम सेट A का उपयोग करने वालों के साथ एक ही अखाड़े में प्रतिस्पर्धा कर सकें।

समाधान: एक नया "यूनिवर्सल ट्रांसलेटर"

यह पेपर व्यंजनों के एक नए, सावधानीपूर्वक परिभाषित उपसमूह को पेश करता है जिसे एक्सटेंडेड पैटर्न रीराइट सिस्टम्स (EPRSs) कहा जाता है। इसे एक विशेष "यूनिवर्सल ट्रांसलेटर" प्रारूप के रूप में सोचें।

लेखकों ने केवल यह नहीं कहा कि "आइए हम सभी को HRSs का उपयोग करने दें।" इसके बजाय, उन्होंने इन लचीले HRS व्यंजनों को लिखने का एक विशिष्ट, सरल तरीका खोजा ताकि उन्हें मौजूदा प्रतियोगिता प्रणाली (जो STMRS नामक प्रारूप का उपयोग करती है) द्वारा समझा जा सके।

उन्होंने व्यंजनों का एक "स्वीट स्पॉट" खोजा जहाँ:

नियम सख्त लेकिन स्मार्ट हैं: उन्होंने नियमों का एक वर्ग परिभाषित किया जहाँ "लेफ्ट-हैंड साइड" (वह हिस्सा जिसे मैच किया जा रहा है) एक विशिष्ट पैटर्न का पालन करता है जिसे "एक्सटेंडेड पैटर्न" कहा जाता है। यह सुनिश्चित करता है कि जब आप सामग्रियों को मिलाने का प्रयास करते हैं, तो कंप्यूटर भ्रमित या अटक न जाए।
अनुवाद पूरी तरह से काम करता है: उन्होंने गणितीय रूप से सिद्ध किया कि यदि आप इस नए "यूनिवर्सल ट्रांसलेटर" प्रारूप (EPRS) में लिखे गए व्यंजन को लेते हैं और उसे मौजूदा प्रतियोगिता प्रणाली (STMRS) के माध्यम से चलाते हैं, तो परिणाम ठीक वैसा ही होता है जैसा कि मूल, अधिक जटिल HRS नियमों का उपयोग करके चलाने पर होता।

"जादुई ट्रिक" की उपमा

कल्पना कीजिए कि आपके पास एक जटिल जादू का खेल (HRS नियम) है जिसमें टोपी से खरगोश प्रकट होता है।

पुराना तरीका: इस जादू को सिद्ध करने के लिए, आपको उस विशिष्ट खरगोश के लिए एक पूरा नया मंच बनाना पड़ता था।
नया तरीका: लेखकों ने दिखाया कि यदि आप खरगोश, टोपी और छड़ी को एक बहुत ही विशिष्ट, सरल तरीके से व्यवस्थित करते हैं (एक "वेल-बिहेव्ड" EPRS), तो आप उसी जादू के खेल को प्रतियोगिता के लिए पहले से बने मानक मंच (STMRS) का उपयोग करके सफलतापूर्वक प्रदर्शित कर सकते हैं।

उन्होंने सिद्ध किया कि हर बार जब HRS शेफ एक कदम उठाता है, तो STMRS शेफ एक कदम उठाने के बाद एक त्वरित "सफाई" (जिसे $\beta$ -नॉर्मलाइजेशन कहा जाता है) करता है और ठीक वही परिणाम प्राप्त करता है।

यह क्यों महत्वपूर्ण है

यह केवल गणित नहीं है; यह निष्पक्षता और प्रगति के बारे में है।

अधिक शेफ, अधिक प्रतिस्पर्धा: इस विशिष्ट उपसमूह को परिभाषित करके, प्रतियोगिता आयोजक अब HRS शैली का उपयोग करने वाले अधिक उपकरणों (शेफ) को प्रतिस्पर्धा करने के लिए आमंत्रित कर सकते हैं।
बेह‌تر बेंचमार्क: यह प्रतियोगिता डेटाबेस (TPDB) को नियमों को तोड़े बिना विविध प्रकार की समस्याओं को शामिल करने की अनुमति देता है।
सिद्ध समानता: यह पेपर केवल अनुमान नहीं लगाता कि यह काम करेगा; यह इस विशिष्ट वर्ग की समस्याओं के लिए दोनों विधियों की समानता के लिए एक कठोर गणितीय प्रमाण (थ्योरम 15) प्रदान करता है।

मुख्य निष्कर्ष

लेखकों ने सफलतापूर्वक कंप्यूटर रीराइटिंग के सोचने के दो अलग-अलग तरीकों के बीच एक सेतु का निर्माण किया है। उन्होंने दिखाया कि नियमों को थोड़ा सीमित करके ( "वेल-बिहेव्ड" पैटर्न का उपयोग करके), लचीली HRS शैली को मौजूदा TermCOMP ढांचे के भीतर पूरी तरह से काम करने के लिए बनाया जा सकता है। यह प्रतियोगिता के लिए एक नए, निष्पक्ष उप-वर्ग के लिए औपचारिक आधार तैयार करता है जहाँ अधिक शक्तिशाली उपकरण अंततः एक-दूसरे के विरुद्ध प्रतिस्पर्धा कर सकते हैं।

नोट: यह पेपर पूरी तरह से इस समानता के गणितीय आधार पर केंद्रित है। यह चिकित्सा निदान या नैदानिक उपयोगों जैसे विशिष्ट वास्तविक दुनिया के अनुप्रयोगों के बारे में चर्चा नहीं करता है, न ही यह प्रतियोगिता के दायरे से परे भविष्य की तकनीकों की भविष्यवाणी करता है। यह पूरी तरह से कंप्यूटर प्रमाणों के लिए "कुकिंग कॉम्पिटिशन" को अधिक समावेशी और कठोर बनाने के बारे में है।

तकनीकी सारांश: TermCOMP में एक HRS श्रेणी की ओर

समस्या विवरण (Problem Statement)
वार्षिक टर्मिनेशन कॉम्पिटिशन (TermCOMP) में हायर-ऑर्डर रीराइटिंग के लिए एक श्रेणी शामिल है। ऐतिहासिक रूप से, इस श्रेणी ने अल्जेब्रिक फंक्शनल सिस्टम्स (AFSs) की सिमेंटिक्स का उपयोग किया है, जो प्लेन मैचिंग और स्पष्ट $\beta$ -रिडक्शन नियमों पर निर्भर करती है। जबकि निपकॉव के हायर-ऑर्डर रीराइट सिस्टम्स (HRSs), जो $\beta\eta$ के मोड्यूलो रीराइटिंग करते हैं और आमतौर पर मिलर के पैटर्न (PRSs) या हालिया डिटरमिनिस्टिक हायर-ऑर्डर पैटर्न रीराइट सिस्टम्स (DPRSs) का उपयोग करते हैं, स्थापित औपचारिकताएं हैं, उन्हें TermCOMP के प्रतिस्पर्धी ढांचे में पूरी तरह से एकीकृत नहीं किया गया है। चुनौती HRSs की सिमेंटिक्स ( $\beta\eta$ के मोड्यूलो रीराइटिंग) को मौजूदा TermCOMP फ्रेमवर्क (AFSs और मेटा-सबस्टीट्यूशन पर आधारित) के साथ सामंजस्य बिठाने में है, ताकि HRSs को लक्षित करने वाले टूल्स सीधे AFSs को लक्षित करने वाले टूल्स के विरुद्ध प्रतिस्पर्धा कर सकें।

कार्यप्रणाली (Methodology)
लेखक HRSs और वर्तमान TermCOMP हायर-ऑर्डर सिमेंटिक्स (जिसे सिंपली-टाइप्ड मेटा-सबस्टीट्यूशन रीराइट सिस्टम्स (STMRSs) के रूप में परिभाषित किया गया है) के बीच एक औपचारिक सेतु प्रस्तावित करते हैं। कार्यप्रणाली में तीन मुख्य चरण शामिल हैं:

पैटर्न का सामान्यीकरण (Generalization of Patterns): लेखक एक्सटेंडेड पैटर्न रीराइट सिस्टम्स (EPRSs) पेश करते हैं, जो PRSs और DPRSs दोनों का सामान्यीकरण करने वाला एक उपवर्ग है। EPRSs, "एक्सटेंडेड पैटर्न्स" (EPATs) का उपयोग करते हैं, जो DPRSs के डिटरमिनिस्टिक मैचिंग प्रतिबंधों को शिथिल करते हैं, जबकि एक ऐसी संरचना बनाए रखते हैं जहाँ फ्री वेरिएबल्स को नॉन-एब्स्ट्रैक्शन आर्गुमेंट्स पर लागू किया जाता है। यह वर्ग मुख्य रूप से सैद्धांतिक प्रमाण को सुगम बनाने के लिए परिभाषित किया गया है, न कि एक स्टैंडअलोन व्यावहारिक टूल के रूप में।
STMRS सिमेंटिक्स का विस्तार (Extension of STMRS Semantics): लेखक STMRS नियमों (वर्तमान TermCOMP मानक) को विस्तारित करते हैं ताकि लेफ्ट-हैंड साइड्स को केवल मानक पैटर्न के बजाय EPATs के रूप में अनुमति दी जा सके। वे वेल-बिहेव्ड (well-behaved) और क्वासी-वेल-बिहेव्ड (quasi-well-behaved) टर्म्स की अवधारणा पेश करते हैं। ये सिंटैक्टिक प्रतिबंध सुनिश्चित करते हैं कि जब मेटा-सबस्टीट्यूशन लागू किए जाते हैं, तो परिणामी टर्म्स $\beta$ -नॉर्मल फॉर्म (विशेष रूप से $\beta\eta$ -लॉन्ग नॉर्मल फॉर्म) में रहते हैं और नए $\beta$ -रेडेक्स उत्पन्न नहीं करते हैं जिन्हें अतिरिक्त रिडक्शन स्टेप्स की आवश्यकता हो।
नॉर्मलाइज्ड रीराइटिंग के माध्यम से कार्यान्वयन (Implementation via Normalized Rewriting): मुख्य तकनीकी योगदान यह स्थापित करना है कि एक वेल-बिहेव्ड STMRS में रीराइटिंग, $\beta$ -नॉर्मलाइजेशन के बाद, संगत EPRS में रीराइटिंग का अनुकरण (simulate) करती है। लेखक साधारण सब्स्टीट्यूशन (जो EPRSs में उपयोग किए जाते हैं) और मेटा-सब्स्टीट्यूशन (जो STMRSs में उपयोग किए जाते हैं) के बीच एक अनुवाद को परिभाषित करते हैं ताकि टर्मिनेशन के संबंध में दोनों प्रणालियों की समानता को सिद्ध किया जा सके।

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

EPRSs की परिभाषा: HRSs का एक नया सिंटैक्टिक उपवर्ग, जो DPRSs का सामान्यीकरण करता है, जिससे प्रबंधनीय मैचिंग गुणों को बनाए रखते हुए व्यापक रेंज के बेंचमार्क की अनुमति मिलती है।
समानता के लिए सिंटैक्टिक प्रतिबंध: "वेल-बिहेव्ड" STMRS नियमों का परिचय। ये नियम लेफ्ट-हैंड साइड्स को वेल-बिहेव्ड होने और राइट-हैंड साइड्स को क्वोसी-वेल-बिहेव्ड होने के लिए प्रतिबंधित करते हैं। यह सुनिश्चित करता है कि मेटा-सबस्टीट्यूशन का अनुप्रयोग $\beta$ -रेडेक्स नहीं बनाता है, जिससे टर्म्स का $\beta$ -नॉर्मल फॉर्म बना रहता है।
औपचारिक समानता प्रमेय (Formal Equivalence Theorem): यह पेपर सिद्ध करता है कि एक वेल-बिहेव्ड STMRS $R$ और एक टर्म $s$ (जो $\beta\eta$ -लॉन्ग नॉर्मल फॉर्म में है) के लिए, EPRS सिमेंटिक्स में एक रीराइट स्टेप ( $s \to_R t$ ) होता है यदि और केवल यदि STMRS सिमेंटिक्स में एक रीराइट स्टेप के बाद $\beta$ -नॉर्मलाइजेशन होता है ( $s \Rightarrow_R \cdot \Rightarrow!_\beta t$ )।

परिणाम (Results)
प्राथमिक परिणाम थ्योरम 15 (Theorem 15) है, जो वेल-बिहेव्ड STMRSs और उनके संगत EPRSs के रीराइट संबंधों के बीच संबंध स्थापित करता है। विशेष रूप से:

$s \Rightarrow_R \cdot \Rightarrow!_\beta t$ यदि और केवल यदि $s \to_R t$ (R को एक EPRS के रूप में देखते हुए)।
इससे कोरोलरी 20 (Corollary 20) प्राप्त होता है, जो बताता है कि एक वेल-बिहेव्ड STMRS में "रीराइट फिर $\beta$ -नॉर्मलाइज़" रणनीति का टर्मिनेशन, संगत EPRS के यूनिवर्सल टर्मिनेशन के साथ मेल खाता है।

लेखक प्रदर्शित करते हैं कि यह समानता $\beta\eta$ -लॉन्ग नॉर्मल फॉर्म वाले टर्म्स के लिए बनी रहती है। वे नोट करते हैं कि सेकंड-ऑर्डर STMRSs के लिए, यह पत्राचार (correspondence) और भी मजबूत है, क्योंकि मेटा-सबस्टीट्यूशन उस विशिष्ट संदर्भ में $\beta$ -रेडेक्स नहीं बना सकते हैं।

महत्व (Significance)
यह पेपर दावा करता है कि यह TermCOMP में एक HRS (उप)श्रेणी के लिए औपचारिक आधार तैयार करता है। मौजूदा TPDB फॉर्मेट के भीतर सिंटैक्टिक रूप से जांच योग्य बेंचमार्क (वेल-बिहेव्ड STMRSs) को परिभाषित करके, लेखक निम्नलिखित सक्षम बनाते हैं:

प्रत्यक्ष प्रतिस्पर्धा: HRSs ( $\beta\eta$ -रीराइटिंग का उपयोग करने वाले) के लिए डिज़ाइन किए गए टूल्स अब एक ही श्रेणी के भीतर AFSs को लक्षित करने वाले टूल्स के विरुद्ध प्रतिस्पर्धा कर सकते हैं, क्योंकि उनके टर्मिनेशन गुण प्रस्तावित सिमेंटिक्स के तहत समान सिद्ध होते हैं।
व्यापक टूल सपोर्ट: कार्यान्वयन का परिणाम केवल वैश्विक टर्मिनेशन प्रॉपर्टी के बजाय स्टेप-बाय-स्टेप पत्राचार पर आधारित होने के कारण, केवल टर्मिनेशन के गुणों से परे तुलना करने की अनुमति देता है।
मौजूदा कार्य का परिशोधन: यह परिणाम AFSMs (Kop) और कॉम्बिनेटरी सिस्टम्स (van Oostrom और van Raamsdonk) में PRSs के पिछले कार्यान्वयन को अधिक सामान्य वर्ग के HRSs (EPRSs) तक विस्तारित करके और नॉर्मलाइज्ड रीराइटिंग और हायर-ऑर्डर रीराइटिंग के बीच समानता के लिए एक कठोर प्रमाण प्रदान करके उनके कार्य को मजबूत करता है।

लेखक अपने दायरे के संबंध में विनम्र बने हुए हैं, यह स्वीकार करते हुए कि यह परिणाम सभी HRSs को कवर नहीं करता है क्योंकि मेटा-सबस्टीट्यूशन पूर्ण हायर-ऑर्डर सब्स्टीट्यूशन की तुलना में स्ट्रिक्टली कम शक्तिशाली है। हालांकि, उनका तर्क है कि परिभाषित उपवर्ग मौजूदा बेंचमार्क के एक महत्वपूर्ण हिस्से और उनके पिछले कार्य में पेश किए गए विशिष्ट DPRSs को समायोजित करने के लिए पर्याप्त है।

समस्या: दो अलग-अलग भाषाएँ

समाधान: एक नया "यूनिवर्सल ट्रांसलेटर"

"जादुई ट्रिक" की उपमा

यह क्यों महत्वपूर्ण है

मुख्य निष्कर्ष

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