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