कम्प्यूटेबिलिटी तर्क: Difference between revisions
(Created page with "{{distinguish|Computational logic}} {{One source|text=All references in this article are exclusively by a single author, G. Japaridze.|date=May 2020}} कम्प्यू...") |
No edit summary |
||
| Line 1: | Line 1: | ||
{{distinguish|Computational logic}} | {{distinguish|Computational logic}} | ||
[[कम्प्यूटेबिलिटी]] लॉजिक (सीओएल) शोध कार्यक्रम और गणितीय रूपरेखा है, जो कि कम्प्यूटेबिलिटी के व्यवस्थित औपचारिक सिद्धांत के रूप में तर्क को पुनर्विकसित करता है, जो कि [[शास्त्रीय तर्क]] के विपरीत है, जो सत्य का औपचारिक सिद्धांत है। इसे 2003 में जियोर्गी जैपरिडेज़ द्वारा पेश किया गया था और इसका नाम रखा गया था।<ref> G. Japaridze, ''Introduction to computability logic''. Annals of Pure and Applied Logic 123 (2003), pages 1–99. {{doi|10.1016/S0168-0072(03)00023-X}}</ref> शास्त्रीय तर्क में, सूत्र सही/गलत कथनों का प्रतिनिधित्व करते हैं। सीओएल में, सूत्र [[कम्प्यूटेशनल समस्या]]ओं का प्रतिनिधित्व करते हैं। शास्त्रीय तर्क में, किसी सूत्र की वैधता केवल उसके रूप पर निर्भर करती है, उसके अर्थ पर नहीं। सीओएल में, वैधता का अर्थ हमेशा गणना योग्य होना है। अधिक सामान्यतः, शास्त्रीय तर्क हमें बताता है कि किसी दिए गए कथन की सत्यता हमेशा अन्य कथनों के दिए गए सेट की सत्यता से मेल खाती है। इसी प्रकार, सीओएल हमें बताता है कि किसी दी गई समस्या ए की संगणनीयता हमेशा अन्य दी गई समस्याओं बी की संगणनीयता से अनुसरण करती है<sub>1</sub>,...,बी<sub>n</sub>. इसके अलावा, यह वास्तव में बी के किसी भी ज्ञात समाधान से ऐसे ए के लिए समाधान ([[कलन विधि]]) बनाने का समान तरीका प्रदान करता है<sub>1</sub>,...,बी<sub>n</sub>. | |||
[[कम्प्यूटेबिलिटी]] लॉजिक (सीओएल) | |||
सीओएल कम्प्यूटेशनल समस्याओं को उनके सबसे सामान्य - [[इंटरैक्टिव गणना]] अर्थ में तैयार करता है। सीओएल | सीओएल कम्प्यूटेशनल समस्याओं को उनके सबसे सामान्य - [[इंटरैक्टिव गणना]] अर्थ में तैयार करता है। सीओएल कम्प्यूटेशनल समस्या को मशीन द्वारा उसके पर्यावरण के विरुद्ध खेले जाने वाले खेल के रूप में परिभाषित करता है। ऐसी समस्या की गणना तब की जा सकती है जब कोई ऐसी मशीन हो जो पर्यावरण के हर संभावित व्यवहार के खिलाफ गेम जीतती हो। ऐसी गेम-प्लेइंग मशीन [[चर्च-ट्यूरिंग थीसिस]] को इंटरैक्टिव स्तर पर सामान्यीकृत करती है। सत्य की शास्त्रीय अवधारणा संगणनीयता का विशेष, शून्य-अंतःक्रियाशीलता-डिग्री वाला मामला बन जाती है। यह शास्त्रीय तर्क को CoL का विशेष टुकड़ा बनाता है। इस प्रकार सीओएल शास्त्रीय तर्क का [[रूढ़िवादी विस्तार]] है। संगणनीयता तर्क शास्त्रीय तर्क की तुलना में अधिक अभिव्यंजक, रचनात्मक और कम्प्यूटेशनल रूप से सार्थक है। शास्त्रीय तर्क के अलावा, [[स्वतंत्रता-अनुकूल तर्क]]|स्वतंत्रता-अनुकूल (आईएफ) तर्क और [[रैखिक तर्क]] और [[अंतर्ज्ञानवादी तर्क]] के कुछ उचित विस्तार भी सीओएल के प्राकृतिक टुकड़े बन जाते हैं।<ref>G. Japaridze, ''In the beginning was game semantics?''. Games: Unifying Logic, Language and Philosophy. O. Majer, A.-V. Pietarinen and T. Tulenheimo, eds. Springer 2009, pp. 249–350. {{doi|10.1007/978-1-4020-9374-6_11}} [https://arxiv.org/abs/cs/0507045 Prepublication]</ref><ref>G. Japaridze, ''The intuitionistic fragment of computability logic at the propositional level''. Annals of Pure and Applied Logic 147 (2007), pages 187–227. {{doi|10.1016/j.apal.2007.05.001}}</ref> इसलिए अंतर्ज्ञानवादी सत्य, रैखिक-तर्क सत्य और आईएफ-तर्क सत्य की सार्थक अवधारणाएं सीओएल के शब्दार्थ से प्राप्त की जा सकती हैं। | ||
सीओएल व्यवस्थित रूप से मूलभूत प्रश्न का उत्तर देता है कि क्या गणना की जा सकती है और कैसे; इस प्रकार सीओएल के कई अनुप्रयोग हैं, जैसे रचनात्मक व्यावहारिक सिद्धांत, ज्ञान आधार प्रणाली, योजना और कार्रवाई के लिए प्रणाली। इनमें से, अब तक केवल रचनात्मक व्यावहारिक सिद्धांतों में अनुप्रयोगों का बड़े पैमाने पर पता लगाया गया है: सीओएल-आधारित संख्या सिद्धांतों की | सीओएल व्यवस्थित रूप से मूलभूत प्रश्न का उत्तर देता है कि क्या गणना की जा सकती है और कैसे; इस प्रकार सीओएल के कई अनुप्रयोग हैं, जैसे रचनात्मक व्यावहारिक सिद्धांत, ज्ञान आधार प्रणाली, योजना और कार्रवाई के लिए प्रणाली। इनमें से, अब तक केवल रचनात्मक व्यावहारिक सिद्धांतों में अनुप्रयोगों का बड़े पैमाने पर पता लगाया गया है: सीओएल-आधारित संख्या सिद्धांतों की श्रृंखला, जिसे क्लैरिथमेटिक्स कहा जाता है, का निर्माण किया गया है।<ref>G. Japaridze, ''Introduction to clarithmetic I''. Information and Computation 209 (2011), pp. 1312–1354. {{Doi|10.1016/j.ic.2011.07.002}} [https://arxiv.org/abs/1003.4719 Prepublication]</ref><ref>G. Japaridze, ''[https://lmcs.episciences.org/2020/pdf Build your own clarithmetic I: Setup and completeness]''. Logical Methods is Computer Science 12 (2016), Issue 3, paper 8, pp. 1–59.</ref> कम्प्यूटेशनल और जटिलता-सैद्धांतिक रूप से शास्त्रीय-तर्क-आधारित पीनो सिद्धांतों और इसकी विविधताओं जैसे कि बंधे हुए अंकगणित की प्रणालियों के सार्थक विकल्प के रूप में। | ||
[[प्राकृतिक कटौती]] और अनुक्रमिक कैलकुलस जैसी पारंपरिक प्रमाण प्रणालियाँ सीओएल के गैर-तुच्छ अंशों को स्वयंसिद्ध करने के लिए अपर्याप्त हैं। इसके लिए प्रमाण के वैकल्पिक, अधिक सामान्य और लचीले तरीकों को विकसित करना आवश्यक हो गया है, जैसे कि [[सर्कुएंट कैलकुलस]]<ref>G. Japaridze, ''Introduction to cirquent calculus and abstract resource semantics''. Journal of Logic and Computation 16 (2006), pages 489–532. {{doi|10.1093/logcom/exl005}} [https://arxiv.org/abs/math/0506553 Prepublication]</ref><ref>G. Japaridze, ''The taming of recurrences in computability logic through cirquent calculus, Part I''. Archive for Mathematical Logic 52 (2013), pp. 173–212. {{Doi|10.1007/s00153-012-0313-8}} [https://arxiv.org/abs/1105.3853 Prepublication]</ref> | [[प्राकृतिक कटौती]] और अनुक्रमिक कैलकुलस जैसी पारंपरिक प्रमाण प्रणालियाँ सीओएल के गैर-तुच्छ अंशों को स्वयंसिद्ध करने के लिए अपर्याप्त हैं। इसके लिए प्रमाण के वैकल्पिक, अधिक सामान्य और लचीले तरीकों को विकसित करना आवश्यक हो गया है, जैसे कि [[सर्कुएंट कैलकुलस]]<ref>G. Japaridze, ''Introduction to cirquent calculus and abstract resource semantics''. Journal of Logic and Computation 16 (2006), pages 489–532. {{doi|10.1093/logcom/exl005}} [https://arxiv.org/abs/math/0506553 Prepublication]</ref><ref>G. Japaridze, ''The taming of recurrences in computability logic through cirquent calculus, Part I''. Archive for Mathematical Logic 52 (2013), pp. 173–212. {{Doi|10.1007/s00153-012-0313-8}} [https://arxiv.org/abs/1105.3853 Prepublication]</ref> | ||
==भाषा== | ==भाषा== | ||
[[File:Operators_of_computability_logic.png|thumb|संगणनीयता तर्क के संचालक: नाम, प्रतीक और रीडिंग]]सीओएल की पूरी भाषा शास्त्रीय प्रथम-क्रम तर्क की भाषा का विस्तार करती है। इसकी तार्किक शब्दावली में कई प्रकार के संयोजन, विच्छेदन, परिमाणक, निहितार्थ, निषेध और तथाकथित पुनरावृत्ति ऑपरेटर हैं। इस संग्रह में शास्त्रीय तर्क के सभी संयोजक और परिमाणक शामिल हैं। भाषा में भी दो प्रकार के अतार्किक परमाणु होते हैं: प्राथमिक और सामान्य। प्राथमिक परमाणु, जो शास्त्रीय तर्क के परमाणुओं के अलावा और कुछ नहीं हैं, प्राथमिक समस्याओं का प्रतिनिधित्व करते हैं, यानी, बिना किसी चाल वाले खेल जो सही होने पर मशीन द्वारा स्वचालित रूप से जीते जाते हैं और गलत होने पर हार जाते हैं। दूसरी ओर, सामान्य परमाणुओं की व्याख्या किसी भी खेल, प्राथमिक या गैर-प्राथमिक के रूप में की जा सकती है। शब्दार्थ और वाक्यात्मक रूप से, शास्त्रीय तर्क और कुछ नहीं बल्कि अपनी भाषा में सामान्य परमाणुओं को प्रतिबंधित करके और ¬, ∧, ∨, →, ∀, ∃ के अलावा अन्य सभी ऑपरेटरों को प्रतिबंधित करके प्राप्त CoL का टुकड़ा है। | [[File:Operators_of_computability_logic.png|thumb|संगणनीयता तर्क के संचालक: नाम, प्रतीक और रीडिंग]]सीओएल की पूरी भाषा शास्त्रीय प्रथम-क्रम तर्क की भाषा का विस्तार करती है। इसकी तार्किक शब्दावली में कई प्रकार के संयोजन, विच्छेदन, परिमाणक, निहितार्थ, निषेध और तथाकथित पुनरावृत्ति ऑपरेटर हैं। इस संग्रह में शास्त्रीय तर्क के सभी संयोजक और परिमाणक शामिल हैं। भाषा में भी दो प्रकार के अतार्किक परमाणु होते हैं: प्राथमिक और सामान्य। प्राथमिक परमाणु, जो शास्त्रीय तर्क के परमाणुओं के अलावा और कुछ नहीं हैं, प्राथमिक समस्याओं का प्रतिनिधित्व करते हैं, यानी, बिना किसी चाल वाले खेल जो सही होने पर मशीन द्वारा स्वचालित रूप से जीते जाते हैं और गलत होने पर हार जाते हैं। दूसरी ओर, सामान्य परमाणुओं की व्याख्या किसी भी खेल, प्राथमिक या गैर-प्राथमिक के रूप में की जा सकती है। शब्दार्थ और वाक्यात्मक रूप से, शास्त्रीय तर्क और कुछ नहीं बल्कि अपनी भाषा में सामान्य परमाणुओं को प्रतिबंधित करके और ¬, ∧, ∨, →, ∀, ∃ के अलावा अन्य सभी ऑपरेटरों को प्रतिबंधित करके प्राप्त CoL का टुकड़ा है। | ||
जैपरिडेज़ ने बार-बार बताया है कि सीओएल की भाषा ओपन-एंडेड है, और इसे और विस्तार से गुजरना पड़ सकता है। इस भाषा की अभिव्यक्ति के कारण, सीओएल में प्रगति, जैसे स्वयंसिद्धीकरण का निर्माण या सीओएल-आधारित व्यावहारिक सिद्धांतों का निर्माण, आमतौर पर भाषा के | जैपरिडेज़ ने बार-बार बताया है कि सीओएल की भाषा ओपन-एंडेड है, और इसे और विस्तार से गुजरना पड़ सकता है। इस भाषा की अभिव्यक्ति के कारण, सीओएल में प्रगति, जैसे स्वयंसिद्धीकरण का निर्माण या सीओएल-आधारित व्यावहारिक सिद्धांतों का निर्माण, आमतौर पर भाषा के या किसी अन्य उचित टुकड़े तक ही सीमित है। | ||
==शब्दार्थ== | ==शब्दार्थ== | ||
सीओएल के शब्दार्थ में अंतर्निहित खेलों को स्थिर खेल कहा जाता है। ऐसे खेलों में कोई बारी क्रम नहीं होता; | सीओएल के शब्दार्थ में अंतर्निहित खेलों को स्थिर खेल कहा जाता है। ऐसे खेलों में कोई बारी क्रम नहीं होता; खिलाड़ी हमेशा तब आगे बढ़ सकता है जब दूसरे खिलाड़ी सोच रहे हों। हालाँकि, स्थिर खेल कभी भी किसी खिलाड़ी को बहुत देर तक सोचने (अपनी चाल में देरी करने) के लिए दंडित नहीं करते हैं, इसलिए ऐसे खेल कभी भी गति की प्रतियोगिता नहीं बनते हैं। सभी प्राथमिक खेल स्वचालित रूप से स्थिर होते हैं, और इसलिए खेलों को सामान्य परमाणुओं की व्याख्या करने की अनुमति दी जाती है। | ||
स्थिर खेलों में दो खिलाड़ी होते हैं: मशीन और पर्यावरण। मशीन केवल एल्गोरिथम रणनीतियों का पालन कर सकती है, जबकि पर्यावरण के व्यवहार पर कोई प्रतिबंध नहीं है। प्रत्येक रन (खेल) इनमें से | स्थिर खेलों में दो खिलाड़ी होते हैं: मशीन और पर्यावरण। मशीन केवल एल्गोरिथम रणनीतियों का पालन कर सकती है, जबकि पर्यावरण के व्यवहार पर कोई प्रतिबंध नहीं है। प्रत्येक रन (खेल) इनमें से खिलाड़ी द्वारा जीता जाता है और दूसरे द्वारा हारा जाता है। | ||
सीओएल के तार्किक ऑपरेटरों को खेलों पर संचालन के रूप में समझा जाता है। यहां हम अनौपचारिक रूप से उनमें से कुछ परिचालनों का सर्वेक्षण करते हैं। सरलता के लिए हम मानते हैं कि प्रवचन का क्षेत्र हमेशा सभी प्राकृतिक संख्याओं का समुच्चय होता है: {0,1,2,...}। | सीओएल के तार्किक ऑपरेटरों को खेलों पर संचालन के रूप में समझा जाता है। यहां हम अनौपचारिक रूप से उनमें से कुछ परिचालनों का सर्वेक्षण करते हैं। सरलता के लिए हम मानते हैं कि प्रवचन का क्षेत्र हमेशा सभी प्राकृतिक संख्याओं का समुच्चय होता है: {0,1,2,...}। | ||
| Line 24: | Line 21: | ||
नकार (नहीं) का ऑपरेशन दो खिलाड़ियों की भूमिकाओं को बदल देता है, मशीन की चालों और जीतों को पर्यावरण की चालों और जीतों में बदल देता है, और इसके विपरीत। उदाहरण के लिए, यदि श्वेत खिलाड़ी के दृष्टिकोण से शतरंज शतरंज का खेल है (लेकिन संबंधों को खारिज कर दिया गया है), तो काले खिलाड़ी के दृष्टिकोण से शतरंज भी वही खेल है। | नकार (नहीं) का ऑपरेशन दो खिलाड़ियों की भूमिकाओं को बदल देता है, मशीन की चालों और जीतों को पर्यावरण की चालों और जीतों में बदल देता है, और इसके विपरीत। उदाहरण के लिए, यदि श्वेत खिलाड़ी के दृष्टिकोण से शतरंज शतरंज का खेल है (लेकिन संबंधों को खारिज कर दिया गया है), तो काले खिलाड़ी के दृष्टिकोण से शतरंज भी वही खेल है। | ||
समानांतर संयोजन ∧ ( पांड ) और समानांतर विच्छेदन ∨ ( पोर ) खेलों को समानांतर रूप से जोड़ते हैं। A∧B या A∨B का | समानांतर संयोजन ∧ ( पांड ) और समानांतर विच्छेदन ∨ ( पोर ) खेलों को समानांतर रूप से जोड़ते हैं। A∧B या A∨B का रन दो संयोजनों में साथ होने वाला खेल है। मशीन A∧B जीतती है यदि वह इन दोनों को जीतती है। मशीन A∨B जीतती है यदि वह उनमें से कम से कम जीतती है। उदाहरण के लिए, शतरंज∨¬शतरंज दो बोर्डों पर खेला जाने वाला खेल है, सफेद और काला खेला जाता है, और जहां मशीन का काम कम से कम बोर्ड पर जीतना है। इस तरह का खेल आसानी से जीता जा सकता है, भले ही प्रतिद्वंद्वी कोई भी हो, उसकी चालों को बोर्ड से दूसरे बोर्ड पर कॉपी करके। | ||
समानांतर निहितार्थ ऑपरेटर → (पिम्प्लिकेशन) को A→B = ¬A∨B द्वारा परिभाषित किया गया है। इस ऑपरेशन का सहज अर्थ बी को ए में कम करना है, यानी, जब तक प्रतिद्वंद्वी बी को हल करता है तब तक ए को हल करना है। | समानांतर निहितार्थ ऑपरेटर → (पिम्प्लिकेशन) को A→B = ¬A∨B द्वारा परिभाषित किया गया है। इस ऑपरेशन का सहज अर्थ बी को ए में कम करना है, यानी, जब तक प्रतिद्वंद्वी बी को हल करता है तब तक ए को हल करना है। | ||
समानांतर परिमाणक <big><big>∧</big></big> ( pall ) और <big><big>∨</big></big> ( pexists ) को <big><big> द्वारा परिभाषित किया जा सकता है ∧</big></big>xA(x) = A(0)∧A(1)∧A(2)∧... और <big><big>∨</big></big>xA( x) = A(0)∨A(1)∨A(2)∨.... इस प्रकार ये A(0),A(1),A(2),... के | समानांतर परिमाणक <big><big>∧</big></big> ( pall ) और <big><big>∨</big></big> ( pexists ) को <big><big>द्वारा परिभाषित किया जा सकता है ∧</big></big>xA(x) = A(0)∧A(1)∧A(2)∧... और <big><big>∨</big></big>xA( x) = A(0)∨A(1)∨A(2)∨.... इस प्रकार ये A(0),A(1),A(2),... के साथ नाटक हैं, प्रत्येक पर अलग बोर्ड. यदि मशीन इन सभी खेलों को जीतती है तो वह <big><big>∧</big></big>xA(x) जीतती है, और <big><big>∨</big></big>xA(x) अगर यह कुछ जीतता है। | ||
दूसरी ओर, ब्लाइंड क्वांटिफायर ∀ ( ब्लॉल ) और ∃ ( ब्लेक्सिस्ट ) सिंगल-बोर्ड गेम उत्पन्न करते हैं। ∀xA(x) या ∃xA(x) का | दूसरी ओर, ब्लाइंड क्वांटिफायर ∀ ( ब्लॉल ) और ∃ ( ब्लेक्सिस्ट ) सिंगल-बोर्ड गेम उत्पन्न करते हैं। ∀xA(x) या ∃xA(x) का रन, A का एकल रन है। मशीन ∀xA(x) जीतती है (सम्मान ∃xA(x)) यदि ऐसा रन A(x) का जीता हुआ रन है ) x के सभी (कम से कम के संबंध में) संभावित मानों के लिए, और ∃xA(x) जीतता है यदि यह कम से कम के लिए सत्य है। | ||
अब तक वर्णित सभी ऑपरेटर बिल्कुल अपने शास्त्रीय समकक्षों की तरह व्यवहार करते हैं जब उन्हें प्राथमिक (मूवलेस) गेम पर लागू किया जाता है, और समान सिद्धांतों को मान्य करते हैं। यही कारण है कि सीओएल उन ऑपरेटरों के लिए उन्हीं प्रतीकों का उपयोग करता है जैसा कि शास्त्रीय तर्क करता है। हालाँकि, जब ऐसे ऑपरेटरों को गैर-प्राथमिक खेलों पर लागू किया जाता है, तो उनका व्यवहार शास्त्रीय नहीं रह जाता है। इसलिए, उदाहरण के लिए, यदि p | अब तक वर्णित सभी ऑपरेटर बिल्कुल अपने शास्त्रीय समकक्षों की तरह व्यवहार करते हैं जब उन्हें प्राथमिक (मूवलेस) गेम पर लागू किया जाता है, और समान सिद्धांतों को मान्य करते हैं। यही कारण है कि सीओएल उन ऑपरेटरों के लिए उन्हीं प्रतीकों का उपयोग करता है जैसा कि शास्त्रीय तर्क करता है। हालाँकि, जब ऐसे ऑपरेटरों को गैर-प्राथमिक खेलों पर लागू किया जाता है, तो उनका व्यवहार शास्त्रीय नहीं रह जाता है। इसलिए, उदाहरण के लिए, यदि p प्राथमिक परमाणु है और P सामान्य परमाणु है, तो p→p∧p वैध है जबकि P→P∧P मान्य नहीं है। हालाँकि, बहिष्कृत मध्य P∨¬P का सिद्धांत वैध बना हुआ है। विच्छेदन के अन्य तीनों प्रकारों (विकल्प, अनुक्रमिक और टॉगलिंग) के साथ भी यही सिद्धांत अमान्य है। | ||
गेम A और B का चॉइस डिसजंक्शन ⊔ ( chor ), जिसे A⊔B लिखा जाता है, | गेम A और B का चॉइस डिसजंक्शन ⊔ ( chor ), जिसे A⊔B लिखा जाता है, ऐसा गेम है, जहां जीतने के लिए मशीन को दो डिसजंक्ट्स में से को चुनना होता है और फिर चुने गए घटक में जीत हासिल करनी होती है। अनुक्रमिक विच्छेदन (सोर) ए<small>ᐁ</small>बी ए के रूप में शुरू होता है; यह भी ए के रूप में समाप्त होता है जब तक कि मशीन स्विच मूव नहीं करती है, जिस स्थिति में ए को छोड़ दिया जाता है और खेल फिर से शुरू होता है और बी के रूप में जारी रहता है। टॉगलिंग डिसजंक्शन (टोर) ए⩛बी में, मशीन ए और बी के बीच किसी भी परिमित संख्या में स्विच कर सकती है कई बार. प्रत्येक डिसजंक्शन ऑपरेटर का अपना दोहरा संयोजन होता है, जो दो खिलाड़ियों की भूमिकाओं को आपस में बदलकर प्राप्त किया जाता है। संगत परिमाणकों को आगे अनंत संयोजनों या वियोजनों के रूप में उसी तरह परिभाषित किया जा सकता है जैसे समानांतर परिमाणकों के मामले में होता है। प्रत्येक प्रकार का विच्छेदन भी उसी तरह से समान निहितार्थ संचालन को प्रेरित करता है जैसे कि यह समानांतर निहितार्थ → के मामले में था। उदाहरण के लिए, विकल्प निहितार्थ (चिम्प्लिकेशन) A⊐B को ¬A⊔B के रूप में परिभाषित किया गया है। | ||
A की समानांतर पुनरावृत्ति (precurrence) को अनंत समानांतर संयोजन A∧A∧A∧ के रूप में परिभाषित किया जा सकता है... अनुक्रमिक (recurrence) और टॉगल (trecurrence) प्रकार की पुनरावृत्ति को समान रूप से परिभाषित किया जा सकता है। | A की समानांतर पुनरावृत्ति (precurrence) को अनंत समानांतर संयोजन A∧A∧A∧ के रूप में परिभाषित किया जा सकता है... अनुक्रमिक (recurrence) और टॉगल (trecurrence) प्रकार की पुनरावृत्ति को समान रूप से परिभाषित किया जा सकता है। | ||
कोरकरेंस ऑपरेटरों को अनंत विच्छेदन के रूप में परिभाषित किया जा सकता है। शाखाबद्ध पुनरावृत्ति ( brecurrence ) <big>⫰</big>, जो पुनरावृत्ति का सबसे मजबूत प्रकार है, इसका कोई संगत संयोजन नहीं है। <बिग>⫰</बिग>ए | कोरकरेंस ऑपरेटरों को अनंत विच्छेदन के रूप में परिभाषित किया जा सकता है। शाखाबद्ध पुनरावृत्ति ( brecurrence ) <big>⫰</big>, जो पुनरावृत्ति का सबसे मजबूत प्रकार है, इसका कोई संगत संयोजन नहीं है। <बिग>⫰</बिग>ए ऐसा खेल है जो ए के रूप में शुरू होता है और आगे बढ़ता है। हालांकि, किसी भी समय, पर्यावरण को प्रतिकृति चाल बनाने की अनुमति दी जाती है, जो ए की तत्कालीन-वर्तमान स्थिति की दो प्रतियां बनाती है, इस प्रकार विभाजित हो जाती है सामान्य अतीत लेकिन संभवतः अलग-अलग भविष्य के विकास के साथ दो समानांतर धागों में नाटक। उसी तरह, पर्यावरण किसी भी थ्रेड की किसी भी स्थिति को दोहरा सकता है, इस प्रकार ए के अधिक से अधिक थ्रेड बना सकता है। उन थ्रेड को समानांतर में खेला जाता है, और मशीन को <बिग में विजेता बनने के लिए सभी थ्रेड में ए जीतने की आवश्यकता होती है >⫰ए. ब्रांचिंग कोरकरेंस (cobrecurrence) <big>⫯</big> को मशीन और पर्यावरण को इंटरचेंज करके सममित रूप से परिभाषित किया गया है। | ||
प्रत्येक प्रकार की पुनरावृत्ति निहितार्थ के संबंधित कमजोर संस्करण और निषेध के कमजोर संस्करण को प्रेरित करती है। पहले को अनुप्रमाणन कहा जाता है, और बाद को खंडन कहा जाता है। ब्रांचिंग रिफ्यूटेशन ( ब्रिम्प्लिकेशन ) ए<बिग>⟜</बिग>बी और कुछ नहीं बल्कि <बिग>⫰</बिग>ए→बी है, और ए का ब्रांचिंग रिफ्यूटेशन ( ब्रेफ्यूटेशन ) ए<बिग>⟜</बिग> है ⊥, जहां ⊥ हमेशा हारा हुआ प्राथमिक खेल है। इसी प्रकार अन्य सभी प्रकार के प्रतिरूपण और खंडन के लिए भी। | प्रत्येक प्रकार की पुनरावृत्ति निहितार्थ के संबंधित कमजोर संस्करण और निषेध के कमजोर संस्करण को प्रेरित करती है। पहले को अनुप्रमाणन कहा जाता है, और बाद को खंडन कहा जाता है। ब्रांचिंग रिफ्यूटेशन ( ब्रिम्प्लिकेशन ) ए<बिग>⟜</बिग>बी और कुछ नहीं बल्कि <बिग>⫰</बिग>ए→बी है, और ए का ब्रांचिंग रिफ्यूटेशन ( ब्रेफ्यूटेशन ) ए<बिग>⟜</बिग> है ⊥, जहां ⊥ हमेशा हारा हुआ प्राथमिक खेल है। इसी प्रकार अन्य सभी प्रकार के प्रतिरूपण और खंडन के लिए भी। | ||
==एक समस्या विनिर्देशन उपकरण के रूप में== | ==एक समस्या विनिर्देशन उपकरण के रूप में== | ||
सीओएल की भाषा साहित्य में स्थापित नामों के साथ या उनके बिना, अनंत प्रकार की कम्प्यूटेशनल समस्याओं को निर्दिष्ट करने का | सीओएल की भाषा साहित्य में स्थापित नामों के साथ या उनके बिना, अनंत प्रकार की कम्प्यूटेशनल समस्याओं को निर्दिष्ट करने का व्यवस्थित तरीका प्रदान करती है। नीचे कुछ उदाहरण हैं. | ||
मान लीजिए f | मान लीजिए f एकात्मक फलन है। f की गणना करने की समस्या को <big><big>⊓</big></big>x<big><big>⊔</big></big>y(y=f(x)) के रूप में लिखा जाएगा। सीओएल के शब्दार्थ के अनुसार, यह ऐसा खेल है जहां पहली चाल (इनपुट) पर्यावरण द्वारा होती है, जिसे x के लिए मान m चुनना चाहिए। सहज रूप से, इसका मतलब मशीन से f(m) का मान बताने के लिए कहना है। खेल <big><big>⊔</big></big>y(y=f(m)) के रूप में जारी है। अब मशीन से चाल (आउटपुट) की उम्मीद की जाती है, जिसे y के लिए मान n चुनना चाहिए। इसका तात्पर्य यह है कि n, f(m) का मान है। गेम को अब प्रारंभिक n=f(m) पर लाया गया है, जिसे मशीन द्वारा जीता जाता है यदि और केवल तभी जब n वास्तव में f(m) का मान हो। | ||
मान लीजिए p | मान लीजिए p एकात्मक विधेय है। फिर <big><big>⊓</big></big>x(p(x)⊔¬p(x)) Decidability (तर्क) p की समस्या को व्यक्त करता है, <big><big>⊓</big></big>x(p(x)&<small>ᐁ</small>¬p(x)) पुनरावर्ती रूप से गणना योग्य सेट p की समस्या को व्यक्त करता है, और <big><big>⊓</big></big>x(p(x)⩛¬p(x)) सीमा p में गणना की समस्या को व्यक्त करता है। | ||
मान लीजिए कि p और q दो एकात्मक विधेय हैं। फिर <big><big>⊓</big></big>x(p(x)⊔¬p(x))<big>⟜</big><big><big>⊓</big></big>x(q(x)⊔¬q(x)) [[ ट्यूरिंग में कमी ]] की समस्या को व्यक्त करता है | ट्यूरिंग-कम करने वाले q को p (इस अर्थ में कि q ट्यूरिंग को p में रिड्यूस करने योग्य है यदि और केवल यदि इंटरैक्टिव समस्या <big><big>⊓</big></big >x(p(x)⊔¬p(x))<big>⟜</big><big><big>⊓</big></big>x(q(x)⊔¬q(x)) गणना योग्य है)। <big><big>⊓</big></big>x(p(x)⊔¬p(x))<big>→</big><big><big>⊓</big></big>x(q(x)⊔¬q(x)) वही करता है लेकिन ट्यूरिंग रिडक्शन के मजबूत संस्करण के लिए जहां p के लिए ओरेकल से केवल | मान लीजिए कि p और q दो एकात्मक विधेय हैं। फिर <big><big>⊓</big></big>x(p(x)⊔¬p(x))<big>⟜</big><big><big>⊓</big></big>x(q(x)⊔¬q(x)) [[ ट्यूरिंग में कमी |ट्यूरिंग में कमी]] की समस्या को व्यक्त करता है | ट्यूरिंग-कम करने वाले q को p (इस अर्थ में कि q ट्यूरिंग को p में रिड्यूस करने योग्य है यदि और केवल यदि इंटरैक्टिव समस्या <big><big>⊓</big></big >x(p(x)⊔¬p(x))<big>⟜</big><big><big>⊓</big></big>x(q(x)⊔¬q(x)) गणना योग्य है)। <big><big>⊓</big></big>x(p(x)⊔¬p(x))<big>→</big><big><big>⊓</big></big>x(q(x)⊔¬q(x)) वही करता है लेकिन ट्यूरिंग रिडक्शन के मजबूत संस्करण के लिए जहां p के लिए ओरेकल से केवल बार पूछताछ की जा सकती है। <big><big>⊓</big></big>x<big><big>⊔</big></big>y(q(x)↔p(y)) [[अनेक-एक कमी]]|मैनी-वन कमिंग क्यू टू पी की समस्या के लिए भी यही करता है। अधिक जटिल अभिव्यक्तियों के साथ कोई भी कम्प्यूटेशनल समस्याओं पर सभी प्रकार के नामहीन लेकिन संभावित रूप से सार्थक संबंधों और संचालन को पकड़ सकता है, जैसे, उदाहरण के लिए, अर्ध-निर्णय आर की समस्या को ट्यूरिंग-कम करना, क्यू को पी में कई-एक को कम करने की समस्या को कम करना। मशीन के काम पर समय या स्थान प्रतिबंध लगाने से, ऐसे संबंधों और संचालन के जटिलता-सैद्धांतिक समकक्ष प्राप्त होते हैं। | ||
==समस्या समाधान उपकरण के रूप में== | ==समस्या समाधान उपकरण के रूप में== | ||
सीओएल के विभिन्न टुकड़ों के लिए ज्ञात डिडक्टिव सिस्टम में यह गुण होता है कि सिस्टम में किसी समस्या के प्रमाण से | सीओएल के विभिन्न टुकड़ों के लिए ज्ञात डिडक्टिव सिस्टम में यह गुण होता है कि सिस्टम में किसी समस्या के प्रमाण से समाधान (एल्गोरिदम) स्वचालित रूप से निकाला जा सकता है। यह संपत्ति उन प्रणालियों पर आधारित सभी लागू सिद्धांतों द्वारा विरासत में मिली है। इसलिए, किसी दी गई समस्या का समाधान खोजने के लिए, इसे सीओएल की भाषा में व्यक्त करना और फिर उस अभिव्यक्ति का प्रमाण ढूंढना पर्याप्त है। इस घटना को देखने का दूसरा तरीका कार्यक्रम विनिर्देश (लक्ष्य) के रूप में सीओएल के सूत्र जी के बारे में सोचना है। फिर G का प्रमाण है - अधिक सटीक रूप से, इसका अनुवाद उस विनिर्देश को पूरा करने वाला प्रोग्राम है। यह सत्यापित करने की कोई आवश्यकता नहीं है कि विनिर्देश पूरा हो गया है, क्योंकि प्रमाण ही, वास्तव में, ऐसा सत्यापन है। | ||
सीओएल-आधारित अनुप्रयुक्त सिद्धांतों के उदाहरण तथाकथित क्लैरिथमेटिक्स हैं। ये सीओएल पर आधारित संख्या सिद्धांत हैं, उसी अर्थ में जैसे पीनो अंकगणित पीए शास्त्रीय तर्क पर आधारित है। ऐसी प्रणाली आमतौर पर पीए का | सीओएल-आधारित अनुप्रयुक्त सिद्धांतों के उदाहरण तथाकथित क्लैरिथमेटिक्स हैं। ये सीओएल पर आधारित संख्या सिद्धांत हैं, उसी अर्थ में जैसे पीनो अंकगणित पीए शास्त्रीय तर्क पर आधारित है। ऐसी प्रणाली आमतौर पर पीए का रूढ़िवादी विस्तार है। इसमें आम तौर पर सभी पीनो स्वयंसिद्धों को शामिल किया जाता है, और उनमें या दो अतिरिक्त-पीनो स्वयंसिद्धों को जोड़ा जाता है जैसे कि <big><big>⊓</big></big>x<big><big>⊔</big></big>y(y=x') जो उत्तराधिकारी फ़ंक्शन की संगणना को व्यक्त करता है। आमतौर पर इसमें अनुमान के या दो गैर-तार्किक नियम भी होते हैं, जैसे प्रेरण या समझ के रचनात्मक संस्करण। ऐसे नियमों में नियमित बदलाव के माध्यम से कोई व्यक्ति या किसी अन्य इंटरैक्टिव कम्प्यूटेशनल जटिलता वर्ग सी को चिह्नित करने वाली ध्वनि और पूर्ण प्रणाली प्राप्त कर सकता है। यह इस अर्थ में है कि समस्या सी से संबंधित है यदि और केवल अगर सिद्धांत में इसका प्रमाण है। इसलिए, इस तरह के सिद्धांत का उपयोग न केवल एल्गोरिथम समाधान खोजने के लिए किया जा सकता है, बल्कि मांग पर कुशल समाधान भी खोजा जा सकता है, जैसे कि बहुपद समय या लघुगणकीय स्थान में चलने वाले समाधान। यह बताया जाना चाहिए कि सभी क्लैरिथमेटिकल सिद्धांत समान तार्किक अभिधारणाओं को साझा करते हैं, और केवल उनके गैर-तार्किक अभिधारणाएं लक्ष्य जटिलता वर्ग के आधार पर भिन्न होती हैं। समान आकांक्षाओं (जैसे कि सीमित अंकगणित) के साथ अन्य दृष्टिकोणों से उनकी उल्लेखनीय विशिष्ट विशेषता यह है कि वे पीए को कमजोर करने के बजाय विस्तार करते हैं, बाद की पूर्ण कटौतीत्मक शक्ति और सुविधा को संरक्षित करते हैं। | ||
==यह भी देखें== | ==यह भी देखें== | ||
| Line 64: | Line 61: | ||
==संदर्भ== | ==संदर्भ== | ||
{{Reflist}} | {{Reflist}} | ||
==बाहरी संबंध== | ==बाहरी संबंध== | ||
*[http://www.csc.villanova.edu/~japaridz/CL/ Computability Logic Homepage] Comprehensive survey of the subject. | *[http://www.csc.villanova.edu/~japaridz/CL/ Computability Logic Homepage] Comprehensive survey of the subject. | ||
| Line 73: | Line 68: | ||
* [http://www.mathnet.ru/php/presentation.phtml?option_lang=eng&presentid=4373 On abstract resource semantics and computabilty logic] Video lecture by N.Vereshchagin. | * [http://www.mathnet.ru/php/presentation.phtml?option_lang=eng&presentid=4373 On abstract resource semantics and computabilty logic] Video lecture by N.Vereshchagin. | ||
*[https://arxiv.org/abs/1612.04513 A Survey of Computability Logic] (PDF) Downloadable equivalent of the above homepage. | *[https://arxiv.org/abs/1612.04513 A Survey of Computability Logic] (PDF) Downloadable equivalent of the above homepage. | ||
[[Category: कम्प्यूटेबिलिटी सिद्धांत]] [[Category: कंप्यूटर विज्ञान में तर्क]] [[Category: गैर-शास्त्रीय तर्क]] | [[Category: कम्प्यूटेबिलिटी सिद्धांत]] [[Category: कंप्यूटर विज्ञान में तर्क]] [[Category: गैर-शास्त्रीय तर्क]] | ||
Revision as of 21:43, 25 July 2023
कम्प्यूटेबिलिटी लॉजिक (सीओएल) शोध कार्यक्रम और गणितीय रूपरेखा है, जो कि कम्प्यूटेबिलिटी के व्यवस्थित औपचारिक सिद्धांत के रूप में तर्क को पुनर्विकसित करता है, जो कि शास्त्रीय तर्क के विपरीत है, जो सत्य का औपचारिक सिद्धांत है। इसे 2003 में जियोर्गी जैपरिडेज़ द्वारा पेश किया गया था और इसका नाम रखा गया था।[1] शास्त्रीय तर्क में, सूत्र सही/गलत कथनों का प्रतिनिधित्व करते हैं। सीओएल में, सूत्र कम्प्यूटेशनल समस्याओं का प्रतिनिधित्व करते हैं। शास्त्रीय तर्क में, किसी सूत्र की वैधता केवल उसके रूप पर निर्भर करती है, उसके अर्थ पर नहीं। सीओएल में, वैधता का अर्थ हमेशा गणना योग्य होना है। अधिक सामान्यतः, शास्त्रीय तर्क हमें बताता है कि किसी दिए गए कथन की सत्यता हमेशा अन्य कथनों के दिए गए सेट की सत्यता से मेल खाती है। इसी प्रकार, सीओएल हमें बताता है कि किसी दी गई समस्या ए की संगणनीयता हमेशा अन्य दी गई समस्याओं बी की संगणनीयता से अनुसरण करती है1,...,बीn. इसके अलावा, यह वास्तव में बी के किसी भी ज्ञात समाधान से ऐसे ए के लिए समाधान (कलन विधि) बनाने का समान तरीका प्रदान करता है1,...,बीn.
सीओएल कम्प्यूटेशनल समस्याओं को उनके सबसे सामान्य - इंटरैक्टिव गणना अर्थ में तैयार करता है। सीओएल कम्प्यूटेशनल समस्या को मशीन द्वारा उसके पर्यावरण के विरुद्ध खेले जाने वाले खेल के रूप में परिभाषित करता है। ऐसी समस्या की गणना तब की जा सकती है जब कोई ऐसी मशीन हो जो पर्यावरण के हर संभावित व्यवहार के खिलाफ गेम जीतती हो। ऐसी गेम-प्लेइंग मशीन चर्च-ट्यूरिंग थीसिस को इंटरैक्टिव स्तर पर सामान्यीकृत करती है। सत्य की शास्त्रीय अवधारणा संगणनीयता का विशेष, शून्य-अंतःक्रियाशीलता-डिग्री वाला मामला बन जाती है। यह शास्त्रीय तर्क को CoL का विशेष टुकड़ा बनाता है। इस प्रकार सीओएल शास्त्रीय तर्क का रूढ़िवादी विस्तार है। संगणनीयता तर्क शास्त्रीय तर्क की तुलना में अधिक अभिव्यंजक, रचनात्मक और कम्प्यूटेशनल रूप से सार्थक है। शास्त्रीय तर्क के अलावा, स्वतंत्रता-अनुकूल तर्क|स्वतंत्रता-अनुकूल (आईएफ) तर्क और रैखिक तर्क और अंतर्ज्ञानवादी तर्क के कुछ उचित विस्तार भी सीओएल के प्राकृतिक टुकड़े बन जाते हैं।[2][3] इसलिए अंतर्ज्ञानवादी सत्य, रैखिक-तर्क सत्य और आईएफ-तर्क सत्य की सार्थक अवधारणाएं सीओएल के शब्दार्थ से प्राप्त की जा सकती हैं।
सीओएल व्यवस्थित रूप से मूलभूत प्रश्न का उत्तर देता है कि क्या गणना की जा सकती है और कैसे; इस प्रकार सीओएल के कई अनुप्रयोग हैं, जैसे रचनात्मक व्यावहारिक सिद्धांत, ज्ञान आधार प्रणाली, योजना और कार्रवाई के लिए प्रणाली। इनमें से, अब तक केवल रचनात्मक व्यावहारिक सिद्धांतों में अनुप्रयोगों का बड़े पैमाने पर पता लगाया गया है: सीओएल-आधारित संख्या सिद्धांतों की श्रृंखला, जिसे क्लैरिथमेटिक्स कहा जाता है, का निर्माण किया गया है।[4][5] कम्प्यूटेशनल और जटिलता-सैद्धांतिक रूप से शास्त्रीय-तर्क-आधारित पीनो सिद्धांतों और इसकी विविधताओं जैसे कि बंधे हुए अंकगणित की प्रणालियों के सार्थक विकल्प के रूप में।
प्राकृतिक कटौती और अनुक्रमिक कैलकुलस जैसी पारंपरिक प्रमाण प्रणालियाँ सीओएल के गैर-तुच्छ अंशों को स्वयंसिद्ध करने के लिए अपर्याप्त हैं। इसके लिए प्रमाण के वैकल्पिक, अधिक सामान्य और लचीले तरीकों को विकसित करना आवश्यक हो गया है, जैसे कि सर्कुएंट कैलकुलस[6][7]
भाषा
सीओएल की पूरी भाषा शास्त्रीय प्रथम-क्रम तर्क की भाषा का विस्तार करती है। इसकी तार्किक शब्दावली में कई प्रकार के संयोजन, विच्छेदन, परिमाणक, निहितार्थ, निषेध और तथाकथित पुनरावृत्ति ऑपरेटर हैं। इस संग्रह में शास्त्रीय तर्क के सभी संयोजक और परिमाणक शामिल हैं। भाषा में भी दो प्रकार के अतार्किक परमाणु होते हैं: प्राथमिक और सामान्य। प्राथमिक परमाणु, जो शास्त्रीय तर्क के परमाणुओं के अलावा और कुछ नहीं हैं, प्राथमिक समस्याओं का प्रतिनिधित्व करते हैं, यानी, बिना किसी चाल वाले खेल जो सही होने पर मशीन द्वारा स्वचालित रूप से जीते जाते हैं और गलत होने पर हार जाते हैं। दूसरी ओर, सामान्य परमाणुओं की व्याख्या किसी भी खेल, प्राथमिक या गैर-प्राथमिक के रूप में की जा सकती है। शब्दार्थ और वाक्यात्मक रूप से, शास्त्रीय तर्क और कुछ नहीं बल्कि अपनी भाषा में सामान्य परमाणुओं को प्रतिबंधित करके और ¬, ∧, ∨, →, ∀, ∃ के अलावा अन्य सभी ऑपरेटरों को प्रतिबंधित करके प्राप्त CoL का टुकड़ा है।
जैपरिडेज़ ने बार-बार बताया है कि सीओएल की भाषा ओपन-एंडेड है, और इसे और विस्तार से गुजरना पड़ सकता है। इस भाषा की अभिव्यक्ति के कारण, सीओएल में प्रगति, जैसे स्वयंसिद्धीकरण का निर्माण या सीओएल-आधारित व्यावहारिक सिद्धांतों का निर्माण, आमतौर पर भाषा के या किसी अन्य उचित टुकड़े तक ही सीमित है।
शब्दार्थ
सीओएल के शब्दार्थ में अंतर्निहित खेलों को स्थिर खेल कहा जाता है। ऐसे खेलों में कोई बारी क्रम नहीं होता; खिलाड़ी हमेशा तब आगे बढ़ सकता है जब दूसरे खिलाड़ी सोच रहे हों। हालाँकि, स्थिर खेल कभी भी किसी खिलाड़ी को बहुत देर तक सोचने (अपनी चाल में देरी करने) के लिए दंडित नहीं करते हैं, इसलिए ऐसे खेल कभी भी गति की प्रतियोगिता नहीं बनते हैं। सभी प्राथमिक खेल स्वचालित रूप से स्थिर होते हैं, और इसलिए खेलों को सामान्य परमाणुओं की व्याख्या करने की अनुमति दी जाती है।
स्थिर खेलों में दो खिलाड़ी होते हैं: मशीन और पर्यावरण। मशीन केवल एल्गोरिथम रणनीतियों का पालन कर सकती है, जबकि पर्यावरण के व्यवहार पर कोई प्रतिबंध नहीं है। प्रत्येक रन (खेल) इनमें से खिलाड़ी द्वारा जीता जाता है और दूसरे द्वारा हारा जाता है।
सीओएल के तार्किक ऑपरेटरों को खेलों पर संचालन के रूप में समझा जाता है। यहां हम अनौपचारिक रूप से उनमें से कुछ परिचालनों का सर्वेक्षण करते हैं। सरलता के लिए हम मानते हैं कि प्रवचन का क्षेत्र हमेशा सभी प्राकृतिक संख्याओं का समुच्चय होता है: {0,1,2,...}।
नकार (नहीं) का ऑपरेशन दो खिलाड़ियों की भूमिकाओं को बदल देता है, मशीन की चालों और जीतों को पर्यावरण की चालों और जीतों में बदल देता है, और इसके विपरीत। उदाहरण के लिए, यदि श्वेत खिलाड़ी के दृष्टिकोण से शतरंज शतरंज का खेल है (लेकिन संबंधों को खारिज कर दिया गया है), तो काले खिलाड़ी के दृष्टिकोण से शतरंज भी वही खेल है।
समानांतर संयोजन ∧ ( पांड ) और समानांतर विच्छेदन ∨ ( पोर ) खेलों को समानांतर रूप से जोड़ते हैं। A∧B या A∨B का रन दो संयोजनों में साथ होने वाला खेल है। मशीन A∧B जीतती है यदि वह इन दोनों को जीतती है। मशीन A∨B जीतती है यदि वह उनमें से कम से कम जीतती है। उदाहरण के लिए, शतरंज∨¬शतरंज दो बोर्डों पर खेला जाने वाला खेल है, सफेद और काला खेला जाता है, और जहां मशीन का काम कम से कम बोर्ड पर जीतना है। इस तरह का खेल आसानी से जीता जा सकता है, भले ही प्रतिद्वंद्वी कोई भी हो, उसकी चालों को बोर्ड से दूसरे बोर्ड पर कॉपी करके।
समानांतर निहितार्थ ऑपरेटर → (पिम्प्लिकेशन) को A→B = ¬A∨B द्वारा परिभाषित किया गया है। इस ऑपरेशन का सहज अर्थ बी को ए में कम करना है, यानी, जब तक प्रतिद्वंद्वी बी को हल करता है तब तक ए को हल करना है।
समानांतर परिमाणक ∧ ( pall ) और ∨ ( pexists ) को द्वारा परिभाषित किया जा सकता है ∧xA(x) = A(0)∧A(1)∧A(2)∧... और ∨xA( x) = A(0)∨A(1)∨A(2)∨.... इस प्रकार ये A(0),A(1),A(2),... के साथ नाटक हैं, प्रत्येक पर अलग बोर्ड. यदि मशीन इन सभी खेलों को जीतती है तो वह ∧xA(x) जीतती है, और ∨xA(x) अगर यह कुछ जीतता है।
दूसरी ओर, ब्लाइंड क्वांटिफायर ∀ ( ब्लॉल ) और ∃ ( ब्लेक्सिस्ट ) सिंगल-बोर्ड गेम उत्पन्न करते हैं। ∀xA(x) या ∃xA(x) का रन, A का एकल रन है। मशीन ∀xA(x) जीतती है (सम्मान ∃xA(x)) यदि ऐसा रन A(x) का जीता हुआ रन है ) x के सभी (कम से कम के संबंध में) संभावित मानों के लिए, और ∃xA(x) जीतता है यदि यह कम से कम के लिए सत्य है।
अब तक वर्णित सभी ऑपरेटर बिल्कुल अपने शास्त्रीय समकक्षों की तरह व्यवहार करते हैं जब उन्हें प्राथमिक (मूवलेस) गेम पर लागू किया जाता है, और समान सिद्धांतों को मान्य करते हैं। यही कारण है कि सीओएल उन ऑपरेटरों के लिए उन्हीं प्रतीकों का उपयोग करता है जैसा कि शास्त्रीय तर्क करता है। हालाँकि, जब ऐसे ऑपरेटरों को गैर-प्राथमिक खेलों पर लागू किया जाता है, तो उनका व्यवहार शास्त्रीय नहीं रह जाता है। इसलिए, उदाहरण के लिए, यदि p प्राथमिक परमाणु है और P सामान्य परमाणु है, तो p→p∧p वैध है जबकि P→P∧P मान्य नहीं है। हालाँकि, बहिष्कृत मध्य P∨¬P का सिद्धांत वैध बना हुआ है। विच्छेदन के अन्य तीनों प्रकारों (विकल्प, अनुक्रमिक और टॉगलिंग) के साथ भी यही सिद्धांत अमान्य है।
गेम A और B का चॉइस डिसजंक्शन ⊔ ( chor ), जिसे A⊔B लिखा जाता है, ऐसा गेम है, जहां जीतने के लिए मशीन को दो डिसजंक्ट्स में से को चुनना होता है और फिर चुने गए घटक में जीत हासिल करनी होती है। अनुक्रमिक विच्छेदन (सोर) एᐁबी ए के रूप में शुरू होता है; यह भी ए के रूप में समाप्त होता है जब तक कि मशीन स्विच मूव नहीं करती है, जिस स्थिति में ए को छोड़ दिया जाता है और खेल फिर से शुरू होता है और बी के रूप में जारी रहता है। टॉगलिंग डिसजंक्शन (टोर) ए⩛बी में, मशीन ए और बी के बीच किसी भी परिमित संख्या में स्विच कर सकती है कई बार. प्रत्येक डिसजंक्शन ऑपरेटर का अपना दोहरा संयोजन होता है, जो दो खिलाड़ियों की भूमिकाओं को आपस में बदलकर प्राप्त किया जाता है। संगत परिमाणकों को आगे अनंत संयोजनों या वियोजनों के रूप में उसी तरह परिभाषित किया जा सकता है जैसे समानांतर परिमाणकों के मामले में होता है। प्रत्येक प्रकार का विच्छेदन भी उसी तरह से समान निहितार्थ संचालन को प्रेरित करता है जैसे कि यह समानांतर निहितार्थ → के मामले में था। उदाहरण के लिए, विकल्प निहितार्थ (चिम्प्लिकेशन) A⊐B को ¬A⊔B के रूप में परिभाषित किया गया है।
A की समानांतर पुनरावृत्ति (precurrence) को अनंत समानांतर संयोजन A∧A∧A∧ के रूप में परिभाषित किया जा सकता है... अनुक्रमिक (recurrence) और टॉगल (trecurrence) प्रकार की पुनरावृत्ति को समान रूप से परिभाषित किया जा सकता है।
कोरकरेंस ऑपरेटरों को अनंत विच्छेदन के रूप में परिभाषित किया जा सकता है। शाखाबद्ध पुनरावृत्ति ( brecurrence ) ⫰, जो पुनरावृत्ति का सबसे मजबूत प्रकार है, इसका कोई संगत संयोजन नहीं है। <बिग>⫰</बिग>ए ऐसा खेल है जो ए के रूप में शुरू होता है और आगे बढ़ता है। हालांकि, किसी भी समय, पर्यावरण को प्रतिकृति चाल बनाने की अनुमति दी जाती है, जो ए की तत्कालीन-वर्तमान स्थिति की दो प्रतियां बनाती है, इस प्रकार विभाजित हो जाती है सामान्य अतीत लेकिन संभवतः अलग-अलग भविष्य के विकास के साथ दो समानांतर धागों में नाटक। उसी तरह, पर्यावरण किसी भी थ्रेड की किसी भी स्थिति को दोहरा सकता है, इस प्रकार ए के अधिक से अधिक थ्रेड बना सकता है। उन थ्रेड को समानांतर में खेला जाता है, और मशीन को <बिग में विजेता बनने के लिए सभी थ्रेड में ए जीतने की आवश्यकता होती है >⫰ए. ब्रांचिंग कोरकरेंस (cobrecurrence) ⫯ को मशीन और पर्यावरण को इंटरचेंज करके सममित रूप से परिभाषित किया गया है।
प्रत्येक प्रकार की पुनरावृत्ति निहितार्थ के संबंधित कमजोर संस्करण और निषेध के कमजोर संस्करण को प्रेरित करती है। पहले को अनुप्रमाणन कहा जाता है, और बाद को खंडन कहा जाता है। ब्रांचिंग रिफ्यूटेशन ( ब्रिम्प्लिकेशन ) ए<बिग>⟜</बिग>बी और कुछ नहीं बल्कि <बिग>⫰</बिग>ए→बी है, और ए का ब्रांचिंग रिफ्यूटेशन ( ब्रेफ्यूटेशन ) ए<बिग>⟜</बिग> है ⊥, जहां ⊥ हमेशा हारा हुआ प्राथमिक खेल है। इसी प्रकार अन्य सभी प्रकार के प्रतिरूपण और खंडन के लिए भी।
एक समस्या विनिर्देशन उपकरण के रूप में
सीओएल की भाषा साहित्य में स्थापित नामों के साथ या उनके बिना, अनंत प्रकार की कम्प्यूटेशनल समस्याओं को निर्दिष्ट करने का व्यवस्थित तरीका प्रदान करती है। नीचे कुछ उदाहरण हैं.
मान लीजिए f एकात्मक फलन है। f की गणना करने की समस्या को ⊓x⊔y(y=f(x)) के रूप में लिखा जाएगा। सीओएल के शब्दार्थ के अनुसार, यह ऐसा खेल है जहां पहली चाल (इनपुट) पर्यावरण द्वारा होती है, जिसे x के लिए मान m चुनना चाहिए। सहज रूप से, इसका मतलब मशीन से f(m) का मान बताने के लिए कहना है। खेल ⊔y(y=f(m)) के रूप में जारी है। अब मशीन से चाल (आउटपुट) की उम्मीद की जाती है, जिसे y के लिए मान n चुनना चाहिए। इसका तात्पर्य यह है कि n, f(m) का मान है। गेम को अब प्रारंभिक n=f(m) पर लाया गया है, जिसे मशीन द्वारा जीता जाता है यदि और केवल तभी जब n वास्तव में f(m) का मान हो।
मान लीजिए p एकात्मक विधेय है। फिर ⊓x(p(x)⊔¬p(x)) Decidability (तर्क) p की समस्या को व्यक्त करता है, ⊓x(p(x)&ᐁ¬p(x)) पुनरावर्ती रूप से गणना योग्य सेट p की समस्या को व्यक्त करता है, और ⊓x(p(x)⩛¬p(x)) सीमा p में गणना की समस्या को व्यक्त करता है।
मान लीजिए कि p और q दो एकात्मक विधेय हैं। फिर ⊓x(p(x)⊔¬p(x))⟜⊓x(q(x)⊔¬q(x)) ट्यूरिंग में कमी की समस्या को व्यक्त करता है | ट्यूरिंग-कम करने वाले q को p (इस अर्थ में कि q ट्यूरिंग को p में रिड्यूस करने योग्य है यदि और केवल यदि इंटरैक्टिव समस्या ⊓x(p(x)⊔¬p(x))⟜⊓x(q(x)⊔¬q(x)) गणना योग्य है)। ⊓x(p(x)⊔¬p(x))→⊓x(q(x)⊔¬q(x)) वही करता है लेकिन ट्यूरिंग रिडक्शन के मजबूत संस्करण के लिए जहां p के लिए ओरेकल से केवल बार पूछताछ की जा सकती है। ⊓x⊔y(q(x)↔p(y)) अनेक-एक कमी|मैनी-वन कमिंग क्यू टू पी की समस्या के लिए भी यही करता है। अधिक जटिल अभिव्यक्तियों के साथ कोई भी कम्प्यूटेशनल समस्याओं पर सभी प्रकार के नामहीन लेकिन संभावित रूप से सार्थक संबंधों और संचालन को पकड़ सकता है, जैसे, उदाहरण के लिए, अर्ध-निर्णय आर की समस्या को ट्यूरिंग-कम करना, क्यू को पी में कई-एक को कम करने की समस्या को कम करना। मशीन के काम पर समय या स्थान प्रतिबंध लगाने से, ऐसे संबंधों और संचालन के जटिलता-सैद्धांतिक समकक्ष प्राप्त होते हैं।
समस्या समाधान उपकरण के रूप में
सीओएल के विभिन्न टुकड़ों के लिए ज्ञात डिडक्टिव सिस्टम में यह गुण होता है कि सिस्टम में किसी समस्या के प्रमाण से समाधान (एल्गोरिदम) स्वचालित रूप से निकाला जा सकता है। यह संपत्ति उन प्रणालियों पर आधारित सभी लागू सिद्धांतों द्वारा विरासत में मिली है। इसलिए, किसी दी गई समस्या का समाधान खोजने के लिए, इसे सीओएल की भाषा में व्यक्त करना और फिर उस अभिव्यक्ति का प्रमाण ढूंढना पर्याप्त है। इस घटना को देखने का दूसरा तरीका कार्यक्रम विनिर्देश (लक्ष्य) के रूप में सीओएल के सूत्र जी के बारे में सोचना है। फिर G का प्रमाण है - अधिक सटीक रूप से, इसका अनुवाद उस विनिर्देश को पूरा करने वाला प्रोग्राम है। यह सत्यापित करने की कोई आवश्यकता नहीं है कि विनिर्देश पूरा हो गया है, क्योंकि प्रमाण ही, वास्तव में, ऐसा सत्यापन है।
सीओएल-आधारित अनुप्रयुक्त सिद्धांतों के उदाहरण तथाकथित क्लैरिथमेटिक्स हैं। ये सीओएल पर आधारित संख्या सिद्धांत हैं, उसी अर्थ में जैसे पीनो अंकगणित पीए शास्त्रीय तर्क पर आधारित है। ऐसी प्रणाली आमतौर पर पीए का रूढ़िवादी विस्तार है। इसमें आम तौर पर सभी पीनो स्वयंसिद्धों को शामिल किया जाता है, और उनमें या दो अतिरिक्त-पीनो स्वयंसिद्धों को जोड़ा जाता है जैसे कि ⊓x⊔y(y=x') जो उत्तराधिकारी फ़ंक्शन की संगणना को व्यक्त करता है। आमतौर पर इसमें अनुमान के या दो गैर-तार्किक नियम भी होते हैं, जैसे प्रेरण या समझ के रचनात्मक संस्करण। ऐसे नियमों में नियमित बदलाव के माध्यम से कोई व्यक्ति या किसी अन्य इंटरैक्टिव कम्प्यूटेशनल जटिलता वर्ग सी को चिह्नित करने वाली ध्वनि और पूर्ण प्रणाली प्राप्त कर सकता है। यह इस अर्थ में है कि समस्या सी से संबंधित है यदि और केवल अगर सिद्धांत में इसका प्रमाण है। इसलिए, इस तरह के सिद्धांत का उपयोग न केवल एल्गोरिथम समाधान खोजने के लिए किया जा सकता है, बल्कि मांग पर कुशल समाधान भी खोजा जा सकता है, जैसे कि बहुपद समय या लघुगणकीय स्थान में चलने वाले समाधान। यह बताया जाना चाहिए कि सभी क्लैरिथमेटिकल सिद्धांत समान तार्किक अभिधारणाओं को साझा करते हैं, और केवल उनके गैर-तार्किक अभिधारणाएं लक्ष्य जटिलता वर्ग के आधार पर भिन्न होती हैं। समान आकांक्षाओं (जैसे कि सीमित अंकगणित) के साथ अन्य दृष्टिकोणों से उनकी उल्लेखनीय विशिष्ट विशेषता यह है कि वे पीए को कमजोर करने के बजाय विस्तार करते हैं, बाद की पूर्ण कटौतीत्मक शक्ति और सुविधा को संरक्षित करते हैं।
यह भी देखें
- खेल शब्दार्थ
- इंटरैक्टिव गणना
- तर्क
- कम्प्यूटेबिलिटी के लिए तर्क
संदर्भ
- ↑ G. Japaridze, Introduction to computability logic. Annals of Pure and Applied Logic 123 (2003), pages 1–99. doi:10.1016/S0168-0072(03)00023-X
- ↑ G. Japaridze, In the beginning was game semantics?. Games: Unifying Logic, Language and Philosophy. O. Majer, A.-V. Pietarinen and T. Tulenheimo, eds. Springer 2009, pp. 249–350. doi:10.1007/978-1-4020-9374-6_11 Prepublication
- ↑ G. Japaridze, The intuitionistic fragment of computability logic at the propositional level. Annals of Pure and Applied Logic 147 (2007), pages 187–227. doi:10.1016/j.apal.2007.05.001
- ↑ G. Japaridze, Introduction to clarithmetic I. Information and Computation 209 (2011), pp. 1312–1354. doi:10.1016/j.ic.2011.07.002 Prepublication
- ↑ G. Japaridze, Build your own clarithmetic I: Setup and completeness. Logical Methods is Computer Science 12 (2016), Issue 3, paper 8, pp. 1–59.
- ↑ G. Japaridze, Introduction to cirquent calculus and abstract resource semantics. Journal of Logic and Computation 16 (2006), pages 489–532. doi:10.1093/logcom/exl005 Prepublication
- ↑ G. Japaridze, The taming of recurrences in computability logic through cirquent calculus, Part I. Archive for Mathematical Logic 52 (2013), pp. 173–212. doi:10.1007/s00153-012-0313-8 Prepublication
बाहरी संबंध
- Computability Logic Homepage Comprehensive survey of the subject.
- Giorgi Japaridze
- Game Semantics or Linear Logic?
- Lecture Course on Computability Logic
- On abstract resource semantics and computabilty logic Video lecture by N.Vereshchagin.
- A Survey of Computability Logic (PDF) Downloadable equivalent of the above homepage.
