आवास टाइप करें

प्रकार सिद्धांत में, गणितीय तर्क की एक शाखा, किसी दिए गए टाइप किए गए कैलकुलस में, इस कैलकुलस के लिए टाइप इनहेबिटेशन समस्या निम्न समस्या है: एक प्रकार दिया $\tau$ और एक टाइपिंग वातावरण $\Gamma$, क्या कोई उपस्तिथ है $\lambda$-टर्म एम ऐसा है कि $\Gamma \vdash M:\tau$? एक खाली प्रकार के वातावरण के साथ, ऐसा M का निवासी कहा जाता है $\tau$.

तर्क से संबंध

बस टाइप किए गए लैम्ब्डा कैलकुस के स्थितियों में, एक प्रकार में निवासी होता है यदि और एकमात्र यदि इसकी करी-हावर्ड प्रस्ताव न्यूनतम निहितार्थ तर्क का एक टॉटोलॉजी (तर्क) है। इसी तरह, एक सिस्टम एफ प्रकार में एक निवासी है यदि और एकमात्र यदि इसकी करी-हावर्ड प्रस्ताव अंतर्ज्ञानवादी तर्क दूसरे क्रम के तर्क का एक पुनरुत्पादन है।

गिरार्ड का विरोधाभास दर्शाता है कि प्रकार का आवास करी-हावर्ड पत्राचार के साथ एक प्रकार की प्रणाली की स्थिरता से दृढ़ता से संबंधित है। ध्वनि होने के लिए, ऐसी प्रणाली में निर्जन प्रकार होना चाहिए।

औपचारिक गुण

अधिकांश टाइप की गई गणनाओं के लिए, टाइप इनहेबिटेशन समस्या बहुत कठिन है। रिचर्ड स्टेटमैन ने सिद्ध किया कि एकमात्र टाइप किए गए लैम्ब्डा कैलकुस के लिए टाइप इनहेबिटेशन समस्या पीएसपीएसीई-पूर्ण है। अन्य गणनाओं के लिए, प्रणाली एफ की तरह, समस्या निर्णय समस्या भी है।

यह भी देखें

• करी-हावर्ड समरूपता