Проблемы разрешимости: проверка типа, синтез типа и населенность типа. Лемма об образовании редексов. Меры типа и терма. Слабая нормализация для \( \lambda_{\rightarrow} \). Сильная нормализация. Интерпретации \( {\rightarrow} \)-типов. Расширение системы константами. \( \delta \)-редукция.