Курс лекций Николая Николаевича Непейводы «Конструктивная математика и ее применения»
Данный курс лекций имеет отдалённое отношение к тематике семинара, но, ввиду отсутствия прочих информационных ресурсов и наличия заинтересованности отдельных участников семинара в них, информация о них помещена здесь.
- Курс предназначен для магистров и бакалавров 3-4 года обучения.
- Курс предполагает прохождение стандартного курса математики (алгебра, начала топологии, анализ, начала теории алгоритмов) и начального курса логики (прежде всего, умение корректно записывать и читать логические формулы), а также знакомство с высокоуровневыми концепциями современной информатики (языки спецификаций, альтернативные стили программирования).
- Курс рассчитан на 16 часов лекций и 16 часов практики.
- Отчетность: домашняя контрольная работа (теоретическая), программная модель простейших конструктивных конструкций, зачет по окончанию курса.
Лекции проходят в течение марта 2010 года по следующему расписанию:
По пятницам в 18:00 в аудитории 523 2-го учебного корпуса МГУ проводятся дополнительные лекции для ВМК.
По субботам с 10:40 до 16:10 в аудитории Е335 нового первого учебного корпуса проводятся лекции для ВМК и философского факультета.
Аннотация
Конструктивизм (понимаемый здесь в широком смысле слова, как совокупность течений от интуционизма до советского конструктивизма) явился интереснейшим математическим экспериментом ХХ века. Впервые была точно показана возможность рациональной альтернативы общепринятому рационализму. который претендовал на монополию в области научного подхода. Точно так же впервые была показана неразрывная связь в математике идеальных и реальных объектов, являющаяся источником «непостижимой эффективности математики в приложениях», причем как раз тех ее разделов, которые на первый взгляд кажутся наиболее оторванными от практики. Было выявлено еще одно измерение математических понятий: степерь конструктивности, и тем самым получены неожиданные и глубокие результаты в анализа понятий.
В частности, в связи с развитием конструктивизма были осознаны математические парадигмы, мимо которых сама математика пренебрежительно прошла, но которые стали необходимы в информатике: концепция типов данных и строгой типизации, концепция взаимосвязи спецификации и построения, концепция некорректных (неконструктивных, если называть так, как называли первооткрыватели) задач и методов их превращения в корректные, возможность инкапсуляции знаний и позитивного использования незнания.
Поучительна и история конструктивизма. 0.1% математиков смело строили альтернативу общепринятой математике, достигли принципиального прорыва, но как раз к этому моменту наступление выдохлось. Сказались и малочисленность сил, и дьявольская ловушка, когда создалось впечатление возможности немедленного и прямого приложения достигнутых результатов для логического синтеза программ.
Тем самым в данном направлении накоплен значительный багаж идей, некоторые из которых уточняют и углубляют представления о фундаментальных концепциях информатики, некоторые показывают их с другой, не освещаемой в современной литературе, стороны, а некоторые до сих пор не использованы как следует.
Тематика курса
- Обзор исторического развития конструктивной математики в различных ее формах (интуиционизм, советский конструктивизм, американский конструктивизм и т.д.) с позиций современной информатики.
- Даются основные математические результаты конструктивной математики и показывается их взаимосвязь с вычислительной математикой, в частности, с теорией некорректных задач.
- Показана взаимосвязь концепций конструктивной математики с высокоуровневыми концепциями информатики и потенциал дальнейшего развития в данном направлении.
- Строятся модели различных систем конструктивной математики и показывается взаимоотношение различных концепций конструктивизма.
Программа курса
- Грязные и чистые теоремы. Проблема существования в математике. Концепция Брауэра.
- Конструктивная интуиционистская логика. Реализуемость по Колмогорову. Изоморфизм Гливенко.
- Результаты математического конструктивизма и их взаимосвязь с прикладной математикой. Принцип конечной информации. Принцип бар-индукции. Беззаконные и творческие последовательности
- Реализуемость по Клини. Советский конструктивизм. Результат Шанина о выявлении конструктивной задачи. Конструктивное и дескриптивное в построениях. Алгоритмические контрпримеры.
- Математические модели конструктивных систем. Результаты о совместимости и несовместимости различных конструктивных принципов. Теорема Трулстра (формулировка).
- Взаимосвязь конструктивной математики и информатики. Извлечение программ и анализ концепций.
- Обзор направлений дальнейших исследований.
Литература
Положение с литературой по данной тематике в мире неудовлетворительное. Имеющиеся книги рассматривают лишь какую-либо одну из конструктивных концепций и лишь с одной стороны. Взаимосвязи с информатикой вообще не освещены в доступных источниках.
- А. Гейтинг. Интуиционизм. М.: Мир, 1966.
- Р. Л. Гудстейн. Рекурсивный математический анализ. М.: Наука, 1970.
- Б. А. Кушнер. Лекции по конструктивному математическому анализу. М.: Наука, 1974.
- Справочная книга по математической логике. Т. 3. Теория рекурсий и конструктивная математика. М: Наука, 1986.
- А. А. Марков. Н. М. Нагорный. Теория алгорифмов. М.: Наука, 2004.
- А. Г. Драгалин. Математический интуиционизм и теория доказательств. М: Наука, 2006.