S2S (गणित): Difference between revisions

गणित में, S2S दो उत्तराधिकारियों के साथ मोनैडिक दूसरे क्रम का तर्क है। यह ज्ञात सबसे अभिव्यंजक प्राकृतिक निर्णायक सिद्धांतों में से एक है, जिसमें S2S में कई निर्णायक सिद्धांतों की व्याख्या की जा सकती है। इसकी निर्णायकता 1969 में माइकल ओ. राबिन द्वारा सिद्ध की गई थी।<ref>{{Cite journal |title=अनंत पेड़ों पर दूसरे क्रम के सिद्धांतों और ऑटोमेटा की निर्णायकता|last=Rabin |first=Michael |journal=Transactions of the American Mathematical Society |volume=141 |date=1969 |url=https://www.ams.org/journals/tran/1969-141-00/S0002-9947-1969-0246760-1/S0002-9947-1969-0246760-1.pdf}}</ref>

S2S की प्रथम क्रम की वस्तुएं परिमित बाइनरी स्ट्रिंग हैं। दूसरे क्रम की वस्तुएं परिमित बाइनरी स्ट्रिंग्स के मनमाने समुच्चय (या एकात्मक विधेय) हैं। S2S में स्ट्रिंग्स पर फ़ंक्शन s→s0 और s→s1 हैं, और विधेय s∈S (समकक्ष, S(s)) का अर्थ है कि स्ट्रिंग s समुच्चय S से संबंधित है।

* डिफ़ॉल्ट रूप से, लोअरकेस अक्षर पहले क्रम की वस्तुओं को संदर्भित करते हैं, और अपरकेस दूसरे क्रम की वस्तुओं को संदर्भित करते हैं।

* स्ट्रिंग्स s और t का संयोजन st द्वारा दर्शाया जाता है, और यह आम तौर पर S2S में उपलब्ध नहीं है, यहां तक ​​कि s→0s में भी नहीं। स्ट्रिंग्स के बीच [[स्ट्रिंग ऑपरेशन]] निश्चित है।

* समानता आदिम है, या इसे s = t ⇔ ∀S (S(s) ⇔ S(t)) और S = T ⇔ ∀s (S(s) ⇔ T(s)) के रूप में परिभाषित किया जा सकता है।

* स्ट्रिंग्स के स्थान पर, कोई (उदाहरण के लिए) n→2n+1 और n→2n+2 के साथ प्राकृतिक संख्याओं का उपयोग कर सकता है, लेकिन कोई अन्य ऑपरेशन नहीं।

* सभी बाइनरी स्ट्रिंग्स का समुच्चय {0,1} द्वारा दर्शाया गया है^*, [[क्लेन स्टार]] का उपयोग करते हुए।

* {0,1} का मनमाना उपसमुच्चय^* को कभी-कभी पेड़ों से पहचाना जाता है, विशेष रूप से {0,1}-लेबल वाले पेड़ {0,1} के रूप में^*; {0,1}^* एक पूर्ण अनंत बाइनरी ट्री बनाता है।

* सूत्र जटिलता के लिए, स्ट्रिंग्स पर उपसर्ग संबंध को आम तौर पर पहले क्रम के रूप में माना जाता है। इसके बिना, सभी सूत्र Δ के समतुल्य नहीं होंगे¹₂ सूत्र.<ref>{{Cite conference |title=बाइनरी ट्री के मोनैडिक लॉजिक की संरचना पर|last1=Janin |first1=David |last2=Lenzi |first2=Giacomo |url=https://hal.archives-ouvertes.fr/hal-00676277 |conference=MFCS 1999 |doi=10.1007/3-540-48340-3_28}}</ref>

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

* एक निश्चित k के लिए, स्ट्रिंग से k तक एक फ़ंक्शन (यानी k के नीचे की प्राकृतिक संख्या) को एक समुच्चय द्वारा एन्कोड किया जा सकता है। इसके अलावा, s,t ⇒ s01t{{prime}} जहां टी{{prime}} t के प्रत्येक वर्ण को दोगुना कर देता है, और s ⇒ {s01t{{prime}}: t∈{0,1}^*} S2S निश्चित है। इसके विपरीत, संचार जटिलता तर्क के अनुसार, S1S (नीचे) में समुच्चय की एक जोड़ी एक समुच्चय द्वारा एन्कोड करने योग्य नहीं है।

S2S की कमजोरियाँ: कमजोर S2S (WS2S) के लिए सभी समुच्चयों का परिमित होना आवश्यक है (ध्यान दें कि परिमितता कोनिग के लेम्मा का उपयोग करके S2S में व्यक्त की जा सकती है)। S1S को यह आवश्यक करके प्राप्त किया जा सकता है कि '1' स्ट्रिंग्स में प्रकट न हो, और WS1S को भी परिमितता की आवश्यकता होती है। यहां तक ​​कि WS1S भी 2 की शक्तियों के विधेय के साथ [[प्रेस्बर्गर अंकगणित]] की व्याख्या कर सकता है, क्योंकि समुच्चय का उपयोग निश्चित जोड़ के साथ असीमित बाइनरी संख्याओं का प्रतिनिधित्व करने के लिए किया जा सकता है।

'निर्णय जटिलता'

S2S निर्णय लेने योग्य है, और S2S, S1S, WS2S, WS1S में से प्रत्येक में घातांक के रैखिक रूप से बढ़ते ढेर के अनुरूप एक [[गैर-प्राथमिक समस्या]] निर्णय जटिलता है। निचली सीमा के लिए, Σ पर विचार करना पर्याप्त है¹₁ WS1S वाक्य. अंकगणित (या अन्य) गणना का प्रस्ताव करने के लिए एक दूसरे क्रम के क्वांटिफायर का उपयोग किया जा सकता है, जिसे पहले ऑर्डर क्वांटिफायर का उपयोग करके सत्यापित किया जा सकता है यदि हम परीक्षण कर सकते हैं कि कौन सी संख्याएं बराबर हैं। इसके लिए, यदि हम संख्याओं 1..m को उचित रूप से एन्कोड करते हैं, तो हम बाइनरी प्रतिनिधित्व i के साथ एक संख्या को एनकोड कर सकते हैं₁i₂...मैं_''m'' जैसे मैं₁ 1 मैं₂ 2... मैं_''m'' मी, एक गार्ड से पहले। गार्ड के परीक्षण को मर्ज करने और चर नामों का पुन: उपयोग करने से, बिट्स की संख्या घातांक की संख्या में रैखिक होती है। ऊपरी सीमा के लिए, निर्णय प्रक्रिया (नीचे) का उपयोग करके, के-गुना क्वांटिफायर विकल्प वाले वाक्यों को वाक्य की लंबाई (समान स्थिरांक के साथ) के के + ओ (1)-गुना घातांक के अनुरूप समय में तय किया जा सकता है।

(1) ∃!s ∀t ( t0≠s ∧ t1≠s) (खाली स्ट्रिंग, जिसे ε द्वारा दर्शाया गया है; ∃!s का अर्थ है कि अद्वितीय s है)<br />

(2) ∀s,t ∀i∈{0,1} ∀j∈{0,1} (si=tj ⇒ s=t ∧ i=j) (i और j का उपयोग एक संक्षिप्त नाम है; i= के लिए j, 0 1 के बराबर नहीं है)<br />

(3) ∀S (S(ε) ∧ ∀s (S(s) ⇒ S(s0) ∧ S(s1))⇒ ∀s S(s)) ([[गणितीय प्रेरण]])<br />

(4) ∃S ∀s (S(s) ⇔ φ(s)) (S φ में मुक्त नहीं है)

(4) सूत्र φ पर विनिर्देशन की स्वयंसिद्ध स्कीमा है, जो हमेशा दूसरे क्रम के तर्क के लिए होती है। हमेशा की तरह, यदि φ में मुक्त चर नहीं दिखाए गए हैं, तो हम अभिगृहीत का सार्वभौमिक समापन लेते हैं। यदि समानता विधेय के लिए आदिम है, तो कोई विस्तारात्मकता का सिद्धांत भी जोड़ता है S=T ⇔ ∀s (S(s) ⇔ T(s))। चूँकि हमारे पास समझ है, इंडक्शन स्कीमा के बजाय एकल कथन हो सकता है।

S1S का अनुरूप स्वयंसिद्धीकरण पूरा हो गया है।<ref>{{Cite conference |url=https://link.springer.com/content/pdf/10.1007%2F978-3-642-33475-7_22.pdf |last=Riba |first=Colin |title=अनंत शब्दों पर राक्षसी दूसरे क्रम के तर्क के स्वयंसिद्धीकरण की पूर्णता का एक मॉडल सैद्धांतिक प्रमाण|conference=TCS 2012 |date=2012 |doi=10.1007/978-3-642-33475-7_22}}</ref> हालाँकि, S2S के लिए, पूर्णता खुली है (2021 तक)। जबकि S1S में एकरूपता है, कोई S2S परिभाषित (यहां तक ​​कि पैरामीटर की अनुमति देने वाला) विकल्प फ़ंक्शन नहीं है जो एक गैर-खाली समुच्चय दिया गया S, S का एक तत्व लौटाता है,<ref>{{Citation |chapter-url=https://hal-upec-upem.archives-ouvertes.fr/hal-00620169/file/csl07.pdf |chapter=MSO on the Infinite Binary Tree: Choice and Order |last1=Carayol |first1=Arnaud |last2= Löding|first2=Christof |title=Computer Science Logic |series=Lecture Notes in Computer Science |date=2007 |volume=4646 |pages=161–176 |doi=10.1007/978-3-540-74915-8_15|isbn=978-3-540-74914-1 |s2cid=14580598 }}</ref> और समझ स्कीमों को आम तौर पर पसंद के सिद्धांत के विभिन्न रूपों के साथ संवर्धित किया जाता है। हालाँकि, (1)-(4) कुछ [[समता खेल]]ों के लिए निर्धारण स्कीमा के साथ विस्तारित होने पर पूर्ण हो जाता है।<ref>{{Cite journal |title=अनंत पेड़ों का एक कार्यात्मक (मोनैडिक) दूसरे क्रम का सिद्धांत|last1=Das |first=Anupam |last2=Riba |first2=Colin |journal=Logical Methods in Computer Science |volume=16|issue=4 |date=2020 |doi=10.23638/LMCS-16(4:6)2020 |arxiv=1903.05878}} (A preliminary 2015 version erroneously claimed proof of completeness without the determinacy schema.)</ref>

S2S को Π द्वारा भी स्वयंसिद्ध किया जा सकता है¹₃ वाक्य (स्ट्रिंग्स पर उपसर्ग संबंध को आदिम के रूप में उपयोग करना)। हालाँकि, यह अंतिम रूप से स्वयंसिद्ध नहीं है, न ही इसे Σ द्वारा स्वयंसिद्ध किया जा सकता है¹₃ वाक्य भले ही हम प्रेरण स्कीमा और अन्य वाक्यों का एक सीमित समुच्चय जोड़ते हैं (यह Π से इसके संबंध से पता चलता है)¹₂-वह₀).

प्रत्येक परिमित k के लिए, वृक्ष-चौड़ाई ≤k (और संबंधित वृक्ष अपघटन) के साथ गणनीय ग्राफ़ का मोनैडिक द्वितीय क्रम (MSO) सिद्धांत S2S में व्याख्या योग्य है (कोर्सेल का प्रमेय देखें)। उदाहरण के लिए, पेड़ों का एमएसओ सिद्धांत (ग्राफ़ के रूप में) या [[श्रृंखला-समानांतर ग्राफ]]़ का निर्णय लेने योग्य है। यहां (यानी बंधे हुए पेड़ की चौड़ाई के लिए), हम शीर्षों (या किनारों) के एक समुच्चय के लिए परिमितता परिमाणक की व्याख्या भी कर सकते हैं, और एक निश्चित पूर्णांक के समुच्चय मॉड्यूलो में शीर्षों (या किनारों) की गिनती भी कर सकते हैं। बेशुमार ग्राफ़ की अनुमति देने से सिद्धांत नहीं बदलता है। इसके अलावा, तुलना के लिए, S1S बंधे हुए [[पथ-चौड़ाई]] के जुड़े ग्राफ़ की व्याख्या कर सकता है।

इसके विपरीत, असंबद्ध वृक्ष-चौड़ाई के ग्राफ़ के प्रत्येक समुच्चय के लिए, इसका अस्तित्व (यानी Σ)¹₁) यदि हम शीर्षों और किनारों दोनों पर विधेय की अनुमति देते हैं तो एमएसओ सिद्धांत अनिर्णीत है। इस प्रकार, एक अर्थ में, S2S की निर्णायकता सर्वोत्तम संभव है। अनबाउंड ट्रीविड्थ वाले ग्राफ़ में बड़े ग्रिड माइनर होते हैं, जिनका उपयोग [[ट्यूरिंग मशीन]] का अनुकरण करने के लिए किया जा सकता है।

S2S कुछ मोडल लॉजिक्स की निर्णायकता के लिए उपयोगी है, [[क्रिपके शब्दार्थ]] स्वाभाविक रूप से पेड़ों की ओर ले जाता है।

S2S+U (या सिर्फ S1S+U) अनिर्णीत है यदि U अनबाउंडिंग क्वांटिफायर है - UX Φ(X) यदि Φ(X) कुछ मनमाने ढंग से बड़े परिमित X के लिए है।<ref>{{Citation |title=The MSO+U theory of (N, &lt;) is undecidable |first1=Mikołaj |last1=Bojańczyk |first2=Paweł |last2=Parys |first3=Szymon |last3=Toruńczyk |arxiv=1502.04578 |date=2015}}</ref> हालाँकि, WS2S+U, अनंत पथों पर परिमाणीकरण के साथ भी, निर्णय लेने योग्य है, यहां तक ​​कि S2S उपसूत्रों के साथ भी, जिनमें U शामिल नहीं है।<ref>{{Citation |title=Weak MSO+U with path quantifiers over infinite trees |first1=Mikołaj |last1=Bojańczyk |arxiv=1404.7278 |date=2014}}</ref>

बाइनरी स्ट्रिंग्स का एक समुच्चय S2S में निश्चित है यदि यह नियमित है (यानी एक [[नियमित भाषा]] बनाता है)। S1S में, समुच्चय पर एक (एकात्मक) विधेय (पैरामीटर-मुक्त) निश्चित है यदि यह एक ओमेगा-नियमित भाषा है|ω-नियमित भाषा है। S2S के लिए, उन सूत्रों के लिए जो अपने मुक्त चर का उपयोग केवल उन स्ट्रिंग्स पर करते हैं जिनमें 1 नहीं है, अभिव्यक्ति S1S के समान ही है।

प्रत्येक S2S सूत्र के लिए φ(S₁,...,एस_''k''), (k मुक्त चर के साथ) और बाइनरी स्ट्रिंग्स T, φ(S) का परिमित वृक्ष₁∩टी,...,एस_''k''∩T) की गणना |T| में रैखिक समय में की जा सकती है (कोर्सेल का प्रमेय देखें), लेकिन जैसा कि ऊपर बताया गया है, ओवरहेड को सूत्र आकार में घातीय रूप से दोहराया जा सकता है (अधिक सटीक रूप से, समय है <math>O(|T|k)+2_{O(|\phi|)}^2</math>).

S1S के लिए, प्रत्येक सूत्र Δ के बराबर है¹₁ सूत्र, और Π के बूलियन संयोजन के लिए⁰₂ अंकगणितीय सूत्र. इसके अलावा, प्रत्येक S1S सूत्र सूत्र के मापदंडों के संगत ω-ऑटोमेटन द्वारा स्वीकृति के बराबर है। ऑटोमेटन एक नियतात्मक समता ऑटोमेटन हो सकता है: एक समता ऑटोमेटन में प्रत्येक राज्य के लिए एक पूर्णांक प्राथमिकता होती है, और यदि अनंत रूप से देखी जाने वाली सर्वोच्च प्राथमिकता अक्सर विषम (वैकल्पिक रूप से, सम) होती है, तो इसे स्वीकार करता है।

S2S के लिए, ट्री ऑटोमेटा (नीचे) का उपयोग करते हुए, प्रत्येक सूत्र Δ के बराबर है¹₂ सूत्र. इसके अलावा, प्रत्येक S2S सूत्र केवल चार क्वांटिफायर, ∃S∀T∃s∀t ... वाले सूत्र के बराबर है (यह मानते हुए कि हमारी औपचारिकता में उपसर्ग संबंध और उत्तराधिकारी कार्य दोनों हैं)। S1S के लिए, तीन परिमाणक (∃S∀s∃t) पर्याप्त हैं, और WS2S और WS1S के लिए, दो परिमाणक (∃S∀t) पर्याप्त हैं; WS2S और WS1S के लिए यहां उपसर्ग संबंध की आवश्यकता नहीं है।

हालाँकि, मुक्त दूसरे क्रम के चर के साथ, प्रत्येक S2S सूत्र को केवल Π के माध्यम से दूसरे क्रम के अंकगणित में व्यक्त नहीं किया जा सकता है¹₁ ट्रांसफ़िनिट रिकर्सन (रिवर्स गणित देखें)। आरसीए₀ + (स्कीमा) {τ: τ एक सच्चा S2S वाक्य है} (स्कीमा) के बराबर है {τ: τ एक Π है¹₃ Π में सिद्ध वाक्य¹₂-वह₀ }.<ref name="S2S--Pi-1-2-CA_0">{{Cite conference |conference=LICS '16: 31st Annual ACM/IEEE Symposium on Logic in Computer Science |date=2016  |title=राबिन की निर्णायकता प्रमेय कितनी अप्रमाणित है?|first1=Leszek |last1=Kołodziejczyk |first2=Henryk |last2=Michalewski |arxiv=1508.06780 }}</ref><ref>{{Cite web |last=Kołodziejczyk |first=Leszek |url = https://cs.nyu.edu/pipermail/fom/2015-October/019257.html |title=Question on Decidability of S2S |publisher=FOM |date=October 19, 2015}}</ref> आधार सिद्धांत पर, स्कीमा (k पर स्कीमा) ∀S⊆ω ∃α के बराबर हैं₁<...<ए_''k'' L_{α₁</उप>(एस) ≺_Σ₁... ≺ उप>एस₁</उप>एल उप>ए_''k''}(एस) जहां एल रचनात्मक ब्रह्मांड है ([[बड़े गणनीय क्रमसूचक]] भी देखें)। सीमित प्रेरण के कारण, Π¹₂-वह₀ यह सिद्ध नहीं करता कि सब सत्य है (मानक निर्णय प्रक्रिया के अंतर्गत) Π¹₃ S2S कथन वास्तव में सत्य हैं, भले ही ऐसा प्रत्येक वाक्य सिद्ध करने योग्य हो¹₂-वह₀.

इसके अलावा, बाइनरी स्ट्रिंग एस और टी के दिए गए समुच्चय, निम्नलिखित समतुल्य हैं:<br />