Семантика языков программирования
Когда мы пишем программы, мы не оперируем элементарными терминами языка программирования, подобно тому, как, говоря на родном языке, мы не размышляем в терминах синтаксиса и морфологии. Человеческое мышление мнемонично, оно действует в терминах абстракций и идиом. Такой способ рассуждений хорошо работает при создании прикладных программ, однако даёт странные и иногда необъяснимые результаты при реализации языковых инструментов, то есть программ, которые получают на вход одни программы и возвращают другие (компиляторов, интерпретаторов, специализаторов и т. д.).
Это происходит оттого, что такие инструменты должны правильно работать для всех исходных программ, а не только для таких, которые состоят из удобных нам мнемонических структур. Например, что следует делать, если в программе на языке C в теле цикла while мы встретили оператор case (сразу, без switch)?
Довольно быстро (после каких-то 20 лет развития науки о языках программирования) оказалось, что для надёжной работы таких инструментов (или, как минимум, для правдоподобного обоснования, почему они работают именно так) необходимы способы формальной и точной спецификации семантики языков программирования, которые предоставили бы средства для математического доказательства свойств программ и их преобразователей.
В рамках данного курса мы познакомимся со способами формального описания семантик языков программирования, которые позволяют всё это проделывать, а также научимся доказывать свойства программ и их преобразований, пользуясь инструментом для автоматизированного доказательства теорем Rocq.
Пререквизиты курса:
- знание какого-либо языка программирования (а лучше нескольких, а лучше — принадлежащих разным парадигамам (C — Java — Haskell и т.д.))
- начала мат. логики
- начала дискретного анализа
Занятия
15 лекцийЛекция 1
Лекция 1. Основные понятия и примеры.
Лекция 1. Основные понятия и примеры.
Лекция 1. Основные понятия и примеры.
Семантика я.п. как наука о "смыслах" программ. Множественность семантик, статическая и динамическая семантики. "Стандартная семантика" я.п. Семантически-зависимые конструкции: интерпретатор, транслятор, оптимизатор, специализатор и их программные воплощения. Проекции Футамуры-Ершова-Турчина. Вопросы практического применения.
Лекция 2
Лекция 2. Формы семантических описаний
Лекция 2. Формы семантических описаний
Лекция 2. Формы семантических описаний
Семантический домен, семантическая функция. Понятие "стиля" описания семантики. Язык простых варажений и его денотационная семантика. Операционные семантики малого и большого шага. Семантика в терминах редукционных контекстов. Помеченные системы переходов. Композиционность, структурная индукция.
Лекция 3
Лекция 3. Язык чистых выражений
Лекция 3. Язык чистых выражений
Лекция 3. Язык чистых выражений
Синтаксис языка чистых выражений. Денотационная семантика языка чистых выражений. Операционная семантика языка чистых выражений: семантика большого и малого шага, семантика с редукционными контекстами, семантика в виде системы помеченных переходов. Строгость семантики чистых выражений. Эквивалентность семантик, описанных различными стилями.
Лекция 4
Лекция 4. Простой имеративный язык: семантика большого и малого шага
Лекция 4. Простой имеративный язык: семантика большого и малого шага
Лекция 4. Простой имеративный язык: семантика большого и малого шага
Простой императивный язык: присваивания, последовательное исполнение, пустой оператор, ветвления, циклы, ввод-вывод. Операционные семантики большого и малого шага для императивных конструкций.
Лекция 5
Лекция 5. Простой императивнй язык: помеченные системы переходов, редукционные контексты, проблема денотационной семантики
Лекция 5. Простой императивнй язык: помеченные системы переходов, редукционные контексты, проблема денотационной семантики
Лекция 5. Простой императивнй язык: помеченные системы переходов, редукционные контексты, проблема денотационной семантики
Семантика в стиле редукционных контекстов и помеченных систем переходов. Ненаблюдаемые действия. Некомпозиционность семантики простого императивного языка, принципы доказательств индукцией по дереву вывода и длине последовательности вывода. Проблема денотационного описания для простого императивного языка.
Лекция 6
Лекция 6. Семантика рекурсивного определения как неподвижная точка его абстрагированной правой части
Лекция 6. Семантика рекурсивного определения как неподвижная точка его абстрагированной правой части
Лекция 6. Семантика рекурсивного определения как неподвижная точка его абстрагированной правой части
Рекурсивные определения и неподвижные точки. Частично-упорядоченные множества, монотонные и дистрибутивные функции. Свойства редуктивности и экстенсивности. Решетки и полные решётки. Теорема Тарского-Кнастера. Варианты теорем о неподвижных точках. Индуктивные и коиндуктивные определения и принципы доказательства.
Лекция 7
Лекция 7. Денотационная семантика рекурсивных определений
Лекция 7. Денотационная семантика рекурсивных определений
Лекция 7. Денотационная семантика рекурсивных определений
Частичный порядок, основанный на доопределении. Мотовация и связь с рекурсией. Частичные порядки с упорядоченными цепями. Теорема о неподвижной точке монотонной функции. Денотационная семантика циклических конструкций.
Лекция 8
Лекция 8. Лямбда-исчисление: синтаксис и основные определения
Лекция 8. Лямбда-исчисление: синтаксис и основные определения
Лекция 8. Лямбда-исчисление: синтаксис и основные определения
Синтаксис нетипизированного лямбда-исчисления. Интуитивная семантика. Свободные и связанные переменные. Подстановка, альфа-эквивалентность, бета-редукция, эта-расширение. Проблема захвата переменных. Конгруэнтные отношения. Бета-сводимость и бета-эквивалентность. Бета-нормальная форма, теорема Чёрча-Россера.
Лекция 9
Лекция 9. Лямбда-представимость; нумералы Чёрча.
Лекция 9. Лямбда-представимость; нумералы Чёрча.
Лекция 9. Лямбда-представимость; нумералы Чёрча.
Представление булевских значений лямбда-термами. Кодирование условного оператора. Нумералы Чёрча, кодирование арифметических операций. Комбинатор неподвижной точки, кодирование рекурсии/циклических конструкций. Y- и Z-комбинаторы.
Лекция 10
Лекция 10
Лекция 10
Лекция 10
Лекция 11
Лекция 11
Лекция 11
Лекция 11
Лекция 12
Лекция 12
Лекция 12
Лекция 12
Лекция 13
Лекция 13
Лекция 13
Лекция 13
Лекция 14
Лекция 14
Лекция 14
Лекция 14
Лекция 15
Лекция 15
Лекция 15
Лекция 15
Лекторы
Дополнительные материалы
1 материал
Партнеры
