Formalizing the Real Numbers in Homotopy Type Theory with Cubical Agda
यह शोधपत्र क्यूबिकल अगाडा (Cubical Agda) में कौशी वास्तविक संख्याओं (Cauchy real numbers) के होमोटॉपी टाइप थ्योरी (Homotopy Type Theory) निर्माण के औपचारिकीकरण को प्रस्तुत करता है, जो यह प्रदर्शित करता है कि यह दृष्टिकोण अन्य रचनात्मक परिभाषाओं में निहित गणनीय चयन (countable choice), सेटॉइड ओवरहेड (setoid overhead), और यूनिवर्स-स्तर ट्रैकिंग (universe-level tracking) की समस्याओं से बचते हुए बिना पोस्टुलेट्स (postulates) के टाइप-चेक होता है।
मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें
कल्पना कीजिए कि आप ब्रह्मांड की हर चीज़ को मापने के लिए एक आदर्श, अनंत पैमाने (रूलर) का निर्माण करने की कोशिश कर रहे हैं। शास्त्रीय गणित (classical math) की दुनिया में, इस पैमाने का वर्णन करना आसान है: आप बस सभी संभावित "अनुमानित" मापों (जैसे 3.1, 3.14, 3.141, आदि) को लेते हैं और कहते हैं, "यदि दो अनुक्रम (sequences) के माप एक-दूसरे के करीब आते जा रहे हैं, तो वे पैमाने पर एक ही बिंदु का प्रतिनिधित्व करते हैं।"
हालाँकि, रचनात्मक गणित (Constructive Mathematics) में—जो एक ऐसी गणितीय शैली है जो इस बात पर जोर देती है कि आपको उस चीज़ को वास्तव में बनाना या गणना योग्य बनाना होगा जिसके बारे में आप बात कर रहे हैं—यह सरल दृष्टिकोण एक दीवार से टकरा जाता है। पैमाने को पूर्ण सिद्ध करने के लिए, आपको एक जादुई चुनाव करना होगा: आपको अंतिम बिंदु का प्रतिनिधित्व करने के लिए अनंत विकल्पों की सूची में से एक विशिष्ट माप चुनना होगा। रचनात्मक गणित कहता है, "कोई जादू नहीं चलेगा। यदि आप मुझे यह नहीं दिखा सकते कि आपने इसे कैसे चुना, तो आपने अभी तक पैमाना नहीं बनाया है।"
दशकों तक, गणितज्ञों को समझौता करना पड़ा। या तो उन्होंने "बुककीपिंग" (लेखांकन) के ऐसे तरीकों का उपयोग किया जिससे हर गणना जटिल हो गई, या उन्होंने पैमाने को इस तरह बनाया कि उन्हें जटिल "यूनिवर्स लेवल" (जैसे कि आपके बॉक्स कितने बड़े हैं, इसका हिसाब रखना) को ट्रैक करना पड़ता था।
नया ब्लूप्रिंट (HoTT बुक रील्स)
यह शोध प्रबंध (thesis) पैमाने को बनाने के लिए एक नया ब्लूप्रिंट प्रस्तुत करता है, जो प्रसिद्ध होमोटॉपी टाइप थ्योरी (HoTT) पुस्तक से लिया गया है। पैमाने के टुकड़ों को जोड़ने और फिर उन्हें चिकना करने के बजाय, यह विधि पैमाने और "चिकनाई" के नियमों को एक साथ बनाती है।
एक घर बनाने जैसा है जहाँ दीवारें और उसका ब्लूप्रिंट दोनों एक ही समय में खींचे जा रहे हैं।
- ईंटें: आप सरल, ज्ञात संख्याओं (जैसे भिन्न/fractions) से शुरुआत करते हैं।
- गोंद (Glue): आप एक विशेष नियम जोड़ते हैं जो कहता है, "यदि दो बिंदु पर्याप्त करीब हैं, तो वे वास्तव में एक ही बिंदु हैं।"
- जादू: क्योंकि "निकटता" का नियम स्वयं घर की परिभाषा में ही शामिल है, इसलिए आपको बाद में उन जादुई चुनावों की आवश्यकता नहीं होती है। जैसे ही आप ईंटें बिछाना समाप्त करते हैं, घर पूर्ण हो जाता है।
चुनौती: कंप्यूटर अनुवादक
लेखक, जैक्सन ब्रौ (Jackson Brough) ने इस सैद्धांतिक ब्लूप्रिंट को लिया और इसे एक ऐसी भाषा में अनुवादित करने का प्रयास किया जिसे कंप्यूटर समझ सके और सत्यापित कर सके: क्यूबिकल एगडा (Cubical Agda)।
कल्पना कीजिए कि आप एक जटिल नृत्य की दिनचर्या को एक रोबोट को समझाने की कोशिश कर रहे हैं जो केवल सख्त, शाब्दिक निर्देशों को समझता है।
- समस्या: इस ब्लूप्रंती का अनुवाद करने के पिछले प्रयास विफल रहे क्योंकि कंप्यूटर भाषा में सही "मूव्स" (विशेष रूप से, यह पैमाने और निकटता के नियमों की एक साथ परिभाषा को संभालने में सक्षम नहीं थी) की कमी थी। अनुवादकों को कहना पड़ता था, "मान लीजिए कि यह मूव मौजूद है," जो गणित में धोखाधड़ी है।
- समाधान: क्यूबिकल एगडा एक नया, स्मार्ट रोबोट है जो इन जटिल मूव्स को मूल रूप से (natively) समझता है। यह लेखक को ब्लूप्रिंट को ठीक वैसे ही लिखने की अनुमति देता है जैसा उसे डिज़ाइन किया गया था, बिना किसी धोखाधड़ी के।
अनुवाद के दौरान क्या हुआ?
यह शोध प्रबंध केवल कोड टाइप करने के बारे में नहीं है; यह इस बारे में है कि जब लेखक ने कंप्यूटर को गणित समझाने की कोशिश की तो क्या हुआ। कंप्यूटर की सख्ती ने लेखक को मूल स्पष्टीकरण में छिपी हुई कमियों को खोजने के लिए मजबूर किया:
- "वैकल्पिक" मानचित्र: मूल पुस्तक ने यह वर्णन किया कि दो बिंदुओं को करीब कैसे जांचा जाए। लेकिन जब लेखक ने कोड लिखने की कोशिश की, तो उन्हें एहसास हुआ कि पुस्तक की विधि एक "वन-वे स्ट्रीट" की तरह थी। आप यह सिद्ध कर सकते थे कि बिंदु करीब हैं, लेकिन आप आसानी से पीछे जाकर यह नहीं देख सकते थे कि वे क्यों करीब थे। लेखक को एक दूसरा, "कंप्यूटेशनल" मानचित्र (जिसे वैकल्पिक संबंध कहा जाता है) बनाना पड़ा जो एक रिवर्स गियर की तरह काम करता है, जिससे कंप्यूटर वास्तव में उत्तर की गणना कर सकता है।
- लापता सामग्री: पुस्तक ने कार्यों (जैसे गुणा) के निर्माण के लिए एक नियम इस तरह वर्णित किया जैसे कंप्यूटर मूल अनुमानों की सूची को "याद" रख सकता है। लेखक के पहले कोड संस्करण ने इस स्मृति को भूल दिया। कंप्यूटर ने इसे अस्वीकार कर दिया। लेखक को नियम को फिर से लिखना पड़ा ताकि वह स्पष्ट रूप से स्मृति को साथ लेकर चले, यह महसूस करते हुए कि मूल पाठ मशीन के लिए बहुत अस्पष्ट था।
- बहु-चर (Multi-variable) पहेली: पुस्तक ने संकेत दिया था कि एकल संख्याओं के नियमों को आसानी से संख्याओं के जोड़े या त्रिकों पर लागू किया जा सकता है। कंप्यूटर इस बात से सहमत नहीं था। लेखक को एक नया, विशिष्ट लेम्मा (lemma) सिद्ध करना पड़ा जो यह दिखाता है कि यदि कोई नियम एक चर के लिए काम करता है, तो यह दो के लिए भी काम करता है, बशर्ते आप उन्हें एक-एक करके जांचें।
परिणाम
अंतिम उत्पाद कोड की एक विशाल, ओपन-सोर्स लाइब्रेरी (13,000 से अधिक लाइनें) है जो सिद्ध करती है कि HoTT बुक रील्स पूरी तरह से काम करते हैं।
- यह सिद्ध करता है कि ये संख्याएँ एक पूर्ण, क्रमित क्षेत्र (ordered field) बनाती हैं (आप उन्हें जोड़, घटा, गुणा, भाग और तुलना कर सकते हैं)।
- यह सिद्ध करता है कि पैमाना "आर्किमिडीय" (Archimedean) है (अर्थात, चाहे आपके पास कितना भी छोटा अंतराल हो, आप हमेशा इसके भीतर फिट होने वाला एक भिन्न/fraction ढूंढ सकते हैं)।
- सबसे महत्वपूर्ण बात यह है कि यह यह सब बिना धोखाधड़ी के करता है। कंप्यूटर ने हर एक कदम की जाँच की, और कोड बिना किसी "जादुई धारणाओं" के चलता है।
सारांश में
यह शोध प्रबंध एक सुंदर, उच्च-स्तरीय गणितीय विचार को एक कठोर, शाब्दिक दुनिया में जीवित रहने के लिए मजबूर करने की कहानी है। ऐसा करके, लेखक ने केवल एक डिजिटल पैमाना ही नहीं बनाया; उन्होंने ब्लूप्रिंट को ही पॉलिश किया, जिससे छिपे हुए विवरण सामने आए और सिद्धांत पहले की तुलना में अधिक मजबूत और सटीक हो गया। यह कोड अब किसी के लिए भी भविष्य की गणितीय खोजों के लिए एक ठोस आधार के रूप में उपयोग करने के लिए उपलब्ध है।
अपने क्षेत्र के पेपरों की भीड़ में उलझे हुए हैं?
आपके रिसर्च कीवर्ड से मेल खाने वाले सबसे नए और अलग सोच वाले पेपरों का रोज़ाना Digest पाएँ—तकनीकी सारांश के साथ, आपकी भाषा में।