Задача обитаемости в системах типов низкого ранга

Типы являются важной абстракцией в языках программирования. Ограничивая множество корректных программ, они позволяют программистам писать более безопасный код и избегать ошибок. Теория типов – математический аппарат, формализующий данную область. Одним из базовых вопросов теории типов является задача обитаемости: «Существует ли терм (выражение в языке) заданного типа?». Задача обитаемости может быть поставлена в различных системах типов (моделях, описывающих часть языка программирования, относящуюся к типам). Цель данной работы – решить проблему обитаемости для некоторой определённой системы типов, а именно для просто типизированного лямбда исчисления с пересечениями второго ранга и подтипизацией. Недавние работы показывают, что задача обитаемости неразрешима в системах без ограничения на ранг и EXPSPACE-полной в системе с пересечениями второго ранга, но без подтипизации. Однако система и с пересечениями второго ранга, и с подтипизацией до сих пор не была изучена. В данной работе мы показываем, что задача обитаемости разрешима и в этой системе. Для этого мы приводим алгоритм, решающий её, доказывая его корректность, полноту и завершаемость; представлена также реализация алгоритма на языке Haskell. Помимо этого, работа закрывает некоторые неточности предыдущих статей и предлагает новые подходы к реализации описанных в них алгоритмов.