Научно-образовательный математический центр Приволжского федерального округа (НОМЦ ПФО) и Институт математики и механики им. Н.И. Лобачевского КФУ организуют два мини-курса лекций для студентов, магистрантов, аспирантов и молодых ученых.
Мини-курсы лекций пройдут в Казанском федеральном университете с 5 по 7 ноября 2024 года и будут прочитаны приглашенными лекторами из Математического института им. В. А. Стеклова Российской академии наук (МИАН).
Мини-курс: Лямбда-исчисление
Лектор: Кузнецов Степан Львович, д.ф.-м.н., специалист в области математической логики, ведущий научный сотрудник отдела математической логики Математического института им. В. А. Стеклова Российской академии наук (Москва)
Расписание лекций:
• 5 ноября (вторник) в 15:50 ауд. 609
• 7 ноября (четверг) в 17:30 ауд. 710
II-высотный корпус КФУ, ул. Кремлевская, д. 35
Аннотация курса: Лямбда-исчисление — это логическая система для формализации вычислений посредством операций применения функций и функциональной абстракции. Лямбда-исчисление является основой семейства современных языков программирования, называемых функциональными языками.
В рамках мини-курса будет дано введение в лямбда-исчисление, в двух его видах — бестиповом и типизованном. На первой лекции будет рассказано о лямбда-исчислении без типов (в котором любое лямбда-выражение может быть применено, как функция, к любому другому), о его основных свойствах и о представлении в нём произвольных вычислимых функций.
На второй лекции будут рассмотрены несколько вариантов типизованного лямбда-исчисления (здесь применение ограничено дисциплиной типов), описаны их вычислительные возможности и установлена связь между типизованным лямбда-термами и конструктивными доказательствами (соответствие Карри — Говарда).
Информационный плакат доступен по ссылке.
Мини-курс: Формальная теория истины по Крипке
Лектор: Сперанский Станислав Олегович, к.ф.-м.н., старший научный сотрудник отдела математической логики Математического института им. В. А. Стеклова Российской академии наук (Москва)
Основные направления исследований: вероятностная логика, модальная логика, теория вычислимости.
Расписание лекций:
• 5 ноября (вторник) в 13:50 ауд. 710
• 7 ноября (четверг) в 15:50 ауд. 710
II-высотный корпус КФУ, ул. Кремлевская, д. 35
Аннотация курса: Пусть L — первопорядковый язык арифметики Пеано, а L' получается из L добавлением особого одноместного предикатного символа T. Из леммы о диагонализации легко следует теорема Тарского о неопределимости истины: если L'-структура M обогащает стандартную модель арифметики, то множество всех (гёделевых номеров) L'-предложений, истинных в M, не определимо в самой M. Стало быть, если мы хотим интерпретировать T как истинностный предикат для L', то он должен принимать как минимум три значения: «истинно», «ложно» и «неопределено», где последнее, в частности, соответствует парадоксу лжеца и ему подобным утверждениям.
Наиболее известный трёхзначный подход к формальной теории истины был предложен Солом Крипке. Здесь роль допустимых (частичных) интерпретаций истинностного предиката T играют наименьшие неподвижные точки специальных монотонных операторов. Основой этих операторов являются различные схемы частичных означиваний, которые соответствуют тем или иным трёхзначным логикам, таким как, например, сильная или слабая логика Клини. Получающиеся в результате наименьшие неподвижные точки могут быть представлены как пределы трансфинитных последовательностей аппроксимирующих интерпретаций.
Информационный плакат доступен по ссылке.