En la teoría de tipos , una rama de la lógica matemática , en un cálculo tipificado dado, el problema de habitabilidad de tipos para este cálculo es el siguiente problema: [1] dado un tipoy un entorno de escritura , existe un -término M tal que ? Con un entorno de tipo vacío, se dice que tal M es un habitante de.
Relación con la lógica
En el caso del cálculo lambda simplemente tipado , 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 de Sistema F tiene un habitante si y solo si su proposición correspondiente es una tautología de la lógica de segundo orden .
La paradoja de Girard muestra que la ocupación de tipos está fuertemente relacionada con la consistencia de un sistema de tipos con la correspondencia Curry-Howard. Para ser sólido, tal sistema debe tener tipos deshabitados.
Propiedades formales
Para la mayoría de los cálculos mecanografiados, el problema de la ocupación de tipos es muy difícil . Richard Statman demostró que para el cálculo lambda simplemente mecanografiado, el problema de la ocupación de tipos es PSPACE-completo . Para otros cálculos, como el Sistema F , el problema es incluso indecidible .
Ver también
Referencias
- ^ Pawel Urzyczyn (1997). "Inhabitation in Typed Lambda-Calculi (A Syntactic Approach)" . Apuntes de conferencias en Ciencias de la Computación . Springer: 373–389.