En teoría de tipos , una rama de la lógica matemática , en un cálculo tipado dado , el problema de habitabilidad de tipo para este cálculo es el siguiente problema: [1] dado un tipo y un entorno de tipado , ¿existe un término M tal que ? Con un entorno de tipos vacío, se dice que dicho M es un habitante de .
En el caso del cálculo lambda de tipos simples , un tipo tiene un habitante si y solo si su proposición correspondiente es una tautología de lógica implicativa mínima. De manera similar, un tipo del Sistema F tiene un habitante si y solo si su proposición correspondiente es una tautología de lógica intuicionista de segundo orden .
La paradoja de Girard muestra que la presencia de tipos está estrechamente relacionada con la consistencia de un sistema de tipos con correspondencia Curry-Howard. Para que sea sólido, un sistema de este tipo debe tener tipos no presentes.
Para la mayoría de los cálculos tipificados, el problema de habitabilidad de tipo es muy difícil . Richard Statman demostró que para el cálculo lambda tipificado de forma simple, el problema de habitabilidad de tipo es PSPACE-completo . Para otros cálculos, como el Sistema F , el problema es incluso indecidible .
