Курс лекций Николая Николаевича Непейводы «Конструктивная математика и ее применения» для магистров факультета ВМК и философского факультета в марте 2010 года

Лекции Николая Николаевича Непейводы имеют отдалённое отношение к тематике семинара, но, ввиду отсутствия прочих информационных ресурсов и заинтересованности отдельных участников семинара в них, информация о них помещена здесь.

• Курс предназначен для магистров и бакалавров 3-4 года обучения.
• Курс предполагает прохождение стандартного курса математики (алгебра, начала топологии, анализ, начала теории алгоритмов) и начального курса логики (прежде всего, умение корректно записывать и читать логические формулы), а также знакомство с высокоуровневыми концепциями современной информатики (языки спецификаций, альтернативные стили программирования).
• Курс рассчитан на 16 час. лекций и 16 час. практики.
• Отчетность: домашняя контрольная работа (теоретическая), программная модель простейших конструктивных конструкций, зачет по окончанию курса.

Лекции проходят в течение марта по следующему расписанию:

• По пятницам в 18:00 в аудитории 523 2-го учебного корпуса МГУ проводятся дополнительные лекции для магистров ВМК.

• По субботам с 10:40 до 16:10 в аудитории Е331 нового первого учебного корпуса проводятся лекции для магистров ВМК и философского факультета.

Аннотация

Конструктивизм (понимаемый здесь в широком смысле слова, как совокупность течений от интуционизма до советского конструктивизма) явился интереснейшим математическим экспериментом ХХ века. Впервые была точно показана возможность рациональной альтернативы общепринятому рационализму. который претендовал на монополию в области научного подхода. Точно так же впервые была показана неразрывная связь в математике идеальных и реальных объектов, являющаяся источником «непостижимой эффективности математики в приложениях», причем как раз тех ее разделов, которые на первый взгляд кажутся наиболее оторванными от практики. Было выявлено еще одно измерение математических понятий: степерь конструктивности, и тем самым получены неожиданные и глубокие результаты в анализа понятий.

В частности, в связи с развитием конструктивизма были осознаны математические парадигмы, мимо которых сама математика пренебрежительно прошла, но которые стали необходимы в информатике: концепция типов данных и строгой типизации, концепция взаимосвязи спецификации и построения, концепция некорректных (неконструктивных, если называть так, как называли первооткрыватели) задач и методов их превращения в корректные, возможность инкапсуляции знаний и позитивного использования незнания.

Поучительна и история конструктивизма. 0.1% математиков смело строили альтернативу общепринятой математике, достигли принципиального прорыва, но как раз к этому моменту наступление выдохлось. Сказались и малочисленность сил, и дьявольская ловушка, когда создалось впечатление возможности немедленного и прямого приложения достигнутых результатов для логического синтеза программ.

Тем самым в данном направлении накоплен значительный багаж идей, некоторые из которых уточняют и углубляют представления о фундаментальных концепциях информатики, некоторые показывают их с другой, не освещаемой в современной литературе, стороны, а некоторые до сих пор не использованы как следует.

Тематика курса

1. Обзор исторического развития конструктивной математики в различных ее формах (интуиционизм, советский конструктивизм, американский конструктивизм и т.д.) с позиций современной информатики.
2. Даются основные математические результаты конструктивной математики и показывается их взаимосвязь с вычислительной математикой, в частности, с теорией некорректных задач.
3. Показана взаимосвязь концепций конструктивной математики с высокоуровневыми концепциями информатики и потенциал дальнейшего развития в данном направлении.
4. Строятся модели различных систем конструктивной математики и показывается взаимоотношение различных концепций конструктивизма.

Программа курса

1. Грязные и чистые теоремы. Проблема существования в математике. Концепция Брауэра.
2. Конструктивная интуиционистская логика. Реализуемость по Колмогорову. Изоморфизм Гливенко.
3. Результаты математического конструктивизма и их взаимосвязь с прикладной математикой. Принцип конечной информации. Принцип бар-индукции. Беззаконные и творческие последовательности
4. Реализуемость по Клини. Советский конструктивизм. Результат Шанина о выявлении конструктивной задачи. Конструктивное и дескриптивное в построениях. Алгоритмические контрпримеры.
5. Математические модели конструктивных систем. Результаты о совместимости и несовместимости различных конструктивных принципов. Теорема Трулстра (формулировка).
6. Взаимосвязь конструктивной математики и информатики. Извлечение программ и анализ концепций.
7. Обзор направлений дальнейших исследований.

Литература

Положение с литературой по данной тематике в мире неудовлетворительное. Имеющиеся книги рассматривают лишь какую-либо одну из конструктивных концепций и лишь с одной стороны. Взаимосвязи с информатикой вообще не освещены в доступных источниках.

1. А. Гейтинг. Интуиционизм. М.: Мир, 1966.
2. Р. Л. Гудстейн. Рекурсивный математический анализ. М.: Наука, 1970.
3. Б. А. Кушнер. Лекции по конструктивному математическому анализу. М.: Наука, 1974.
4. Справочная книга по математической логике. Т. 3. Теория рекурсий и конструктивная математика. М: Наука, 1986.
5. А. А. Марков. Н. М. Нагорный. Теория алгорифмов. М.: Наука, 2004.
6. А. Г. Драгалин. Математический интуиционизм и теория доказательств. М: Наука, 2006.

Материалы