A coalgebraic higher-order modal fixed-point logic

कल्पना कीजिए कि आप एक कंप्यूटर को भविष्य के बारे में सोचना सिखाने की कोशिश कर रहे हैं। आप चाहते हैं कि वह एक जटिल प्रणाली को देखे—जैसे कि ट्रैफिक लाइट नेटवर्क, एक वीडियो गेम की दुनिया, या किसी रोबोट की निर्णय लेने की प्रक्रिया—और सवालों के जवाब दे जैसे, "क्या यह रोबोट कभी फंस जाएगा?" या "क्या ऐसा कोई रास्ता है जहाँ रोबोट निश्चित रूप से जीत जाता है?" दशकों से, कंप्यूटर वैज्ञानिकों ने इन सवालों को पूछने के लिए "मोडल लॉजिक" (modal logic) नामक एक विशेष प्रकार की गणितीय भाषा का उपयोग किया है। इस भाषा को एक "जादुई मंत्रों" के सेट के रूप में सोचें। कुछ मंत्र यह जांचते हैं कि अभी क्या सच है, जबकि अन्य यह जांचते हैं कि भविष्य में क्या होगा।

लेकिन वास्तविक जीवन अव्यवस्थित है। कभी-कभी, एक प्रणाली केवल "चालू" या "बंद" नहीं होती; यह 70% संभावना के साथ बाईं ओर जाने और 30% संभावना के साथ दाईं ओर जाने जैसी हो सकती है। अन्य समय में, खेल के नियम इस बात पर निर्भर करते हैं कि आप उन्हें कैसे देखते हैं, या प्रणाली इतनी जटिल होती है कि इसमें एक दूसरे पर कार्य करने वाले फंक्शन्स (functions) शामिल होते हैं (जैसे कि एक ऐसी रेसिपी जो अपनी सामग्री की सूची खुद लिखती है)। इन चीजों को संभालने के लिए, वैज्ञानिकों ने दो शक्तिशाली उपकरण विकसित किए: एक उन प्रणालियों के लिए जिनमें प्रायिकता (probabilities) होती हैं (जैसे कि एक सिक्का उछालना) और दूसरा उच्च-क्रम की जटिलता (higher-order complexity) वाली प्रणालियों के लिए (जहाँ नियम नियमों को बदल सकते हैं)। बड़ा सवाल यह था: क्या हम एक ही, सार्वभौमिक "मास्टर भाषा" बना सकते हैं जो इन दोनों दुनियाओं को एक साथ समझ सके? यह वह पहेली है जिसे कंप्यूटर वैज्ञानिक रयान टे, हर्ष बेहार और चार्ल्स ग्रेलोइस ने हल करने का प्रयास किया।

कंप्यूटर दुनिया के लिए सार्वभौमिक अनुवादक

इस शोध पत्र में, लेखक एक नई, सुपर-पावर्ड भाषा पेश करते हैं जिसे को-एल्जेब्रिक हायर-ऑर्डर मोडल फिक्स्ड-पॉइंट लॉजिक (या संक्षेप में "Coalgebraic HFL") कहा जाता है। इसे समझने के लिए, एक "को-एल्जेब्रा" (coalgebra) को एक डरावने गणितीय शब्द के रूप में नहीं, बल्कि किसी भी प्रकार की चलती हुई प्रणाली के लिए एक सार्वभौमिक ब्लूप्रिंट के रूप में देखें। चाहे वह एक साधारण ट्रैफिक लाइट हो, एक जटिल रोबोट हो, या संयोग का एक संभाव्य खेल हो, एक को-एल्जेब्रा बस इस बात का वर्णन करने का एक तरीका है कि एक प्रणाली एक अवस्था से अगली अवस्था में कैसे बढ़ती है।

लेखकों ने एक मौजूदा लॉजिक भाषा (HFL) ली जो पहले से ही जटिल, उच्च-स्तरीय नियमों को संभालने में अच्छी थी, और उन्होंने इसे "प्रेडिकेट लिफ्टिंग्स" (predicate liftings) नामक चश्मे का एक नया सेट दिया। इन चश्मों को "एडाप्टर" के रूप में सोचें। पहले, यह लॉजिक केवल विशिष्ट प्रकार की प्रणालियों को देख सकता था। अब, इन एडाप्टर के साथ, यह किसी भी प्रणाली को देख सकता है जो को-एल्जेब्रा ब्लूप्रिंट में फिट बैठती है, चाहे वह प्रणाली सरल हाँ/ना के विकल्पों वाली हो, जटिल प्रायिकता बादलों वाली हो, या यहाँ तक कि उच्च-क्रम के फंक्शन्स वाली हो। यह एक यूनिवर्सल रिमोट कंट्रोल लेने जैसा है जो अचानक आपके टीवी, आपके ड्रोन और आपके स्मार्ट फ्रिज को संचालित कर सकता है, और वह भी उन्हीं बटनों का उपयोग करके।

बड़ी खोज: एक लॉजिक जो उन सब पर राज करे

इस शोध पत्र की मुख्य खोज यह है कि यह नया "Coalgebraic HFL" अपने दो प्रसिद्ध पूर्वजों के कार्यों को एक साथ करने के लिए पर्याप्त शक्तिशाली है। यह मानक कंप्यूटर प्रोग्रामों (जो अक्सर केवल "हाँ या ना" के निर्णय होते हैं) के तर्क को भी वर्णित कर सकता है और संभाव्य प्रणालियों (जहाँ चीजें एक निश्चित संभावना के साथ होती हैं) के तर्क को भी।

इसे सिद्ध करने के लिए, लेखकों ने केवल यह नहीं कहा कि "यह काम करता है"; उन्होंने दिखाया कि पुराने जगत की दो बहुत कठिन समस्याओं को इस नई भाषा में पूरी तरह से अनुवादित किया जा सकता है:

1. "खाली सेट" (Empty Set) की समस्या: कल्पना कीजिए कि आपके पास एक नॉन-डिटरमिनिस्टिक मशीन (एक रोबोट जो एक साथ कई रास्ते चुन सकता है) है। आप जानना चाहते हैं कि क्या कोई ऐसा रास्ता है जहाँ रोबोट सफल होता है, या वह हर हाल में विफल हो जाता है। लेखकों ने दिखाया कि यह प्रश्न पूछना बिल्कुल वैसा ही है जैसा कि उनके नए लॉजिक में एक विशिष्ट प्रश्न पूछना।
2. "वैल्यू-1" (Value-1) की समस्या: कल्पना कीजिए कि एक रोबोट संभावनाओं के आधार पर निर्णय लेता है (जैसे पासा फेंकना)। आप जानना चाहते हैं कि क्या ऐसी कोई रणनीति है जहाँ रोबोट ठीक 100% (या "1") की प्रायिकता के साथ सफल होता है। लेखकों ने सिद्ध किया कि यह पेचीदा प्रायिकता प्रश्न भी इस नए लॉजिक में एक मॉडल-चेकिंग समस्या में बदल जाता है।

सरल शब्दों में, उन्होंने एक पुल बनाया। यदि आप नई लॉजिक में एक समस्या को हल कर सकते हैं, तो आपने प्रभावी रूप से पुराने संसारों की इन कठिन समस्याओं को हल कर दिया है। यह एक बड़ी बात है क्योंकि यह कंप्यूटर प्रणालियों के बारे में सोचने के दो अलग-अलग तरीकों को एक ही छत के नीचे लाता है।

उन्होंने यह कैसे किया: "सपोर्ट" (Support) की ट्रिक

इसे काम करने के लिए, लेखकों को नियमों को परिभाषित करने के बारे में बहुत सावधान रहना पड़ा। उन्होंने "सपोर्ट" (support) की एक अवधारणा पेश की, जो किसी प्रणाली की अवस्था के लिए एक "फिंगरप्रिंट" की तरह है। उन्होंने दिखाया कि यदि उनकी प्रणाली कुछ गणितीय नियमों का पालन करती है (विशेष रूपв से, यदि यह "इनक्लूजन" और "वीक वाइड पुलबैक" को संरक्षित करती है—जो कि फैंसी तरीके हैं यह कहने के कि प्रणाली ज़ूम इन या ज़ूम आउट करने पर सुसंगत व्यवहार करती है), तो वे किसी भी मशीन के लिए एक "टॉप वैल्यू" (top value) को परिभाषित कर सकते हैं।

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

यह क्या नहीं करता (अभी तक)

यह ध्यान रखना महत्वपूर्ण है कि यह शोध पत्र क्या दावा नहीं करता है। लेखक बहुत स्पष्ट हैं कि हालांकि उनका लॉजिक संभाव्य प्रणालियों के सार को पकड़ता है, लेकिन यह अभी भी सबसे उन्नत संभाव्य लॉजिक (PHFL) की हर एक बारीकी को नहीं पकड़ता है। विशेष रूप से, "अपवर्ड्स-क्लोज्ड सबसेट्स" (ऊपर की ओर बढ़ने वाले मानों के समूह) से जुड़े कुछ बहुत जटिल फॉर्मूले हैं जिन्हें उनका वर्तमान संस्करण पूरी तरह से हैंडल नहीं करता है। वे स्वीकार करते हैं कि यह एक सीमा है और इसे भविष्य के कार्य के रूपए सुझाते हैं।

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

यह क्यों मायने रखता है

एक किशोर को रोबोट के रास्तों की जाँच करने वाले लॉजिक की परवाह क्यों होनी चाहिए? क्योंकि जैसे-जैसे हमारी दुनिया अधिक स्वचालित हो रही है, हम ऐसी प्रणालियाँ बना रहे हैं जो पहले से कहीं अधिक जटिल और अनिश्चित हैं। हमारे पास सेल्फ-ड्राइविंग कारें हैं जो बारिश और धुंध (संभावनाओं) से निपटती हैं, और AI है जो नियमों की परतों (उच्च-क्रम के फंक्शन्स) के आधार पर निर्णय लेता है।

यह शोध पत्र इन सभी प्रणालियों के बारे में बात करने के लिए एक एकल, एकीकृत तरीके का सैद्धांतिक आधार प्रदान करता है। हर नए प्रकार के रोबोट या खेल के लिए एक नई भाषा बनाने के बजाय, हम अंततः इस "Coalgebraic HFL" का उपयोग यह सत्यापित करने के लिए कर सकते हैं कि हमारी डिजिटल दुनिया सुरक्षित, निष्पक्ष और इच्छित रूप से काम कर रही है। यह एक ऐसी दुनिया की ओर एक कदम है जहाँ हम गणितीय रूप से सिद्ध कर सकते हैं कि हमारी तकनीक क्रैश नहीं होगी, बेईमानी नहीं करेगी, और ठीक वही करेगी जो हम उससे करने को कहेंगे, चाहे नियम कितने भी जटिल क्यों न हो जाएं।