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

[deniok]

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

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

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

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


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


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

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

Comments

[deni-ok.livejournal.com]

Да, там о том же. В реальности SK, как целое, более мощен, чем его выведенный тип. В том смысле, что раз уж он отбрасывает на фиг свой первый аргумент, то зачем сохранять память о том, что этот аргумент - стрелочка. Нет никаких оснований запрещать, скажем, оптимизатору заменять SK на \x y->y. И тут дилемма: либо мы сохраняем (статическую :))) ) типизацию, запрещая

(SK) 13 42

либо говорим, "а чо, 42 же..." ;-)