Реферат: Теория категорий в преподавании оснований математики для информатиков

Теория категорий в преподавании оснований математики для информатиков Непейвода А.Н., Удмуртский государственный университет
Традиционно в ВУЗе в начале курса математической логики преподаётся теория множеств как основание современной математики. Однако этот подход для программистских специальностей ныне можно считать устаревшим, поскольку теория множеств не соответствует требованиям строгости, выдвигаемым современной информатикой [1]. Например, функция в теории множеств определяется как множество упорядоченных пар. Однако такое определение функции не учитывает его области определения и делает возможным композицию функций, имеющих не соответствующие области определения и значения. Главной проблемой, порождающей такие помарки, на наш взгляд, является совершенная неконструктивность теории множеств: как и классическая логика, она дескриптивна и описывает свойства объектов, а не построений. Излишние упражнения в теории множеств приводят к привычке неаккуратно пользоваться определениями (весьма размытыми в рамках этой теории).

Возникает вопрос, как же преподнести студентам основания математики в более подходящем русле для информатики. Самой яркой альтернативой теории множеств в решении данного вопроса может выступать теория категорий [2]. В противоположность теории множеств, теория категорий рассматривает прежде всего не объекты, а их преобразования (морфизмы). Чтобы объекты и их преобразования образовывали категорию, необходимо существование тождественного преобразования для каждого объекта, и композиции. Подробно это раскрывается в [2,3,4].

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

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

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


Литература


1. Непейвода Н.Н. «Прикладная логика», Новосибирск, 2000.

2. Маклейн С. «Категории для работающего математика», М.: Физматлит, 2004.

3. Mitchell J.C. «Foundations for programming languages». MIT Press, 1996

4. Goguen J. A. «A categorical manifesto», Oxford.