Декартово-замкнутая категория

В теории категорий декартово замкнутой называется категория, допускающая интернализацию понятия морфизма. Другими словами, каждому морфизму $A\to B$ в ней соответствует некоторый объект $A\Rightarrow B$, представляющий его. Декартово замкнутые категории, находятся, в известном смысле, между абстрактными категориями и теорией множеств, так как позволяют корректно оперировать с функциями, но не позволяют, к примеру, оперировать с подобъектами.

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

Определение

Категория C называется декартово замкнутой, если она удовлетворяет трём условиям:

• в C имеется терминальный объект;
• любые два объекта X, Y в C имеют произведение X × Y;
• любые два объекта Y, Z в C имеют экспоненциал Z^Y.

Примеры декартово замкнутых категорий

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

Топос, является декартово замкнутой категорией по определению.

Алгебра Гейтинга также является стандартным примером декартово замкнутой категории. Так как Булева алгебра является её частным случаем она тоже всегда будет декартово замкнутой.

Применение

Декартово замкнутые категории служат категорной моделью для типизированного λ-исчислении и комбинаторной логики.

См. также

• Комбинаторная логика
• Лямбда-исчисление с типами
• Категориальная абстрактная машина

Литература

• Curien P.-L. Categorical combinatory logic.-- LNCS, 194, 1985, pp.~139-151.
• Roy L. Crole, Categories for Types, Cambridge University Press, 1994.

Ссылки