Факультатив "Теория вычислений и логика"
Факультатив дополняет курс дискретной математики-2 рядом сюжетов из математической логики и теории алгоритмов. Содержание курса может меняться в соответствии с желаниями слушателей: мы уделим больше внимания вопросам, заинтересовавшим аудиторию. Занятия планируется проводить в формате живой беседы участников. Мы будем пытаться самостоятельно приходить к некоторым важным идеям, прежде чем вводить формальные определения. Факультатив желательно (хотя и необязательно) посещать одновременно с изучением курса дискретной математики-2 или после прохождения этого курса.
Содержание
Общая информация
Официальное название: «Избранные вопросы теории вычислений и математической логики».
Преподаватель: Антон Гнатенко, почта: agnatenko@hse.ru, телеграм: @antongnatenko. Всюду на этой странице местоимение «я» обозначает именно этого человека.
Время и место: среда (с 16 сентября), 9:30-10:50, Zoom: <для получения ссылки — добавляйтесь в чат>
Записи занятий: https://www.youtube.com/playlist?list=PLbjUsKUoAqLPFWgiaIFX4QW__3Obyipcw
Доски (начиная с занятия 7 (11 ноября)): https://drive.google.com/drive/folders/1ahvNYYDqhXqWDyhUYwX-OteyWKOLaa05?usp=sharing
Телеграм-чат: https://t.me/joinchat/FehKYBXfk1Mu7npLZ3Tt_w
Ссылка на эту страницу: https://tinyurl.com/logicomp
Форма для задач: https://forms.gle/erSRPvvgTbroDK5G8
Таблица с оценками: https://docs.google.com/spreadsheets/d/1FhHnZJBfumvzNVqcnviWxmR8cIulIwRSmCQmaRXoC6g/edit?usp=sharing
История
16 сентября 2020. Занятие 1. Конечные автоматы и регулярные языки.
Видеозапись: https://youtu.be/80Ur1TKLU48
Конспект: https://drive.google.com/file/d/1Xa8nprULWAkrj5E1OFAci06ucIZoHCo_/view?usp=sharing
18 сентября 2020. Выложена первая порция задач. См. раздел «Задачи»
23 сентября 2020. Занятие 2. Лемма о накачке. Двусторонние автоматы.
Видеозапись: https://youtu.be/ssBN5EcUIqU
30 сентября 2020. Занятие 3. Некоторые открытые проблемы теории автоматов. Древесные автоматы.
Видеозапись: https://youtu.be/nSO7Uzze0YI
7 октября 2020. Занятие 4. Проблема усердного бобра. Примитивно рекурсивные функции.
Видеозапись: https://youtu.be/YKBEfiTU-YI
11 октября 2020. Выложена вторая порция задач и новая бонусная задача по автоматам. См. раздел «Задачи»
14 октября 2020. Занятие 5. Функция Аккермана. Частично рекурсивные функции.
Видеозапись: https://youtu.be/hqtfPIGA72k
28 октября 2020. Занятие 6. Лямбда-исчисление. Моделирование примитивно рекурсивных функций.
Видеозапись: https://youtu.be/bCSIW_3Pzwg
4 ноября 2020. Добавлены задачи по лямбда-исчислению. См. раздел «Задачи»
11 ноября 2020. Занятие 7. Лямбда-исчисление: теоремы о неподвижной точке и о рекурсии
Видеозапись: https://youtu.be/O95mbv5YH_8
Доска: https://jamboard.google.com/d/1YjDm4adrO31QKmvgktj6uTcPPkYZEygYwYT_nc6CyIM/edit?usp=sharing
18 ноября 2020. Занятие 8. Теорема о неразрешимости для лямбда-исчисления, простые типы по Чёрчу
Видеозапись: https://youtu.be/P0N-Pxzep4E
Доска: https://jamboard.google.com/d/1eVMbsdByjNvyD07d6zaTYKKozTDsd5qZtP1TUYuUneU/edit?usp=sharing
Поскольку я потерял счёт времени, занятие 8 продолжалось примерно 50 минут.
11 октября 2020. Выложена третья порция задач (включающая пару бонусных). См. раздел «Задачи»
Программа курса (примерная)
Темы, написанные курсивом, являются дополнительными. Мы рассмотрим их, если будет на то желание слушателей. Если курсивные темы станут реальностью, они могут вытеснить обычные темы и занять их место.
Регулярные языки и автоматы
- Детерминированные конечные автоматы и их языки
- Нерегулярные языки и лемма о накачке
- Недетерминированные автоматы
- Автоматы и поиск подстроки в строке
- Алгебраические свойства регулярных языков. Минимизация автоматов
- Регулярные выражения
- Автоматы на термах, на деревьях, над бесконечными словами, ...
Теория алгоритмов
- Частично рекурсивные функции
- Лямбда-исчисление
- Вычисления с оракулом
Логика
- Логические способы описания языков. Выразительная сила логик. Трансляция формул в автоматы и автоматов в формулы.
- Логическое программирование
- Арифметика и вычислимые функции. Теоремы Чёрча, Тарского и Гёделя
- Доказуемость в арифметике и ещё одна теорема Гёделя
- Логика второго порядка
- ... (это многоточие написано курсивом)
Правила оценивания
Чтобы получить оценку, нужно набрать необходимое количество баллов (обычных и бонусных). Вот как это сделать:
- Решать задачи, которые предлагаются на занятиях и появляются на этой страничке в разделе «Задачи». Для каждой задачи указано количество баллов, которые можно получить за правильное решение. У каждой задачи есть мягкий дедлайн — после него правильные решения получат половину баллов. Задачи можно сдавать устно или письменно. В случае письменной сдачи может потребоваться устная защита некоторых неслучайно выбранных задач. Баллы за задачу выставляются только в случае успешной защиты.
- Решать трудные задачи, которые появляются там же. За трудные задачи даются бонусные баллы (см. ниже).
- Участвовать в занятиях. Иногда можно получить один или два бонусных балла за высказанную идею решения задачи, идею доказательства, ответ на вопрос.
Пусть теперь M = «максимально возможное количество обычных баллов», а S = «сумма всех баллов (обычных и бонусных), набранных студентом за семестр». Тогда накопленная оценка равна P = min{S / M * 10, 10}.
Таким образом, можно получить 10 баллов, просто решая обычные задачи. Но это проще сделать, если набирать бонусные баллы.
Если P >= 4, то по желанию студента можно объявить её итоговой оценкой за факультатив. Если P < 4 или студент хочет улучшить оценку, проводится письменный экзамен, состоящий из нескольких обычных задач. Оценка за экзамен E равна доле решённых задач от общего количества, умноженной на 10. Итоговая оценка вычисляется по формуле F = 0.5P + 0.5E. Если F всё ещё меньше 4, экзамен можно пересдать. Если и это не поможет, можно сдавать устный экзамен комиссии. При этом P аннулируется и оценка, полученная на экзамене, является окончательной. (Будем надеяться, что до этого не дойдёт.)
Задачи
Письменные решения нужно сдавать вот этой гугл-форме. Пожалуйста, оформляйте решения аккуратно. Для оцифровки записей лучше всего использовать не фото, а специальные приложения-сканеры. Например, Camscanner. Если вы сдаёте несколько задач сразу, объединяйте их в один пдф или в один архив.
Для сдачи файлов в форму нужен гугл-аккаунт. Если его нет и по каким-то причинам вы совсем не хотите его заводить, можно сдавать задачи устно или договориться о каком-либо ещё варианте. Но лучше всё-таки завести аккаунт.
Правила оформления решений. При изложении решений рекомендуется соблюдать разумный баланс между строгостью и размахиванием руками. Если требуется доказать, например, регулярность языка, то достаточно предоставить словесное описание соответствующего автомата (если только в условии явно не просят построить автомат). Описание должно быть, тем не менее, чётким и подробным (но без фанатизма). Если какие-то важные детали из этого описания будут неясны, я попрошу сделать пояснения (возможно, устные).
Можно сдавать задачи устно:
- В Зуме в среду. О своём желании сдавать задачи нужно сообщить мне в конце занятия или написать в Телеграме, и мы договоримся об удобном времени. Точно недоступен интервал 15:10-16:40.
- В Вышке (о желании прийти и сдать задачи тоже нужно сообщить заранее):
- в понедельник (16:00-17:00)
- в пятницу (15:00-16:00)
Задачи по автоматам. Мягкий дедлайн: 1 ноября. Дедлайн по задаче 8 перенесён на конец курса.
Бонусные задачи по автоматам. Можно сдавать до конца курса.
Задачи по рекурсивным функциям и лямбда-исчислению. Мягкий дедлайн: 1 декабря.
Задачи по лямбда-исчислению и комбинаторной логике (есть бонусы). Мягкий дедлайн: 21 декабря.
Литература
- Dexter C. Kozen. Automata and Computability. (Моя любимая книга про автоматы)
- Н.К. Верещагин, А. Шень. Вычислимые функции. (Незаменимая книга по курсу ДМ-2, в которой также можно почитать про рекурсивные функции, оракулы, арифметичность вычислимых функций)
- Дж. Булос, Р. Джеффри. Вычислимость и логика. (Немного философская книга про логику и алгоритмы, в которой есть много всего интересного и, в частности, кое-что про логику второго порядка)
- Dexter C. Kozen. Theory of Computation. (Ещё одна замечательная книга Декстера Козена по теории (сложности) вычислений; здесь можно прочитать про автоматы над бесконечными словами и про многое другое, не вошедшее, увы, в нашу программу)
- С.Л. Кузнецов, Л.Д. Беклемишев. Плейлист спецкурса "Лямбда-исчисление и вычислительная теория доказательств"
- J.R. Hindley, J.P. Seldin. Lambda-Calculus and Combinators, an Introduction.
