टाइपिंग नियम: Difference between revisions

Revision as of 17:37, 23 May 2023

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

जिस पर फ़ंक्शन को तत्काल किया जाना चाहिए।^[3] डिसाइडेबिलिटी (तर्क) एल्गोरिथ्म के लिए एक घोषणात्मक नियम सिस्टम को

टिप्पणी

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

{\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$ जो चरों को उनके वर्गों से संबंधित करता है। इस संकेतन का उपयोग सरल रूप से टाइप किए गए लैम्ब्डा कैलकुलस में चर संदर्भों और लैम्ब्डा अमूर्तता के लिए टाइपिंग नियम देने के लिए किया जा सकता है |^[1]^{: 101–102}

{\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}}}

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

यह भी देखें

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

संदर्भ

↑ ^1.0 ^1.1 ^1.2 ^1.3 ^1.4 Pierce, Benjamin C. (2002). प्रकार और प्रोग्रामिंग भाषाएँ (1st ed.). Cambridge, Mass.: MIT Press. ISBN 0262162091.
↑ Baez, John. "The n-Category Café". golem.ph.utexas.edu (in English). Retrieved 30 September 2022.
↑ ^3.0 ^3.1 Clément, Dominique; Despeyroux, Thierry; Kahn, Gilles; Despeyroux, Joëlle (8 August 1986). "A simple applicative language: mini-ML". Proceedings of the 1986 ACM Conference on LISP and Functional Programming. Association for Computing Machinery: 13–27. doi:10.1145/319838.319847. ISBN 0897912004. S2CID 5126579.
↑ Dunfield, Jana; Krishnaswami, Neel (23 May 2021). "द्विदिश टाइपिंग". ACM Computing Surveys. 54 (5): 98:19. doi:10.1145/3450952. ISSN 0360-0300. S2CID 201058734.

अग्रिम पठन

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

\Gamma \!\vdash

This programming language theory or type theory-related article is a stub. You can help Wikipedia by expanding it.

[TAPL-1] 1.0 ^1.1 ^1.2 ^1.3 ^1.4 Pierce, Benjamin C. (2002). प्रकार और प्रोग्रामिंग भाषाएँ (1st ed.). Cambridge, Mass.: MIT Press. ISBN 0262162091.

[2] Baez, John. "The n-Category Café". golem.ph.utexas.edu (in English). Retrieved 30 September 2022.

[:0-3] 3.0 ^3.1 Clément, Dominique; Despeyroux, Thierry; Kahn, Gilles; Despeyroux, Joëlle (8 August 1986). "A simple applicative language: mini-ML". Proceedings of the 1986 ACM Conference on LISP and Functional Programming. Association for Computing Machinery: 13–27. doi:10.1145/319838.319847. ISBN 0897912004. S2CID 5126579.

[:1-4] Dunfield, Jana; Krishnaswami, Neel (23 May 2021). "द्विदिश टाइपिंग". ACM Computing Surveys. 54 (5): 98:19. doi:10.1145/3450952. ISSN 0360-0300. S2CID 201058734.

[1]

[2]

[3]

[4]

@@ Line 3: / Line 3: @@
 [[प्रकार सिद्धांत|वर्ग सिद्धांत]] में, एक टाइपिंग नियम एक [[अनुमान नियम|निष्कर्ष नियम]] है | जो वर्णन करता है कि कैसे एक [[प्रकार प्रणाली|वर्ग सिस्टम]] एक सिंटेक्स (प्रोग्रामिंग भाषा) निर्माण के लिए एक वर्ग प्रदान करती है।<ref name="TAPL">{{cite book |last1=Pierce |first1=Benjamin C. |title=प्रकार और प्रोग्रामिंग भाषाएँ|date=2002 |publisher=MIT Press |location=Cambridge, Mass. |isbn=0262162091 |edition=1st}}</ref>{{rp|94}} इन नियमों को टाइप सिस्टम द्वारा यह निर्धारित करने के लिए प्रयुक्त किया जा सकता है कि क्या [[कंप्यूटर प्रोग्राम]] अच्छी तरह से टाइप किया गया है और किस वर्ग की [[अभिव्यक्ति (कंप्यूटर विज्ञान)]] है। टाइपिंग नियमों के उपयोग का एक प्रोटोटाइपिकल उदाहरण सामान्य रूप से टाइप किए गए लैम्ब्डा कैलकुलस में परिभाषित वर्ग के निष्कर्ष में है | जो कार्टेशियन बंद श्रेणियों की [[आंतरिक भाषा]] है।<ref>{{cite web |last1=Baez |first1=John |title=The n-Category Café |url=https://golem.ph.utexas.edu/category/2006/08/cartesian_closed_categories_an_1.html |website=golem.ph.utexas.edu |access-date=30 September 2022 |language=en}}</ref>
-'''जिस पर फ़ंक्शन को तत्काल किया जाना चाहिए।<ref name=":0" /> डिसाइडेबिलिटी (तर्क) एल्गोरिथ्म के लिए एक घोषणात्मक नियम सिस्टम को अपनाने के लिए एक अलग, एल्गोरिथम सिस्टम के उत्पादन की आवश्यकता होती है | जिसे समान टाइपिंग संबंध निर्दिष्ट करने के लिए सिद्ध किया जा सकता है।<ref name=":1" />'''
+'''जिस पर फ़ंक्शन को तत्काल किया जाना चाहिए।<ref name=":0" /> डिसाइडेबिलिटी (तर्क) एल्गोरिथ्म के लिए एक घोषणात्मक नियम सिस्टम को'''
 == टिप्पणी ==
 टाइपिंग नियम एक टाइपिंग [[संबंध (गणित)]] की संरचना को निर्दिष्ट करते हैं | जो वाक्यात्मक शब्दों को उनके वर्गों से संबंधित करता है।<ref name="TAPL" />{{rp|92}} सांकेतिक रूप से, टाइपिंग संबंध सामान्यतः एक कोलन द्वारा दर्शाया जाता है, उदाहरण के लिए <math>e:\tau</math> दर्शाता है कि एक अभिव्यक्ति <math>e</math> वर्ग है | <math>\tau</math>. नियमों को सामान्यतः [[प्राकृतिक कटौती|प्राकृतिक परिणाम]] के अंकन का उपयोग करके निर्दिष्ट किया जाता है।<ref name="TAPL" />{{rp|26}} उदाहरण के लिए, निम्नलिखित टाइपिंग नियम [[बूलियन डेटा प्रकार|बूलियन डेटा वर्ग]] की सरल भाषा के लिए टाइपिंग संबंध निर्दिष्ट करते हैं |<ref name="TAPL" />{{rp|93}}

Anonymous

Search

टाइपिंग नियम: Difference between revisions

Namespaces

More

Page actions

Revision as of 17:37, 23 May 2023

Contents

टिप्पणी

यह भी देखें

संदर्भ

अग्रिम पठन

Navigation

Navigation

Wiki tools

Wiki tools

Anonymous

Search

टाइपिंग नियम: Difference between revisions

Revision as of 17:37, 23 May 2023

टिप्पणी

यह भी देखें

संदर्भ

अग्रिम पठन

Navigation

Wiki tools

Page tools

Other projects

Categories