💻 computer science

Uniform Lyndon Interpolation via Non-wellfounded Proofs

यह शोधपत्र नॉन-वेलफाउंडेड (non-wellfounded) प्रूफ़ थ्योरी को लागू करते हुए प्रूवेबिलिटी लॉजिक GLS के लिए पूर्व में खुली यूनिफॉर्म लिंडन इंटरपोलेशन (uniform Lyndon interpolation) की विशेषता को स्थापित करता है, साथ ही एक वैकल्पिक कट एलिमिनेशन (cut elimination) प्रमाण प्रदान करता है और अन्य प्रूवेबिलिटी लॉजिक्स के अनुकूल एक कार्यप्रणाली की रूपरेखा प्रस्तुत करता है।

मूल लेखक: Borja Sierra Miranda (University of Bern), Thomas Studer (University of Bern)

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

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

CC BY 4.0

मूल लेखक: Borja Sierra Miranda (University of Bern), Thomas Studer (University of Bern)

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

कल्पना कीजिए कि आप एक जासूस हैं जो एक जटिल रहस्य को सुलझाने की कोशिश कर रहे हैं। आपके पास सुरागों की एक विशाल फ़ाइल (एक तार्किक तर्क) है, और आपको उस विशिष्ट साक्ष्य को खोजना है जो अपराध की व्याख्या कर सके बिना किसी ऐसे रहस्य को उजागर किए जिसे आपको नहीं बताना चाहिए।

यह शोधपत्र इस बारे में है कि जासूसों (तर्कशास्त्रियों) के लिए उस विशिष्ट साक्ष्य को खोजने का एक नया, शक्तिशाली तरीका क्या है। लेखक, बोर्जा सिएरा मिरांडा और थॉमस स्टुडर, प्रूवेबिलिटी लॉजिक (Provability Logic) के क्षेत्र में काम कर रहे हैं, जो अनिवार्य रूप से इस बात का अध्ययन है कि हम यह कैसे सिद्ध कर सकते हैं कि कुछ चीज़ सिद्ध करने योग्य है।

यहाँ उनके कार्य का सरल उपमाओं (analogies) का उपयोग करके विवरण दिया गया है:

1. समस्या: "डायगोनल" (विकर्ण) जाल

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

इसे एक गलियारे में रखे जादुई दर्पण की तरह समझें। जब आप इसमें देखते हैं, तो इसका प्रतिबिंब आपकी छवि को उलट देता है। तर्कशास्त्र में, यह दर्पण एक चर (variable) की "पोलैरिटी" (ध्रुवीयता) को उलट देता है (एक "सकारात्मक" सुराग को "नकारात्मक" में, या इसके विपरीत)। यदि आप एक ऐसा सुराग खोजने की कोशिश कर रहे हैं जिसे सकारात्मक ही रहना चाहिए, तो यह दर्पण आपकी खोज को बिगाड़ देता है। लंबे समय तक, तर्कशास्त्रियों को पता था कि दर्पण की चिंता किए बिना साक्ष्य कैसे खोजा जाए, लेकिन उन्हें यह नहीं पता था कि वह साक्ष्य कैसे खोजा जाए जो दर्पण के नियमों का सम्मान करता हो (सकारात्मक चीजों को सकारात्मक और नकारात्मक चीजों को नकारात्मक बनाए रखना)। इसे यूनिफॉर्म लिंडन इंटरपोलेशन (Uniform Lyndon Interpolation) कहा जाता है।

2. नया उपकरण: नॉन-वेलफाउंडेड प्रूफ (Non-Wellfounded Proofs)

लेखक एक नया उपकरण पेश करते हैं जिसे नॉन-वेलफाउंडेड प्रूफ कहा जाता है।

पुराना तरीका (वेलफाउंडेड): ब्लॉक का एक टॉवर बनाने की कल्पना करें। आप नीचे से शुरू करते हैं, एक ब्लॉक रखते हैं, फिर उसके ऊपर दूसरा, और ऊपर की ओर बढ़ते रहते हैं जब तक कि आप शीर्ष तक न पहुँच जाएँ। आप कभी भी एक ब्लॉक को अपने ऊपर खुद पर नहीं रख सकते। यह एक मानक, परिमित (finite) प्रमाण है।
नया तरीका (नॉन-वेलफाउंडेड): एक ऐसे टॉवर की कल्पना करें जिसमें एक लूप (loop) होने की अनुमति है। आप एक ब्लॉक बना सकते हैं, कुछ स्तर ऊपर जा सकते हैं, और फिर एक रस्सी जोड़ सकते हैं जो वापस नीचे एक ऐसे ब्लॉक से जुड़ती है जिसे आपने पहले ही रख दिया था। यह एक "वृत्ताकार" (circular) टॉवर है।

तर्कशास्त्र की दुनिया में, ये वृत्ताकार टॉवर अविश्वसनीय रूप से उपयोगी हैं क्योंकि वे जासूस को "डायगोनल मिरर" के जाल से बचने में मदद करते हैं। लूप यह सुनिश्चित करता है कि तर्क का प्रवाह सुरागों की "पोलैरिटी" (सकारात्मक/नकारात्मक प्रकृति) को बनाए रखे, जो पुराने सीधे टॉवर नहीं कर सके।

3. सफलता: GLS का रहस्य सुलझाना

यह विशेष तर्क जिसका वे अध्ययन कर रहे हैं, उसे GLS कहा जाता है।

क्या ज्ञात था: लोग पहले से जानते थे कि GLS में साक्ष्य खोजा जा सकता है (यूनिफॉर्म इंटरपोलेशन)।
क्या अज्ञात था: कोई नहीं जानता था कि क्या आप पोलैरिटी नियमों का सम्मान करते हुए साक्ष्य खोज सकते हैं (यूनिफॉर्म लिंडन इंटरपोलेशन)। यह एक खुला प्रश्न था: "क्या GLS के पास एक ऐसा समाधान है जो सुरागों को उनकी उचित दिशा में रखता है?"

लेखकों की उपलब्धि:
उन्होंने अपने "वृत्ताकार टॉवर" पद्धति का उपयोग करके यह सिद्ध किया कि हाँ, GLS के पास यह विशेष समाधान है। उन्होंने केवल समाधान ही नहीं खोजा; बल्कि उन्होंने एक मशीन (नियमों का एक सेट) बनाई जो इसे स्वचालित रूप से उत्पन्न करती है।

4. उन्होंने यह कैसे किया: "इक्वेशन" (समीकरण) मशीन

इसे काम करने के योग्य बनाने के लिए, उन्होंने कुछ नई अवधारणाएँ विकसित कीं:

लिंडन फिक्स्पॉइंट्स (Lyndon Fixpoints): इसे एक "स्व-संदर्भित रेसिपी" के रूप में समझें। यह एक ऐसा फॉर्मूला है जिसे जब आप स्वयं में डालते हैं, तो यह वही परिणाम देता है। यह केक बनाने की एक ऐसी रेसिपी की तरह है जो, जब आप इसे पकाते हैं, तो यह ठीक वही बताती है कि अगली बार केक को पूरी तरह से कैसे बनाना है।
लिंडन इक्वेशनल सिस्टम्स (Lyndon Equational Systems): उन्होंने समीकरणों की एक प्रणाली स्थापित की जहाँ चर (variables) सुरागों का प्रतिनिधित्व करते हैं। क्योंकि उन्होंने "वृत्ताकार टॉवर" पद्धति का उपयोग किया था, इसलिए वे इन समीकरणों को हल कर सके और यह भी सुनिश्चित कर सके कि प्रत्येक "सकारात्मक" चर सकारात्मक ही रहे और प्रत्येक "नकारात्मक" चर नकारात्मक ही रहे।

5. परिणाम

इन वृत्ताकार प्रमाणों का उपयोग करके, उन्होंने सफलतापूर्वक GLS के लिए एक "यूनिफॉर्म लिंडन इंटरपोलांट" का निर्माण किया।

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

योगदान का सारांश

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

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

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

तकनीकी सारांश: गैर-वेलफाउंडेड प्रमाणों के माध्यम से एकसमान लिंडन इंटरपोलेशन (Uniform Lyndon Interpolation)

समस्या विवरण
गैर-वेलफाउंडेड (non-wellfounded) प्रमाण सिद्धांत का सफलतापूर्वक उपयोग विभिन्न तर्कशास्त्रों, जिनमें प्रूवेबिलिटी लॉजिक (provability logics) भी शामिल हैं, के लिए क्रेग इंटरपोलेशन (Craig interpolation), लिंडन इंटरपोलेशन (Lyndon interpolation) और एकसमान इंटरपोलेशन (uniform interpolation) स्थापित करने के लिए किया गया है। हालाँकि, इस कार्य से पूर्व गैर-वेलफाउंडेड विधियों का उपयोग करके इन गुणों के संयोजन—विशेष रूप से एकसमान लिंडन इंटरपोलेशन प्रॉपर्टी (ULIP)—को संबोधित नहीं किया गया था। यह शोध प्रूवेबिलिटी लॉजिक GLS (जिसे S भी कहा जाता है, जो ट्रू अर्थमैटिक के तहत पीनो अरिथमेटिक के प्रूवेबिलिटी प्रेडिकेट के अनुरूप है) पर केंद्रित है। जबकि GLS के पास एकसमान इंटरपोलेशन और क्रेग इंटरपोलेशन होने के रूप में ज्ञात था, यह एक खुला प्रश्न बना हुआ था कि क्या GLS एकसमान लिंडन इंटरपोलेशन (या यहाँ तक कि गैर-एकसमान लिंडन इंटरपोलेशन भी) को स्वीकार करता है। वेलफाउंडेड प्रूफ सिस्टम में एक प्राथमिक बाधा मोडल नियमों में "डायगोनल फॉर्मूला" (diagonal formula) है, जो वेरिएबल पोलैरिटी (variable polarity) को बनाए रखने में विफल रहता है, जो लिंडोन् इंटरपोलेशन के लिए एक आवश्यकता है।

कार्यप्रणाली (Methodology)
लेखक वेलफाउंडेड प्रमाणों की सीमाओं को दूर करने के लिए गैर-वेलफाउंडेड सिक्वेंट कैलकुली (non-wellfounded sequent calculi) और लोकल प्रोग्रेस प्रूफ थ्योरी (local progress proof theory) का उपयोग करते हैं। कार्यप्रणाली तीन मुख्य तकनीकी घटकों पर निर्भर करती है:

लोकल प्रोग्रेस सिक्वेंट कैलकुली: लेखक एक कैलकुलस, $G_{\infty}^{GLS}$ का उपयोग करते हैं, जो एक लोकल प्रोग्रेस सिस्टम है। मानक वेलफाउंडेड कैलकुली के विपरीत, इस सिस्टम में प्रमाण ऐसे वृक्ष (trees) होते हैं जिनमें अनंत शाखाएं हो सकती हैं, बशर्ते कि प्रत्येक अनंत शाखा में अनंत बार "प्रोग्रेसिंग नोड्स" (विशेष रूप से, मोडल नियम $\square K4_{sat}$ के अनुप्रयोग) शामिल हों। यह सिस्टम $G_{GLS}$ नामक वेलफाउंडेड कैलकुलस में पाए जाने वाले डायगोनल फॉर्मूला से बचता है, जिससे पूरे प्रमाण खोज के दौरान वेरिएबल्स की पोलैरिटी सुरक्षित रहती है।
इंटरपोलेशन टेम्पलेट्स (Interpolation Templates): इंटरपुलेंट्स के निर्माण के लिए, लेखक "इंटरपोलेशन टेम्पलेट्स" को परिभाषित करते हैं, जो एक विशिष्ट सेट के सैचुरेशन नियमों द्वारा उत्पन्न चक्रीय प्रीप्रूफ (cyclic preproofs - बैक-एज के साथ प्रमाण) हैं। ये टेम्पलेट्स उन नियमों को लागू करके बनाए जाते हैं जो फॉर्मूलों को एक सैचुरेटेड अवस्था तक विघटित करते हैं। टेम्पलेट्स को "प्रीइंटरपुलेंट्स" (preinterpolants) के साथ एनोटेट किया जाता है, जो चक्रीय प्रमाण में रिपीट नोड्स के अनुरूप बाउंड वेरिएबल्स वाले स्यूडोफॉर्मूला (pseudoformulas) हैं।
लिंडोन इक्वेशनल सिस्टम्स (Lyndon Equational Systems): प्रीइंटरपुलेंट्स को वैध फॉर्मूलों में हल करने के लिए, लेखक लिंडोन फिक्स्पॉइंट्स (Lyndon fixpoints) और लिंडोन इक्वेशनल सिस्टम्स की अवधारणाओं को पेश करते हैं। एक इक्वेशनल सिस्टम में अज्ञात वेरिएबल्स को फॉर्मूलों से जोड़ने वाले समीकरण शामिल होते हैं, जो पॉजिटिव और नेगेटिव वोकैबुलरी (विशिष्ट ध्रुवता के साथ दिखने वाले वेरिएबल्स के सेट) द्वारा बाधित होते हैं। लेखक सिद्ध करते हैं कि "सिंपल" और "पॉजिटिव मोडलाइज्ड" लिंडोन इक्वेशनल सिस्टम GLS में समाधान योग्य हैं। यह समाधान क्षमता प्रीइंटरपुलेंट्स में बाउंड वेरिएबल्स को वास्तविक फॉर्मूलों के साथ प्रतिस्थापित करने की अनुमति देती है जो आवश्यक पोलैरिटी का सम्मान करते हैं।

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

वैकल्पिक कट एलिमिनेशन (Alternative Cut Elimination): यह $G_{GLS}$ से $G_{\infty}^{GLS}$ में प्रमाणों को अनुवादित करके और दूसरे में कट नियम की स्थानीय स्वीकार्यता (local admissibility) स्थापित करके $G_{GLS}$ के लिए कट एलिमिनेशन का एक नया प्रमाण प्रदान करता है।
नई सैद्धांतिक अवधारणाएँ: यह लिंडोन फिक्स्पॉइंट्स और लिंडोन इक्वेशनल सिस्टम्स को पेश करता है। ये अवधारणाएं यह प्रदर्शित करने के लिए आवश्यक हैं कि गैर-वेलफाउंडेड प्रमाणों के माध्यम से निर्मित एकसमान इंटरपुलेंट्स लिंडोन इंटरपोलेशन के लिए आवश्यक पोलैरिटी बाधाओं का सम्मान करते हैं।
GLS के लिए ULIP का प्रमाण: यह प्रस्तुत करता है कि GLS के पास एकसमान लिंडोन इंटरपोलेशन प्रॉपर्टी (ULIP) है, जो पहला प्रमाण है।

परिणाम
केंद्रीय परिणाम थ्योरम 4.16 है, जो बताता है कि GLS में एकसमान लिंडोन इंटरपोलेशन प्रॉपर्टी है। प्रमाण इस प्रकार आगे बढ़ता है:

एक दिए गए सिक्वेंट के लिए इंटरपोलेशन टेम्पलेट का निर्माण करना।
टेम्पलेट के रिपीट नोड्स से एक पॉजिटिव मोडलाइज्ड लिंडोन इक्वेशनल सिस्टम को जोड़ना।
समाधान अनुक्रम प्राप्त करने के लिए इस सिस्टम को GLS में हल करना (थ्योरम 4.7 द्वारा गारंटीकृत)।
वास्तविक फॉर्मूला $\iota_T$ उत्पन्न करने के लिए रूट नोड के प्रीइंटरपुलेंट में इस समाधान को प्रतिस्थापित करना।
लेम्मा 4.14 और 4.15 के माध्यम से यह सत्यापित करना कि $\iota_T$ ULIP की शर्तों को पूरा करता है: इसमें केवल निर्दिष्ट पॉजिटिव और नेगेटिव वोकैबुलरी शामिल है, और यह संगत वोकैबुलरी वाले किसी भी फॉर्मूला $\psi$ के लिए एक इंटरपुलेंट के रूप में कार्य करता है।

इसके अतिरिक्त, यह शोध स्थापित करता है कि $G_{\infty}^{GLS}$ में अनुवाद के माध्यम से $G_{GLS}$ में कट नियम को समाप्त किया जा सकता है, और $G_{\infty}^{GLS}$ में कट नियम स्थानीय रूप से स्वीकार्य (locally admissible) है।

महत्व और दायरा
यह शोध दावा करता है कि यह गैर-वेलफाउंडेड विधियों का उपयोग करके प्रूवेबिलिटी लॉजिक्स के लिए यूनिफॉर्म लिंडोन इंटरपोलेशन के संबंध में साहित्य के अंतराल को भरता है। लेखक नोट करते हैं कि उनकी कार्यप्रणाली अन्य प्रूवेबिलिटी लॉजिक्स के लिए भी अनुकूलनीय है, बशर्ते उनके लिए एक गैर-वेलफाउंडेड सिक्वेंट कैलकुलस उपलब्ध हो। वे भविष्य की दिशाओं को स्पष्ट रूप से पहचानते हैं, जिसमें यूनरी इंटरप्रिटेबिलिटी लॉजिक्स, बाईमोडल प्रूवेबिलिटी लॉजिक्स और इंट्यूशनिस्टिक प्रूवेबिलिटी लॉजिक्स पर विधि को लागू करना शामिल है। वे उन लॉजिक्स की जांच करने का भी सुझाव देते हैं जहाँ सिंपल लिंडोन फिक्स्पॉइंट्स मौजूद नहीं हैं (जैसे इंटरप्रिटेबिलिटी लॉजिक IL) और क्या पॉजिटिव मोडलाइज्ड लिंडोन इक्वेशनल सिस्टम अभी भी उन संदर्भों में हल किए जा सकते हैं। यह कार्य सभी मोडल लॉजिक्स के लिए ULIP को हल करने का दावा नहीं करता है, बल्कि GLS के लिए गैर-वेलफाउंडेड दृष्टिकोण की व्यवहार्यता को प्रदर्शित करता है और विस्तार के लिए एक ढांचा तैयार करता है।