deniok | О сколько нам открытий чудных...

О сколько нам открытий чудных дарит изучение просто типизированной чистой лямбды.

Пусть есть лямбда-терм, который может быть редуцирован к другому лямбда-терму с помощью цепочки обычных бета-редукций:

Сохраняется ли при этом тип? То есть верно ли утверждение

(Двойная стрелочка читается "бета-редуцируемо к")

Ответ: Нет, и, более того, дело даже не в нетипизируемости чего-то вроде Y-комбинатора и проблеме останова. Тип в процессе бета-редукций (aka вычислений) может измениться. Вот простейший пример:

Сама бета-редукция выглядит так

В чём тут дело? При применении канцеллятора аппликативная сущность y, определяемая выражением yz, теряется. Тип выражения становится более общим. Вот так-то :)

Flat | Top-Level Comments Only

Даже если понимать под типизацией не определение principle type (наиболее общего типа), а указание какого-то из допустимых, то

Проблема всегда в том, что значит "имеет тип". Если тип неявен и выводится из структуры терма по определенным правилам - это типизация по Карри, в этом случае данный артефакт имеется. А при типизации по Черчу, где каждый подтерм изучаемого терма явно типизирован (тип явно приписан любому терму), всё OK и есть лемма уникальности типов.

О сколько нам открытий чудных...

no subject