💻 computer science

Labelled Process Logic

यह शोधपत्र एक समान चक्रीय लेबल युक्त प्रमाण-सिद्धांतिक ढांचे (uniform cyclic labelled proof-theoretic framework) को प्रस्तुत करता है, जिसमें प्रणालियाँ G3PPL और G3FOPL शामिल हैं, जो सूत्रों को लेबल के साथ समृद्ध करके प्रोपोज़िशनल और फर्स्ट-ऑर्डर प्रोसेस लॉजिक का एक पूर्ण उपचार प्राप्त करता है ताकि व्युत्पत्तियों (derivations) के दौरान ट्रेस और अपडेट जानकारी को स्पष्ट रूप से ट्रैक किया जा सके।

मूल लेखक: Yuanrui Zhang

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

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

CC BY 4.0

मूल लेखक: Yuanrui Zhang

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

कल्पना कीजिए कि आप यह सिद्ध करने की कोशिश कर रहे हैं कि एक रोबोट भूलभुलैया (maze) में चलते समय कभी टकराएगा नहीं।

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

प्रोसेस लॉजिक (Process Logic) एक अपग्रेड है। इसे पूरी यात्रा की परवाह है। यह पूछता है: "क्या रोबोट पूरी यात्रा के दौरान सड़क पर रहा, खाइयों से बचा, और हर एक कदम पर नियमों का पालन किया?" इसे सिद्ध करना बहुत कठिन है क्योंकि आपको रोबोट के पूरे इतिहास को ट्रैक करना पड़ता है, न कि केवल उसके अंतिम पड़ाव को।

युआनरुई झांग (Yuanrui Zhang) का शोध पत्र एक नया, शक्तिशाली टूल पेश करता है जिसे लेबल वाले प्रोसेस लॉजिक (Labelled Process Logic) कहा जाता है। यह इस कठिन गणितीय समस्या को हल करने के लिए काम करता है। यहाँ बताया गया है कि यह कैसे काम करता है, सरल उपमाओं का उपयोग करके:

1. समस्या: "विभाजन" का दुःस्वप्न (The "Splitting" Nightmare)

कल्पना कीजिए कि आप यह सिद्ध करने की कोशिश कर रहे हैं कि एक रोबोट दो सेक्शन (सेक्शन A और सेक्शन B) वाले एक लंबे टनल से सुरक्षित रूप से गुजर सकता है।

पारंपरिक गणितीय प्रमाणों में, पूरी यात्रा को सुरक्षित सिद्ध करने के लिए, आपको अक्सर समस्या को "विभाजित" करना पड़ता है। आप प्रयास करते हैं कि सेक्शन A सुरक्षित है, फिर सेक्शन B सुरक्षित है, और फिर उन दोनों प्रमाणों को जोड़ने (glue) की कोशिश करते हैं।
समस्या यह है कि वह "गोंद" (glue) बहुत उलझा हुआ है। यदि सेक्शन A में रोबमाट का रास्ता सेक्शन B के व्यवहार को बदल देता है, तो गणित अविश्वसनीय रूप से जटिल हो जाता है। मौजूदा उपकरण साधारण टनल को तो संभाल सकते थे, लेकिन जब टनल जटिल हो गई, खुद पर वापस मुड़ गई (loops), या उसमें कई संभावित रास्ते बन गए, तो वे विफल हो गए।

2. समाधान: "बैकपैक" (लेबल्स)

लेखक का बड़ा विचार अंत में टुकड़ों को जोड़ने की कोशिश करना बंद करना है। इसके बजाय, प्रमाण को एक बैकपैक (जिसे "लेबल" कहा जाता है) दें।

यह कैसे काम करता है: जैसे-जैसे प्रमाण रोबोट के निर्देशों के माध्यम से आगे बढ़ता है, यह केवल यह नहीं लिखता कि "क्या यह सुरक्षित है?" बल्कि यह लिखता है "हम स्टेप 5 पर हैं, रोबोट ने बाएँ मुड़ा, और बैटरी 80% पर है।"
जादू: यह "बैकपैक" (लेबल) यात्रा के इतिहास को प्रमाण के अंदर ही लेकर चलता है।
- समस्या को दो कठिन हिस्सों में विभाजित करने के बजाय, प्रमाण बस उस नए स्टेप को बैकपैक में जोड़ देता है।
- यदि रोबोट स्टेप A फिर स्टेप B करता है, तो प्रमाण बस बैकपैक को अपडेट करता है कि इतिहास: स्टेप A + स्टेप B।
- यह गणित को बहुत साफ-सुथरा बनाता है। आपको चीजों को "जोड़ने" के लिए जटिल नियमों की आवश्यकता नहीं है; आप बस जो हुआ उसकी सूची में चीजें जोड़ते जाते हैं।

3. लूप की समस्या: "अनंत गलियारा" (The "Infinite Hallway")

कंप्यूटर और रोबोट अक्सर लूप (loops) का उपयोग करते हैं (जैसे, "तब तक चलते रहो जब तक तुम्हें लाल बत्ती न दिखे")।

यदि आप मानक गणित का उपयोग करके लूप को सिद्ध करने का प्रयास करते हैं, तो आप एक अनंत गलियारे में फंस सकते हैं। आप स्टेप 1 सिद्ध करते हैं, फिर स्टेप 2, फिर स्टेप 3... और चूंकि लूप दोहराता रहता है, आप कभी भी प्रमाण के अंत तक नहीं पहुँच पाते।
चक्रीय समाधान (The Cyclic Fix): लेखक प्रमाण को "अपने आप पर वापस लूप" करने की अनुमति देते हैं। कल्पना कीजिए कि एक प्रमाण जो अपनी ही पूंछ खाते हुए सांप जैसा दिखता है।
- प्रमाण कहता है: "मैं स्टेप 10 पर हूँ। मैं जानता हूँ कि मैं स्टेप 1 पर था। चूंकि नियम समान हैं, इसलिए मैं स्टेप 1 पर वापस जा सकता हूँ और कह सकता हूँ, 'मैंने इस हिस्से की पहले ही जाँच कर ली है, इसलिए मैं ठीक हूँ।'"
- सुरक्षा जाँच: यह सुनिश्चित करने के लिए कि यह कोई धोखाधड़ी नहीं है, लेखक एक नियम जोड़ते हैं: हर बार जब प्रमाण लूप करता है, तो उसे यह सिद्ध करना होगा कि "बैकपैक" (लेबल) एक विशिष्ट, घटते हुए तरीके से बदला है। यह एक खेल की तरह है जहाँ आप केवल तभी लूप कर सकते हैं जब आपके जार में कम कुकीज़ बची हों। अंततः, आप कुकीज़ खत्म कर देते हैं, जिससे यह सिद्ध होता है कि लूप सुरक्षित और सीमित है।

4. टूल के दो संस्करण

शोध पत्र इस प्रणाली के दो संस्करण बनाता है:

G3PPL (सरल संस्करण): यह अमूर्त तर्क पहेलियों (abstract logic puzzles) के लिए काम करता है जहाँ आप केवल "सत्य" (True) या "असत्य" (False) अवस्थाओं की परवाह करते हैं। यह रास्तों को ट्रैक करने के लिए लेबल्स का उपयोग करता है।
G3FOPL (उन्नत संस्करण): यह संख्याओं और वेरिएबल्स (जैसे x = x + 1) वाले वास्तविक दुनिया के गणित के लिए काम करता है। यहाँ, "बैकपैक" केवल पथ को ही नहीं ट्रैक करता; यह अपडेट्स को भी ट्रैक करता है। यदि रोबोट एक संख्या बदलता है, तो लेबल उस बदलाव को स्पष्ट रूप से रिकॉर्ड करता है (जैसे, "x अब 5 है")। यह सिस्टम को उनके भीतर गणित वाले वास्तविक कंप्यूटर प्रोग्रामों को संभालने की अनुमति देता है।

निचोड़ (The Bottom Line)

लेखक का दावा है कि उन्होंने पहला पूर्ण, विश्वसनीय गणितीय ढांचा बनाया है जो जटिल कंप्यूटर प्रोग्रामों (जिसमें लूप और गणित वाले लूप शामिल हैं) के संपूर्ण निष्पादन पथों (execution paths) के बारे में गुण सिद्ध कर सकता है।

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

लेखक यह सिद्ध करते हैं कि यह प्रणाली सत्यनिष्ठ (Sound) है (यह कभी झूठ नहीं बोलती; यदि यह कहता है कि एक प्रोग्राम सुरक्षित है, तो वह वास्तव में सुरक्षित है) और पूर्ण (Complete) है (यह वह सब कुछ सिद्ध कर सकती है जो वास्तव में सत्य है)। यह सुनिश्चित करने की दिशा में एक बड़ा कदम है कि सॉफ्टवेयर पहले सेकंड से लेकर आखिरी सेकंड तक बिल्कुल वैसा ही व्यवहार करे जैसा हम उम्मीद करते हैं।

तकनीकी सारांश: लेबल वाला प्रोसेस लॉजिक (Labelled Process Logic)

1. समस्या विवरण (Problem Statement)

प्रोसेस लॉजिक (PL), डायनेमिक लॉजिक (DL) का विस्तार करता है, जो अंतिम प्रोग्राम अवस्थाओं (final program states) के तर्क करने के बजाय संपूर्ण निष्पादन ट्रेस (execution traces) पर तर्क करने पर ध्यान केंद्रित करता है। जबकि प्रपोजिशनल प्रोसेस लॉजिक (PPL) का प्रपोजिशनल सिद्धांत, निर्णय क्षमता (decidability) और पूर्णता (completeness) के संबंध में अच्छी तरह से समझा गया है, फर्स्ट-ऑर्डर एक्सटेंशन (FOPL) महत्वपूर्ण चुनौतियाँ प्रस्तुत करता है।

मुख्य कठिनाई रेगुलर प्रोग्राम्स पर फर्स्ट-ऑर्डर प्रोसेस लॉजिक के लिए आवश्यक कंपोजिशनल रीजनिंग (compositional reasoning) में निहित है। मानक डायनेमिक लॉजिक में, $[\alpha]\phi$ यह दावा करता है कि $\alpha$ का प्रत्येक टर्मिनेटिंग निष्पादन एक ऐसी अवस्था में समाप्त होता है जो $\phi$ को संतुष्ट करती है। प्रोसेस लॉजिक में, $[\alpha]\pi$ यह दावा करता है कि $\alpha$ का प्रत्येक निष्पादन ट्रेस एक टेम्पोरल प्रॉपर्टी $\pi$ (जो next, always, eventually, और until जैसे लिनियर टेम्पोरल लॉजिक ऑपरेटर्स के माध्यम से व्यक्त की जाती है) को संतुष्ट करता है।

मौजूदा कंपोजिशनल कैलकुली (compositional calculi) जो इस लॉजिक के अंशों (fragments) के लिए हैं (जैसे, डिटर्मिनिस्टिक व्हाइल प्रोग्राम्स के लिए बेकर्ट का सीक्वेंट कैलकुलस, या DLT और DTL जैसे एक्सटेंशन), रेगुलर (संभावित रूप से नॉन-डिटरमिनिस्टिक) प्रोग्राम्स के लिए पूर्ण फर्स्ट-ऑर्डर प्रोसेस लॉजिक के लिए पूर्ण उपचार प्रदान करने में विफल रहते हैं:

अनुक्रमिक प्रोग्राम्स (sequential programs) के लिए कंपोजिशनल नियम (जैसे, एक अनुक्रमिक ट्रेस प्रॉपर्टी $\pi$ को $\alpha; \beta$ में विभाजित करना) अक्सर टेम्पोरल फॉर्मूला के विशिष्ट आकार (जैसे, "always" बनाम "eventually" के लिए विशिष्ट नियम) पर बहुत अधिक निर्भर करते हैं।
कुछ प्रस्तावित नियम रेगुलर प्रोग्राम्स के लिए अपर्याप्त हैं क्योंकि अनुक्रमिक कंपोजिशन में 'टेस्ट' ट्रेस को ब्लॉक कर सकते हैं, जिससे सरल कंपोजिशनल स्प्लिट अमान्य हो जाते हैं।
कोई भी मौजूदा सिस्टम ऐसा यूनिफॉर्म फ्रेमवर्क नहीं देता जहाँ ट्रेस-आधारित प्रॉपर्टीज और फर्स्ट-ऑर्डर कंप्यूटेशन्स को एक ही प्रूफ स्ट्रक्चर के भीतर संभाला जा सके।

2. कार्यप्रणाली: साइक्लिक लेबल वाला प्रूफ सिस्टम (Cyclic Labelled Proof Systems)

यह शोध पत्र एक नवीन प्रूफ-थ्योरेटिकल फ्रेमवर्क प्रस्तावित करता है जो बढ़ते हुए जटिल कंपोजिशनल नियमों पर निर्भर रहने के बजाय, निष्पादन जानकारी को स्पष्ट रूप से रिकॉर्ड करने के लिए प्रोसेस लॉजिक फॉर्मूला को लेबल्स (labels) से समृद्ध करता है।

2.1 लेबल वाले फॉर्मूला (Labelled Formulas)

लेखक $\sigma : \phi$ के रूप में लेबल वाले फॉर्मूला पेश करते हैं, जहाँ:

$\phi$ एक प्रोसेस लॉजिक फॉर्मूला है।
$\sigma$ $σ$ एक लेबल है जो अब तक संचित निष्पादन ट्रेस या प्रोग्राम कॉन्फ़िगरेशन का प्रतिनिधित्व करता है।
- प्रपोजिशनल प्रोसेस लॉजिक (PPL) में, लेबल्स वर्ल्ड ट्रेसेस ( $\sigma \in L$ ) के होते हैं, जो वर्ल्ड वेरिएबल्स, ट्रेस वेरिएबल्स और कॉनकेटेनेशन (concatenation) से निर्मित होते हैं।
- फर्स्ट-ऑर्डर प्रोसेस लॉजिक (FOPL) में, लेबल्स को असाइनमेंट्स (जैसे, $\{u := e\}$ ) के संचयी प्रभाव को रिकॉर्ड करने के लिए प्रोग्राम अपडेट्स ( $U$ ) के साथ समृद्ध किया जाता है।

यह दृष्टिकोण मध्यवर्ती निष्पादन जानकारी को प्रूफ सिस्टम के भीतर उपलब्ध कराता है। फलस्वरूप, प्रूफ सिस्टम को अनुक्रम के बिंदु पर विशेष-उद्देश्य वाले टेम्पोरल नियमों का उपयोग करके अनुक्रमिक ट्रेस को विभाजित करने की आवश्यकता नहीं होती है; इसके बजाय, यह लेबल में जानकारी को संचित करते हुए प्रोग्राम स्ट्रक्चर को अनफोल्ड करता है।

2.2 साइक्लिक प्रूफ स्ट्रक्चर (Cyclic Proof Structure)

चूंकि रेगुलर प्रोग्राम्स में इटरेशन ( $\alpha^*$ ) शामिल होता है, इसलिए प्रूफ सर्च अनंत डेरिवेशंस उत्पन्न कर सकता है। इसे संभालने के लिए, लेखक साइक्लिक प्रूफ थ्योरी को अपनाते हैं।

प्रीप्रूफ्स (Preproofs): परिमित वृक्ष (finite trees) जहाँ लीफ नोड्स (buds) समान सिंटैक्टिक फॉर्म (वेरिएबल रीनेमिंग के मॉड्यूलो) वाले पूर्वज नोड्स (ancestor nodes) से "बैक-लिंक" कर सकते हैं।
साइक्लिक कंडीशन (Cyclic Condition): साउंडनेस सुनिश्चित करने के लिए, सभी साइकल वैध नहीं होते हैं। पेपर एक प्रोग्रेसिव डेरिवेशन ट्रेस (progressive derivation trace) को परिभाषित करता है। एक डेरिवेशन एक वैध साइक्लिक प्रूफ है यदि प्रत्येक अनंत पथ में एक "प्रोग्रेसिव स्टेप" (जैसे, एक ऐसा नियम लागू करना जो ट्रेस या फॉर्मूला की जटिलता को कम करता है) शामिल हो।
साउंडनेस मैकेनिज्म (Soundness Mechanism): लेखक साउंडनेस को यह दिखाकर सिद्ध करते हैं कि प्रत्येक प्रोग्रेसिव अनंत डेरिवेशन पाथ, "न्यूनतम काउंटर-एग्जांपल ट्रेसेस" के एक वेल-फाउंडेड मल्टीसेट ऑर्डरिंग (well-founded multiset ordering) में एक अनंत पतन (infinite descent) को प्रेरित करता है। यह विरोधाभास सुनिश्चित करता है कि कोई भी अमान्य फॉर्मूला सिद्ध नहीं किया जा सकता।

2.3 प्रूफ सिस्टम (The Proof Systems)

दो विशिष्ट सिस्टम परिभाषित किए गए हैं:

G3PPL: प्रपोजिशनल प्रोसेस लॉजिक के लिए एक साइक्लिक लेबल वाला प्रूफ सिस्टम। यह लेबल वाले सीक्वेंट तकनीकों को मोडल लॉजिक के लिए विस्तारित करता है, उन्हें ट्रेस सिमेंटिक्स के अनुकूल बनाता है।
G3FOPL: फर्स्ट-ऑर्डर प्रोसेस लॉजिक के लिए एक साइक्लिक लेबल वाला प्रूफ सिस्टम। यह असाइनमेंट्स के लिए नियम (लेबल को अपडेट करना) जोड़कर और मानक फर्स्ट-ऑर्डर क्वांटिफायर नियमों को शामिल करके G3PPL का विस्तार करता है।

3. मुख्य योगदान (Key Contributions)

यह शोध पत्र निम्नलिखित विशिष्ट योगदान देता है:

लेबल वाले फॉर्मूला: PPL के लिए ट्रेस लेबल्स और FOPL के लिए अपडेट-आधारित लेबल्स का परिचय, जिससे प्रूफ स्ट्रक्चर के भीतर निष्पादन इतिहास को ट्रैक करना संभव होता है।
साइक्लिक लेबल वाले सिस्टम: G3PPL और G3FOPL की परिभाषा, जो एक सामान्य लेबल फ्रेमवर्क साझा करते हैं लेकिन क्रमशः प्रपोजिशनल और फर्स्ट-ऑर्डर प्रोसेस लॉजिक के लिए विशिष्ट नियमों का उपयोग करते हैं।
साउंडनेस प्रूफ: दोनों सिस्टम के लिए साउंडनेस का प्रमाण। तर्क एक वेल-फाउंडेड मल्टीसेट ऑर्डरिंग के न्यूनतम काउंटर-एग्जांपल ट्रेसेस में प्रत्येक प्रोग्रेसिव अनंत डेरिवेशन पाथ को कम करने पर आधारित है।
पूर्णता प्रमाण (Completeness Proofs):
- G3PPL के लिए, पूर्णता यह प्रदर्शित करके स्थापित की जाती है कि लेबल वाला सिस्टम PPL के लिए स्थापित हिल्बर्ट-शैली के प्रूफ सिस्टम के प्रत्येक एक्सिओम और नियम को व्युत्पन्न कर सकता है।
- G3FOPL के लिए, पूर्णता को अरिथमेटिकल एनकोडिंग का उपयोग करते हुए, फर्स्ट-ऑर्डर डायनेमिक लॉजिक (FODL) के क्लासिकल पूर्णता तर्क को ट्रेस-आधारित सेटिंग में अनुकूलित करके स्थापित किया जाता है।

4. परिणाम (Results)

यूनिफॉर्म फ्रेमवर्क: पेपर सफलतापूर्वक एक यूनिफॉर्म फ्रेमवर्क का निर्माण करता है जहाँ ट्रेस-आधारित प्रोग्राम प्रॉपर्टीज और फर्स्ट-ऑर्डर कंप्यूटेशन्स को एक ही प्रूफ स्ट्रक्चर के भीतर संभाला जाता है।
रेगुलर प्रोग्राम्स के लिए पूर्णता: ये सिस्टम फुल फर्स्ट-ऑर्डर प्रोसेस लॉजिक (नॉन-डिटरमिनिस्टिक चॉइस और इटरेशन सहित रेगुलर प्रोग्राम्स के लिए) के लिए पहला पूर्ण तार्किक फ्रेमवर्क प्रदान करते हैं।
साउंडनेस और पूर्णता: G3PPL और G3FOPL दोनों को उनके संबंधित सिमेंटिक्स के संबंध में साउंड और कंप्लीट सिद्ध किया गया है।

5. महत्व (Significance)

पेपर का दावा है कि यह कार्य साहित्य में एक लंबे समय से चली आ रही कमी को दूर करता है। पिछले सिस्टम या तो:

डिटर्मिनिस्टिक प्रोग्राम्स तक सीमित थे (जैसे, DLT, DTL)।
सामान्य रेगुलर प्रोग्राम्स के लिए पूर्णता का अभाव था।
नॉन-डिटरमिनिज्म की उपस्थिति में सभी LTL ऑपरेटर्स (जैसे, until) को यूनिफॉर्म रूप से संभालने में सक्षम नहीं थे।

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