Tipo habitacion
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 ? Con un entorno de tipo vacío, se dice que tal M es un habitante de .
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.
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 .
Esta teoría del lenguaje de programación o artículo relacionado con la teoría de tipos es un fragmento . Puedes ayudar a Wikipedia expandiéndolo .