आवास टाइप करें: Difference between revisions
No edit summary |
No edit summary |
||
| Line 1: | Line 1: | ||
[[ प्रकार सिद्धांत ]]में, [[गणितीय तर्क]] की एक शाखा, किसी दिए गए टाइप किए गए कैलकुलस में, इस कैलकुलस के लिए टाइप इनहेबिटेशन समस्या निम्न समस्या है:<ref>{{cite journal |title=टाइप किए गए लैम्ब्डा-कैलकुली में निवास (एक वाक्यात्मक दृष्टिकोण)|author=Pawel Urzyczyn |journal=Lecture Notes in Computer Science |pages=373–389 |year=1997 |volume=1210 |publisher=Springer |doi=10.1007/3-540-62688-3_47 |isbn=978-3-540-62688-6 |url=https://doi.org/10.1007%2F3-540-62688-3_47}}</ref> एक प्रकार दिया <math>\tau</math> और एक टाइपिंग वातावरण <math>\Gamma</math>, क्या कोई उपस्तिथ है <math>\lambda</math>-टर्म एम ऐसा है कि <math>\Gamma \vdash M : \tau</math>? एक खाली प्रकार के वातावरण के साथ, ऐसा | [[ प्रकार सिद्धांत ]]में, [[गणितीय तर्क]] की एक शाखा, किसी दिए गए टाइप किए गए कैलकुलस में, इस कैलकुलस के लिए टाइप इनहेबिटेशन समस्या निम्न समस्या है:<ref>{{cite journal |title=टाइप किए गए लैम्ब्डा-कैलकुली में निवास (एक वाक्यात्मक दृष्टिकोण)|author=Pawel Urzyczyn |journal=Lecture Notes in Computer Science |pages=373–389 |year=1997 |volume=1210 |publisher=Springer |doi=10.1007/3-540-62688-3_47 |isbn=978-3-540-62688-6 |url=https://doi.org/10.1007%2F3-540-62688-3_47}}</ref> एक प्रकार दिया <math>\tau</math> और एक टाइपिंग वातावरण <math>\Gamma</math>, क्या कोई उपस्तिथ है <math>\lambda</math>-टर्म एम ऐसा है कि <math>\Gamma \vdash M : \tau</math>? एक खाली प्रकार के वातावरण के साथ, ऐसा M का निवासी कहा जाता है <math>\tau</math>. | ||
== तर्क से संबंध == | == तर्क से संबंध == | ||
बस टाइप किए गए लैम्ब्डा कैलकुस के | बस टाइप किए गए लैम्ब्डा कैलकुस के स्थितियों में, एक प्रकार में निवासी होता है यदि और एकमात्र यदि इसकी [[करी-हावर्ड]] प्रस्ताव न्यूनतम निहितार्थ तर्क का एक [[टॉटोलॉजी (तर्क)]] है। इसी तरह, एक [[सिस्टम एफ]] प्रकार में एक निवासी है यदि और एकमात्र यदि इसकी करी-हावर्ड प्रस्ताव [[अंतर्ज्ञानवादी तर्क]] दूसरे क्रम के तर्क का एक पुनरुत्पादन है। | ||
गिरार्ड का विरोधाभास दर्शाता है कि प्रकार का आवास करी-हावर्ड पत्राचार के साथ एक प्रकार की प्रणाली की स्थिरता से दृढ़ता से संबंधित है। ध्वनि होने के लिए, ऐसी प्रणाली में निर्जन प्रकार होना चाहिए। | गिरार्ड का विरोधाभास दर्शाता है कि प्रकार का आवास करी-हावर्ड पत्राचार के साथ एक प्रकार की प्रणाली की स्थिरता से दृढ़ता से संबंधित है। ध्वनि होने के लिए, ऐसी प्रणाली में निर्जन प्रकार होना चाहिए। | ||
Revision as of 13:29, 21 May 2023
प्रकार सिद्धांत में, गणितीय तर्क की एक शाखा, किसी दिए गए टाइप किए गए कैलकुलस में, इस कैलकुलस के लिए टाइप इनहेबिटेशन समस्या निम्न समस्या है:[1] एक प्रकार दिया और एक टाइपिंग वातावरण , क्या कोई उपस्तिथ है -टर्म एम ऐसा है कि ? एक खाली प्रकार के वातावरण के साथ, ऐसा M का निवासी कहा जाता है .
तर्क से संबंध
बस टाइप किए गए लैम्ब्डा कैलकुस के स्थितियों में, एक प्रकार में निवासी होता है यदि और एकमात्र यदि इसकी करी-हावर्ड प्रस्ताव न्यूनतम निहितार्थ तर्क का एक टॉटोलॉजी (तर्क) है। इसी तरह, एक सिस्टम एफ प्रकार में एक निवासी है यदि और एकमात्र यदि इसकी करी-हावर्ड प्रस्ताव अंतर्ज्ञानवादी तर्क दूसरे क्रम के तर्क का एक पुनरुत्पादन है।
गिरार्ड का विरोधाभास दर्शाता है कि प्रकार का आवास करी-हावर्ड पत्राचार के साथ एक प्रकार की प्रणाली की स्थिरता से दृढ़ता से संबंधित है। ध्वनि होने के लिए, ऐसी प्रणाली में निर्जन प्रकार होना चाहिए।
औपचारिक गुण
अधिकांश टाइप की गई गणनाओं के लिए, टाइप इनहेबिटेशन समस्या बहुत कठिन है। रिचर्ड स्टेटमैन ने सिद्ध किया कि एकमात्र टाइप किए गए लैम्ब्डा कैलकुस के लिए टाइप इनहेबिटेशन समस्या पीएसपीएसीई-पूर्ण है। अन्य गणनाओं के लिए, प्रणाली एफ की तरह, समस्या निर्णय समस्या भी है।
यह भी देखें
- करी-हावर्ड समरूपता
संदर्भ
- ↑ Pawel Urzyczyn (1997). "टाइप किए गए लैम्ब्डा-कैलकुली में निवास (एक वाक्यात्मक दृष्टिकोण)". Lecture Notes in Computer Science. Springer. 1210: 373–389. doi:10.1007/3-540-62688-3_47. ISBN 978-3-540-62688-6.
This programming language theory or type theory-related article is a stub. You can help Wikipedia by expanding it. |
