Тип проживания

В теории типов , разделе математической логики , в данном типизированном исчислении для проблемой обитаемости типов этого исчисления является следующая проблема: учитывая тип $\tau$ и среда ввода $\Gamma$, существует ли $\lambda$-член M такой, что $\Gamma \vdash M:\tau$? В среде пустого типа такой M называется жителем $\tau$.

Отношение к логике

В случае просто типизированного лямбда-исчисления тип имеет обитателя тогда и только тогда, когда соответствующее ему предложение является тавтологией минимальной импликативной логики. Аналогично, тип Системы F имеет обитателя тогда и только тогда, когда соответствующее ему предложение является тавтологией интуиционистской логики второго порядка .

Парадокс Жирара показывает, что обитаемость типов тесно связана с согласованностью системы типов с соответствием Карри-Ховарда. Чтобы быть работоспособной, такая система должна иметь необитаемые типы.

Формальные свойства

Для большинства типизированных исчислений проблема обитаемости типов очень сложна . Ричард Статман доказал, что для просто типизированного лямбда-исчисления проблема обитаемости типов является PSPACE-полной . Для других исчислений, таких как Система F , проблема даже неразрешима .

См. также

• Изоморфизм Карри – Говарда