Tipo de habitabilidad

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 . ${\estilo de visualización \tau}$ ${\estilo de visualización \Gamma}$${\estilo de visualización \lambda}$${\displaystyle \Gamma \vdash M:\tau}$${\estilo de visualización \tau}$

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 .

• Isomorfismo de Curry-Howard