Math.WTF

Осень 2017, ИТМО ВМ-1, группы P3495-P3496.

Лекция 0

Исчисления

2 сентября 2017

Слайды ( без анимаций )

  • Понятие формального языка.
  • Примеры описания исчислений.
  • Логика высказываний как формальный язык.
  • Логика первого порядка.
  • Метод резолюций.
  • Представление формул в дизъюнктах.
Лекция 1

Лямбда-исчисление

16 сентября 2017

Слайды ( без анимаций )

  • Понятие вычисления.
  • Лямбда-исчисление как формальный язык.
  • Решение уравнений на термы.
  • Неподвижная точка и Y-комбинатор.
  • Отношение редукции, виды редукций.
  • Теорема Чёрча-Россера и следствия из неё.
  • Нормальные формы и стратегии редукции.
Лекция 2

Простая теория типов

16 сентября 2017

Слайды ( без анимаций )

  • Мотивация типов в математике.
  • Типы как расширение грамматики лямбда-исчисления.
  • Стили типизации: Карри и Чёрч.
  • Вывод типов в STT.
  • Свойства STT.
  • Подстановки типов и их свойства.
  • Алгоритм унификации.
  • Алгоритм построения ограничений.
  • Алгоритм Хидли-Милнера.
Лекция 3

Язык программирования Haskell

16 сентября 2017

Слайды ( без анимаций )

  • История развития прикладных языков функционального программирования.
  • GHC и его инфраструктура.
  • Элементарный синтаксис языка Haskell.
  • Операторы и сечения.
  • Ленивость и строгость.
  • Типы в Haskell. Понятие полиморфизма. Классы типов.
  • Алгебраические типы данных.
  • Сопоставление с образцом.
  • Модули и структура программ на языке Haskell.
Лекция 4

System F

30 сентября 2017

Слайды ( без анимаций )

  • Типизация самоприменения в STT.
  • Понятие квантификации по типу.
  • Свободные и связанные переменные типа. Расширенное понятие контекста.
  • Вывод типа в System F в стиле Карри.
  • Подстановки типов в System F.
  • Типизация самоприменения в System F по Карри.
  • Ранги типов, связь рангов и задачи вывода типа.
  • Универсальное применение и правила вывода в System F в стиле Чёрча.
  • Вывод типа в System F в стиле Чёрча.
  • Типизация самоприменения в System F по Чёрчу.
  • Полезные типовые конструкции System F.
Лекция 5

Типы, зависящие от типов

14 октября 2017

Слайды ( без анимаций )

  • Типы, зависящие от типов: пары и суммы.
  • Классификация типов по кайндам.
  • Расширение System F до зависимостей от типов.
  • Алгебраическое построение типов.
  • Доказательство простейших теорем на натуральные числа.
  • Рекурсивные типы. Неподвижная точка на типах.
Лекция 6

System Fω в Haskell

21 октября 2017

Слайды ( без анимаций )

  • Типы в языке Haskell.
  • Универсальная квантификация, типы второго ранга.
  • Интерпретатор простейшего языка программирования.
  • Фантомные типы.
  • Обощенные алгебраические типы данных.
  • Безопасный список и вектор.
  • Функции над типами: type families и data families.
Лекция 7

Аппликативные парсеры

21 октября 2017

Слайды ( без анимаций )

  • Класс типов Functor.
  • Класс типов Applicative.
  • Класс типов Alternative.
  • Реализация комбинаторов для парсинга на классе типов Alternative.
  • Библиотека parsec.
Лекция 8

Свободные монады

10 ноября 2017

Слайды ( без анимаций )

  • Рекурсивные типы, кодирование через нерекурсивные функторы.
  • Комбинатор неподвижной точки на типах.
  • Катаморфизмы и F-алгебры.
  • Анаморфизмы и F-коалгебры.
  • Примеры N- и (L a)- алгебр и коалгебр.
  • Интерпретация последовательности действий как списка нерекурсивных функторов.
  • Тип Free как расширение неподвижной точки.
  • Свободный функтор, аппликатив, монада.
  • Реализация бэкендов как F-алгебр свободной монады.
Лекция 9

Исчисление конструкций

10 ноября 2017

Слайды ( без анимаций )

  • Системы типов Simple Type Theory, System F и System Fω.
  • Pure Type Systems.
  • Типизация в PTS.
  • Сорта * и . Правила, определяемые сортами.
  • Лямбда-куб, как PTS.
  • Пример STT как PTS.
  • Пример записи термов в PTS: id, Bool, Nat.
Лекция 10

Template Haskell

18 ноября 2017

Слайды ( без анимаций )

  • Задачи, требующие кодогенерации.
  • Этапы компиляции Haskell-кода.
  • Генерация выражений. Тип выражений Exp.
  • Пример генерации n-арного каррирования.
  • Генерация объявлений. Тип объявлений Dec.
  • Пример генерации объявлений каррирования.
  • Смешанный пример.
Лекция 11

Lens

25 ноября 2017

Слайды ( без анимаций )

  • Проблема обновления полей во вложенных типах-записях.
  • Типовой пример использования линз.
  • Lens: определения и законы.
  • Lens: способы создания, комбинирования и использования.
  • Traversal: определение.
  • Traversal: способы создания, комбинирования и использования.
  • Соотношение между типами Lens и Traversal.
Лекция 12

Формальная верификация

9 декабря 2017

Слайды ( без анимаций )

  • Конструктивные и неконструктивные доказательства.
  • Интуиционистская логика, дедукция.
  • Пример конструктивного доказательства в интуиционизме и на языке Haskell.
  • Изоморфизм Карри-Говарда.
  • Исчисление индуктивных конструкций (CIC).
  • Пример вывода в CIC.
Лекция 13

Индуктивные типы

16 декабря 2017

Слайды ( без анимаций )

  • Примеры типов в CIC.
  • Семантика индуктивных типов.
  • Кодирование индуктивных типов в CIC и COC.
  • Тактики вывода.
  • Практическое применение теории типов.