एक बार हम
जोश लांग और काम के कुछ अन्य दोस्तों के साथ एक बार में बैठे, जब उन्हें पता चला कि मैं गणित में "अरे!" और वह अभी हाल ही में
StackOverflow पर इस सवाल पर आए और अब मुझसे पूछा कि इसका क्या मतलब है:
हालांकि, इस चीनी पत्र के अर्थ को स्पष्ट करने से पहले, मुझे लगता है, सिद्धांत रूप में, यह विचार करने के लायक है कि यह बिल्कुल क्यों आवश्यक है।
डैनियल स्पिवाक की ब्लॉग पोस्ट (
अनुवाद ) हिंडले-मिलनर एल्गोरिथ्म के अंतिम लक्ष्य (इसके अनुप्रयोग के गहन उदाहरण के अलावा) का एक बहुत अच्छा विवरण प्रदान करती है:
कार्यात्मक रूप से, हिंडले-मिलनर (या डैमस-मिलनर) एक एल्गोरिथ्म है जो कि किस प्रकार उपयोग किया जाता है, इस पर विचार करने के आधार पर टाइप निष्कर्ष के लिए एक एल्गोरिथम है। यह शाब्दिक रूप से सहज ज्ञान को दर्शाता है कि एक प्रकार कार्यक्षमता के माध्यम से अनुमान लगाया जा सकता है जो इसे समर्थन करता है।
इसलिए, हम किसी भी दिए गए एक्सप्रेशन के लिए टाइप इनफॉरमेशन एल्गोरिथम को औपचारिक रूप देना चाहते हैं। इस पोस्ट में, मैं इस पर ध्यान केंद्रित करने जा रहा हूं कि इसका अर्थ "किसी चीज़ को औपचारिक बनाना" है, और फिर हिंडले-मिलनर औपचारिकता के "निर्माण ब्लॉकों" का वर्णन करें। दूसरे भाग में मैं इन ब्लॉकों का अधिक विशिष्ट विवरण दूंगा। अंत में, भाग तीन में, मैं StackOverflow से प्रश्न का अनुवाद करूंगा।
औपचारिकता का क्या अर्थ है?
इसलिए, हम भावों के बारे में बात करने जा रहे हैं। मुक्त अभिव्यक्ति। किसी भी भाषा में। हम इन अभिव्यक्तियों के प्रकार के बारे में भी बात करना चाहते हैं। और हम उन नियमों का पता लगाना चाहते हैं जिनके द्वारा हम टाइप कर सकते हैं। और फिर हम एक एल्गोरिथ्म बनाना चाहते हैं जो इन नियमों का उपयोग करता है। इसलिए हमें कुछ मेटा-भाषा की आवश्यकता है। ऐसा है कि इसकी मदद से किसी भी मनमानी प्रोग्रामिंग भाषा में अभिव्यक्ति के बारे में बात करना संभव होगा। यह मेटा-भाषा चाहिए:
- सार और सामान्य होने के लिए हमें सामग्री के बारे में चिंता किए बिना, उनके प्रकार (इसलिए औपचारिकता ) के आधार पर केवल प्रकार के अनुमान के बयानों के बारे में बात करने की अनुमति देने के लिए
- अभिव्यक्ति क्या है, इसकी सटीक, स्पष्ट लेकिन सहज परिभाषा दें
- यह परिभाषा कम संख्या में निर्विवाद आदिम अवधारणाओं के संदर्भ में देने के लिए
- इसी प्रकार, प्रकारों के लिए एक परिभाषा दीजिए, यह विचार कि एक अभिव्यक्ति का एक प्रकार है, और यह विचार कि हम यह बता सकते हैं कि यह अभिव्यक्ति एक दिया हुआ प्रकार है
- एक सरल, संक्षिप्त प्रतीकात्मक प्रतिनिधित्व के आगे झुकना। यानी यह कहने के बजाय "पहली अभिव्यक्ति को दूसरी अभिव्यक्ति पर लागू करने से बनने वाली अभिव्यक्ति में स्ट्रिंग से कुछ प्रकार होता है जिसे हमें इस संदर्भ में विशेषज्ञता की आवश्यकता नहीं होती है," हम बस "
e 1 ( e 2 )" कह सकते हैं: String → t " - किसी ऐसी चीज़ में अनुवाद करना आसान है जिसे कंप्यूटर समझ सकता है और लागू कर सकता है ताकि वह पूरी तरह से आक्षेप को स्वचालित कर सके
उपरोक्त अधिक बारीकियों को बताने के लिए, आइए औपचारिककरण के एक बहुत ही संक्षिप्त उदाहरण पर ध्यान दें। क्या होगा अगर, एक मनमाने ढंग से प्रोग्रामिंग भाषा में अभिव्यक्ति के प्रकार के बारे में बात करने के लिए एक भाषा को औपचारिक बनाने के बजाय, हम एक प्राकृतिक प्राकृतिक भाषा में एक बयान की सच्चाई के बारे में बात करने के लिए एक भाषा को औपचारिक बनाना चाहते हैं? औपचारिकता के बिना, हम कुछ कह सकते हैं:
मान लीजिए मुझे पता है कि अगर बारिश होती है, तो बॉब हमेशा एक छाता लेता है।
और मान लीजिए मुझे पता है कि अब बारिश हो रही है।
इस प्रकार, मैं यह निष्कर्ष निकाल सकता हूं कि बॉब ने छाता लिया।
और इस तरह के निष्कर्ष के लिए एक ही तर्क रखने वाला कोई भी तर्क मान्य है।
प्रॉपोजल कैलकुलस इन सभी चीजों को एक नियम के रूप में औपचारिक रूप देता है, जिसे मोडस पोंनस ("अनुमान नियम") के रूप में जाना जाता है:
जहां
और
एक अनियंत्रित प्राकृतिक भाषा में कथन (उर्फ वाक्य या प्रावधान) का प्रतिनिधित्व करने वाले चर हैं।
अब आइए हिंडले-मिलनर औपचारिकता के निर्माण खंडों को सूचीबद्ध करें:
औपचारिकता बिल्डिंग ब्लॉक्स
हमें आवश्यकता होगी:
- अभिव्यक्ति के बारे में बात करने का एक औपचारिक तरीका। यह औपचारिकता ऊपर सूचीबद्ध मानदंडों को पूरा करना चाहिए; इस उद्देश्य के लिए हम लैम्ब्डा कैलकुलस का उपयोग करते हैं। मैं एक मिनट में सब कुछ समझा दूंगा, लेकिन अलौकिक कुछ भी नहीं है
- प्रकारों के बारे में बात करने का एक औपचारिक तरीका, और प्रकारों और अभिव्यक्तियों के बारे में बात करने का एक औपचारिक तरीका। अंत में, Hindley-Milner एल्गोरिथ्म का लक्ष्य एक निष्कर्ष निकालने में सक्षम होना है जैसे "अभिव्यक्ति
e टाइप t " - अन्य कथनों के माध्यम से अभिव्यक्ति के प्रकार के बारे में कथन प्राप्त करने के लिए नियमों का एक औपचारिक सेट। ये नियम इस प्रकार हैं: "यदि मैं पहले से ही प्रदर्शित कर सकता हूँ कि कुछ अभिव्यक्ति का एक प्रकार है और दूसरी अभिव्यक्ति दूसरी प्रकार की है, तो तीसरी अभिव्यक्ति का तीसरा प्रकार होगा।" नियमों का यह सेट ठीक वैसा ही है जैसा आप स्टैकऑवरफ्लो प्रश्न में देखते हैं । मैं इसका पूरा विस्तार से अनुवाद करूंगा
- प्रारंभिक बिंदु से आवश्यक कथन प्राप्त करने के लिए एल्गोरिथ्म को निष्कर्ष नियमों का उचित उपयोग करना चाहिए: "अभिव्यक्ति
e मेरी रुचि t प्रकार की t "। "हिंडले-मिलनर एल्गोरिथ्म" वाक्यांश में "एल्गोरिथ्म" भाग इसके लिए जिम्मेदार है, और इन पदों में मैं इस मुद्दे पर चर्चा करने की योजना नहीं बनाता हूं।
अच्छा, चलिए!
- भाग 2 , जिसमें हम स्पष्ट रूप से पैराग्राफ 1 और 2 को परिभाषित करते हैं
- भाग 3 , जिसमें हम खंड 3 से प्रकार के निष्कर्ष नियमों का अनुवाद करते हैं
अनुवादक का नोट: अनुवाद के बारे में पीएम की किसी भी टिप्पणी के लिए मैं बहुत आभारी रहूंगा।