Setoids in Intensional Type Theory
यह शोध पत्र प्रदर्शित करता है कि इंटेंशनल टाइप थ्योरी (सेफ एगडा में औपचारिक रूप से प्रस्तुत) के भीतर प्रदर्शित सेटोइड्स, यूनिवर्स के साथ एक्सटेंशनल टाइप थ्योरी के लिए एक सिमेंटिक्स प्रदान कर सकते हैं, जिससे एक कोरोलरी के रूप में बाद की निरंतरता स्थापित होती है।
मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें
महान अनुवाद: कठोर नियमों को लचीले उपकरणों में बदलना
कल्पना कीजिए कि आप निर्देशों के एक सेट का उपयोग करके एक घर बनाने की कोशिश कर रहे हैं जो अविश्वसनीय रूप से सख्त हैं। हर ईंट को एक विशिष्ट क्रम में रखा जाना चाहिए, और यदि आप एक छोटी सी गलती करते हैं, तो पूरी योजना विफल हो जाती है। इंटेंशनल टाइप थ्योरी (Intensional Type Theory) इसी तरह काम करती है। यह कंप्यूटर वैज्ञानिकों और गणितज्ञों द्वारा उपयोग की जाने वाली एक अत्यंत सटीक भाषा है जिसका उपयोग यह सिद्ध करने के लिए किया जाता है कि सॉफ्टवेयर बग-मुक्त है। यह एक ऐसे रोबोट की तरह है जो केवल सटीक, चरण-दर-चरण कमांड का पालन करता है। यदि दो चीजें एक जैसी दिखती हैं लेकिन उन्हें अलग तरह से बनाया गया है, तो रोबोट कहता है, "नहीं, वे अलग हैं!" क्योंकि वह इस बात पर ध्यान नहीं देता कि आपके पास क्या है, बल्कि इस पर ध्यान देता है कि आप वहाँ कैसे पहुँचे।
अब, एक अलग प्रकार के निर्माता की कल्पना करें जिसे केवल अंतिम परिणाम की परवाह है। यदि दो घर बाहर से समान दिखते हैं, तो यह निर्माता कहता है, "वे एक ही घर हैं!" यह एक्सटेंशनल टाइप थ्योरी (Extensional Type Theory) है। यह जटिल गणितीय संरचनाओं, जैसे ब्रह्मांड के आकार या एक मशरूम (toadstool) की वृद्धि के तर्क का वर्णन करने के लिए बहुत अधिक लचीला और स्वाभाविक है। हालाँकि, इस लचीलेपन के साथ एक पेंच भी आता है: इस लचीली भाषा के नियमों के विरोधाभासी होने (जैसे कि एक ऐसा घर जो खड़ा भी है और ढहा हुआ भी है) की संभावना को सिद्ध करना बहुत कठिन है।
लंबे समय तक, वैज्ञानिक सोचते रहे: क्या हम पहले से मौजूद सख्त, "इंटेंशनल" उपकरणों का उपयोग करके इस लचीली, "एक्सटेंशनल" भाषा का एक मॉडल बना सकते हैं? यह एक कठोर, वर्गाकार लेगो (Lego) ईंटों का उपयोग करके एक तरल, आकार बदलने वाली मूर्ति बनाने की कोशिश करने जैसा है। यदि हम ऐसा कर सकते हैं, तो यह सिद्ध होता है कि लचीली भाषा उपयोग करने के लिए सुरक्षित है, भले ही हमारे पास केवल सख्त उपकरण ही क्यों न हों। यही वह बड़ा सवाल है जिसे एंड्रयू पिट्स (Andrew Pitts) अपने शोध पत्र में सुलझाते हैं।
शोध पत्र: कठोर ईंटों के साथ एक लचीली दुनिया का निर्माण
कैम्ब्रिज विश्वविद्यालय के एंड्रयू पिट्स इस शोध पत्र में दिखाते हैं कि हम सख्त, इंटेंशनल टाइप थ्योरी (जिसे वे IRU कहते हैं) का उपयोग करके लचीली, एक्सटेंशनल टाइप थ्योरी (जिसे वे ETU कहते हैं) का एक मॉडल बना सकते हैं। वह इसे डिस्प्लेड सेटॉइड्स (displayed setoids) नामक एक विशेष प्रकार के "अनुवाद परत" (translation layer) बनाकर करते हैं।
एक सेटॉइड (setoid) को एक "धुंधले बॉक्स" के रूप में समझें। बॉक्स के अंदर, आपके पास वस्तुओं का एक संग्रह है। लेकिन यह कहने के बजाय कि दो वस्तुएं "बिल्कुल एक समान" हैं (जो कि सख्त रोबोट के लिए बहुत कठिन है), बॉक्स में एक विशेष नियम है: "ये दो वस्तुएं तुल्य (equivalent) हैं यदि वे एक विशिष्ट परीक्षण पास करती हैं।" यह एक क्लब की तरह है जहाँ आपको सदस्य होने के लिए अध्यक्ष के बिल्कुल समान होने की आवश्यकता नहीं है; आपको बस सदस्यता परीक्षण पास करने की आवश्यकता है।
डिस्प्लेड सेटॉइड्स (displayed setoids) वाला हिस्सा पेचीदा है। कल्पना कीजिए कि आपके पास एक मुख्य मानचित्र (सख्त इंटेंशनल दुनिया) है। अब, आप उस पहले मानचित्र के ऊपर एक दूसरा, अधिक लचीला मानचित्र बनाना चाहते हैं (एक्सटेंशनल दुनिया)। एक "डिस्प्लेड सेटॉइड" उस मानचित्र के ऊपर चिपकाई गई पारदर्शी फिल्म की एक परत की तरह है। इस फिल्म पर, आप नए संबंध और नियम खींचते हैं जो मानचित्र के कठोर बिंदुओं को इस तरह से प्रवाहित और परिवर्तनशील दिखाते हैं, जैसा कि लचीली दुनिया को चाहिए।
पिट्स की मुख्य खोज यह है कि उन्होंने इन "पारदर्शी फिल्मों" (डिस्प्लेड सेटॉइड्स) को डिजाइन करने का एक तरीका खोज निकाला है जो IRU के सख्त उपकरणों से बनाई जा जाने में सरल हैं, लेकिन ETU के व्यवहार की नकल करने के लिए पर्याप्त जटिल हैं। उन्होंने केवल अनुमान नहीं लगाया; उन्होंने अगा (Agda) (विशेष रूप से एक "सुरक्षित" मोड का उपयोग करते हुए जो प्रोग्राम को अपने स्वयं के नियम बनाने से रोकता है) नामक एक कंप्यूटर प्रोग्राम के भीतर एक पूर्ण, कार्यशील मॉडल बनाया।
यहाँ जादू कैसे होता है:
- समस्या: सख्त दुनिया में, दो चीजों के समान होने को सिद्ध करना कठिन है। लचीली दुनिया में, यह आसान है। शोध पत्र को एक तरीका चाहिए था जिससे सख्त दुनिया बिना अपने नियमों को तोड़े, लचीली दुनिया की तरह व्यवहार कर सके।
- समाधान: पिट्स ने एक ऐसी तकनीक का उपयोग किया जहाँ उन्होंने प्रकारों (types) के लिए "कोड" (जैसे लेगो ईंटों के ब्लूप्रिंट) को परिभाषित किया और फिर नियम बनाए कि कब दो कोड "तुल्य" माने जाएंगे। उन्होंने इन कोडों का एक पदानुक्रम (hierarchy) बनाया, जैसे कि नेस्टेड बक्सों का एक सेट, जहाँ प्रत्येक बॉक्स के अंदर वाले बॉक्स के लिए नियम होते हैं।
- परिणाम: इन डिस्प्लेड सेटॉइड्स का उपयोग करके, वह हर नियम को सख्त IRU में अनुवादित करने में सक्षम रहे जो लचीले ETU का हिस्सा है। उन्होंने सिद्ध किया कि यदि आप ETU के नियमों का पालन करते हैं, तो आप कभी भी विरोधाभास (जैसे कि यह सिद्ध करना कि एक विशिष्ट प्रकार का "खाली" बॉक्स वास्तव में कुछ सामग्री रखता है) में नहीं फंसेंगे।
यह शोध पत्र स्पष्ट रूप से इस विचार को खारिज करता है कि यह आसान है या पिछले प्रयास पूर्ण थे। लेखक नोट करते हैं कि हालांकि दूसरों ने ऐसा करने की कोशिश की है, लेकिन वे अक्सर कठिन हिस्सों को छोड़ देते हैं या ऐसे उपकरणों का उपयोग करते हैं जो बहुत शक्तिशाली थे (जैसे कि यह मान लेना कि चीजें समान हैं क्योंकि वे एक जैसी दिखती हैं)। पिट्स का दृष्टिकोण "बेयर-बोन्स" (bare-bones) है, जिसका अर्थ है कि उन्होंने इस काम को करने के लिए सबसे सरल उपकरणों का उपयोग किया, जिससे यह सिद्ध होता है कि इस काम को करने के लिए आपको फैंसी, अपुष्ट विशेषताओं की आवश्यकता नहीं है।
इस शोध पत्र का सबसे रोमांचक हिस्सा इसका निष्कर्ष है: क्योंकि उन्होंने सफलतापूर्वक इस मॉडल का निर्माण किया, उन्होंने सिद्ध किया कि ETU सुसंगत (consistent) है। सरल शब्दों में, इसका अर्थ है कि उन्होंने दिखाया है कि एक्सटेंशनल टाइप थ्योरी की लचीली भाषा कभी क्रैश नहीं होगी या खुद का खंडन नहीं करेगी, जब तक कि आप इसे उनके सख्त, इंटेंशनल मॉडल के लेंस से देखते हैं। यह एक अस्थिर, आकार बदलने वाले टॉवर को यह सिद्ध करने जैसा है कि वह वास्तव में स्थिर है क्योंकि आपने उसे अटूट कंक्रीट की नींव पर बनाया है।
यह केवल एक सैद्धांतिक खेल नहीं है। यह मायने रखता है क्योंकि कंप्यूटर वैज्ञानिक इन सिद्धांतों का उपयोग उन सॉफ़्टवेयर को लिखने के लिए करते हैं जो हवाई जहाजों से लेकर चिकित्सा उपकरणों तक सब कुछ नियंत्रित करते हैं। यदि भाषा के नियम डगमगाते हैं, तो सॉफ़्टवेयर विफल हो सकता है। यह दिखाकर कि लचीले नियम सुरक्षित हैं, पिट्स इंजीनियरों और गणितज्ञों को जटिल प्रणालियों के निर्माण के लिए अधिक आत्मविश्वास प्रदान करते हैं। शोध पत्र यह दावा नहीं करता है कि उसने कंप्यूटर विज्ञान की हर समस्या को हल कर दिया है, न ही यह कहता है कि यह करने का एकमात्र तरीका है। यह केवल यह सिद्ध करता है कि यह विशिष्ट, कठिन अनुवाद संभव है, और वह भी उस स्तर की निश्चितता के साथ जो केवल एक मशीन-चेक्ड प्रूफ (machine-checked proof) प्रदान कर सकता है।
अंत में, पिट्स ने केवल दो दुनियाओं के बीच एक पुल नहीं बनाया; उन्होंने दिखाया कि वह पुल हमारे पास मौजूद सबसे जटिल गणितीय विचारों के भार को उठाने के लिए पर्याप्त मजबूत है, और इसके लिए उन्होंने केवल सबसे सरल, सबसे विश्वसनीय उपकरणों का उपयोग किया है। यह अक्सर जाल के साथ धुएं को पकड़ने की कोशिश करने जैसा महसूस होने वाले क्षेत्र में, सावधानीपूर्वक, चरण-दर-चरण सोच की शक्ति का प्रमाण है।
अपने क्षेत्र के पेपरों की भीड़ में उलझे हुए हैं?
आपके रिसर्च कीवर्ड से मेल खाने वाले सबसे नए और अलग सोच वाले पेपरों का रोज़ाना Digest पाएँ—तकनीकी सारांश के साथ, आपकी भाषा में।