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

[deniok]

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

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

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

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


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


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

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

Comments

[antilamer.livejournal.com]

О-хо-хо! Круто!

*вызывает дух Карри-Ховарда*

*загробным голосом*
Все значения с типом (s -> t) -> s -> s также имеют тип a -> b -> b.

Так что тип становится более общим в том смысле, что расширяется кодомен функции - однако и НЕ становится более общим в том смысле, что множество значений, имеющих такой тип, не расширяется.

[deni-ok.livejournal.com]

>вызывает дух Карри-Ховарда

О, да! В процессе упрощения доказательства выясняется, что оно (после упрощения) доказывает более мощную теорему.

[deni-ok.livejournal.com]

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


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