डीप लिंक इक्वेटिंग मैथ प्रूफ़ और कंप्यूटर प्रोग्राम | क्वांटा पत्रिका

कुछ वैज्ञानिक खोजें मायने रखती हैं क्योंकि वे कुछ नया उजागर करती हैं - उदाहरण के लिए, डीएनए की दोहरी पेचदार संरचना, या ब्लैक होल का अस्तित्व। हालाँकि, कुछ खुलासे गहरे हैं क्योंकि वे दिखाते हैं कि दो पुरानी अवधारणाएँ, जिन्हें कभी अलग माना जाता था, वास्तव में एक ही हैं। जेम्स क्लर्क मैक्सवेल के समीकरणों को लें जो दिखाते हैं कि बिजली और चुंबकत्व एक ही घटना के दो पहलू हैं, या सामान्य सापेक्षता का गुरुत्वाकर्षण को घुमावदार स्थान-समय के साथ जोड़ना है।

करी-हावर्ड पत्राचार ऐसा ही करता है लेकिन बड़े पैमाने पर, न केवल अलग-अलग अवधारणाओं को एक क्षेत्र में जोड़ता है, बल्कि संपूर्ण विषयों को जोड़ता है: कम्प्यूटर साइंस और गणितीय तर्क. इसे करी-हावर्ड आइसोमोर्फिज्म (एक शब्द का अर्थ है कि दो चीजों के बीच किसी प्रकार का एक-से-एक पत्राचार मौजूद है) के रूप में भी जाना जाता है, यह गणितीय प्रमाण और कंप्यूटर प्रोग्राम के बीच एक लिंक स्थापित करता है।

सीधे शब्दों में कहें तो, करी-हावर्ड पत्राचार का मानना ​​है कि कंप्यूटर विज्ञान की दो अवधारणाएं (प्रकार और कार्यक्रम) क्रमशः प्रस्तावों और प्रमाणों के बराबर हैं - तर्क से अवधारणाएं।

इस पत्राचार का एक प्रभाव यह है कि प्रोग्रामिंग - जिसे अक्सर एक व्यक्तिगत शिल्प के रूप में देखा जाता है - को गणित के आदर्श स्तर तक बढ़ाया जाता है। प्रोग्राम लिखना केवल "कोडिंग" नहीं है, यह एक प्रमेय सिद्ध करने का कार्य बन जाता है। यह प्रोग्रामिंग के कार्य को औपचारिक बनाता है और कार्यक्रमों की शुद्धता के बारे में गणितीय रूप से तर्क करने के तरीके प्रदान करता है।

इस पत्राचार का नाम उन दो शोधकर्ताओं के नाम पर रखा गया है जिन्होंने स्वतंत्र रूप से इसकी खोज की थी। 1934 में, गणितज्ञ और तर्कशास्त्री हास्केल करी ने गणित में कार्यों और तर्क में निहितार्थ संबंध के बीच समानता देखी, जो दो प्रस्तावों के बीच "यदि-तब" कथन का रूप लेता है।

करी के अवलोकन से प्रेरित होकर, गणितीय तर्कशास्त्री विलियम एल्विन हॉवर्ड ने 1969 में गणना और तर्क के बीच एक गहरा संबंध खोजा, जिससे पता चला कि कंप्यूटर प्रोग्राम चलाना तार्किक प्रमाण को सरल बनाने जैसा है। जब कोई कंप्यूटर प्रोग्राम चलता है, तो एकल आउटपुट प्राप्त करने के लिए प्रत्येक पंक्ति का "मूल्यांकन" किया जाता है। इसी तरह, एक प्रमाण में, आप जटिल कथनों से शुरू करते हैं जिन्हें आप सरल बना सकते हैं (उदाहरण के लिए, अनावश्यक चरणों को हटाकर, या जटिल अभिव्यक्तियों को सरल अभिव्यक्तियों के साथ प्रतिस्थापित करके) जब तक आप किसी निष्कर्ष पर नहीं पहुँच जाते - कई अंतरिम कथनों से प्राप्त एक अधिक संक्षिप्त और संक्षिप्त कथन .

हालाँकि यह विवरण पत्राचार का एक सामान्य अर्थ बताता है, इसे पूरी तरह से समझने के लिए हमें कंप्यूटर वैज्ञानिक जिसे "टाइप थ्योरी" कहते हैं, उसके बारे में थोड़ा और जानने की आवश्यकता है।

आइए एक प्रसिद्ध विरोधाभास से शुरू करें: एक गाँव में एक नाई रहता है जो उन सभी पुरुषों की हजामत बनाता है जो खुद हजामत नहीं बनाते, और केवल उनकी हजामत बनाता है। क्या नाई स्वयं दाढ़ी बनाता है? यदि उत्तर हाँ है, तो उसे स्वयं दाढ़ी नहीं बनानी चाहिए (क्योंकि वह केवल उन पुरुषों की दाढ़ी बनाता है जो स्वयं दाढ़ी नहीं बनाते हैं)। यदि उत्तर नहीं है, तो उसे स्वयं दाढ़ी बनानी होगी (क्योंकि वह उन सभी पुरुषों की दाढ़ी बनाता है जो स्वयं दाढ़ी नहीं बनाते हैं)। यह विरोधाभास बर्ट्रेंड रसेल का एक अनौपचारिक संस्करण है जिसे सेट नामक अवधारणा का उपयोग करके गणित की नींव स्थापित करने की कोशिश करते समय खोजा गया था। अर्थात्, ऐसे समुच्चय को परिभाषित करना असंभव है जिसमें सभी समुच्चय शामिल हों जो विरोधाभासों का सामना किए बिना स्वयं को समाहित नहीं करते हैं।

इस विरोधाभास से बचने के लिए, रसेल ने दिखाया, हम "प्रकारों" का उपयोग कर सकते हैं। मोटे तौर पर कहें तो, ये श्रेणियां हैं जिनके विशिष्ट मानों को ऑब्जेक्ट कहा जाता है। उदाहरण के लिए, यदि कोई प्रकार है जिसे "नैट" कहा जाता है, जिसका अर्थ प्राकृतिक संख्या है, तो इसकी वस्तुएँ 1, 2, 3, इत्यादि हैं। शोधकर्ता आमतौर पर किसी वस्तु के प्रकार को दर्शाने के लिए कोलन का उपयोग करते हैं। पूर्णांक प्रकार की संख्या 7 को "7: पूर्णांक" के रूप में लिखा जा सकता है। आपके पास एक ऐसा फ़ंक्शन हो सकता है जो टाइप ए का एक ऑब्जेक्ट लेता है और टाइप बी का एक ऑब्जेक्ट निकालता है, या वह जो टाइप ए और टाइप बी की वस्तुओं की एक जोड़ी को एक नए प्रकार में जोड़ता है, जिसे "ए × बी" कहा जाता है।

इसलिए, विरोधाभास को हल करने का एक तरीका इन प्रकारों को एक पदानुक्रम में रखना है, ताकि उनमें केवल अपने से "निचले स्तर" के तत्व शामिल हो सकें। तब एक प्रकार स्वयं को शामिल नहीं कर सकता है, जो विरोधाभास पैदा करने वाली आत्म-संदर्भितता से बचता है।

टाइप थ्योरी की दुनिया में, यह साबित करना कि कोई कथन सत्य है, उस चीज़ से भिन्न दिख सकता है जिसके हम आदी हैं। यदि हम यह साबित करना चाहते हैं कि पूर्णांक 8 सम है, तो यह दिखाने की बात है कि 8 वास्तव में एक विशिष्ट प्रकार की वस्तु है जिसे "सम" कहा जाता है, जहां सदस्यता के नियम को 2 से विभाज्य किया जा रहा है। यह सत्यापित करने के बाद कि 8 विभाज्य है 2 से, हम यह निष्कर्ष निकाल सकते हैं कि 8 वास्तव में सम प्रकार का "निवासी" है।

करी और हॉवर्ड ने दिखाया कि प्रकार मौलिक रूप से तार्किक प्रस्तावों के बराबर हैं। जब कोई फ़ंक्शन किसी प्रकार का "निवास" करता है - अर्थात, जब आप उस फ़ंक्शन को सफलतापूर्वक परिभाषित कर सकते हैं जो उस प्रकार का ऑब्जेक्ट है - तो आप प्रभावी रूप से दिखा रहे हैं कि संबंधित प्रस्ताव सत्य है। इसलिए ऐसे फ़ंक्शन जो प्रकार ए का इनपुट लेते हैं और प्रकार बी का आउटपुट देते हैं, जिसे प्रकार ए → बी के रूप में दर्शाया जाता है, उन्हें एक निहितार्थ के अनुरूप होना चाहिए: "यदि ए, तो बी।" उदाहरण के लिए, प्रस्ताव लें "यदि बारिश हो रही है, तो जमीन गीली है।" टाइप थ्योरी में, इस प्रस्ताव को "रेनिंग → ग्राउंडइज़वेट" प्रकार के एक फ़ंक्शन द्वारा मॉडल किया जाएगा। अलग-अलग दिखने वाले फॉर्मूलेशन वास्तव में गणितीय रूप से एक जैसे हैं।

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

और गणित के लिए, पत्राचार के कारण जन्म हुआ है प्रमाण सहायक, जिसे इंटरैक्टिव प्रमेय कहावतें भी कहा जाता है। ये सॉफ़्टवेयर उपकरण हैं जो Coq और Lean जैसे औपचारिक प्रमाण बनाने में सहायता करते हैं। Coq में, प्रूफ़ का प्रत्येक चरण अनिवार्य रूप से एक प्रोग्राम है, और प्रूफ़ की वैधता को टाइप-चेकिंग एल्गोरिदम के साथ जांचा जाता है। गणितज्ञ भी प्रमाण सहायकों का उपयोग कर रहे हैं - विशेष रूप से, लीन प्रमेय कहावत - गणित को औपचारिक बनाने के लिए, जिसमें गणितीय अवधारणाओं, प्रमेयों और प्रमाणों को एक कठोर, कंप्यूटर-सत्यापन योग्य प्रारूप में प्रस्तुत करना शामिल है। यह गणित की कभी-कभी अनौपचारिक भाषा को कंप्यूटर द्वारा जांचने की अनुमति देता है।

शोधकर्ता अभी भी गणित और प्रोग्रामिंग के बीच इस संबंध के परिणामों की खोज कर रहे हैं। मूल करी-हावर्ड पत्राचार प्रोग्रामिंग को एक प्रकार के तर्क के साथ जोड़ता है जिसे अंतर्ज्ञानवादी तर्क कहा जाता है, लेकिन यह पता चला है कि अधिक प्रकार के तर्क भी ऐसे एकीकरण के लिए उत्तरदायी हो सकते हैं।

"करी की अंतर्दृष्टि के बाद से सदी में क्या हुआ है कि हम अधिक से अधिक उदाहरणों की खोज करते रहते हैं जहां 'तार्किक प्रणाली एक्स कम्प्यूटेशनल प्रणाली वाई से मेल खाती है," ने कहा माइकल क्लार्कसन, कॉर्नेल विश्वविद्यालय में एक कंप्यूटर वैज्ञानिक। शोधकर्ताओं ने प्रोग्रामिंग को पहले से ही अन्य प्रकार के तर्क से जोड़ा है जैसे कि रैखिक तर्क, जिसमें "संसाधन" और मोडल तर्क की अवधारणा शामिल है, जो संभावना और आवश्यकता की अवधारणाओं से संबंधित है।

और जबकि इस पत्राचार में करी और हॉवर्ड के नाम हैं, वे किसी भी तरह से अकेले नहीं हैं जिन्होंने इसकी खोज की है। यह पत्राचार की मूलभूत प्रकृति को प्रमाणित करता है: लोग इसे बार-बार नोटिस करते रहते हैं। क्लार्कसन ने कहा, "यह कोई संयोग नहीं है कि गणना और तर्क के बीच गहरा संबंध है।"