deniok

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

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

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

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

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

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

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