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

[deniok]

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

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

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

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


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


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

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

Comments

[deni-ok.livejournal.com]

Канцеллятор K - это в точности хаскелловский const :)

Аппликативная - в смысле применяемая к чему-то, то есть имеющая тип со стрелочкой.

> Что, кстати, про типизированную лямбду почитать?
Сам разбираюсь с этим хозяйством :)
Засада в том, что лямбда одна, а типизировать можно по-разному. К счастью есть классика, покрывающая большинство интересных направлений: Barendregt "Lambda Calculi with Types" 1992
http://citeseer.ist.psu.edu/barendregt92lambda.html

Всё остальное, насколько я понимаю - либо перепевы и пояснения, либо довольно специальные вещи. Есть, например, такая штучка от SPJ
http://citeseer.comp.nus.edu.sg/75539.html

[dtim.livejournal.com]

Ну про канцеллятор и аппликативность - это я шучу, конечно, кое-что читал все-таки :).
А за ссылки спасибо большое, буду осваивать :).