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

[deniok]

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

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

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

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


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


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

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

Comments

[dtim.livejournal.com]

Ну не извращенцы ли эти математики? Канцелляторы, аппликативные сущности... У меня вот тут в php типы меняются в процессе вычислений без всяких комбинаторов и бета-редукций, и ничего - дельше строчки им деваться все равно некуда :).

(Что, кстати, про типизированную лямбду почитать? А то у меня в этой области явный пробел.)

[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]

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

[antilamer.livejournal.com]

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

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

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

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

[deni-ok.livejournal.com]

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

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

[deni-ok.livejournal.com]

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


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

[lomeo.livejournal.com]

Забавно. Напомнило вот это.

Просто по ассоциации :-)

[deni-ok.livejournal.com]

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

(SK) 13 42

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