Факультатив "Теория вычислений и логика" — различия между версиями

Материал из Wiki - Факультет компьютерных наук
Перейти к: навигация, поиск
(История: Добавлена информация про занятие 9)
м
 
(не показано 56 промежуточных версии этого же участника)
Строка 1: Строка 1:
Факультатив дополняет курс дискретной математики-2 рядом сюжетов из математической логики и теории алгоритмов. Содержание курса может меняться в соответствии с желаниями слушателей: мы уделим больше внимания вопросам, заинтересовавшим аудиторию. Занятия планируется проводить в формате живой беседы участников. Мы будем пытаться самостоятельно приходить к некоторым важным идеям, прежде чем вводить формальные определения. Факультатив желательно (хотя и необязательно) посещать одновременно с изучением курса дискретной математики-2 или после прохождения этого курса.
+
Прямая ссылка на эту страницу: [https://tinyurl.com/logicomp tinyurl.com/logicomp]
  
==Общая информация==
+
==Архив==
'''Официальное название:''' «Избранные вопросы теории вычислений и математической логики».
+
* [http://wiki.cs.hse.ru/%D0%A4%D0%B0%D0%BA%D1%83%D0%BB%D1%8C%D1%82%D0%B0%D1%82%D0%B8%D0%B2_%22%D0%A2%D0%B5%D0%BE%D1%80%D0%B8%D1%8F_%D0%B2%D1%8B%D1%87%D0%B8%D1%81%D0%BB%D0%B5%D0%BD%D0%B8%D0%B9_%D0%B8_%D0%BB%D0%BE%D0%B3%D0%B8%D0%BA%D0%B0%22_(%D0%9E%D1%81%D0%B5%D0%BD%D1%8C_2020) Факультатив "Вычислимость и логика", осень 2020]
  
'''Преподаватель:''' [https://www.hse.ru/org/persons/305069360 Антон Гнатенко], почта: [mailto:agnatenko@hse.ru agnatenko@hse.ru], телеграм: [https://t.me/antongnatenko @antongnatenko]. Всюду на этой странице местоимение «я» обозначает именно этого человека.
+
* [http://wiki.cs.hse.ru/%D0%A4%D0%B0%D0%BA%D1%83%D0%BB%D1%8C%D1%82%D0%B0%D1%82%D0%B8%D0%B2_%22%D0%A2%D0%B5%D0%BE%D1%80%D0%B8%D1%8F_%D0%B2%D1%8B%D1%87%D0%B8%D1%81%D0%BB%D0%B5%D0%BD%D0%B8%D0%B9%22_(%D0%92%D0%B5%D1%81%D0%BD%D0%B0_2021) Факультатив "Теория вычислений", весна 2021]
 
+
'''Время и место:''' среда (с 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
+
<br />
+
<br />
+
 
+
'''18 сентября 2020. Выложена первая порция задач.''' См. раздел [http://wiki.cs.hse.ru/%D0%A4%D0%B0%D0%BA%D1%83%D0%BB%D1%8C%D1%82%D0%B0%D1%82%D0%B8%D0%B2_%22%D0%A2%D0%B5%D0%BE%D1%80%D0%B8%D1%8F_%D0%B2%D1%8B%D1%87%D0%B8%D1%81%D0%BB%D0%B5%D0%BD%D0%B8%D0%B9_%D0%B8_%D0%BB%D0%BE%D0%B3%D0%B8%D0%BA%D0%B0%22#.D0.97.D0.B0.D0.B4.D0.B0.D1.87.D0.B8 «Задачи»]
+
<br />
+
<br />
+
 
+
'''23 сентября 2020. Занятие 2.''' Лемма о накачке. Двусторонние автоматы.
+
 
+
Видеозапись: https://youtu.be/ssBN5EcUIqU
+
<br />
+
<br />
+
 
+
'''30 сентября 2020. Занятие 3.''' Некоторые открытые проблемы теории автоматов. Древесные автоматы.
+
 
+
Видеозапись: https://youtu.be/nSO7Uzze0YI
+
<br />
+
<br />
+
 
+
'''7 октября 2020. Занятие 4.''' Проблема усердного бобра. Примитивно рекурсивные функции.
+
 
+
Видеозапись: https://youtu.be/YKBEfiTU-YI
+
<br />
+
<br />
+
 
+
'''11 октября 2020. Выложена вторая порция задач и новая бонусная задача по автоматам.''' См. раздел [http://wiki.cs.hse.ru/%D0%A4%D0%B0%D0%BA%D1%83%D0%BB%D1%8C%D1%82%D0%B0%D1%82%D0%B8%D0%B2_%22%D0%A2%D0%B5%D0%BE%D1%80%D0%B8%D1%8F_%D0%B2%D1%8B%D1%87%D0%B8%D1%81%D0%BB%D0%B5%D0%BD%D0%B8%D0%B9_%D0%B8_%D0%BB%D0%BE%D0%B3%D0%B8%D0%BA%D0%B0%22#.D0.97.D0.B0.D0.B4.D0.B0.D1.87.D0.B8 «Задачи»]
+
<br />
+
<br />
+
 
+
'''14 октября 2020. Занятие 5.''' Функция Аккермана. Частично рекурсивные функции.
+
 
+
Видеозапись: https://youtu.be/hqtfPIGA72k
+
<br />
+
<br />
+
 
+
'''28 октября 2020. Занятие 6.''' Лямбда-исчисление. Моделирование примитивно рекурсивных функций.
+
 
+
Видеозапись: https://youtu.be/bCSIW_3Pzwg
+
<br />
+
<br />
+
 
+
'''4 ноября 2020. Добавлены задачи по лямбда-исчислению.''' См. раздел [http://wiki.cs.hse.ru/%D0%A4%D0%B0%D0%BA%D1%83%D0%BB%D1%8C%D1%82%D0%B0%D1%82%D0%B8%D0%B2_%22%D0%A2%D0%B5%D0%BE%D1%80%D0%B8%D1%8F_%D0%B2%D1%8B%D1%87%D0%B8%D1%81%D0%BB%D0%B5%D0%BD%D0%B8%D0%B9_%D0%B8_%D0%BB%D0%BE%D0%B3%D0%B8%D0%BA%D0%B0%22#.D0.97.D0.B0.D0.B4.D0.B0.D1.87.D0.B8 «Задачи»]
+
<br />
+
<br />
+
 
+
'''11 ноября 2020. Занятие 7.''' Лямбда-исчисление:  теоремы о неподвижной точке и о рекурсии
+
 
+
Видеозапись: https://youtu.be/O95mbv5YH_8
+
 
+
Доска: https://jamboard.google.com/d/1YjDm4adrO31QKmvgktj6uTcPPkYZEygYwYT_nc6CyIM/edit?usp=sharing
+
<br />
+
<br />
+
 
+
'''18 ноября 2020. Занятие 8.''' Теорема о неразрешимости для лямбда-исчисления, простые типы по Чёрчу
+
 
+
Видеозапись: https://youtu.be/P0N-Pxzep4E
+
 
+
Доска: https://jamboard.google.com/d/1eVMbsdByjNvyD07d6zaTYKKozTDsd5qZtP1TUYuUneU/edit?usp=sharing
+
 
+
Поскольку я потерял счёт времени, занятие 8 продолжалось примерно 50 минут.
+
<br />
+
<br />
+
 
+
'''17 ноября 2020. Выложена третья порция задач (включающая пару бонусных).''' См. раздел [http://wiki.cs.hse.ru/%D0%A4%D0%B0%D0%BA%D1%83%D0%BB%D1%8C%D1%82%D0%B0%D1%82%D0%B8%D0%B2_%22%D0%A2%D0%B5%D0%BE%D1%80%D0%B8%D1%8F_%D0%B2%D1%8B%D1%87%D0%B8%D1%81%D0%BB%D0%B5%D0%BD%D0%B8%D0%B9_%D0%B8_%D0%BB%D0%BE%D0%B3%D0%B8%D0%BA%D0%B0%22#.D0.97.D0.B0.D0.B4.D0.B0.D1.87.D0.B8 «Задачи»]
+
<br />
+
<br />
+
 
+
'''25 ноября 2020. Занятие 9.'''  Арифметика Пеано: язык, аксиомы и представление вычислимых функций. Теорема Чёрча о неразрешимости.
+
 
+
Видеозапись: https://youtu.be/gCZtU8iAwsw
+
 
+
Доска: https://jamboard.google.com/d/1aq6BRgMAevit7HDjbd0rGBSwJ09oaN9Pqj1v9vNI7XE/edit?usp=sharing
+
 
+
==Программа курса (примерная)==
+
 
+
Темы, ''написанные курсивом'', являются дополнительными. Мы рассмотрим их, если будет на то желание слушателей. Если ''курсивные темы'' станут реальностью, они могут вытеснить обычные темы и занять их место.
+
 
+
====Регулярные языки и автоматы====
+
* Детерминированные конечные автоматы и их языки
+
* Нерегулярные языки и лемма о накачке
+
* Недетерминированные автоматы
+
* Автоматы и поиск подстроки в строке
+
* ''Алгебраические свойства регулярных языков. Минимизация автоматов''
+
* ''Регулярные выражения''
+
* ''Автоматы на термах, на деревьях, над бесконечными словами, ...''
+
 
+
====Теория алгоритмов====
+
* Частично рекурсивные функции
+
* Лямбда-исчисление
+
* ''Вычисления с оракулом''
+
 
+
====Логика====
+
* Логические способы описания языков. Выразительная сила логик. Трансляция формул в автоматы и автоматов в формулы.
+
* Логическое программирование
+
* ''Арифметика и вычислимые функции. Теоремы Чёрча, Тарского и Гёделя''
+
* ''Доказуемость в арифметике и ещё одна теорема Гёделя''
+
* ''Логика второго порядка''
+
* '''''...''''' (это многоточие написано ''курсивом'')
+
 
+
==Правила оценивания==
+
Чтобы получить оценку, нужно набрать необходимое количество баллов (обычных и бонусных). Вот как это сделать:
+
 
+
* '''Решать задачи''', которые предлагаются на занятиях и появляются на этой страничке в разделе [http://wiki.cs.hse.ru/%D0%A4%D0%B0%D0%BA%D1%83%D0%BB%D1%8C%D1%82%D0%B0%D1%82%D0%B8%D0%B2_%22%D0%A2%D0%B5%D0%BE%D1%80%D0%B8%D1%8F_%D0%B2%D1%8B%D1%87%D0%B8%D1%81%D0%BB%D0%B5%D0%BD%D0%B8%D0%B9_%D0%B8_%D0%BB%D0%BE%D0%B3%D0%B8%D0%BA%D0%B0%22#.D0.97.D0.B0.D0.B4.D0.B0.D1.87.D0.B8 «Задачи»]. Для каждой задачи указано количество баллов, которые можно получить за правильное решение. У каждой задачи есть мягкий дедлайн — после него правильные решения получат половину баллов. Задачи можно сдавать устно или письменно. В случае письменной сдачи может потребоваться устная защита некоторых неслучайно выбранных задач. Баллы за задачу выставляются только в случае успешной защиты.
+
 
+
* '''Решать трудные задачи''', которые появляются там же. За трудные задачи даются '''бонусные баллы''' (см. ниже).
+
 
+
* '''Участвовать в занятиях'''. Иногда можно получить один или два '''бонусных балла''' за высказанную идею решения задачи, идею доказательства, ответ на вопрос.
+
 
+
Пусть теперь M = «максимально возможное количество обычных баллов», а S = «сумма всех баллов (обычных и бонусных), набранных студентом за семестр».
+
Тогда накопленная оценка равна P = min{S / M * 10, 10}.
+
 
+
Таким образом, можно получить 10 баллов, просто решая обычные задачи. Но это проще сделать, если набирать бонусные баллы.
+
 
+
Если P >= 4, то по желанию студента можно объявить её итоговой оценкой за факультатив. Если P < 4 или студент хочет улучшить оценку, проводится письменный экзамен, состоящий из нескольких обычных задач. Оценка за экзамен E равна доле решённых задач от общего количества, умноженной на 10. Итоговая оценка вычисляется по формуле F = 0.5P + 0.5E. Если F всё ещё меньше 4, экзамен можно пересдать. Если и это не поможет, можно сдавать устный экзамен комиссии. При этом P аннулируется и оценка, полученная на экзамене, является окончательной. (Будем надеяться, что до этого не дойдёт.)
+
 
+
==Задачи==
+
'''Письменные решения нужно сдавать [https://forms.gle/erSRPvvgTbroDK5G8 вот этой гугл-форме].''' Пожалуйста, оформляйте решения аккуратно. Для оцифровки записей лучше всего использовать не фото, а специальные приложения-сканеры. Например, Camscanner. Если вы сдаёте несколько задач сразу, объединяйте их в один пдф или в один архив.
+
 
+
Для сдачи файлов в форму нужен гугл-аккаунт. Если его нет и по каким-то причинам вы совсем не хотите его заводить, можно сдавать задачи устно или договориться о каком-либо ещё варианте. Но лучше всё-таки завести аккаунт.
+
 
+
'''Правила оформления решений.''' При изложении решений рекомендуется соблюдать разумный баланс между строгостью и размахиванием руками. Если требуется доказать, например, регулярность языка, то достаточно предоставить словесное описание соответствующего автомата (если только в условии явно не просят построить автомат). Описание должно быть, тем не менее, чётким и подробным (но без фанатизма). Если какие-то важные детали из этого описания будут неясны, я попрошу сделать пояснения (возможно, устные).
+
 
+
'''Можно сдавать задачи устно:'''
+
* В Зуме в среду. О своём желании сдавать задачи нужно сообщить мне в конце занятия или написать в Телеграме, и мы договоримся об удобном времени. Точно недоступен интервал 15:10-16:40.
+
* В Вышке (о желании прийти и сдать задачи тоже нужно сообщить заранее):
+
**в понедельник (16:00-17:00)
+
**в пятницу (15:00-16:00)
+
 
+
[https://drive.google.com/file/d/1ix0jHA7Wb5QbOZ-whAXXLFPNk7M-N7kw/view?usp=sharing Задачи по автоматам]. Мягкий дедлайн: 1 ноября. Дедлайн по задаче 8 перенесён на конец курса.
+
 
+
[https://drive.google.com/file/d/18CZkDW3LvnIdAz45NAenWWqO2lxdAD7h/view?usp=sharing Бонусные задачи по автоматам]. Можно сдавать до конца курса.
+
 
+
[https://drive.google.com/file/d/1tO_A5gueirUT9MTURjGc9v04bRmaJefE/view?usp=sharing Задачи по рекурсивным функциям и лямбда-исчислению]. Мягкий дедлайн: 1 декабря.
+
 
+
[https://drive.google.com/file/d/19IspepZ3a9UXmaIfnQp5OUoH2WKUE5P7/view?usp=sharing Задачи по лямбда-исчислению и комбинаторной логике ('''есть бонусы''')]. Мягкий дедлайн: 21 декабря.
+
 
+
==Литература==
+
# Dexter C. Kozen. Automata and Computability. (Моя любимая книга про автоматы)
+
# Н.К. Верещагин, А. Шень. Вычислимые функции. (Незаменимая книга по курсу ДМ-2, в которой также можно почитать про рекурсивные функции, оракулы, арифметичность вычислимых функций)
+
# Дж. Булос, Р. Джеффри. Вычислимость и логика. (Немного философская книга про логику и алгоритмы, в которой есть много всего интересного и, в частности, кое-что про логику второго порядка)
+
# Dexter C. Kozen. Theory of Computation. (Ещё одна замечательная книга Декстера Козена по теории (сложности) вычислений; здесь можно прочитать про автоматы над бесконечными словами и про многое другое, не вошедшее, увы, в нашу программу)
+
# С.Л. Кузнецов, Л.Д. Беклемишев. [https://www.youtube.com/playlist?list=PLUbD59ZHv1GTHQ8fFYc1stXVQ-RGRzy8q Плейлист спецкурса "Лямбда-исчисление и вычислительная теория доказательств"]
+
# J.R. Hindley, J.P. Seldin. Lambda-Calculus and Combinators, an Introduction.
+

Текущая версия на 14:29, 4 сентября 2021

Прямая ссылка на эту страницу: tinyurl.com/logicomp

Архив