Системы типизации лямбда-исчисления

Общая информация
ЛекторД. Н. Москвин
Семестрвесна 2011
Дата начала27.02.2011
Количество пар12
Язык курсарусский
Анонсы
Встреча на сайте T&Phttp://theoryandpractice.ru/courses/1997-sistemy-tipizatsii-lyambda-ischisleniya
Анонс на сайте it-event.ruhttp://it-event.ru/2363/
Аннотация

Современные функциональные языки программирования, такие как Haskell, наследники ML (SML, Ocaml, F#), Agda2 и т.п., обладают весьма богатыми и сложными системами типов. Несмотря на такое разнообразие, эти системы имеют в своей основе хорошо проработанную формальную теорию типизированных лямбда-исчислений.

В рамках курса рассматриваются различные системы типизации лямбда-исчисления. Понятие типа вводится на примере просто типизированного чистого лямбда-исчисления. Исследуются два основных подхода к типизации лямбда-исчисления: в стиле Карри и в стиле Чёрча. Обсуждаются следующие системы: полиморфные типы (System F), операторы над типами, полиморфизм высших порядков, зависимые типы, рекурсивные типы. Для изучаемых систем исследуются проблемы проверки, присваивания (синтеза) и населенности типов. Обсуждается связь между различными логическими системами и системами типов.

Решения домашних заданий можно присылать на адрес dmoskvin()gmail.com

Слайды первой лекции
Лекции Подсказка: слайды, видеозапись и другие материалы лекции доступны со страницы лекции, попасть на которую можно, нажав на её название.

1. Система лямбда-исчисления без типов
(27.02.2011 - 11:15 - 12:50)

Применение и абстракция. Свободные и связанные переменные. Комбинаторы. Функции нескольких переменных, каррирование. Подстановка, лемма подстановки. Бета-преобразование. Теорема о неподвижной точке, Y-комбинатор. http://lektorium.tv/lecture/?id=13181
2. Программирование в лямбда-исчислении и лямбда-определимость
(27.02.2011 - 13:00 - 14:35)

$ \lambda $-исчисление как язык программирования. Булевы значения, пары. Числа Чёрча, операции над ними. Примитивная рекурсия. Списки. Лямбда-определимость и вычислимость по Тьюрингу. Неразрешимость бестипового $ \lambda $-исчисления. http://lektorium.tv/lecture/?id=13182
3. Отношение редукции
(06.03.2011 - 11:15 - 12:50)

Редексы. Одношаговая и многошаговая $ \beta $-редукция, $ \beta $-эквивалентность. $ \beta $-нормальная форма. Редукционные графы. Теорема Чёрча-Россера. Следствия: редуцируемость к нормальной форме, единственность нормальной формы. Нормальная и аппликативные стратегии редукции. Теорема о нормализации. http://lektorium.tv/lecture/?id=13183
4. Просто типизированное лямбда-исчисление
(06.03.2011 - 13:00 - 14:35)

Система $ \lambda_{\rightarrow} $. Предтермы. Отношение типизации. Контексты. Правила типизации по Карри и по Чёрчу. Деревья вывода типов. Система минимальной пропозициональной логики. Соответствие Карри-Говарда. http://lektorium.tv/lecture/?id=13184
5. Свойства просто типизированной системы
(13.03.2011 - 11:15 - 12:50)

Леммы о контекстах. Типизируемость подтермов, нетипизируемые предтермы. Лемма подстановки. Теорема о редукции субъекта. Незамкнутость относительно экспансии. Уникальность типов для типизации по Чёрчу. Связь между системами Карри и Черча. Главный (наиболее общий) тип для $ \lambda_{\rightarrow} $ в стиле Карри. Свойства подстановки. Унификация. Алгоритм Хиндли-Милнера. http://lektorium.tv/lecture/?id=13185
6. Просто типизированная система: разрешимость, нормализация, расширения
(13.03.2011 - 13:00 - 14:35)

Проблемы разрешимости: проверка типа, синтез типа и населенность типа. Лемма об образовании редексов. Меры типа и терма. Слабая нормализация для $ \lambda_{\rightarrow} $. Сильная нормализация. Интерпретации $ {\rightarrow} $-типов. Расширение системы константами. $ \delta $-редукция. http://lektorium.tv/lecture/?id=13186
7. Полиморфные системы типов
(27.03.2011 - 11:15 - 12:50)

Полиморфные системы в стиле Карри. Сильный и слабый полиморфизм. Типы в контекстах. Введение и удаление $ \forall $. Проблемы разрешимости в полиморфном $ \lambda $-исчислении в стиле Карри. Let-полиморфизм. Полиморфизм высших рангов. Система $ \lambda2 $ в стиле Чёрча. Универсальные абстракция и применение. Импредикативность. Связь между $ \lambda2 $ в стиле Карри и Черча. Сильная нормализация. Интерпретации $ \forall $-типов. Параметричность. http://lektorium.tv/lecture/?id=13208
8. Полиморфные системы: логическая интерпретация и программирование
(27.03.2011 - 13:00 - 14:35)

Интуиционистская пропозициональная логика второго порядка. Представление стандартных пропозициональных связок в $ \lambda2 $. Экзистенциальные типы. Пустой тип, булев тип, произведение и сумма типов. Типы для чисел Чёрча и списков. Индуктивные типы. http://lektorium.tv/lecture/?id=13209
9. Лямбда-куб Барендрегта
(15.05.2011 - 11:15 - 12:50)

Зависимости между термами и типами. Система с операторами над типами $ \lambda\underline{\omega} $. Конструкторы типов. Виды (kinds). Система с зависимыми типами $ \lambda P $. Семейства типов. Виды для семейств типов. Тип зависимого произведения ($ Pi $-тип). Проблема равенства типов. Системы лямбда-куба. Общие и специальные правила присваивания типов.
10. Лямбда-куб и логические системы
(15.05.2011 - 13:00 - 14:35)

Интерпретация "высказывания-как-типы". Правильность и полнота представления. Прямое представление логик в системах лямбда-куба. Logical Framework: представление различных логик в $ \lambda P $.
11. Чистые системы типов
(22.05.2011 - 11:15 - 12:50)

Спецификация чистой системы типов, правила и аксиомы типизации. Примеры PTS. Свойства PTS: редукция субъекта, лемма генерации, единственность типа. Сильная нормализуемость и разрешимость TCP и TSP. Населенность $ \bot $. Алгоритм синтеза типа для $ \lambda P $.
12. Рекурсивные типы и типы-пересечения
(22.05.2011 - 13:00 - 14:35)

Рекурсивные типы: система $ \lambda\mu $. Отношение эквивалентности между типами, дерево типа. Типизация Y-комбинатора. Cвойства системы $ \lambda\mu $. Типы-пересечения: система $ \lambda\cap $. Отношение подтипирования, общий надтип $ \top $. Экспансия субъекта. Cвойства системы $ \lambda\cap $.
Ваша оценка: Пусто Средняя: 4.5 (19 votes)
Share |
Денис Николаевич Москвин
Денис Николаевич Москвин
Денис Николаевич Москвин