Программирование с использованием математики | Лямбда-исчисление

Лямбда-исчисление — это небольшой математический язык программирования, обладающий такой же вычислительной мощью, как любой другой язык программирования, о котором вы только можете мечтать. В этом видео мы сначала рассмотрим это исчисление, а затем рассмотрим, как можно превратить его в функциональный язык программирования.

После краткого обзора простой системы типов мы увидим, почему лямбда-исчисление находит удивительное применение в области математической логики, и как последствия этой взаимосвязи могут навсегда изменить наш подход к изучению математики.

― Временные метки ―

0:00 — Введение
0:42 — Определение
5:30 — Множественные входные данные
8:10 — Булевы значения и условные операторы
13:11 — Простые типы
16:32 — Соответствие Карри-Ховарда
20:58 — Заключение

― Титры ―

Вся анимация и озвучка созданы Eyesomorphic.
Доказательство бесконечности простых чисел в Lean4 взято из mathlib4 по лицензии Apache 2.0: https://github.com/leanprover-communi...
Фоновая музыка: «Reminisce», автор — Кейлеб Пеппиат.

― Дополнительная литература ―

«Типы и языки программирования» Бенджамина К. Пирса (книга)
«Теория категорий и почему мы заботимся» Eyesomorphic (серия лекций):    • Category Theory and Why We Care  

― Исправления ―

На 4:35 слово «comptuter» очевидно должно быть «computer», извините за это!

Запись на #SoMEPi