Русская Википедия:Декартово замкнутая категория
Декартово замкнутая категория — категория, допускающая каррирование, то есть содержащая для каждого класса морфизмов <math>A\to B</math> некоторый объект <math>A\Rightarrow B</math>, представляющий его. Декартово замкнутые категории занимают в некотором смысле промежуточное положение между абстрактными категориями и множествами, так как позволяют корректно оперировать с функциями, но не позволяют, к примеру, оперировать с подобъектами.
С точки зрения программирования декартово замкнутые категории реализуют инкапсуляцию аргументов функций — каждый аргумент представляется объектом категории и используется как чёрный ящик. Вместе с тем выразительности декартово замкнутых категорий вполне достаточно, чтобы оперировать с функциями способом, принятым в λ-исчислении. Это делает их естественными категорными моделями типизированного λ-исчисления.
Определение
Категория Шаблон:Math называется декартово замкнутой[1], если она удовлетворяет трём условиям:
- в Шаблон:Math имеется терминальный объект;
- любые два объекта Шаблон:Math, Шаблон:Math в Шаблон:Math имеют произведение Шаблон:Math;
- любые два объекта Шаблон:Math, Шаблон:Math в Шаблон:Math имеют экспоненциал Шаблон:Math.
Категория, такая, что для любого её объекта категория объектов над ним декартово замкнута, называется локально декартово замкнутой.
Примеры декартово замкнутых категорий
- Категория множеств естественным образом представляет собой декартово замкнутую категорию, так как функции из одного множества в другое являются множеством, и, следовательно, объектом. Также в ней существуют произведения (декартовы произведения) и терминальные объекты — синглетоны.
- Категория Шаблон:Math всех малых категорий (и функторов в качестве морфизмов) декартово замкнута; экспоненциал Шаблон:Math — это категория функторов из Шаблон:Math в Шаблон:Math с естественными преобразованиями в качестве морфизмов. Также существует категория произведения и терминальный объект — категория Шаблон:Math из одного объекта и одного морфизма.
- Элементарный топос является декартово замкнутой категорией по определению.
- Шаблон:Нп2 также является стандартным примером декартово замкнутой категории. Так как булева алгебра является её частным случаем, она тоже всегда декартово замкнута.
Применение
В декартово замкнутой категории «функция двух переменных» (морфизм Шаблон:Math) всегда может быть представлена как «функция одной переменной» (морфизм Шаблон:Math). В программировании эта операция известна как каррирование; это позволяет интерпретировать просто типизированное лямбда-исчисление в любой декартово замкнутой категории. Декартово замкнутые категории служат категорной моделью для типизированного <math>\lambda</math>-исчисления и комбинаторной логики.
Соответствие Карри — Ховарда предоставляет изоморфизм между интуиционистской логикой, просто типизированным лямбда-исчислением и декартово замкнутыми категориями. Определённые декартово замкнутые категории (топосы) предлагались как основные объекты альтернативных оснований математики вместо традиционной теории множеств.
Примечания
Литература
- Curien P.-L. Categorical combinatory logic.-- LNCS, 194, 1985, pp.~139—151.
- Roy L. Crole, Categories for Types, Cambridge University Press, 1994.
