💻 computer science

Non-Termination of Logic Programs Using Patterns

यह शोध पत्र एक नई अनफोल्डिंग तकनीक को पेश करके गैर-लूपिंग गैर-समाप्ति (non-looping non-termination) का पता लगाने के लिए टर्म रीराइटिंग दृष्टिकोण को लॉजिक प्रोग्रामिंग के अनुकूल बनाता है, जो अनंत परिमित रीराइट अनुक्रमों (infinite sets of finite rewrite sequences) का प्रतिनिधित्व करने वाले पैटर्न उत्पन्न करता है, जिसका NTI टूल का उपयोग करके प्रयोगात्मक रूप से मूल्यांकन किया गया है।

मूल लेखक: Etienne Payet

प्रकाशित 2026-08-10

📖 4 मिनट में पढ़ें☕ कॉफ़ी ब्रेक में पढ़ें

CC BY 4.0

मूल लेखक: Etienne Payet

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

कल्पना कीजिए कि आप एक रोबोट को पहेली सुलझाने की कोशिश करते हुए देख रहे हैं। कभी-कभी, रोबोट एक लूप में फंस जाता है: वह कदम A करता है, फिर कदम B, फिर फिर से कदम A, और फिर से, हमेशा के लिए। यह एक हैम्स्टर के पहिये पर दौड़ने जैसा है; वह चल तो रहा है, लेकिन कहीं पहुँच नहीं रहा है। कंप्यूटर विज्ञान की दुनिया में, विशेष रूप से लॉजिक प्रोग्रामिंग नामक एक क्षेत्र में, ये रोबोट ऐसे प्रोग्राम हैं जो नियमों के एक सेट का पालन करके सवालों के जवाब देने की कोशिश करते हैं। यदि कोई प्रोग्राम लूप में फंस जाता है, तो वह अपना काम कभी पूरा नहीं कर पाता, जो कि एक ऐसा बग है जिसे प्रोग्रामर पकड़ना चाहते हैं।

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

यह शोध पत्र इन मायावी, गैर-दोहराने वाले अनंत लूपों को पकड़ने का एक चतुर नया तरीका पेश करता है। लेखक, एटिएन पायेट (Etienne Payet) ने एक उपकरण बनाया है जिसे NTI कहा जाता है, जो लॉजिक प्रोग्रामों के लिए एक सुपर-पावर्ड डिटेक्टिव की तरह काम करता है। प्रोग्राम को चरण-दर-चरण चलते हुए देखने के बजाय, यह उपकरण अनफोल्डिंग (unfolding) नामक तकनीक का उपयोग करता है। अनफोल्डिंग को एक जटिल ओरिगामी क्रेन को सीधा करके उसके नीचे के फोल्ड्स के पैटर्न को देखने जैसा समझें। प्रोग्राम के नियमों को 'अनफोल्ड' करके, यह उपकरण "पैटर्न" बनाता है—अमूर्त ब्लूप्रिंट जो न केवल एक विशिष्ट पथ का वर्णन करते हैं, बल्कि उन संभावित पथों के एक अनंत परिवार का वर्णन करते हैं जो प्रोग्राम ले सकता है।

शोध पत्र की मुख्य खोज यह है कि इन ब्लूप्रिंट्स का उपयोग करके, विशेष रूप से एक सरलीकृत संस्करण जिसे "सिंपल पैटर्न्स" कहा जाता है, यह उपकरण गणितीय रूप से सिद्ध कर सकता है कि एक प्रोग्राम एक साधारण लूप में फंसे बिना अनंत काल तक कैसे चलेगा। लेखक ने इसका परीक्षण 41 अलग-अलग लॉजिक प्रोग्रामों पर किया जो ज्ञात रूप से कठिन थे। उनके उपकरण ने उनमें से कई में अनंत, गैर-दोहराने वाले पथों की सफलतापूर्वक पहचान की, जिनमें चार ऐसे प्रोग्राम भी शामिल थे जिन्हें किसी अन्य मौजूदा टूल ने इससे पहले नॉन-टर्मिनेटिंग साबित नहीं कर पाया था। हालाँकि, शोध पत्र अपनी सीमाओं के बारे में ईमानदार है: उपकरण ने हर एक मामले को हल नहीं किया, और कुछ प्रोग्रामों के लिए, यह 10 सेकंड तक चलने के बाद अटक गया या टाइम आउट हो गया। लेखक का सुझाव है कि हालांकि उनकी विधि डिटेक्टिव के किट में एक शक्तिशाली नया जुड़ाव है, लेकिन यह कोई जादुई छड़ी नहीं है जो अभी तक हर रहस्य को हल करती है। वे भविष्य में टूल को और स्मार्ट बनाने की योजना बना रहे हैं, इस उम्मीद में कि वे इन ट्रिकी, गैर-दोहराने वाले अनंत लूपों को और भी अधिक पकड़ सकें।

तकनीकी सारांश: पैटर्नों का उपयोग करके लॉजिक प्रोग्राम्स की नॉन-टर्मिनेशन (Non-Termination)

समस्या विवरण (Problem Statement)
यह शोध पत्र लॉजिक प्रोग्राम्स (LPs) में नॉन-टर्मिनेशन के स्वचालित पता लगाने (automatic detection) को संबोधित करता है। जबकि मौजूदा शोध का एक बड़ा हिस्सा 'लूप्स' (loops - वे परिमित रीराइट सीक्वेंस जिन्हें अनिश्चित काल तक दोहराया जा सकता है) का पता लगाने पर केंद्रित है, यह कार्य 'नॉन-लूपिंग नॉन-टर्मिनेशन' (non-looping non-termination) को लक्षित करता है। ये ऐसे अनंत रीराइट सीक्वेंस हैं जिनमें कोई लूप शामिल नहीं होता, जिससे वे स्वाभाविक रूप से गैर-आवर्ती (non-periodic) और पता लगाने में कठिन हो जाते हैं। लेखक नोट करते हैं कि ऐसे सीक्वेंस सरल लॉजिक प्रोग्राम्स से उत्पन्न हो सकते हैं, फिर भी मानक लूप-डिटेक्शन विधियाँ उन्हें पहचानने में विफल रहती हैं। इसके दो कारण हैं: सैद्धांतिक (अनंत अनुक्रमों के उल्लेखनीय रूपों का अध्ययन करना) और व्यावहारिक (प्रोग्रामर्स को उन क्वेरीज़ की पहचान करने में मदद करना जो अनंत काल तक चलती रहती हैं)।

कार्यप्रणाली (Methodology)
लेखक ने एमेस एट अल. (2012) द्वारा टर्म रीराइटिंग (term rewriting) के लिए पेश किए गए एक दृष्टिकोण को लॉजिक प्रोग्रामिंग के क्षेत्र में अनुकूलित किया है। मुख्य कार्यप्रणाली में एक नई 'अनफोल्डिंग तकनीक' (unfolding technique) को परिभाषित करना शामिल है जो संभावित रूप से अनंत परिमित रीराइट सीक्वेंस के "पैटर्न" (patterns) उत्पन्न करती है।

पैटर्न परिभाषाएँ (Pattern Definitions):
- पैटर्न प्रतिस्थापन (Pattern Substitutions): इन्हें जोड़े $\theta = (\sigma, \mu)$ के रूप में परिभाषित किया गया है, जिसे $\sigma \star \mu$ द्वारा दर्शाया जाता है, जो प्रतिस्थापन के सेट $\{\theta(n) = \sigma^n\mu \mid n \in \mathbb{N}\}$ का वर्णन करता है।
- पैटर्न टर्म्स (Pattern Terms): जोड़े $(s, \theta)$ जो सेट $\{s\theta(n) \mid n \in \mathbb{N}\}$ का वर्णन करते हैं।
- पैटर्न रूल्स (Pattern Rules): पैटर्न टर्म्स के जोड़े $(p, q)$ जो बाइनरी रूल्स के सेट $\{(p(n), q(n)) \mid n \in \mathbb{N}\}$ का वर्णन करते हैं।
शुद्धता और अनफोल्डिंग (Correctness and Unfolding):
- एक पैटर्न रूल को प्रोग्राम $P$ के संबंध में सही (correct) माना जाता है यदि वह वर्णित नियमों का सेट $P$ के बाइनरी अनफोल्डिंग ($binunf(P)$) का उपसमुच्चय (subset) हो।
- लेखक एक नया अनफोल्डिंग ऑपरेटर $T^\pi_{P,B}$ पेश करते हैं जो एक प्रोग्राम $P$ और सही पैटर्न रूल्स के एक आधार सेट $B$ से पैटर्न रूल्स की गणना करता है। यह ऑपरेटर पैटर्न टर्म्स के लिए एक यूनिफिकेशन एल्गोरिदम का उपयोग करके नियमों को जोड़ता है, जो पारंपरिक बाइनरी अनफोल्डिंग की तुलना में तेजी से "अनफोल्ड" करता है, क्योंकि यह $binunf(P)$ के अनंत उपसमुच्चयों को परिमित प्रस्तुतियों (finite representations) में कैप्चर करता है।
सरल पैटर्न और यूनिफिकेशन (Simple Patterns and Unification):
- इस दृष्टिकोण को ऑटोमेटेबल बनाने के लिए, लेखक डोमेन को सरल पैटर्न टर्म्स (simple pattern terms) तक सीमित करते हैं, जहाँ प्रतिस्थापन एक विशिष्ट संरचना (unary contexts के साथ) का पालन करते हैं।
- सरल टर्म्स के लिए एक यूनिफिकेशन एल्गोरिदम प्रदान किया गया है। यह सरल पैटर्न टर्म्स को एक विशेष सिग्नेचर $\Upsilon$ (बार-बार होने वाले एम्बेडिंग को दर्शाने के लिए $c_{a,b}$ जैसे यूनरी प्रतीकों का उपयोग करते हुए) के ऊपर टर्म्स में मैप करता है और शास्त्रीय यूनिफिकेशन एल्गोरिदम (जैसे रोबिन्सन, मार्टेली-मोंटानेरी) लागू करता है।
- यह एल्गोरिदम आंशिक रूप से सही (partially correct) सिद्ध है: यदि यह सफलतापूर्वक समाप्त होता है, तो यह इनपुट पैटर्न अनुक्रमों के लिए एक मोस्ट जनरल यूनिफायर (mgu) उत्पन्न करता है।
नॉन-टर्मिनेशन मानदंड (Non-Termination Criteria):
- सामान्य मानदंड (Theorem 3): एमेस एट अल. से अनुकूलित, यह बताता है कि यदि पैटर्न अनफोल्डिंग में $(u \star \sigma \star \mu, u\sigma^a \star \sigma^b\sigma' \star \mu\mu')$ के रूप में एक नियम मौजूद है, जहाँ $\sigma'$ , $\sigma$ और $\mu$ के साथ कम्यूट (commute) करता है, तो एक अनंत श्रृंखला (infinite chain) मौजूद होती है।
- विशेष मानदंड (Theorem 5): विशेष पैटर्न रूल्स (सरल नियमों का एक उपसमुच्चय) के लिए एक अधिक आसानी से जांचा जाने वाला मानदंड। यदि ऐसी ही कोई नियम अनफोल्डिंग में मौजूद है, तो यह पेपर नियम के लेफ्ट-हैंड साइड के विशिष्ट इंस्टेंस से एक अनंत श्रृंखला के अस्तित्व को सिद्ध करता है।

मुख्य योगदान (Key Contributions)
पेपर चार प्राथमिक योगदान प्रस्तुत करता है:

नई अनफोल्डिंग तकनीक: लॉजिक प्रोग्रामिंग के लिए सही पैटर्न रूल्स बनाने की एक विधि, जो टर्म रीराइटिंग में उपयोग किए जाने वाले नौ इन्फरेंस रूल्स की तुलना में अधिक संक्षिप्त प्रस्तुति प्रदान करती है और जटिल एप्लीकेशन रणनीतियों की आवश्यकता को समाप्त करती है।
सरल पैटर्न टर्म्स और यूनिफिकेशन: पैटर्न टर्म्स के एक प्रतिबंधित रूप ("सरल") और एक संगत यूनिफिकेशन एल्गोरिदम की परिभाषा, जो सही सिद्ध है।
ऑटोमेटेबल पर्याप्त स्थिति (Sufficient Condition): सरल पैटर्न रूल्स से नॉन-लूपिंग नॉन-टर्मिनेशन का पता लगाने के लिए एक आसानी से जांचने योग्य स्थिति (Theorem 5)।
कार्यान्वयन (NTI): NTI नामक एक टूल में इस दृष्टिकोण का कार्यान्वयन।

प्रायोगिक परिणाम (Experimental Results)
लेखक ने TPDB (Termination Problem Data Base) में मौजूद नॉन-लूपिंग नॉन-टर्मिनेटिंग टर्म रीवेट सिस्टम्स (TRSs) से प्राप्त 41 लॉजिक प्रोग्राम्स पर NTI का मूल्यांकन किया।

सफलता: टूल ने 41 में से 36 प्रोग्राम्स के लिए नॉन-टर्मिनेशन को सफलतापूर्वक सिद्ध किया। विशेष रूप से, यह 4 प्रोग्राम्स (टेबल्स में † के साथ चिह्नित) पर सफल रहा जिन्हें 2024 तक इंटरनेशनल टर्मिनेशन कॉम्पिटिशन में किसी भी अन्य TRS एनालाइज़र द्वारा नॉन-टर्मिनेटिंग सिद्ध नहीं किया गया था।
विफलता: यह दृष्टिकोण 5 प्रोग्राम्स पर विफल रहा, जिसका मुख्य कारण "नेचुरल चॉइस" (उदाहरण 12 में चर्चा की गई) का उपयोग करते समय यूनिफिकेशन एल्गोरिदम की अपूर्णता या सरल पैटर्न (उदाहरण 9) तक प्रतिबंध था।
प्रदर्शन: निष्पादन समय (execution times) आम तौर पर कम था (सफल मामलों के लिए 300ms से कम), हालांकि कुछ जटिल मामलों में टाइमआउट भी हुआ।

महत्व और दावे (Significance and Claims)
लेखक का दावा है कि उनका दृष्टिकोण लॉजिक प्रोग्राम्स के टर्मिनेशन को गलत सिद्ध करने में सक्षम इंटरनेशनल टर्मिनेशन कॉम्पिटिशन में भाग लेने वाला एकमात्र टूल है। वे नोट करते हैं कि पेयेट (2024) द्वारा एक अन्य दृष्टिकोण मौजूद है जो नॉन-लूपिंगनेस के एक अलग वर्ग को संबोधित करता है और इस पेपर में परीक्षण किए गए विशिष्ट प्रोग्राम्स के नॉन-लूपिंग नॉन-टर्मिनेशन को सिद्ध करने में असमर्थ है। इसके विपरीत, पेयेट (2024) का दृष्टिकोण उन प्रोग्राम्स के टर्मिनेशन को गलत सिद्ध कर सकता है जहाँ यह विधि विफल होती है। इस प्रकार, दोनों दृष्टिकोणों को पूरक (complementary) के रूप में प्रस्तुत किया गया है।

पेपर विनम्रता से समाप्त होता है, यह स्वीकार करते हुए कि यूनिफिकेशन एल्गोरिदम वर्तमान में अपूर्ण है और सरल पैटर्न तक प्रतिबंध इसकी सीमा को सीमित करता है (जैसे, वेरिएबल्स के साथ 1-कॉन्टेक्स्ट वाले प्रोग्राम्स पर विफल होना)। भविष्य के कार्य में पूर्णता (completeness) को संबोधित करना, प्रारंभिक पैटर्न जनरेशन (Prop. 2) का विस्तार करना और एमेस एट अल. (2012) के साथ सीधा तुलना करने के लिए दृष्टिकोण को TRSs के लिए अनुकूलित करना शामिल है।

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