tt-conspect

tt-conspect copied to clipboard

Добавить что-нибудь про то, что лямбда-выражения — это не строки, и что вся эта муть с подстановками, похожими на строки, это просто формализм

1

artemohanjanyan

Подробнее объяснить роль альфа-эквивалентности в определении бета-редукции

1

artemohanjanyan

Описка в выводе парадокса Карри

2

7 страница, 3 пункт вывода парадокса Карри, неправильно использована схема аксиом, пропущены скобки

Kowalski1337

Противоречивость Хиндли-Милнера с Y-комбинатором

2

Y-комбинатор нетипизируем в HM, но авторы допустили забили на этот факт и дали тип `\forall y. (y->y)->y`. Этот факт делает систему HM неразрешимой, то есть из контекста Y можно доказать...

MekhrubonT

Diaconescu theorem

1

artemohanjanyan

Correct word "меморизация"

1

artemohanjanyan

artemohanjanyan

It's incorrect for chains consisting of zero reductions for terms which are not in NF.

artemohanjanyan

artemohanjanyan

Substitution definition is wrong, it can't be applied to any function which is not `id`. E.g. `S(x) = {y_1, if x=x_1; x otherwise}`, then `S(x_1)=y_1`, `S(x_1->x_1)=y_1->y_1`, `S(x_1->x_1->x_1)=y_1->y_1->y_1`, and so on.

artemohanjanyan