टाइपिंग नियम: Difference between revisions
(Created page with "{{short description|How a type system assigns a type to a syntactic construction}} प्रकार सिद्धांत में, एक टाइपिंग न...") |
No edit summary |
||
| Line 1: | Line 1: | ||
{{short description|How a type system assigns a type to a syntactic construction}} | {{short description|How a type system assigns a type to a syntactic construction}} | ||
[[प्रकार सिद्धांत]] में, एक टाइपिंग नियम एक [[अनुमान नियम]] है जो वर्णन करता है कि कैसे एक [[प्रकार प्रणाली]] एक सिंटेक्स (प्रोग्रामिंग भाषा) निर्माण के लिए एक | [[प्रकार सिद्धांत|वर्ग सिद्धांत]] में, एक टाइपिंग नियम एक [[अनुमान नियम|निष्कर्ष नियम]] है | जो वर्णन करता है कि कैसे एक [[प्रकार प्रणाली|वर्ग सिस्टम]] एक सिंटेक्स (प्रोग्रामिंग भाषा) निर्माण के लिए एक वर्ग प्रदान करती है।<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="TAPL" />{{rp|92}} सांकेतिक रूप से, टाइपिंग संबंध सामान्यतः एक कोलन द्वारा दर्शाया जाता है, उदाहरण के लिए <math>e:\tau</math> दर्शाता है कि एक अभिव्यक्ति <math>e</math> वर्ग है | <math>\tau</math>. नियमों को सामान्यतः [[प्राकृतिक कटौती|प्राकृतिक परिणाम]] के अंकन का उपयोग करके निर्दिष्ट किया जाता है।<ref name="TAPL" />{{rp|26}} उदाहरण के लिए, निम्नलिखित टाइपिंग नियम [[बूलियन डेटा प्रकार|बूलियन डेटा वर्ग]] की सरल भाषा के लिए टाइपिंग संबंध निर्दिष्ट करते हैं |<ref name="TAPL" />{{rp|93}} | |||
:<math> | :<math> | ||
| Line 12: | Line 12: | ||
\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} | \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} | ||
</math> | </math> | ||
प्रत्येक नियम कहता है कि रेखा के नीचे का निष्कर्ष रेखा के ऊपर के परिसर से प्राप्त किया जा सकता है। पहले दो नियमों में रेखा के ऊपर कोई परिसर नहीं है | प्रत्येक नियम कहता है कि रेखा के नीचे का निष्कर्ष रेखा के ऊपर के परिसर से प्राप्त किया जा सकता है। पहले दो नियमों में रेखा के ऊपर कोई परिसर नहीं है | इसलिए वे [[अभिगृहीत]] हैं। तीसरे नियम में रेखा के ऊपर परिसर है | (विशेष रूप से, तीन परिसर), इसलिए यह एक निष्कर्ष नियम है। | ||
प्रोग्रामिंग भाषाओं में, एक [[चर (कंप्यूटर विज्ञान)]] का | प्रोग्रामिंग भाषाओं में, एक [[चर (कंप्यूटर विज्ञान)]] का वर्ग इस बात पर निर्भर करता है कि यह कहाँ [[बाध्य चर]] है | जिसके लिए संदर्भ-संवेदनशील टाइपिंग नियमों की आवश्यकता होती है। ये नियम टाइपिंग जजमेंट (गणितीय तर्क) द्वारा दिए जाते हैं | जो सामान्यतः <math>\Gamma \vdash e : \tau</math> लिखे जाते हैं | जो बताता है कि एक अभिव्यक्ति <math>e</math> वर्ग है | <math>\tau</math> एक टाइपिंग संदर्भ के अनुसार <math>\Gamma</math> जो चरों को उनके वर्गों से संबंधित करता है। इस संकेतन का उपयोग सरल रूप से टाइप किए गए लैम्ब्डा कैलकुलस में चर संदर्भों और लैम्ब्डा अमूर्तता के लिए टाइपिंग नियम देने के लिए किया जा सकता है |<ref name="TAPL" />{{rp|pages=101–102}} | ||
:<math> | :<math> | ||
| Line 20: | Line 20: | ||
\frac{\Gamma,x{:}\tau_1 \vdash e : \tau_2}{\Gamma \vdash (\lambda x{:}\tau_1.\,e) : \tau_1 \rightarrow \tau_2} | \frac{\Gamma,x{:}\tau_1 \vdash e : \tau_2}{\Gamma \vdash (\lambda x{:}\tau_1.\,e) : \tau_1 \rightarrow \tau_2} | ||
</math> | </math> | ||
इसी | इसी वर्ग, निम्नलिखित टाइपिंग नियम [[मानक एमएल]] <math>\mathbf{let}</math> निर्माण का वर्णन करता है | | ||
:<math> | :<math> | ||
| Line 26: | Line 26: | ||
\Gamma \vdash \mathbf{let}\ x = e_1\ \mathbf{in}\ e_2\ \mathbf{end} : \tau_2} | \Gamma \vdash \mathbf{let}\ x = e_1\ \mathbf{in}\ e_2\ \mathbf{end} : \tau_2} | ||
</math> | </math> | ||
टाइपिंग नियमों की सभी प्रणालियाँ सीधे | टाइपिंग नियमों की सभी प्रणालियाँ सीधे वर्ग जाँच एल्गोरिथम निर्दिष्ट नहीं करती हैं। उदाहरण के लिए, हिंडले-मिलनर वर्ग सिस्टम में एक [[पैरामीट्रिक बहुरूपता]] फ़ंक्शन को प्रयुक्त करने के लिए टाइपिंग नियम के लिए उपयुक्त वर्ग का निष्कर्ष लगाने की आवश्यकता होती है | जिस पर फ़ंक्शन को तत्काल किया जाना चाहिए।<ref>{{cite journal |last1=Clément |first1=Dominique |last2=Despeyroux |first2=Thierry |last3=Kahn |first3=Gilles |last4=Despeyroux |first4=Joëlle |title=A simple applicative language: mini-ML |journal=Proceedings of the 1986 ACM Conference on LISP and Functional Programming |date=8 August 1986 |pages=13–27 |doi=10.1145/319838.319847 |url=https://dl.acm.org/doi/10.1145/319838.319847 |publisher=Association for Computing Machinery|isbn=0897912004 |s2cid=5126579 }}</ref> डिसाइडेबिलिटी (तर्क) एल्गोरिथ्म के लिए एक घोषणात्मक नियम सिस्टम को अपनाने के लिए एक अलग, एल्गोरिथम सिस्टम के उत्पादन की आवश्यकता होती है | जिसे समान टाइपिंग संबंध निर्दिष्ट करने के लिए सिद्ध किया जा सकता है।<ref>{{cite journal |last1=Dunfield |first1=Jana |last2=Krishnaswami |first2=Neel |title=द्विदिश टाइपिंग|journal=ACM Computing Surveys |date=23 May 2021 |volume=54 |issue=5 |page=98:19 |doi=10.1145/3450952 |s2cid=201058734 |issn=0360-0300|doi-access=free }}</ref> | ||
Revision as of 17:34, 23 May 2023
वर्ग सिद्धांत में, एक टाइपिंग नियम एक निष्कर्ष नियम है | जो वर्णन करता है कि कैसे एक वर्ग सिस्टम एक सिंटेक्स (प्रोग्रामिंग भाषा) निर्माण के लिए एक वर्ग प्रदान करती है।[1]: 94 इन नियमों को टाइप सिस्टम द्वारा यह निर्धारित करने के लिए प्रयुक्त किया जा सकता है कि क्या कंप्यूटर प्रोग्राम अच्छी तरह से टाइप किया गया है और किस वर्ग की अभिव्यक्ति (कंप्यूटर विज्ञान) है। टाइपिंग नियमों के उपयोग का एक प्रोटोटाइपिकल उदाहरण सामान्य रूप से टाइप किए गए लैम्ब्डा कैलकुलस में परिभाषित वर्ग के निष्कर्ष में है | जो कार्टेशियन बंद श्रेणियों की आंतरिक भाषा है।[2]
टिप्पणी
टाइपिंग नियम एक टाइपिंग संबंध (गणित) की संरचना को निर्दिष्ट करते हैं | जो वाक्यात्मक शब्दों को उनके वर्गों से संबंधित करता है।[1]: 92 सांकेतिक रूप से, टाइपिंग संबंध सामान्यतः एक कोलन द्वारा दर्शाया जाता है, उदाहरण के लिए दर्शाता है कि एक अभिव्यक्ति वर्ग है | . नियमों को सामान्यतः प्राकृतिक परिणाम के अंकन का उपयोग करके निर्दिष्ट किया जाता है।[1]: 26 उदाहरण के लिए, निम्नलिखित टाइपिंग नियम बूलियन डेटा वर्ग की सरल भाषा के लिए टाइपिंग संबंध निर्दिष्ट करते हैं |[1]: 93
प्रत्येक नियम कहता है कि रेखा के नीचे का निष्कर्ष रेखा के ऊपर के परिसर से प्राप्त किया जा सकता है। पहले दो नियमों में रेखा के ऊपर कोई परिसर नहीं है | इसलिए वे अभिगृहीत हैं। तीसरे नियम में रेखा के ऊपर परिसर है | (विशेष रूप से, तीन परिसर), इसलिए यह एक निष्कर्ष नियम है।
प्रोग्रामिंग भाषाओं में, एक चर (कंप्यूटर विज्ञान) का वर्ग इस बात पर निर्भर करता है कि यह कहाँ बाध्य चर है | जिसके लिए संदर्भ-संवेदनशील टाइपिंग नियमों की आवश्यकता होती है। ये नियम टाइपिंग जजमेंट (गणितीय तर्क) द्वारा दिए जाते हैं | जो सामान्यतः लिखे जाते हैं | जो बताता है कि एक अभिव्यक्ति वर्ग है | एक टाइपिंग संदर्भ के अनुसार जो चरों को उनके वर्गों से संबंधित करता है। इस संकेतन का उपयोग सरल रूप से टाइप किए गए लैम्ब्डा कैलकुलस में चर संदर्भों और लैम्ब्डा अमूर्तता के लिए टाइपिंग नियम देने के लिए किया जा सकता है |[1]: 101–102
इसी वर्ग, निम्नलिखित टाइपिंग नियम मानक एमएल निर्माण का वर्णन करता है |
टाइपिंग नियमों की सभी प्रणालियाँ सीधे वर्ग जाँच एल्गोरिथम निर्दिष्ट नहीं करती हैं। उदाहरण के लिए, हिंडले-मिलनर वर्ग सिस्टम में एक पैरामीट्रिक बहुरूपता फ़ंक्शन को प्रयुक्त करने के लिए टाइपिंग नियम के लिए उपयुक्त वर्ग का निष्कर्ष लगाने की आवश्यकता होती है | जिस पर फ़ंक्शन को तत्काल किया जाना चाहिए।[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.
- ↑ 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.
This programming language theory or type theory-related article is a stub. You can help Wikipedia by expanding it. |
