💻 computer science

On A Parameterized Theory of Dynamic Logic for Operationally-based Programs

यह शोध पत्र DLp को प्रस्तुत करता है, जो एक नवीन, पैरामीट्रिक डायनेमिक लॉजिक फ्रेमवर्क है जो किसी प्रोग्राम के ऑपरेशनल सिमेंटिक्स पर सीधे आधारित मॉडल-स्वतंत्र इन्फरेंस नियमों को प्रदान करके प्रोग्राम वेरिफिकेशन को सरल बनाता है, जो चक्रीय तर्क (cyclic reasoning) और मौजूदा सिद्धांतों के साथ अनुकूलता दोनों का समर्थन करता है।

मूल लेखक: Yuanrui Zhang

प्रकाशित 2026-02-11

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

CC BY 4.0

मूल लेखक: Yuanrui Zhang

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

कल्पना कीजिए कि आप एक रोबोट को एक जटिल और निरंतर बदलते हुए बाधा पथ (obstacle course) में नेविगेट करना सिखाने की कोशिश कर रहे हैं।

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

यह शोध पत्र एक नई निर्देश पुस्तिका पेश करता है जिसे $\text{DL}_{\mathfrak{p}}$ कहा जाता है। यहाँ बताया गया है कि यह कुछ सरल उपमाओं का उपयोग करके कैसे काम करता है।

1. "लाइव ट्रैफिक वाला जीपीएस" (ऑपरेशनल सिमेंटिक्स)

पारंपरिक तर्क एक मुद्रित मानचित्र (printed map) की तरह है: यह आपको बताता है कि आप कहाँ से शुरू करते हैं और कहाँ पहुँचते हैं, लेकिन इसे बीच में आपके द्वारा लिए गए मोड़ों की परवाह नहीं होती। यदि सड़क बदल जाती है, तो मानचित्र बेकार हो जाता है।

$\text{DL}_{\mathfrak{p}}$ लाइव जीपीएस वाले गूगल मैप्स की तरह है: यह केवल गंतव्य को नहीं देखता; यह वास्तव में उन "मोड़ों" (ऑपरेशनल सिमेंटिक्स) का अनुसरण करता है जो प्रोग्राम चरण-दर-चरण लेता है। क्योंकि यह वास्तविक गति का अनुसरण करता है, इसलिए आपको हर बार रोबोट बदलने पर मैनुअल को फिर से डिजाइन करने की आवश्यकता नहीं है, आप बस नए "टर्न-बाय-टर्न" निर्देश प्लग इन कर सकते हैं।

2. "स्टिकी नोट" प्रणाली (लेबलिंग और पैरामीट्राइजेशन)

पुराने सिस्टम में, यदि आप किसी वेरिएबल (जैसे रोबोट के बैटरी स्तर) को ट्रैक करना चाहते थे, तो आपको उस जानकारी को तर्क के आधार में ही समाहित करना पड़ता था। यह ऐसा था जैसे आप एक ऐसी किताब लिखने की कोशिश कर रहे हों जिसका हर पन्ना एक विशिष्ट तापमान से स्थायी रूप से चिपका हुआ हो।

$\text{DL}_{\mathfrak{p}}$ "स्टिकी नोट्स" (Labels) का उपयोग करता है। पूरी किताब को बदलने के बजाय, आप बस एक पन्ने पर एक स्टिकी नोट चिपका देते हैं जिस पर लिखा होता है, "वर्तमान बैटरी: 80%"। जैसे-जैसे रोबोट आगे बढ़ता है, आप पुराने नोट को हटा देते हैं और नया नोट चिपका देते हैं: "वर्तमान बैटरी: 75%"। यह तर्क को "पैरामीटराइज्ड" बनाता है—अर्थात, मूल नियम समान रहते हैं, और आप जो कुछ भी ट्रैक कर रहे हैं उसके आधार पर बस स्टिकी नोट्स को बदलते रहते हैं।

3. "अनंत लूप" की समस्या (साइक्लिक रीजनिंग)

एक रोबोट की कल्पना करें जिसे हमेशा के लिए एक घेरे में चलने का कार्य दिया गया है। एक पारंपरिक तर्क पुस्तिका यह सिद्ध करने में अनंत लूप में फंस जाएगी कि क्या होता है, क्योंकि वह एक ऐसे "अंतिम गंतव्य" तक पहुँचने की कोशिश करती रहती है जो कभी आता ही नहीं। यह एक गणितज्ञ की तरह है जो अनंत तक गिनने की कोशिश कर रहा है—वे कभी भी प्रमाण पूरा नहीं कर पाएंगे।

$\text{DL}_{\mathfrak{p}}$ "साइक्लिक रीजनिंग" का उपयोग करता है। अनंत तक गिनने के बजाय, मैनुअल कहता है: "रुको, मैंने पहले भी ठीक यही स्थिति देखी है! मैं उसी स्थान पर वापस आ गया हूँ और मेरे पास वही स्टिकी नोट है। चूंकि मुझे पता है कि पिछली बार यहाँ क्या हुआ था, इसलिए मैं निष्कर्ष निकाल सकता हूँ कि पैटर्न सुरक्षित रूप से जारी रहेगा।" यह "लूप" को पहचान लेता है और किताब को बंद कर देता है, बजाय इसके कि वह इसमें खो जाए।

सारांश: यह क्यों मायने रखता है?

वास्तविक दुनिया में, सॉफ्टवेयर अविश्वसनीय रूप से जटिल होता जा रहा है—ब्लॉकचेन, क्वांटम कंप्यूटर, या सेल्फ-ड्राइविंग कारों के बारे में सोचें। ये सिस्टम सरल "शुरू-से-अंत" वाले रास्तों का पालन नहीं करते; वे प्रतिक्रिया देते हैं, लूप बनाते हैं और लगातार बदलते रहते हैं।

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

तकनीकी सारांश: ऑपरेशनल-आधारित प्रोग्रामों के लिए एक पैरामीटराइज्ड डायनेमिक लॉजिक पर

1. समस्या विवरण

पारंपरिक प्रोग्राम वेरिफिकेशन फ्रेमवर्क, जैसे कि होअर लॉजिक (Hoare logic) और मानक डायनेमिक लॉजिक (DL), मुख्य रूप से डेनोटेशनल सिमेंटिक्स (denotational semantics) पर आधारित हैं। इन मॉडलों में, एक प्रोग्राम के व्यवहार की व्याख्या एक गणितीय वस्तु (जैसे कि ट्रेसेस का एक सेट) के रूप में की जाती है। हालांकि यह शक्तिशाली है, लेकिन यह दृष्टिकोण कई चुनौतियाँ पेश करता है:

अनुकूलन में कठिनाई (Adaptation Difficulty): मौजूदा लॉजिक्स को नए या जटिल प्रोग्रामिंग भाषाओं (जैसे जावा या C) के अनुकूल बनाने के लिए नए एक्सिओमैटिक नियमों (axiomatic rules) के एक विशाल सेट को डिजाइन और मान्य करने की आवश्यकता होती है, जो त्रुटिपूर्ण और खर्चीला है।
रूपांतरण ओवरहेड (Transformation Overhead): मानक नियमों को लागू करने के लिए, प्रोग्रामों को अक्सर "मानक रूपों" (जैसे सिंक्रोनस प्रोग्रामों को STA प्रोग्रामों में बदलना) में रूपांतरित करना पड़ता है, जिससे प्रोग्राम की जानकारी का नुकसान हो सकता है।
सिमेंटिक्स की जटिलता (Complexity of Semantics): आधुनिक या समवर्ती (concurrent) मॉडलों के लिए, ऑपरेशनल सिमेंट्स (कैसे एक प्रोग्राम चरण-दर-चरण संक्रमण करता है) अक्सर डेनोटेशनल सिमेंटिक्स की तुलना में अधिक आसानी से उपलब्ध और विश्वसनीय होता है।

2. कार्यप्रणाली (Methodology)

लेखक $\text{DL}_{\mathfrak{p}}$ का प्रस्ताव करते हैं, जो एक नवीन, पैरामीटराइज्ड डायनेमिक लॉजिक है जिसे सीधे प्रोग्राम के स्ट्रक्चरल ऑपरेशनल सिमेंटिक्स का उपयोग करके तर्क करने के लिए डिज़ाइन किया गया है। यह कार्यप्रणाली तीन मुख्य स्तंभों पर आधारित है:

लेबलिंग और पैरामीटराइजेशन (Labeling and Parameterization): $\text{DL}_{\mathfrak{p}}$ सिम्बॉलिक एक्जीक्यूशन के दौरान स्पष्ट प्रोग्राम कॉन्फ़िगरेशन (जैसे वर्तमान वेरिएबल मान, हीप स्टेट्स, या सब्स्टिट्यूशन) को कैप्चर करने के लिए "लेबल्स" ( $\sigma$ ) पेश करता है। एक फॉर्मूला को $\sigma: [\alpha]\phi$ के रूप में दर्शाया जाता है, जिसका अर्थ है "कॉन्फ़िगरेशन $\sigma$ के तहत, प्रोग्राम $\alpha$ के निष्पादन के बाद, फॉर्मूला $\phi$ सत्य है।" यह लॉजिक को मॉडल-स्वतंत्र बनाता है; फ्रेमवर्क समान रहता है जबकि प्रोग्राम मॉडल ( $\alpha$ ) और लॉजिकल फॉर्मूला ( $\phi$ ) को पैरामीटर के रूप में माना जाता है।
चक्रीय प्रमाण प्रणाली (Cyclic Proof System): रिकर्सिव प्रोग्रामों और अनंत सिम्बॉलिक एक्जीक्यूशन (जैसे while लूप) को संभालने के लिए, पेपर एक चक्रीय प्रमाण दृष्टिकोण (cyclic proof approach) का उपयोग करता है। परिमित प्रूफ ट्री (finite proof trees) की आवश्यकता के बजाय, $\text{DL}_{\mathfrak{p}}$ "बड्स" (non-terminating leaf nodes) की अनुमति देता है जो अपने पूर्वजों (ancestors) से वापस जुड़ते हैं। लेखक यह सुनिश्चित करने के लिए कि ये चक्र तार्किक रूप से सुसंगत हैं और अमान्य अनंत लूप का प्रतिनिधित्व नहीं करते हैं, एक "प्रोग्रेसिव डेरिवेशन ट्रेस" (progressive derivation trace) पेश करते हैं।
लिफ्टिंग प्रक्रिया (Lifting Process): मौजूदा सिद्धांतों (जैसे फर्स्ट-ऑर्डर डायनेमिक लॉजिक - FODL) के साथ संगतता सुनिश्चित करने के लिए, लेखक एक "लिफ्टिंग" तकनीक विकसित करते हैं। यह उन्हें "फ्री लेबल्स" को संलग्न करके मौजूदा, डोमेन-विशिष्ट इन्फरेंस नियमों को $\text{DL}_{\mathfrak{p}}$ फ्रेमवर्क में एम्बेड करने की अनुमति देता है, जिससे विशेष नियमों की दक्षता को नए फ्रेमवर्क की व्यापकता के साथ जोड़ा जा सके।

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

एक नया लॉजिकल फ्रेमवर्क: एक नवीन "प्रोग्राम-लेबल वाले क्रिपके स्ट्रक्चर" (program-labeled Kripke structure) का उपयोग करके $\text{DL}_{\mathfrak{p}}$ के सिंटैक्स और सिमेंटिक्स को परिभाषित किया गया।
एक लेबल किया गया प्रूफ सिस्टम ( $Pr_{\text{dlp}}$ ): एक कर्नेल सेट ऑफ इन्फरेंस रूल्स विकसित किया गया जो विशिष्ट प्रोग्राम संरचनाओं से स्वतंत्र है, बल्कि नियमों के एक पैरामीटर ( $\text{Prop}$ ) पर निर्भर करता है जो प्रोग्राम के ट्रांजिशन का वर्णन करता है।
चक्रीय तर्क तंत्र (Cyclic Reasoning Mechanism): एक विशेष चक्रीय व्युत्पत्ति दृष्टिकोण प्रस्तावित किया गया जो बिना किसी पूर्व प्रोग्राम रूपांतरण के रिकर्सिव प्रोग्रामों के लिए वृद्धिशील तर्क (incremental reasoning) को सक्षम बनाता है।
लॉजिक का औपचारिक सत्यापन (Formal Verification of the Logic): विशिष्ट स्थितियों (Termination Finiteness और Well-behaved Loop Programs) के तहत $\text{DL}_{\mathfrak{p}}$ सिस्टम की सत्यता (soundness) और पूर्णता (completeness) के लिए गणितीय प्रमाण प्रदान किए।

4. परिणाम और केस स्टडीज

पेपर $\text{DL}_{\mathfrak{p}}$ की बहुमुखी प्रतिभा को कई इंस्टेंशिएशन के माध्यम से प्रदर्शित करता है:

$\text{DL}_{\mathfrak{p}}\text{-WP}$ : "While प्रोग्रामों" के गुणों को चक्रीय प्रमाणों का उपयोग करके सफलतापूर्वक निकाला गया, जो दिखाता है कि कैसे लूप संरचना स्वाभाविक रूप से व्युत्पत्ति (derivation) में प्रतिबिंबित होती है।
$\text{DL}_{\mathfrak{p}}\text{-FODL}$ : पारंपरिक फर्स्ट-ऑर्डर नियमों को एम्बेड और लिफ्ट करने की क्षमता प्रदर्शित की, जो स्थापित लॉजिक्स के साथ फ्रेमवर्क की संगतता को सिद्ध करता है।
$\text{DL}_{\mathfrak{p}}\text{-PL}$ (प्रोसेस लॉजिक): दिखाया कि अधिक जटिल लेबल्स (कॉन्फ़िगरेशन के अनुक्रम) और टेम्पोरल फॉर्मूला का उपयोग करके, $\text{DL}_{\mathfrak{p}}$ रिएक्टिव सिस्टम्स और उन गुणों के बारे में तर्क कर सकता है जो केवल समाप्ति (termination) पर ही नहीं, बल्कि निष्पादन के दौरान भी बने रहते हैं।
विषमता (Heterogeneity): प्रदर्शित किया कि विभिन्न प्रोग्राम मॉडल (जैसे रेगुलर प्रोग्राम बनाम while प्रोग्राम) को एक ही फ्रेमवर्क के भीतर तुलना किया जा सकता है।

5. महत्व

यह कार्य महत्वपूर्ण है क्योंकि यह प्रोग्राम वेरिफिकेशन के बोझ को लॉजिक नियमों को फिर से डिजाइन करने से हटाकर ऑपरेशनल ट्रांजिशन्स प्रदान करने पर स्थानांतरित कर देता है। डेवलपर्स द्वारा भाषाओं को परिभाषित करने के लिए पहले से उपयोग किए जाने वाले ऑपरेशनल सिमेंटिक्स का लाभ उठाकर, $\text{DL}_{\mathfrak{p}}$ विविध सॉफ्टवेयर मॉडलों—मानक इम्पैरेटिव कोड से लेकर जटिल सिंक्रोनस और रिएक्टिव सिस्टम तक—को सत्यापित करने के लिए एक अधिक सीधा, लचीला और स्केलेबल मार्ग प्रदान करता है। यह उच्च-स्तरीय तार्किक तर्क (high-level logical reasoning) और निम्न-स्तरीय ऑपरेशनल निष्पादन (low-level operational execution) के बीच के अंतर को पाटता है।