Лектор: Кузнецов Степан Львович (д.ф.-м.н., в.н.с., Математический институт им. В.А. Стеклова РАН, г. Москва)
Даты: Пожалуйста, обратите внимание, что указано время в Новосибирске.
18 ноября 2024 г. (понедельник), 16:20-17:55, ауд. 4140 НГУ
19 ноября 2024 г. (вторник), 18:10-19:45, ауд. 4268 НГУ
20 ноября 2024 г. (среда), 16:20-17:55, ауд. 4267 НГУ
Аннотация:
Лямбда-исчисление — это логическая система для формализации вычислений посредством операций применения функций и функциональной абстракции. Лямбда-исчисление является основой семейства современных языков программирования, называемых функциональными языками. В рамках мини-курса будет дано введение в лямбда-исчисление, в двух его видах — бестиповом и типизованном. На первой лекции будет рассказано о лямбда-исчислении без типов (в котором любое лямбда-выражение может быть применено, как функция к любому другому), о его основных свойствах и о представлении в нём произвольных вычислимых функций. На второй лекции будут рассмотрены несколько вариантов типизованного лямбда-исчисления (здесь применение ограничено дисциплиной типов), описаны их вычислительные возможности и установлена связь между типизованным лямбда-термами и конструктивными доказательствами (соответствие Карри-Говарда). На третьей лекции будет рассказано о семантике лямбда-исчисления: теоретико-множественных моделях в типизованном случае и моделях Ершова-Скотта в бестиповом.