तो, आप अभी भी Hindley-Milner को नहीं समझते हैं? भाग २

भाग 1 में, हमने हिंदले-मिलनर औपचारिकता के लिए किन बिल्डिंग ब्लॉक्स की जरूरत है , इस बारे में बात की और इस पोस्ट में हम उनकी परिभाषाएँ निर्दिष्ट करते हैं और औपचारिकता को पूरी तरह से तैयार करते हैं:

अभिव्यक्ति की अवधारणा का औपचारिककरण

हम एक अभिव्यक्ति की पुनरावर्ती परिभाषा देंगे; दूसरे शब्दों में, हम अधिकांश प्रकार के अभिव्यक्तियों को परिभाषित करेंगे, आपको बताएंगे कि मौजूदा के आधार पर नए, अधिक जटिल अभिव्यक्ति कैसे बनाएं, और यह दर्शाएं कि केवल वैध अभिव्यक्तियों को इस तरह से बनाया जा सकता है।

1. चर मान्य अभिव्यक्ति हैं।
2. यदि e एक मनमाना अभिव्यक्ति है, और x एक मनमाना चर है, तो λx.e एक अभिव्यक्ति है। यह e को एक सामान्य (लेकिन जरूरी नहीं) जटिल अभिव्यक्ति के रूप में सोचने में मदद करता है जिसमें x , अर्थात् शामिल हैं। x +2 , और फिर λx.e बारे में एक अनाम फ़ंक्शन के रूप में जो x को इनपुट के रूप में लेता है और x दिए गए मान के लिए अभिव्यक्ति e के मूल्यांकन का परिणाम देता है। सीधे शब्दों में कहें, यह के रूप में लगता है
   

    function(x) { return x^2 + 2; } 

3. यदि f और e वैध अभिव्यक्ति हैं, तो f(e) भी मान्य है। इसे स्पष्ट कारणों के लिए आवेदन कहा जाता है।
4. यदि x एक चर है, और e ₁ और e ₀ वैध अभिव्यक्तियाँ हैं, तो x की प्रत्येक घटना को e _{1 के} साथ e ₁ से प्रतिस्थापित करना भी एक मान्य अभिव्यक्ति देगा। अर्थात, यदि, उदाहरण के लिए, e ₁ = x and +2 और e ₀ = y/3 , तो x = e ₀ को e ₁ में सेट करने पर, हम अभिव्यक्ति (y/3) for +2 ।
   [एनबी: अंतिम पैराग्राफ निरर्थक है और अभिव्यक्ति के लिए लैम्ब्डा कैलकुलस की परिभाषा में आधिकारिक तौर पर शामिल नहीं है, क्योंकि e ₀ को x _{1 के} रूप में प्रतिस्थापित करना अमूर्त λx. को लागू करने के बराबर है λx. e _१ से e _० । यह केवल तथाकथित लेट-पोलीमोर्फिज्म का समर्थन करने के लिए जोड़ा गया है ।]

कुछ भी अधिक स्वीकार्य अभिव्यक्ति नहीं है।

एक तरफ: जो कोई भी इस मुद्दे पर पर्याप्त ध्यान देता है वह आश्चर्यचकित होगा: "एक मिनट रुको, मैं इसमें से कोई उपयोगी अभिव्यक्ति कैसे कर सकता हूं?" केवल पूर्वगामी के आधार पर मैं x ² +2 ² (या कम से कम सिर्फ 2) कैसे प्राप्त कर सकता हूं? अरे, शून्य का क्या? इन नियमों में एक पंक्ति नहीं है जो स्पष्ट रूप से अभिव्यक्ति 0. की ओर ले जाती है। इस मामले में समाधान लैम्ब्डा कैलकुलस में एक अभिव्यक्ति का निर्माण करना है, जो कि 0,1, ..., +, ×, -, / जैसी सही व्याख्या के साथ व्यवहार करता है। दूसरे शब्दों में, हमें संख्याओं, अंकगणितीय परिचालनों, तारों आदि को एनकोड करना चाहिए। पैटर्न में जो हम लैम्ब्डा सिंटैक्स का उपयोग करके बना सकते हैं। इस पोस्ट में संख्याओं और अंकगणितीय कार्यों पर एक छोटा लेकिन बहुत अच्छा खंड है। यह लैम्ब्डा कैलकुलस की एक दिलचस्प विशेषता है: हमारे पास प्राथमिक सिंटैक्स है जिसे हम चार सरल बिंदुओं के साथ पुनरावर्ती रूप से परिभाषित कर सकते हैं, लेकिन यह हमें चार मुख्य चरणों में कई चीजों को सम्मिलित रूप से साबित करने की अनुमति देता है, क्योंकि भाषा में ही संख्याओं, तारों और सभी प्रकारों को लिखने की अभिव्यंजक शक्ति है। संचालन जिनकी हमें आवश्यकता हो सकती है।

दावा औपचारिककरण टाइप करें

किसी भी अभिव्यक्ति को ऐसे मानें कि " e " हमारी बेस-भाषा से किसी भी एक्सप्रेशन को दर्शाते हुए हमारी मेटा-भाषा में परिवर्तनशील है। उदाहरण के लिए, जैसे कि निम्न में से कोई भी:

 x Math.pow(x,2) [1,2].forEach ( function(x) { print(x); } ) 

फिर, यदि t एक मनमाना प्रकार है, तो हम " e है टाइप t " के संदर्भ में व्यक्त कर सकते हैं
e:t

जैसे e , t हमारी मेटा-भाषा में एक चर है जो आधार भाषा (इंट, स्ट्रिंग, आदि) में किसी भी प्रकार से मेल खा सकता है। और सिर्फ e , t किसी भी विशेष प्रकार के मिलान वैकल्पिक है।

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

1. यदि s और t प्रकार हैं, तो t → s; एक प्रकार का फ़ंक्शन है जो इनपुट पर t और आउटपुट पर s
2. यदि r एक प्रकार है, संभवतः अन्य प्रकारों से बना है (इसी तरह से t → s , t और s से बना है s, जिनमें से प्रत्येक, बदले में, संभवतः कुछ अन्य प्रकार की संरचना के रूप में दर्शाया जा सकता है), और α इस प्रकार का एक चर है, तब α.r एक प्रकार है।
   एक उदाहरण के बिना, ऊपर कुछ हद तक अर्थहीन लगता है:
   

    function (x) { return x; } 

   
   यह फंक्शन String → String का प्रकार है। या Int → Int । वास्तव में, किसी भी प्रकार के लिए t इसका प्रकार t → t । हम कहेंगे कि इसका टाइप say tt → t । प्रत्येक प्रकार के String → String या t → t एक "मोनोटाइप" है। ”Tt → t एक" बहुवचन "है। ऊपर लिखे एक के समान कार्य में एक सार बहुपद one tt → t , जिसका अर्थ है कि किसी भी वास्तविक प्रकार t यह टाइप t → t । उपरोक्त सभी को एक साथ रखते हुए, हमें ऐसा एक कॉम्पैक्ट सारांश रिकॉर्ड मिलता है:
   λ xx: ∀ α.α → α

दावा औपचारिककरण टाइप करें

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

मान लीजिए मैं पहले से ही अनुमान लगाने में सक्षम हूं कि duck चर प्रकार का Animal ।
इसके अलावा, मान लीजिए कि मैंने speak कि speak का एक तरीका है Animal -> String ।
फिर मैं यह speak(duck) सकता speak(duck) कि speak(duck) String का प्रकार है।

और इस रूप में फिट होने वाला कोई भी तर्क एक मान्य प्रकार का निष्कर्ष है।

हम इसे इस प्रकार औपचारिक रूप देते हैं:


इस नियम को [ऐप] (ओवरले के लिए) कहा जाता है, और यह उन लोगों में से एक है जो स्टैकऑवरफ्लो पर इस सवाल में मौजूद हैं। हम उसके बारे में और शेष नियमों के बारे में अगली पोस्ट में बात करेंगे। इस बीच, हम उन सभी प्रतीकों का पता लगाते हैं जो हम ऊपर मिले थे:

• To - उन स्थितियों के एक सेट से मेल खाती है जिसे हम पहले से जानते हैं, या, शायद, जिसे हम मान सकते हैं। अधिक आम तौर पर, (केवल बयानों के संग्रह (अभिव्यक्ति और उनके प्रकार) पर एक प्रतिबिंब है। और स्वाभाविक रूप से, पत्र के बारे में कुछ खास नहीं है nothing - ग्रीक कैपिटल अक्षरों का उपयोग अक्सर पदों के सेट को संदर्भित करने के लिए किया जाता है।
• St - "घूमने वाला दरवाज़ा", जिसका अर्थ है कि कुछ वापस लिया जा सकता है। उदाहरण के लिए, we x:t अर्थ है कि यदि हम an धारणा / स्वयंसिद्ध / मौजूदा ज्ञान के रूप में Γ से एक कथन लेते हैं, तो हम यह मान सकते हैं कि x टाइप t ।
• Ps - "एप्सिलॉन", का अर्थ किसी चीज़ से है। x:t that का अर्थ है कि कथन x:t संबंध ∈ से है।
• वह लंबी क्षैतिज रेखा। यह रेखा हमें बताती है कि यदि हम अंश को प्रारंभिक आधार के रूप में लेते हैं तो हम हर में स्थित निष्कर्ष निकाल सकते हैं। जो हमें चीजों को व्यक्त करने की अनुमति देता है जैसे: "यदि हम इसे और इसे प्राप्त कर सकते हैं, तो हम इसे और इसे भी प्राप्त कर सकते हैं।" उदाहरण के लिए:
  
  यदि हम यह कह सकते हैं कि y , then से टाइप that का है, तो हम यह घटा सकते हैं कि x , Γ से टाइप का है।

अगला कदम:

• भाग 3 , जिसमें हम सब कुछ एक साथ रखेंगे और एचएम एल्गोरिथ्म में उपयोग किए गए नियमों का एक विचार प्राप्त करेंगे।

अनुवादक का नोट: अनुवाद के बारे में पीएम की किसी भी टिप्पणी के लिए मैं बहुत आभारी रहूंगा।