![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
Entry tags:
О сколько нам открытий чудных...
О сколько нам открытий чудных дарит изучение просто типизированной чистой лямбды.
Пусть есть лямбда-терм, который может быть редуцирован к другому лямбда-терму с помощью цепочки обычных бета-редукций:
Сохраняется ли при этом тип? То есть верно ли утверждение
(Двойная стрелочка читается "бета-редуцируемо к")
Ответ: Нет, и, более того, дело даже не в нетипизируемости чего-то вроде Y-комбинатора и проблеме останова. Тип в процессе бета-редукций (aka вычислений) может измениться. Вот простейший пример:
Сама бета-редукция выглядит так
В чём тут дело? При применении канцеллятора аппликативная сущность y, определяемая выражением yz, теряется. Тип выражения становится более общим. Вот так-то :)
Пусть есть лямбда-терм, который может быть редуцирован к другому лямбда-терму с помощью цепочки обычных бета-редукций:
Сохраняется ли при этом тип? То есть верно ли утверждение
(Двойная стрелочка читается "бета-редуцируемо к")
Ответ: Нет, и, более того, дело даже не в нетипизируемости чего-то вроде Y-комбинатора и проблеме останова. Тип в процессе бета-редукций (aka вычислений) может измениться. Вот простейший пример:
Сама бета-редукция выглядит так
В чём тут дело? При применении канцеллятора аппликативная сущность y, определяемая выражением yz, теряется. Тип выражения становится более общим. Вот так-то :)
no subject
О, да! В процессе упрощения доказательства выясняется, что оно (после упрощения) доказывает более мощную теорему.