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