💻 computer science

On Higher-Order Probabilistic Verification via the Weighted Relational Model of Linear Logic

यह शोध पत्र लीनियर लॉजिक के वेटेड रिलेशनल सिमेंटिक्स का उपयोग करते हुए, उनके संबंधित जनरेटिंग फंक्शन्स के बीजगणितीय (algebraic) होने को सिद्ध करके, एफ़ाइन सिस्टम्स का विस्तार करने वाले प्रोबेबिलिस्टिक हायर-ऑर्डर रिकर्सन स्कीम्स (PHORS) के एक वर्ग के लिए 'ऑलमोस्ट शुअर टर्मिनेशन' की निर्णयक्षमता (decidability) स्थापित करता है।

मूल लेखक: Ugo Dal Lago, Guido Fiorillo, Paolo Pistone

प्रकाशित 2026-05-01

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

CC BY 4.0

मूल लेखक: Ugo Dal Lago, Guido Fiorillo, Paolo Pistone

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

मुख्य चित्र: "क्या यह कभी रुकेगा?" की समस्या

कल्पना कीजिए कि आप एक कंप्यूटर प्रोग्राम को चलते हुए देख रहे हैं। यह प्रोग्राम एक 'चूज़-योर-ओन-एडवेंचर' (अपनी पसंद का रास्ता चुनें) किताब जैसा है, लेकिन एक ट्विस्ट के साथ: हर पन्ने पर एक सिक्का उछाला जाता है। चित (Heads) आया, तो आप बाएं जाएंगे; पट (Tails) आया, तो आप दाएं जाएंगे। कुछ रास्ते एक अंत (प्रोग्राम रुक जाता है) की ओर ले जाते हैं, जबकि अन्य आपको अनंत काल तक चक्करों में फंसा सकते हैं।

कंप्यूटर वैज्ञानिक एक बड़ा सवाल पूछते हैं: "क्या यह प्रोग्राम अंततः रुक जाएगा, या यह हमेशा के लिए चलता रहेगा?"

सरल प्रोग्रामों के लिए, हम इसका उत्तर आसानी से दे सकते हैं। लेकिन जटिल, "हायर-ऑर्डर" (higher-order) प्रोग्रामों के लिए (ऐसे प्रोग्राम जो दूसरे प्रोग्रामों को डेटा की तरह पास कर सकते हैं), यह सवाल अविश्वसनीय रूप से कठिन हो जाता है। वास्तव में, इन संभाव्य (probabilistic) प्रोग्रामों के सबसे सामान्य प्रकार के लिए, उत्तर यह है: हम कभी भी निश्चित रूप से नहीं जान सकते। एक ऐसा सार्वभौमिक टूल बनाना गणितीय रूप से असंभव है जो इन सभी प्रोग्रामों की जांच कर सके और आपको बता सके कि क्या वे रुकते हैं।

लेखकों का समाधान: जादुई गणित के साथ गणना करना

इस पेपर के लेखकों, उगो डैलगो, गुइडो फियोरिटो और पाओलो पिस्तोने ने हर प्रोग्राम के लिए उस असंभव समस्या को हल करने की कोशिश नहीं की। इसके बजाय, उन्होंने पूछा: "क्या हम इन प्रोग्रामों का एक विशेष, उपयोगी समूह ढूंढ सकते हैं जहाँ हम यह सिद्ध कर सकें कि वे रुकते हैं?"

उन्होंने इसे एक अलग भाषा में अनुवाद करके करने का तरीका खोजा: बीजीय जनरेटिंग फंक्शन्स (Algebraic Generating Functions)।

उपमा: अनंत रेसिपी बुक (व्यंजन पुस्तिका)

कल्पना कीजिए कि प्रोग्राम एक रेसिपी बुक है। हर बार जब प्रोग्राम कोई निर्णय लेता है (सिक्का उछालना), तो वह एक चरण लिख देता है।

यदि प्रोग्राम 1 चरण के बाद रुकता है, तो वह एक पथ है।
यदि वह 2 चरणों के बाद रुकता है, तो वह दूसरा पथ है।
यदि वह 1,000 चरणों के बाद रुकता है, तो वह एक और पथ है।

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

इस कार्ड को एक जादु적인 कैलकुलेटर की तरह समझें:

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

गुप्त सामग्री: लीनियर लॉजिक और "बाउंडेड" (सीमित) उपयोग

उन्होंने इस जादु적인 कैलकुलेटर का निर्माण कैसे किया? उन्होंने लीनियर लॉजिक (Linear Logic) नामक गणित की एक शाखा से एक उपकरण का उपयोग किया।

सामान्य गणित में, आप एक संख्या का जितनी बार चाहें उतनी बार उपयोग कर सकते हैं। लीनियर लॉजिक में, संसाधन कीमती होते हैं। आपको ठीक से ट्रैक करना होता है कि आपने कितनी बार किसी सामग्री का उपयोग किया है।

समस्या: यदि कोई प्रोग्राम किसी वेरिएबल (सामग्री) का अनंत, अनियंत्रित संख्या में उपयोग करता है, तो गणित अव्यवस्थित हो जाता है और "जादु적인 कैलकुलेटर" टूट जाता है।
समाधान: लेखकों ने "बाउंडेड एक्सपोनेंशियल" (Bounded Exponentials) नामक एक नियम पेश किया।

रूपक: कल्पना कीजिए कि आप एक केक बना रहे हैं।

अनबाउंडेड (असीमित): आपके पास एक जादुई ओवन है जो एक साथ अनंत केक बना सकता है। आप ट्रैक खो देते हैं कि आपने कितने बनाए। गणित विस्फोट कर जाता है।
बाउंडेड (लेखकों का नियम): आपके पास एक नियम है कि "आप इस विशिष्ट सामग्री का अधिकतम 2 बार उपयोग कर सकते हैं," या "अधिकतम 5 बार।" भले ही प्रोग्राम जटिल हो, जब तक वह इन "उपयोग सीमाओं" का सम्मान करता है, गणित व्यवस्थित रहता है।

इन सीमाओं का सम्मान करने के लिए प्रोग्राम को मजबूर करके, लेखकों ने सिद्ध किया कि "जादु적인 कैलकुलेटर" (जनरेटिंग फंक्शन) हमेशा एक पॉलीनोमियल समीकरण (polynomial equation) का परिणाम देता है। यह एक बहुत बड़ी बात है क्योंकि पॉलीनोमियल समीकरणों को हल किया जा सकता है। हमारे पास उन्हें हल करने के ज्ञात, विश्वसनीय तरीके हैं।

उन्होंने वास्तव में क्या हासिल किया?

पेपर तीन मुख्य बातें दावा करता है:

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

निचोड़ (The Bottom Line)

लेखकों ने एक नई कंप्यूटर भाषा का आविष्कार नहीं किया। इसके बजाय, उन्होंने दो दुनियाओं के बीच एक पुल (bridge) बनाया:

संभाव्य हायर-ऑर्डर प्रोग्रामिंग की अस्त-व्यस्त, अप्रत्याशित दुनिया।
बीजगणितीय समीकरणों (algebraic equations) की स्वच्छ, समाधान योग्य दुनिया।

इस पुल का निर्माण करके, उन्होंने यह सिद्ध किया कि इन प्रोग्रामों के एक महत्वपूर्ण और उपयोगी वर्ग के लिए, हम अंततः इस प्रश्न का उत्तर दे सकते हैं कि: "क्या यह रुकेगा?" अनुमान लगाने के बजाय मानक गणितीय उपकरणों का उपयोग करके एक निश्चित "हाँ" या "ना" के साथ। उन्होंने मूल रूप से एक अनसुलझी पहेली को एक समाधान योग्य गणितीय पहेली में बदल दिया।

यहाँ डल लैगो, फियोरिटो और पिस्तोने के शोध पत्र "On Higher-Order Probabilistic Verification via the Weighted Relational Model of Linear Logic" का विस्तृत तकनीकी सारांश दिया गया है।

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

यह शोध पत्र प्रायोरिटी हायर-ऑर्डर रिकर्सन स्कीम्स (PHORS) के लिए अल्मोस्ट श्योर टर्मिनेशन (AST) और पॉजिटिव अल्मोस्ट श्योर टर्मिनेशन (PAST) समस्याओं को संबोधित करता है।

संदर्भ: PHORS, हायर-ऑर्डर रिकर्सन स्कीम्स (HORS) के प्रायabilistic विस्तार हैं, जो फिक्स्डपॉइंट ऑपरेटर और प्रायोरिटी चॉइस वाले सिंपली-टाइप्ड $\lambda$ -कैलकुलस के समकक्ष हैं।
चुनौती: जबकि मानक HORS (ऑर्डर-2 और उससे ऊपर) के लिए टर्मिनेशन (समाप्ति) निर्णायक (decidable) है, PHORS के लिए AST समस्या अनडिसाइडेबल (undecidable) है (विशेष रूप से $\Pi^0_2$ -पूर्ण)।
मौजूदा सीमाएँ: पिछले निर्णायकी परिणाम निम्नलिखित तक सीमित थे:
- ऑर्डर-1 PHORS।
- एफाइन PHORS (PAHORS): वे प्रोग्राम जहाँ वेरिएबल्स का उपयोग अधिकतम एक बार किया जाता है (लीनियर/एफाइन टाइप्स)।
- ये परिणाम काफी हद तक ऑटोमेटा थ्योरी (जैसे, ट्री स्टैक ऑटोमेटा) या गेम सेमेंटिक्स पर निर्भर थे।
लक्ष्य: लेखक PHORS के एक व्यापक वर्ग (एफाइन से परे) की पहचान करने का लक्ष्य रखते हैं जिसके लिए AST और PAST निर्णायक हो सके, जिसमें ऑटोमेटा के बजाय जेनरेटिंग फंक्शन्स और लीनियर लॉजिक पर आधारित एक नवीन दृष्टिकोण का उपयोग किया गया है।

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

मुख्य कार्यप्रणाली में लीनियर लॉजिक के वेटेड रिलेशनल मॉडल का उपयोग करके PHORS के प्रायोरिटी निष्पादन (execution) को फॉर्मल पावर सीरीज़ (जेनरेटिंग फंक्शन्स) की गणना में अनुवादित करना शामिल है।

A. वेटेड रिलेशनल सेमेंटिक्स (Weighted Relational Semantics)

लेखक एक निरंतर सेमिरिंज (विशेष रूप से $\mathbb{R}_{\ge 0}^{\infty}[[z]]$ ) पर वेटेड रिलेशनल मॉडल का उपयोग करते हैं।

व्याख्या (Interpretation): टर्म्स को फॉर्मल पावर सीरीज़ के परिवारों के रूप में व्याख्यायित किया जाता है जहाँ गुणांक (coefficients) प्रायिकता (probabilities) का प्रतिनिधित्व करते हैं।
वेरिएबल $z$ : प्रायोरिटी चॉइस (रिडक्शन स्टेप्स) की संख्या गिनने के लिए एक विशिष्ट वेरिएबल $z$ पेश किया गया है।
प्रायोरिटी चॉइस: ऑपरेशन $M \oplus_p N$ को $p \cdot z \cdot \llbracket M \rrbracket + (1-p) \cdot z \cdot \llbracket N \rrbracket$ के रूप में व्याख्यायित किया जाता है।
जेनरेटिंग फंक्शन: एक PHORS $G$ $G$ के लिए, व्याख्या एक जेनरेटिंग फंक्शन $a_G(z) = \sum_{n=0}^{\infty} P(G \downarrow n) z^n$ $a_{G} (z) = \sum_{n = 0}^{\infty} P (G ↓ n) z^{n}$ प्रदान करती है, जहाँ $P(G \downarrow n)$ $P (G ↓ n)$ वह प्रायिकता है कि $G$ $G$ ठीक $n$ $n$ स्टेप्स में समाप्त होता है।
- AST: यदि $a_G(1) = 1$ है, तो यह निर्णायक है।
- PAST: यदि अपेक्षित स्टेप्स की संख्या $a'_G(1) < \infty$ है, तो यह निर्णायक है।

B. अल्जेब्रिक पावर सीरीज़ और FAS

मुख्य अंतर्दृष्टि यह है कि यदि जेनरेटिंग फंक्शन $a_G(z)$ अल्जेब्रिक है (अर्थात, यह बहुपद समीकरणों के एक सिस्टम को संतुष्ट करता है), तो AST और PAST को एक्सिस्टेंशियल थ्योरी ऑफ द रील्स (ETR) के माध्यम से निर्णायक बनाया जा सकता है।

बाधा: सामान्य PHORS अनंत समीकरण प्रणालियाँ उत्पन्न करते हैं (हायर-ऑर्डर टाइप्स के कारण), जो आवश्यक रूप से अल्जेब्रिक नहीं होते हैं।
समाधान: लेखक भाषा को उन वर्गों तक सीमित करते हैं जहाँ अनंत समीकरण प्रणालियों को एक फाइनाइट अल्जेब्रिक सिस्टम (FAS) में कम किया जा सकता है। यह इनपुट के "उपयोग" (usage) को सीमित करके प्राप्त किया जाता है।

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

1. लीनियर लॉजिक के माध्यम से कॉम्बिनेटरियल लक्षण वर्णन

यह शोध पत्र वेटेड रिलेशनल मॉडल का उपयोग करके PHORS के टर्मिनेशन का पहला कॉम्बिनेटरियल अध्ययन प्रदान करता है। यह एक प्रोग्राम में वेरिएबल्स के उपयोग और उसके जेनरेटिंग फंक्शन की अल्जेब्रिक प्रकृति के बीच सीधा संबंध स्थापित करता है।

2. PBHORS $<\infty$ (फाइनाइटली बाउंडेड PHORS) का परिचय

लेखक एक नया प्रोग्राम वर्ग, PBHORS $<\infty$ , पेश करते हैं, जो एफाइन क्लास (PAHORS) का विस्तार करता है और बाउंडेड नॉन-लिनियैरिटी की अनुमति देता है।

टाइप डिसिप्लिन: यह $!_k A \mult de B$ जैसे ग्रेडेड टाइप्स का उपयोग करता है, जिसका अर्थ है कि एक फंक्शन अपने इनपुट $A$ का अधिकतम $k$ बार उपयोग कर सकता है।
परिणाम: इस वर्ग के किसी भी PHORS के लिए, संबंधित जेनरेटिंग फंक्शन अल्जेब्रिक होता है।
लिनियराइजेशन: लेखक सिद्ध करते हैं कि किसी भी PBHORS $<\infty$ को प्रभावी रूप से एक समकक्ष एफाइन PHORS (PAHORS) में बदला जा सकता है। हालाँकि इस रूपांतरण से आकार में घातीय वृद्धि (exponential blow-up) हो सकती है, लेकिन यह सिद्ध करता है कि यह वर्ग सेमेंटिक रूप से एफाइन मामले के समान है, जिससे इसकी निर्णायकी (decidability) विरासत में मिलती है।

3. PBHORS $^\infty$ (पैरामेट्रिक बाउंडेड PHORS) का परिचय

अधिक जटिल प्रोग्रामों को कैप्चर करने के लिए, लेखक PBHORS $^\infty$ पेश करते हैं, जो अनबाउंडेड उपयोग (अनंत ग्रेड $!_\infty$ ) वाले विशिष्ट पैरामीटर्स की अनुमति देता है।

तंत्र: अनंत ग्रेड वाले वेरिएबल्स को वास्तविक इनपुट के बजाय फॉर्मल पैरामीटर्स के रूप में माना जाता है। जेनरेटिंग फंक्शन इन पैरामीटर्स के ऊपर पावर सीरीज़ के रिंग में गुणांकों वाला एक सीरीज़ बन जाता है।
कंपोजिशनलिटी: यह वर्ग कंपोजिशन के अंतर्गत आता है। लेखक दिखाते हैं कि एक क्लोज्ड PBHORS $^\infty$ को एक पैरामेट्रिक PBHORS $<\infty$ में कम किया जा सकता है।
परिणाम: इस बड़े वर्ग के जेनरेटिंग फंक्शन भी अल्जेब्रिक रहते हैं, जिससे AST और PAST के लिए निर्णायकी बनी रहती है।

4. निर्णायकी प्रमाण (Decidability Proofs)

दोनों PBHORS $<\infty$ और PBHORS $^\infty$ के लिए, यह शोध पत्र सिद्ध करता है कि:

जेनरेटिंग फंक्शन $a_G(z)$ बहुपद समीकरणों के एक परिमित सिस्टम का न्यूनतम समाधान है।
AST यह जाँचकर निर्णायक है कि क्या $z=1$ पर न्यूनतम गैर-ऋणात्मक समाधान 1 के बराबर है।
PAST यह जाँचकर निर्णायक है कि क्या $z=1$ पर समाधान का डेरिवेटिव (derivative) परिमित है।
ये जाँच $z=1$ पर समाधान के पहले-क्रम के सिद्धांत (first-order theory of the reals - Tarski's theorem) की निर्णायकी का उपयोग करके की जाती हैं।

4. मुख्य परिणाम (Key Results)

अल्जेब्रिसिटी: सभी प्रोग्रामों के जेनरेटिंग फंक्शन अल्जेब्रिक पावर सीरीज़ हैं। यह सामान्य PHORS के विपरीत है, जहाँ जेनरेटिंग फंक्शन गैर-अल्जेब्रिक (जैसे, इंडेक्स्ड ग्रामर से संबंधित) हो सकते हैं।
निर्णायकी: विस्तारित वर्गों PBHORS $<\infty$ और PBHORS $^\infty$ के लिए AST और PAST निर्णायक हैं।
जटिलता: एक निश्चित ऑर्डर के लिए, निर्णय प्रक्रिया की समय जटिलता प्रोग्राम के आकार के लिए बहुपद (polynomial) होती है, लेकिन ऑर्डर के साथ यह सुपर-एक्सपोनेंशियल रूप से बढ़ती है (जनित FAS के आकार के कारण)।
सेमिलिनियरिटी (Semilinearity): वे स्टेप काउंट्स जिनके लिए एक प्रोग्राम समाप्त होता है, एक सेमिलिनियर सेट (रैखिक सेटों का संघ) हैं, जो सीरीज़ की अल्जेब्रिक प्रकृति से प्राप्त गुण है।
एफाइन के साथ तुलना: नए वर्ग एफाइन PHORS (PAHORS) का सख्ती से विस्तार करते हैं। उदाहरण के लिए, वे उन प्रोग्रामों को संभाल सकते हैं जहाँ एक फंक्शन का दो बार उपयोग किया जाता है (बाउंडेड नॉन-लिनियैरिटी) या जहाँ पैरामीटर्स को अनिश्चित रूप से डुप्लिकेट किया जाता है (अनंत ग्रेड), बशर्ते कि संरचना टाइप डिसिप्लिन के अनुकूल हो।

5. महत्व और प्रभाव (Significance and Impact)

नया प्रतिमान (New Paradigm): यह शोध पत्र प्रायोरिटी हायर-ऑर्डर प्रोग्रामों के सत्यापन को ऑटोमेटा-थ्योरेटिक विधियों (जो एफाइन टाइप्स के लिए जटिल और विशिष्ट हैं) से अल्जेब्रिक/कॉम्बिनेटरियल विधियों की ओर स्थानांतरित करता है। यह एनालिटिक कॉम्बिनेटरिक्स (जैसे, एसिम्प्टोटिक एनालिसिस, सिंगुलैरिटी एनालिसिस) के उपकरणों को प्रायोरिटी वेरिफिकेशन पर लागू करने का मार्ग प्रशस्त करता है।
एफाइन परिणामों की मजबूती: यह कार्य प्रदर्शित करता है कि एफाइन PHORS (PAHORS) के लिए AST की निर्णायकी एक अलग घटना नहीं है, बल्कि एक व्यापक अल्जेब्रिक संरचना का हिस्सा है। यह दिखाता है कि निर्णायकी की "नाजुकता" (जहाँ मामूली विस्तार इसे तोड़ देते है) को ग्रेडेड टाइप्स के माध्यम से वेरिएबल उपयोग को सावधानीपूर्वक नियंत्रित करके प्रबंधित किया जा सकता है।
मॉड्यूलरिटी: PBHORS $^\infty$ की कंपोजिबिलिटी मॉड्यूलर वेरिफिकेशन की अनुमति देती है, जहाँ घटकों का अलग से पैरामेट्रिक सिस्टम के रूप में विश्लेषण किया जा सकता है और फिर उन्हें संयोजित किया जा सकता है।
खुले प्रश्न: लेखक सुझाव देते हैं कि इस ढांचे को D-फाइनाइट पावर सीरीज़ (रैखिक विभेदक समीकरणों के समाधान) तक विस्तारित किया जा सकता है और यह AST समस्या की अरिथमेटिक पदानुक्रम (arithmetic hierarchy) में सटीक स्थिति को हल करने में मदद कर सकता है।

संक्षेप में, यह शोध पत्र लीनियर लॉजिक, फॉर्मल पावर सीरीज़ और प्रायोरिटी वेरिफिकेशन को सफलतापूर्वक जोड़ता है, जो पहले की तुलना में काफी बड़े वर्ग के हायर-ऑर्डर प्रायोरिटी प्रोग्रामों के लिए टर्मिनेशन निर्धारित करने हेतु एक शक्तिशाली, अल्जेब्रिक ढांचा प्रदान करता है।