/tt2018

Primary LanguageTeX

Курс теории типов, КТ, осень 2018

Материалы

Лекция 1

Лямбда-исчисление, базовые определения, примеры

  • Немного об истории
  • Лямбда-выражения, синтаксис
  • Альфа-эквивалентность, бета-редекс, бета-редукция
  • Булевские выражения, чёрчевские нумералы

Где почитать

Лекция 2

Лямбда-исчисление, теорема Чёрча-Россера

  • Формализация лямбда-термов, классы альфа-эквивалентных термов
  • Нормальная форма, лямбда-выражения без нормальной формы, комбинаторы K, I, Ω
  • Бета-редуцируемость (транзитивное и рефлексивное замыкание бета-редукции)
  • Ромбовидное свойство
  • Теорема Чёрча-Россера, следствие о единственности нормальной формы
  • Нормальный и аппликативный порядок вычислений, примеры в лямбда-исчислении и в языках высокого уровня

Где почитать

Лекция 3

Y-комбинатор, просто типизированное лямбда-исчисление

  • Y-комбинатор, рекурсия
  • Парадоксы лямбда-исчисления как исчисления высказываний
  • Импликационный фрагмент интуиционистского исчисления высказываний
  • Просто типизированное лямбда-исчисление
  • Типизация по Карри
  • Отсутствие типа у Y-комбинатора
  • Изоморфизм Карри-Ховарда

Где почитать

Лекция 4

Конъюнкция и дизъюнкция, просто типизированное лямбда-исчисление по Чёрчу.

  • Дизъюнкция и алгебраические типы
  • Конъюнкция и упорядоченные пары
  • Типизация по Чёрчу
  • Связь типизации по Чёрчу и по Карри

Где почитать

Лекция 5

Изоморфизм Карри-Ховарда (завершение), Унификация

  • Теорема об изоморфизме Карри-Ховарда
  • Теорема о выразительной силе просто типизированного лямбда-исчисления (формулировка)
  • Основные задачи типизации в лямбда-исчислении: проверка типа, реконструкция типа, обитаемость типа
  • Алгебраические термы, алгоритм унификации

Где почитать

Лекция 6

Реконструкция типов в просто типизированном лямбда-исчислении, комбинаторы

  • Алгоритм реконструкции (вывода) типов в просто типизированном лямбда-исчислении, сведение задачи реконструкции типов к унификации.
  • Алгоритм унификации даёт наиболее общий унификатор --- формулировка утверждения и доказательство.
  • Наиболее общий унификатор соответствует наиболее общей (основной) паре (тип + контекст) в задаче о реконструкции типов.
  • Сильная и слабая нормализация термов и исчислений. Теорема о сильной нормализуемости просто типизированного лямбда-исчисления (без доказательства)
  • Комбинаторы S,K,I. История возникновения, смысл названий. Выразимость замкнутых лямбда-выражений через S и K (алгоритм устранения абстракций). Альтернативный базис B,C,K,W.
  • Комбинаторы S,K и исчисление высказываний в гильбертовском стиле.

Где почитать

Лекция 7

Интуиционистское исчисление предикатов второго порядка, система F

  • Интуиционистское исчисление предикатов второго порядка, импликационный фрагмент.
  • Представление прочих связок ($&$, $\vee$, $\bot$, $\exists$) через $(\rightarrow)$ и $(\forall)$.
  • Система F, соответствие исчислению предикатов второго порядка.
  • Исключения, упорядоченная пара, значения алгебраических типов в системе F.
  • Обзор результатов без доказательства: базовые теоремы (Чёрча-Россера и т.п.), сильная нормализуемость, неразрешимость задач типизиации.

Где почитать

Лекция 8

Экзистенциальные типы, ранг типа, система Хиндли-Милнера

  • Экзистенциальные типы: определение, пример реализации на Хаскеле
  • Ранг типа
  • Синтаксис лямбда-выражений в системе Хиндли-Милнера

Где почитать

Лекция 9

Алгоритм W, расширения системы (Y-комбинатор и рекурсивные типы), зависимые типы

  • Правила вывода в системе Хиндли-Милнера
  • Алгоритм W
  • Тип Y-комбинатора
  • Изо- и эквирекурсивные типы, оператор μ, операции roll и unroll.
  • Зависимые типы, примеры (printf и int[n]), П-синтаксис.

Где почитать

  • Статья на Википедии довольно информативна, можно начать с неё: https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system
  • Milner, Robin. A Theory of Type Polymorphism in Programming. Journal of Computer and System Sciences. 17: 348–374
  • Damas, Luis; Milner, Robin. Principal type-schemes for functional programs (PDF). 9th Symposium on Principles of programming languages (POPL'82). ACM. pp. 207–212. http://web.cs.wpi.edu/~cs4536/c12/milner-damas_principal_types.pdf
  • Б. Пирс, Типы в языках программирования, М.: Издательство «Лямбда-пресс»: «Добросвет», 2011.

Лекция 10

Обобщённые типовые системы, лямбда-куб

  • Типы, рода, сорта. Символы * и □.
  • Обобщённые типовые системы.
  • Варианты типовых систем и Лямбда-куб. Положение распространённых языков программирования на нём.

Где почитать

  • Barendregt, Henk. Introduction to generalized type systems. Journal of Functional Programming 1 (2): 125-154, April 1991.

Лекция 11

Язык Идрис

  • Языки с зависимыми типами, общая мотивация.
  • Идрис: несколько примеров кода, поясняющих структуру программы, определение функций, сигнатуры, алгебраические типы в языке Идрис.
  • Идрис: конечные множества (ограниченные натуральные числа), вектора с зависимым от размера типом.
  • Идрис: реализация printf с зависимым типом.
  • Идрис: реализация конъюнкции.

Где почитать

Лекция 12

Индекс де Брауна, обобщённые алгебраические типы, равенство, простые доказательства

  • Индекс де Брауна
  • Ещё раз про изоморфизм Карри-Ховарда и BHK-интерпретацию
  • Идрис: определение натуральных чисел
  • Идрис: определение конечных чисел
  • Идрис: определение векторов с зависимым от размера типом
  • Идрис: определение равенства
  • Идрис: доказательство 0+x=x+0

Где почитать

Лекция 13

Немного о конструктивной математике

  • ZF + классическая логика и ZF + интуиционистская логика
  • Аксиома выбора
  • Чем плохи типы как аналоги множеств. Доказательство «аксиомы выбора»
  • Сетоиды
  • Аксиома выбора в сетоидах
  • Теорема Диаконеску. Неформализованное доказательство
  • Теорема Диаконеску. Как выразить в Идрисе

Где почитать