टाइपिंग नियम

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

टिप्पणी

टाइपिंग नियम एक टाइपिंग संबंध (गणित) की संरचना को निर्दिष्ट करते हैं | जो वाक्यात्मक शब्दों को उनके वर्गों से संबंधित करता है। सांकेतिक रूप से, टाइपिंग संबंध सामान्यतः एक कोलन द्वारा दर्शाया जाता है, उदाहरण के लिए $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.