Рецензия на книгу "Информационные системы: категорный подход"

В. Э. Вольфенгаген
Заведующий кафедрой ПКИ и ИТ Института "ЮрИнфоР-МГУ", докт. техн. наук, проф.

Косиков С. В. Информационные системы: категорный подход / Под ред. Л. Ю. Исмаиловой. - М.: "ЮрИнфоР^®-Пресс", 2005. - 96 с. ISBN 5-9587-0005-7.

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

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

Хорошо известно, что именно ламбда-исчисление в бестиповом варианте дает основную модель вычислений. Когда для бестипового ламбда-исчисления впервые была построена модель, то это был впечатляющий результат. Для этих целей была использована решетка D_∞, для которой выполнялось равенство D_∞ = D_∞ -> D_∞, которое давало возможность по-новому взглянуть на связь и соотношение типовых и бестиповых теорий. Тут появился целый пласт работ, в которых обсуждались различные аспекты и применения, да и кого из работавших в области компьютерных наук в 1970-х-1980-х гг. это не затронуло?

Но со второй половины 1980-х гг. заметное влияние на специалистов стали оказывать категории и в особенности одна из них - декартово-замкнутая категория, или д. з. к., - стала притягательной для теоретиков компьютерных наук. Оказалось, что д. з. к. обеспечивает удобную семантическую теорию вычислений, то есть модель вычисления значения выражения. Для этой модели вычислений был введен специальный термин - категориальная абстрактная машина, или КАМ. Именно КАМ позволила на новом технологическом уровне взглянуть на связи ламбда-исчисления, конструкций языка программирования, среды вычислений через такой замечательный инструмент, которым показала себя д. з. к. Было стимулировано развитие языков программирования семейства ML, и среди них оказался язык CAML - Categorical Abstract Machine Language, - язык КАМ. Все это породило новые взгляды на обучение студентов программированию, поскольку теперь во второй раз математическая теория (д. з. к.) совпала с языком программирования (CAML). В первый раз это случилось, когда ламбда-исчисление "почти" совпало с языком обработки списков LISP. Справедливости ради надо отметить, что, по сути, ламбда-исчисление фигурирует в обоих случаях.

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