Лямбда-исчисление
ฝัง
- เผยแพร่เมื่อ 6 ก.ย. 2024
- compscicenter.ru/
Введение. Функциональное и императивное программирование. Лямбда-исчисление. Применение и абстракция. Свободные и связанные переменные. Комбинаторы. Функции нескольких переменных, каррирование. Подстановка, лемма подстановки. Бета-преобразование. Эта-преобразование. Расширение чистого лямбда-исчисления: дельта-преобразование.
Лекция №1 в курсе "Функциональное программирование" (весна 2015).
Преподаватель курса: Денис Николаевич Москвин.
Страница лекции на сайте CS центра: goo.gl/b07ftp
0:48 Императивное программирование
3:12 Пример в императивном стиле (скалярное произведение векторов)
5:16 Функциональное программирование
7:24 Пример в функциональном стиле (скалярное произведение двух векторов)
8:52 Преимущества и недостатки функционального программирования
12:33 Чистота и побочные эффекты
18:34 лямбда-исчисление - введение
20:27 Аппликация
22:00 Абстракция
24:02 Совместное применение абстракции и аппликации.
28:06 Термы
30:18 Примеры термов
32:01 Термы - соглашения и упрощенная запись
35:44 Свободные и связанные переменные
44:25 Комбинаторы
50:05 Функции нескольких переменных, каррирование
57:00 Переименование связанных переменных
спасибо
Уважаемый, Денис Николаевич,
спасибо вам!
пишу этот комент больше для тех кто хочет посвятить больше чем 2.23 часа жизни но не может понять стоит ли .
Лекция не простая.Автору однозначно спасибо Лектору поклон и уважение за труд.
Расчитана больше на людей с мат. багажом(которым легко понятны конструкции в духе "применим выражение к неким произвольным выражениям")
.ибо многие моменты пересмотреть придется.мне после строго императивного программирования не за что было ухватиться, уж очень много мат сленга.очень много формул а применения их маловато покрайне мере в первой части, и чувствуешь себя в школе, когда началась алгебра: пишут на доске кучу формул, которые почему дают какие то результаты, делают это с таким видом как будто ответы для всех очевидны, а если очевидны пойдем дальше. рекомендую перед просмотром лекции прочитать статью на хабре.после нее смотреть, не так больно habr.com/ru/post/215807/
начал лекцию смотреть потому что была не понятна вводная по хаскелю. рекомендую вот этот курс rutracker.org/forum/viewtopic.php?t=4056296
Очень здорово! Такого простого объяснения лямбда-исчисления я не видел никогда.
все замечательно, только на тусклой доске на различить надписей. по крайней мере мне
Материал понял, порешать вместе с аудиторией было приятно) Спасибо!
Я хоть изучаю TypeScript, мне все равно было полезно и интересно смотреть такого рода лекции, чтобы иметь более широкое представление об этом, а не только знать конкретную реализацию той или иной парадигмы на языке, чтоб знать отличия реализаций техник на тех или иных языках.
+ ток я не только TypeScript, а еще и [Assembler(FASM), C, C#, JavaScript, Python] вот теперь haskell жую
Отличная лекция, спасибо.
"разрушающее присваивание" - это когда ломают и воруют, как в 90е (шучу)
спасибо за классный урок!!!
Супер, очень хорошо, я кажется начинаю понимать) Спасибо, Вам, большое!
Максимально понятное объяснение, спасибо!
1:36:45
Это Deep Purple - Burn ?!!
Наш человек))
That shit crazy my nigga he's 100% American
А вот за такие лекции спасибо!
Огромное спасибо за объяснение. Это великолепно
Билл Гейтс приехал в Россию : )
Хорошее объяснение + я угарал с реакций лектора на некоторые моменты)
Сошников, кажется, упоминал фамилию Эйлера, а он создавал учебник по математическому анализу и вот понятие функция у Эйлера пока ещё и не оформилась, а это и к логике имеет отношение. Вообще говоря, математики практически нужны для проведения рассчётов, и вот эти рассчёты делают они по определённому алгоритму, таким образом функция это алгоритм сделать что-то с величинами, подставляемыми в неё чтобы получить результат. А вот ещё функция это соответствие между аргумнтами и результатами, и вот тут то и содержиться некоторая разница, между двумя представлениями о функции, а ещё есть и логическое выражение, которым функция и определяется, вот это то я и не пойму, Чёрч и Хаскел пришли к некоему выводу, который аналогичен выводу практика ЭВМ Тьюринга и Поста. А это имеет отношение и к теории множеств и теореме Гёделя и ещё к какой-то теореме перед теоремой Гёделя.
Классная теория про ФП! 10/10
Пришлось попутно узнать про chokolatey, с помощью этой программы ghc ставится. ghc всё таки поставил. Посмотрим, что будет дальше. Спасибо за лекции лектору. Разбираться как ставить платформу Хаскел пришлось полдня.
1:29:42
C 4 на 5 строчку просто эта-преобразование можно использовать.
некоторые примеры ну очень спорные.
но в целом: очень и очень хорошо!
имхо - в примере с императивным кодом все гораздо хуже. Результат будет зависеть от того, в каком порядке компилятор вычесляет аргументы в операции "+" (а может еще и от оптимизаций компилятора)
1:43:46 Тут ведь все-таки (\xy.P)Q, а не (\y.P)Q?
+Paul Surzh Да, неправильно написал, спасибо.
в чем смысл применения переменной к переменной?
(zx) - это что?
В таком случае вообще не понятно, что за комбинатор омега малое
"omega = \x.xx"
Что он сделает, если я его применю к числу?
А что такое перменная? Каково её значение? Значение - это ж терм. И лямбда в том числе.
Значением переменной может быть функция.
@@mhevakпомог конечно (нет)
@@kazan29а если нет?
И от меня спасибо
40:37
Почему вы говорите что только функция может приминаться к чему то? Хотя ранее применяли переменную к переменной
Я там не слышу слово "только". На 40:37 я просто пример привожу на языке C, имеющий иллюстративный характер.
не подскажите, а лямбда исчисление как нить пересекается с теорией категории или это разные темы?
Не совсем понятно, есть ли различие между понятиями β-эквивалентности и β-преобразованием?
Преобразование это действие, эквивалентность это результат действия преобразования
Тот самый короткий not: \b.\x.\y. b y x
пример:
not tru -> tru y x -> y
not fls -> fls y x -> x
сломал мозг, а потом пришло озарение - надо просто поменять местами аргументы при вызове.
Чёт вообще не понял где тут not, да ещё и короткий
2:13:00
true = \ x y . x
false = \ x y . y
or = \ x y = x true y
проверка:
1. or true false = true true false = true
2. or false true = false true true = true
3. or true true = true true true = true
4. or false false = false true false = false
мне кажется лучше or = \ x y = x x y
@@ivangagarinov4127 О! Я тоже до такого варианта додумался. Можно ещё заюзать комбинатор ω
@@ivangagarinov4127 А чем он лучше?
Is there a no chance to get this in English
No chance, unless we find a volunteer, who can translate the entire playlist.
Дайте этому профессору беговую дорожку, замаялся бедный)
Не понял как преобразовывается (\x.x x)(\y z.y z) = (\y z.y z)(\y z.y z)
если подставить вместо x подставить (\y z.y z) то получится (\y z.y z)x и это в свою очередь равно \x z.x z
Здесь используется бета-редукция, определение которой было в лекции:
(\x.M) Q = M[x:=Q] .
Суть бета-редукции в том, что мы для вычисления абстракции (функции) \x.M для значения Q должны подставить в выражение M вместо всех вхождений x значение Q. То есть это просто вычисление функции при каком-то конкретном значении, как в школьном курсе алгебры.
Теперь берём наш терм: (\x.x x)(\y z.y z). В нем M=(x x), а Q=(\y z.y z). Сделав формальную подстановку Q вместо x в M получим (\y z.y z)(\y z.y z).
1:19:52 - не дзета а кси
А теперь сравните с любым видео по С# и сразу поймете, почему на Хаскеле [ почти ] никто не пишет.
Если не нужна абстракция и выразительность, то пожалуйста
ω 1 = (λx. xx)(λyz. yz)
...
λz. (λy z'.yz')z
как так получается, что это выражение равно
= λzz'.zz'
каким образом z подставилась в y?
(λy z'.yz')z - тело абстракции λz. (λy z'.yz')z,
(λy z'.yz')z => (λy.(λz'.yz'))z (ассоциация вправо)
(λz'.yz') представим как некий лямба терм М => (λy.M)z =β M[y:=z] => (λz'.zz')
возвращаемся к λz. (λy z'.yz')z, где (λy z'.yz')z = (λz'.zz') => λz.(λz'.zz') = λzz'.zz' (ассоциативно вправо)
Как то так
Хмм... Тут вообще можно юзать эта-преобразование.
λx.Mx = M, x не принадлежит FV(M)
В нашем случае x = z, M = (λy z'.yz'). В M икса вообще нет. Поэтому
λz. (λy z'.yz')z = λy z'.yz' = |альфа-преобразование| = λzz'.zz'
Здравствуйте! У меня есть вопрос. При рассмотрении комбинатора iif (2:07:15) мы имеем выражение "(\lambda xy.tru x y)AB" и потом осуществляем подстановку A и B. Но разве выражение "try x y" само не является редексом "(\lambda xy.x)x y", в который можно подставить x, y? Кажется, я где-то не до конца понял приоритет операций. С другой стороны, согласно правилам бета-преобразования, при замене терма в лямбда-терме на эквивалентный (а мы сделаем именно это, если произведем бета-преобразования терма "tru x y"), полученный лямбда-терм будет эквивалентен исходному. Я также провел вручную все преобразования по шагам, раскрыв сначала внутренний редекс, получил точно такой же результат. Но, все же, интересует вопрос: это я что-то не понял с порядком выполнения преобразований или лектор просто опустил для краткости эквивалентное преобразование?
Хороший вопрос. Я думаю, что так как все эти бета-редукции вообще не меняют функцию, а меняют только её выражение т.е. то, как она записана, то это нормально, что получилось то же самое, но я сам на вашем уровне понимания примерно, так что могу ошибиться.
Тема редукционные стратегии на этом этапе пока не освещена. Но, забегая вперед, согласно им β-редукцию можно проводить в любой последовательности(предпочтительнее конечно такая последовательность, которая приводит к "нормальной форме", т. е. когда к полученному выражению(терму) кроме α-редукции другие(β- и η-) конверсии применить больше нельзя).
1:31:20
че там?
Не сразу понял, что ассоциативность влево тождественна правой ассоциативности :)
Пипец какой то , то какая то математика с кучей формул, покруче логарифмов, с тригонометрией, а не програмирование...
Он говорит как-будто пародирует Галустяна который пародирует Рамзана Кадырова
Лекция хороша, но впредь двигайтесь по меньше во время рассказа, а то ваша нервозность передаётся на зрителя
нормально, это не дает уснуть))) как бы всегда есть небольшой раздражитель))
Норм. Главное доходчиво. А как автор эту доходчивость генерирует - его дело.
мне одному кажется, что вектора не так перемножаются?
Отличная лекция,спасибо большое