टाइपिंग नियम

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

टिप्पणी

टाइपिंग नियम एक टाइपिंग संबंध (गणित) की संरचना को निर्दिष्ट करते हैं | जो वाक्यात्मक शब्दों को उनके वर्गों से संबंधित करता है। सांकेतिक रूप से, टाइपिंग संबंध सामान्यतः एक कोलन द्वारा दर्शाया जाता है, उदाहरण के लिए $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{\mathrm{\Gamma <!--\; \Gamma \; -->}⊢<!--\; ⊢\; -->e_1:{\mathrm{\tau <!--\; \tau \; -->}}_1\mathrm{\Gamma <!--\; \Gamma \; -->},x:{\mathrm{\tau <!--\; \tau \; -->}}_1⊢<!--\; ⊢\; -->e:{\mathrm{\tau <!--\; \tau \; -->}}_2}{\mathrm{\Gamma <!--\; \Gamma \; -->}⊢<!--\; ⊢\; -->\mathbf{l}\mathbf{e}\mathbf{t}x=e_1}$