टाइपिंग नियम

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

नोटेशन

टंकण नियम एक टंकण संबंध (गणित) की संरचना को निर्दिष्ट करते हैं जो वाक्यात्मक शब्दों को उनके प्रकारों से संबंधित करता है। सांकेतिक रूप से, टाइपिंग संबंध आमतौर पर एक कोलन द्वारा दर्शाया जाता है, उदाहरण के लिए $e:\tau$ दर्शाता है कि एक अभिव्यक्ति $e$ प्रकार है $\tau$. नियमों को आमतौर पर प्राकृतिक कटौती के अंकन का उपयोग करके निर्दिष्ट किया जाता है। उदाहरण के लिए, निम्नलिखित टंकण नियम बूलियन डेटा प्रकार की सरल भाषा के लिए टंकण संबंध निर्दिष्ट करते हैं:

${\frac {}{{\mathsf {true}}:{\mathsf {Bool}}}}\qquad {\frac {}{{\mathsf {false}}:{\mathsf {Bool}}}}\qquad {\frac {e_{1}:{\mathsf {Bool}}\quad \;e_{2}:\tau \quad \;e_{3}:\tau }{\mathbf {if} \ e_{1}\ \mathbf {then} \ e_{2}\ \mathbf {else} \ e_{3}:\tau }}$

प्रत्येक नियम कहता है कि रेखा के नीचे का निष्कर्ष रेखा के ऊपर के परिसर से प्राप्त किया जा सकता है। पहले दो नियमों में रेखा के ऊपर कोई परिसर नहीं है, इसलिए वे अभिगृहीत हैं। तीसरे नियम में रेखा के ऊपर परिसर है (विशेष रूप से, तीन परिसर), इसलिए यह एक अनुमान नियम है।

प्रोग्रामिंग भाषाओं में, एक चर (कंप्यूटर विज्ञान) का प्रकार इस बात पर निर्भर करता है कि यह कहाँ बाध्य चर है, जिसके लिए संदर्भ-संवेदनशील टाइपिंग नियमों की आवश्यकता होती है। ये नियम टाइपिंग जजमेंट (गणितीय तर्क) द्वारा दिए जाते हैं, जो आमतौर पर लिखे जाते हैं $\Gamma \vdash e:\tau$, जो बताता है कि एक अभिव्यक्ति $e$ प्रकार है $\tau$ एक टाइपिंग संदर्भ के तहत $\Gamma$ जो चरों को उनके प्रकारों से संबंधित करता है। इस संकेतन का उपयोग सरल रूप से टाइप किए गए लैम्ब्डा कैलकुलस में चर संदर्भों और लैम्ब्डा अमूर्तता के लिए टाइपिंग नियम देने के लिए किया जा सकता है:

${\frac {x{:}\tau \in \Gamma }{\Gamma \vdash x:\tau }}\qquad {\frac {\Gamma ,x{:}\tau _{1}\vdash e:\tau _{2}}{\Gamma \vdash (\lambda x{:}\tau _{1}.\,e):\tau _{1}\rightarrow \tau _{2}}}$

इसी प्रकार, निम्नलिखित टाइपिंग नियम का वर्णन करता है $\mathbf {let}$ मानक एमएल का निर्माण:

${\frac {\Gamma \vdash e_{1}:\tau _{1}\qquad \Gamma ,x{:}\tau _{1}\vdash e:\tau _{2}}{\Gamma \vdash \mathbf {let} \ x=e_{1}\ \mathbf {in} \ e_{2}\ \mathbf {end} :\tau _{2}}}$

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

यह भी देखें

• निर्णय (गणितीय तर्क)
• टाइप सिस्टम
• सिद्धांत टाइप करें
• करी-हावर्ड पत्राचार
• अनुक्रमिक पथरी

अग्रिम पठन

• Cardelli, Luca (March 1996). "Type Systems" (PDF). ACM Computing Surveys. 28 (1): 263–264. doi:10.1145/234313.234418. S2CID 227408784.