💻 computer science

Set Automata and Limits of Decidability of Two-Variable Logic on Data Words

यह शोधपत्र सेट ऑटोमेटा (set automata) को पेश करके और यह सिद्ध करके कि यह तर्क (logic) ठीक तभी निर्णय योग्य (decidable) है जब अंतर्निहित मोनोइड (monoid) रैखिक रूप से क्रमबद्ध द्वि-पक्षीय आदर्शों (linearly ordered two-sided ideals) के साथ इडेम्पोटेंट (idempotent) हो, गार्डेड रेगुलर प्रेडिकेट्स (guarded regular predicates) के साथ विस्तारित डेटा वर्ड्स (data words) पर दो-चर तर्क (two-variable logic) की निर्णयक्षमता स्थापित करता है, जो इस समस्या को ऑर्डर्ड मल्टीकाउंटर ऑटोमेटा (ordered multicounter automata) की रिक्तता (emptiness) में अपचयित करके प्राप्त किया गया है।

मूल लेखक: Shibashis Guha, Amaldev Manuel, S P Rishal

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

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

CC BY 4.0

मूल लेखक: Shibashis Guha, Amaldev Manuel, S P Rishal

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

यहाँ "Set Automata and Limits of Decidability of Two-Variable Logic on Data Words" पेपर का एक सरल भाषा में अनुवाद दिया गया है:

मुख्य विचार: "डेटा वर्ड" (Data Word) की पहेली

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

उनका नेम टैग: एक साधारण लेबल जैसे "एलिस," "बॉब," या "चार्ली" (यह अल्फाबेट है)।
उनकी ग्रुप आईडी: एक गुप्त नंबर जो बताता है कि वे किस मेज (Table) पर बैठे हैं। कई मेहमानों की ग्रुप आईडी एक जैसी हो सकती है (जैसे, टेबल 5 पर मौजूद हर व्यक्ति की आईडी #5 है)।

दिक्कत यह है कि आप वास्तविक नंबर नहीं पढ़ सकते। आप केवल यह पूछ सकते हैं: "क्या ये दो लोग एक ही मेज पर हैं?" (समानता परीक्षण/Equality test)। आप यह नहीं पूछ सकते, "क्या टेबल 5, टेबल 3 से बड़ी है?"

लेखक एक पहेली को हल करने की कोशिश कर रहे हैं: क्या हम मेहमानों की इस सूची में पैटर्न का वर्णन करने के लिए नियमों का एक सेट (लॉजिक) लिख सकते हैं जिसे कंप्यूटर वास्तव में यह जांचने के लिए उपयोग कर सके कि वे सत्य हैं या असत्य?

समस्या: जब नियम बहुत जटिल हो जाते हैं

अतीत में, शोधकर्ताओं ने केवल दो "वेरिएबल्स" (मान लीजिए x और y) का उपयोग करके नियम लिखने का एक तरीका खोजा था।

उदाहरण नियम: "यदि व्यक्ति x और व्यक्ति y एक ही मेज पर हैं, और x ने लाल शर्ट पहनी है, तो y को नीली शर्ट पहननी चाहिए।"

यह प्रणाली सरल चीजों के लिए बहुत अच्छी तरह काम करती है। लेकिन, जैसा कि पेपर में उल्लेख किया गया है, यदि आप अधिक जटिल नियम जोड़ने का प्रयास करते हैं—जैसे "व्यक्ति x और व्यक्ति y के बीच, जो एक ही मेज पर हैं, ठीक तीन लोग टोपी पहने हुए होने चाहिए"—तो कंप्यूटर भ्रमित हो जाता है। वह एक अनंत लूप (infinite loop) में चला जाता है और कभी भी आपको यह नहीं बता पाता कि वह नियम संभव है या नहीं। इसे अनिश्चितता (Undecidability) कहा जाता है।

नया विचार: "गार्डेड रेगुलर प्रेडिकेट्स" (Guarded Regular Predicates)

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

इसे पार्टी में एक सुरक्षा गार्ड (Security Guard) के रूप में सोचें।

गार्ड: नियम केवल तभी लागू होता है जब दो लोग एक ही मेज पर हों (यह "गार्ड" है)।
पैटर्न: एक बार जब गार्ड यह पुष्टि कर देता है कि वे एक ही मेज पर हैं, तो गार्ड उनके बीच के रास्ते की जाँच करता है। क्या वह रास्ता एक विशिष्ट पैटर्न जैसा दिखता है? (जैसे, "क्या उनके बीच के लोगों का क्रम 'लाल, नीला, लाल' है?")।

यह पार्टी का बहुत समृद्ध वर्णन करने की अनुमति देता है। हालाँकि, बड़ा सवाल अभी भी वही है: पैटर्न कितना जटिल हो सकता है इससे पहले कि कंप्यूटर काम करना बंद कर दे, इसकी एक सीमा है?

समाधान: "सेट ऑटोमेटा" (Set Automaton)

इस प्रश्न का उत्तर देने के लिए, लेखक एक नए प्रकार की मशीन का आविष्कार करते हैं जिसे सेट ऑटोमेटा कहा जाता है।

कल्पना कीजिए कि पार्टी में एक रोबोट वेटर है।

रोबोट: इसके पास निश्चित संख्या में टोकरियाँ (Baskets/Sets) हैं।
काम: जैसे-जैसे रोबोट मेहमानों की कतार के साथ चलता है, वह एक मेहमान को उठाता है और उसे एक टोकरी में डाल देता है।
जादू: रोबोट मेहमानों को टोकरियों के बीच ले जा सकता है, टोकरियों को मिला सकता है, या उन्हें खाली कर सकता है।
लक्ष्य: रात के अंत में, रोबोट तब जीतता है यदि उसने नियमों के अनुसार मेहमानों को टोकरियों में सही ढंग से छाँट लिया है।

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

"लीनियर बैंड" (Linear Band) की खोज

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

उपमा: कल्पना कीजिए कि "टोकरी नियम" बक्सों का एक ढेर हैं।
- यदि बक्से एक अव्यवस्थित ढेर में रखे हैं जहाँ आप यह नहीं बता सकते कि कौन सा किसके ऊपर है, तो रोबोट भ्रमित हो जाता है (Undecidable)।
- यदि बक्सों को एक परफेक्ट सीधी रेखा में रखा गया है (एक के ऊपर एक, बिना किसी बगल की उलझन के), तो रोबोट हमेशा उनमें रास्ता बना सकता है (Decidable)।

लेखक इस परफेक्ट स्टैक को लीनियर बैंड कहते हैं। वे सिद्ध करते हैं कि:

यदि आपके नियम इस "लीनियर बैंड" संरचना में फिट बैठते हैं: तो कंप्यूटर निश्चित रूप से पहेली को हल कर सकता है।
यदि आपके नियम इस संरचना में फिट नहीं होते हैं: तो पहेली को हल करना असंभव हो जाता है (कंप्यूटर अनंत काल तक घूमता रहेगा)।

यह क्यों महत्वपूर्ण है (पेपर के अनुसार)

पेपर चिकित्सा निदान या सेल्फ-ड्राइविंग कारों जैसे वास्तविक दुनिया के अनुप्रयोगों के बारे में बात नहीं करता है। इसके बजाय, यह तर्क की सैद्धांतिक सीमाओं (theoretical limits of logic) पर ध्यान केंद्रित करता है।

यह प्रसिद्ध "टू-वेरिएबल लॉजिक" (कंप्यूटर विज्ञान का एक मानक उपकरण) को इन नए "गार्डेड" नियमों को शामिल करने के लिए विस्तारित करता है।
यह एक स्पष्ट रेखा खींचता है: यहीं पर वह स्थान है जहाँ तर्क हल करने योग्य नहीं रह जाता।
यह एक नया तरीका प्रदान करता है जिससे ऐसी मशीनें बनाई जा सकें (सेट ऑटोमेटा) जो बिना क्रैश हुए इस प्रकार के डेटा पैटर्न को संभाल सकें।

एक वाक्य में सारांश

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

तकनीकी सारांश: डेटा वर्ड्स पर दो-चर लॉजिक के सेट ऑटोमेटा और डैसिडेबिलिटी की सीमाएँ

समस्या विवरण
यह शोध पत्र डेटा वर्ड्स पर दो-चर प्रथम-क्रम तर्क ( $FO_2$ ) के विस्तार की संतुष्टि समस्या (satisfiability problem) की डैसिडेबिलिटी (decidability) को संबोधित करता है। एक डेटा वर्ड $(a_i, d_i)$ का एक परिमित अनुक्रम है जहाँ $a_i$ एक परिमित वर्णमाला $\Sigma$ से आता है और $d_i$ एक अनंत डोमेन $D$ से आता है, जिसमें समानता (equality) ही एकमात्र परीक्षण योग्य गुण है। जबकि डेटा वर्ड्स पर मानक $FO_2$ तर्क (क्रम, उत्तराधिकारी और डेटा समानता के साथ) ज्ञात रूप से डैसिडेबल है (विशेष रूप से, $EMSO_2[\Sigma, <, +1, \sim, \twoheadrightarrow_1]$ ), लेखक इन तर्कों में गार्डेड रेगुलर प्रेडिकेट्स (guarded regular predicates) को जोड़ने के साथ इस तर्क के डैसिडेबिलिटी के विस्तार की जांच करते हैं।

ये प्रेडिकेट्स, जिन्हें $eL(x, y) $द्वारा दर्शाया जाता है, तब सत्य होते हैं जब स्थितियाँ$ x $और$ y $एक ही डेटा क्लास (अर्थात$ x \sim y $) से संबंधित होती हैं और उनके बीच का स्ट्रिंग का फैक्टर एक रेगुलर लैंग्वेज$ L $से संबंधित होता है। केंद्रीय प्रश्न यह है कि उन मोनॉइड्स (या सेमग्रुप्स)$ M$ के लिए कौन सी श्रेणियाँ (classes) डैसिडेबल हैं जो इन प्रेडिकेट्स में उपयोग की जाने वाली रेगुलर लैंग्वेजेस को पहचानते हैं।

कार्यप्रणाली
लेखक डैसिडेबिलिटी की सीमा को स्पष्ट करने के लिए ऑटोमेटा थ्योरी और बीजगणितीय सेमग्रुप थ्योरी के संयोजन का उपयोग करते हैं।

सेट ऑटोमेटा (Set Automata): लेखक सेट ऑटोमेटा नामक एक नया ऑटोमेटा फॉर्मलिज्म पेश करते हैं। ये परिमित अवस्था वाले ऑटोमेटा हैं जो डेटा मानों को संग्रहीत करने के लिए निश्चित संख्या में सेट रखते हैं। ट्रांज़िशन (Transitions) निम्नलिखित की अनुमति देते हैं:
- लोकल अपडेट्स (Local updates): विशिष्ट सेटों में वर्तमान डेटा मान को जोड़ना या हटाना।
- ग्लोबल अपडेट्स (Global updates): सभी सेटों की सामग्री पर एक संबंध (या रूपांतरण) लागू करना (जैसे, सेट $X_i$ से डेटा को $X_j$ में ले जाना)।
  लेखक स्थापित करते हैं कि सेट ऑटोमेटा, क्लास ऑटोमेटा (बोजाजिक्क और लासोटा द्वारा प्रस्तुत) के अभिव्यंजक रूप से समकक्ष (expressively equivalent) हैं, जो कि एक ऐसा मॉडल है जिसकी एम्प्टीनेस समस्या (emptiness problem) अनडैसिडेबल (undecidable) है।
उप-श्रेणियाँ और डैसिडेबिलिटी: डैसिडेबिलिटी को पुनः प्राप्त करने के लिए, वे ऑर्डर्ड क्वासी-नॉर्मल सेट ऑटोमेटा (ordered quasi-normal set automata) नामक एक उप-श्रेणी को परिभाषित करते हैं।
- क्वासी-नॉर्मल (Quasi-normal): यह सुनिश्चित करता है कि "गैर-स्थिर" (non-stable) सेटों के एक विशिष्ट उपसमुच्चय में डेटा मान केवल एक ही सेट में मौजूद हों।
- ऑर्डर्ड (Ordered): यह गैर-स्थिर सेटों पर एक रैखिक क्रम लागू करता है ताकि ग्लोबल अपडेट्स इन सेटों के एक प्रीफिक्स की सामग्री को खाली कर दें और उन्हें क्रम में उच्च सेटों में स्थानांतरित कर दें।
  ऑर्डर्ड क्वासी-नॉर्मल सेट ऑटोमेटा की एम्प्टीनेस समस्या को ऑर्डर्ड मल्टीकाउंटर ऑटोमेटा (एक ज्ञात डैसिडेबल समस्या) की एम्प्टीनेस समस्या में बदलकर डैसिडेबल दिखाया गया है।
लॉजिकल-टू-ऑटोमेटा अनुवाद: शोध पत्र लॉजिकल फॉर्मूला और ऑटोमेटा के बीच अनुवाद प्रदान करता है:
- प्रत्येक सेट ऑटोमेटा को गार्डेड रेगुलर प्रेडिकेट्स के साथ एक $EMSO_2$ फॉर्मूला के रूप में व्यक्त किया जा सकता है।
- इसके विपरीत, $M$ द्वारा पहचाने जाने वाले प्रेडिकेट्स का उपयोग करने वाले फॉर्मूला को सफिक्स-स्टोरिंग सेट ऑटोमेटा (एक विशिष्ट प्रकार का क्वासी-नॉर्मल ऑटोमेटा) में अनुवादित किया जा सकता है।
बीजगणितीय लक्षण वर्णन (Algebraic Characterization): लेखक $M$ के मोनॉइड्स की बीजगणितीय संरचना का विश्लेषण करते हैं। वे लीनियर बैंड्स (linear bands) को ऐसे इडेम्पोटेंट मोनॉइड्स के रूप में परिभाषित करते हैं जहाँ दो-पक्षीय आइडियल्स (two-sided ideals) रैखिक रूप से व्यवस्थित होते हैं (अर्थात, किसी भी दो आइडियल्स $I, J$ के लिए, या तो $I \subseteq J$ या $J \subseteq I$ )।

मुख्य योगदान और परिणाम

मुख्य प्रमेय (Theorem 6): डेटा वर्ड्स पर $EMSO_2[\Sigma, <, +1, \sim, \twoheadrightarrow_1, \tilde{F}_M]$ फॉर्मूला की संतुष्टि (satisfiability) तभी डैसिडेबल है जब मोनॉइड $M$ एक लीनियर बैंड हो।
- डैसिडेबिलिटी दिशा: यदि $M$ एक लीनियर बैंड है, तो लेखक एक समकक्ष ऑर्डर्ड क्वासी-नॉर्मल सेट ऑटोमेटा का निर्माण करते हैं। चूंकि ऐसे ऑटोमेटा की एम्प्टीनेस डैसिडेबल है, इसलिए तर्क डैसिडेबल है।
- अनडैसिडेबिलिटी दिशा: यदि $M$ लीनियर बैंड नहीं है, तो इसमें $U_1^2$ (दो-तत्व वाले दो मोनॉइड्स का डायरेक्ट प्रोडक्ट जिसमें ज़ीरो है) या $N_2$ (एक विशिष्ट नल मोनॉइड) के समरूप सबस्ट्रक्चर होगा। लेखक दिखाते हैं कि इन विशिष्ट मोनॉइड्स द्वारा पहचाने जाने वाले गार्डेड रेगुलर प्रेडिकेट्स टू-काउंटर मशीनों की हाल्टिंग प्रॉब्लम को एनकोड करने की अनुमति देते हैं, जिससे तर्क अनडसिडेबल हो जाता है।
अभिव्यंजक तुल्यता (Expressive Equivalence): शोध पत्र सिद्ध करता है कि सेट ऑटोमेटा, गार्डेड रेगुलर प्रेडिकेट्स के साथ $EMSO_2$ के अभिव्यंजक रूप से समकक्ष हैं। इसके अलावा, यह दिखाता है कि किसी अन्य मोनॉइड $M'$ (विशेष रूप से, पावर सेट मोनॉइड $P(M)$ ) द्वारा पहचाने जाने वाले रेगुलर प्रेडिकेट्स वाले किसी भी फॉर्मूला को गार्डेड रेगुलर प्रेडिकेट्स का उपयोग करके समकक्ष रूप से फिर से लिखा जा सकता है।
कठोर विस्तार (Strict Extension): पहचाना गया डैसिडेबल खंड [4] के मूल $FO_2$ तर्क का एक कठोर विस्तार है। उदाहरण के लिए, भाषा $L_2$ (जिसके लिए एक ही क्लास के इंक्रिमेंट्स और डिक्रीमेंट्स के बीच ज़ीरो-टेस्ट की आवश्यकता नहीं होती है), जो मानक $FO_2$ या डेटा ऑटोमेटा में परिभाषित नहीं है, इस विस्तारित तर्क में परिभाषित हो जाती है जब अंतर्निहित मोनॉइड एक लीनियर बैंड होता है।

महत्व और दावे

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

लेखक नोट करते हैं कि जबकि लीनियर बैंड्स के लिए डैसिडेबिलिटी स्थापित की गई है, सामान्य सेमग्रुप्स के लिए लक्षण वर्णन अभी भी खुला है। वे यह भी रेखांकित करते हैं कि लीनियर बैंड्स द्वारा मान्यता प्राप्त रेगुलर लैंग्वेजेस की श्रेणी का साहित्य में व्यापक रूप से अध्ययन नहीं किया गया है, जो इस बीजगणितीय डोमेन में आगे के अन्वेषण की आवश्यकता का सुझाव देता है। निर्णय प्रक्रियाओं (decision procedures) की जटिलता नॉन-एलिमेंट्री बनी रहती है, जो अंतर्निहित $FO_2$ और डेटा ऑटोमेटा परिणामों से विरासत में मिली है।

यह कार्य टेम्पोरल लॉजिक (जैसे फ्रीज़-LTL) से खुद को अलग करता है, जो डेटा क्लासेस के भीतर विशिष्ट रेगुलर गुणों को कैप्चर करने वाला एक डैसिडेबल विस्तार प्रदान करता है, जो पहले अनडैसिडेबल थे या जिनके लिए अलग लॉजिकल फ्रेमवर्क की आवश्यकता थी।