Рекурсия и редукция

Подписаться 161 тыс.

Просмотров 16 тыс.

50% 1

compscicenter.ru/
Теорема о неподвижной точке, Y-комбинатор. Редексы. Одношаговая и многошаговая редукция. Нормальная форма. Редукционные графы. Теорема Чёрча-Россера. Следствия: редуцируемость к нормальной форме, единственность нормальной формы. Cтратегии редукции. Теорема о нормализации. Механизмы вызова в функциональных языках.
Лекция №2 в курсе "Функциональное программирование" (весна 2015).
Преподаватель курса: Денис Николаевич Москвин.
Страница лекции на сайте CS центра: goo.gl/Zriq1j

Опубликовано:

8 июл 2015

Ссылка:

Скачать:

Готовим ссылку...

Добавить в:

Мой плейлист

Посмотреть позже

Комментарии : 9

@global_silence2623 6 лет назад

50:58 - конец перерыва.

@Uni-Coder 3 года назад

Перерыв забыли редуцировать :)

@tigershark73 Год назад

@@Uni-Coder рил

@TheOnlyAndreySotnikov Месяц назад

Интересно почему прижился термин «кофлюентность» вместо нормального перевода слова confluence: «слияние»?

@PropMinecast 8 лет назад

В доказательстве теоремы о неподвижной точке следовало упомянуть, что мы выбираем такой x, что он не входит свободно в F(для комбинатора неподвижной точки это не важно, ведь иначе будет коллизия и придется применять альфа-преобразование).

@yuriykochetkov 4 года назад

1:07:20 Стратегия редукции

@user-xq3vp6nt9n 4 года назад

На слайде 16 в примере написано, что терм \xy.x(\z.zx)y находится в бета-нормальной форме. А разве (\z.zx)y не являетя редексом?

@user-xq3vp6nt9n 4 года назад

А кажется само дошло: порядок аппликации такой (x(\z.zx))y. Поэтому это не редекс.

@dimitro.cardellini 3 года назад

@@user-xq3vp6nt9n не, там не так порядок апликации ;) const f = x => y => x( z=> z(x), y ) -- это на JavaScript мы объявили абстракцию с двумя связанными переменными: x y и телом x (\z . z x) y. В теле мы применяем x сначала к новой абстракции над z: \z . z x, а потом к переменной y. Асбстрации тоже могут быть объектом применения (т.е. функции могут быть аргументами функций)