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

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

तर्क से संबंध

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

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

औपचारिक गुण

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

यह भी देखें

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