В теории типов , разделе математической логики , в данном типизированном исчислении проблема обитания типа для этого исчисления является следующей проблемой: [1] при заданном типе и типизированной среде существует ли -терм M такой, что ? При пустом типизированном окружении такой M называется обитателем .
В случае простого типизированного лямбда-исчисления тип имеет жителя тогда и только тогда, когда его соответствующее предложение является тавтологией минимальной импликативной логики. Аналогично, тип Системы F имеет жителя тогда и только тогда, когда его соответствующее предложение является тавтологией интуиционистской логики второго порядка .
Парадокс Жирара показывает, что обитаемость типа тесно связана с согласованностью системы типов с соответствием Карри–Ховарда. Чтобы быть надежной, такая система должна иметь необитаемые типы.
Для большинства типизированных исчислений проблема заселения типов очень сложна . Ричард Статман доказал, что для просто типизированного лямбда-исчисления проблема заселения типов является PSPACE-полной . Для других исчислений, таких как System F , проблема даже неразрешима .
