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

Лямбда-исчисление — это небольшой математический язык программирования, обладающий такой же вычислительной мощью, как любой другой язык программирования, о котором вы только можете мечтать. В этом видео мы сначала рассмотрим это исчисление, а затем рассмотрим, как можно превратить его в функциональный язык программирования. После краткого обзора простой системы типов мы увидим, почему лямбда-исчисление находит удивительное применение в области математической логики, и как последствия этой взаимосвязи могут навсегда изменить наш подход к изучению математики. ― Временные метки ― 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