Введение
Тип категории в теории категорий. В теории категорий категория называется картезиански замкнутой, если, грубо говоря, любой морфизм, определённый на произведении двух объектов, может быть естественным образом отождествлён с морфизмом, определённым на одном из сомножителей. Эти категории особенно важны в математической логике и теории программирования, так как их внутренним языком является просто типизированное лямбда-исчисление. Они обобщаются замкнутыми моноидальными категориями, внутренний язык которых – системы линейных типов – подходят как для квантовых, так и для классических вычислений.
In category theory, a category is Cartesian closed if, roughly speaking, any morphism defined on a product of two objects can be naturally identified with a morphism defined on one of the factors. These categories are particularly important in mathematical logic and the theory of programming, in that their internal language is the simply typed lambda calculus. They are generalized by closed monoidal categories, whose internal language, linear type systems, are suitable for both quantum and classical computation.
Этимология
Названа в честь Рене Декарта (1596–1650), французского философа, математика и ученого, чья разработка аналитической геометрии привела к возникновению понятия декартова произведения, которое впоследствии было обобщено до понятия категориального произведения.
Приложения
В картезианских замкнутых категориях "функция двух переменных" (морфизм f: X×Y → Z) всегда может быть представлена как "функция одной переменной" (морфизм λf: X → ZY). В информатике это известно как каррирование; это привело к осознанию того, что просто типизированное лямбда-исчисление может быть интерпретировано в любой картезианской замкнутой категории. Соответствие Карри — Ховарда — Ламбека обеспечивает глубокий изоморфизм между интуиционистской логикой, просто типизированным лямбда-исчислением и картезианскими замкнутыми категориями. Определенные картезианские замкнутые категории, топосы, были предложены в качестве общей основы для математики, вместо традиционной теории множеств. Компьютерный ученый Джон Бэкус выступал за нотацию, свободную от переменных, или программирование на уровне функций, которое, в ретроспективе, имеет некоторое сходство с внутренним языком картезианских замкнутых категорий. CAML более осознанно моделируется на основе картезианских замкнутых категорий.
Зависимая сумма и произведение
Пусть C — локально декартово замкнутая категория. Тогда C имеет все обратные пределы, поскольку обратный предел двух морфизмов с кообластью Z задается произведением в C/Z. Для каждого морфизма p : X → Y пусть P обозначает соответствующий объект в C/Y. Взятие обратных пределов вдоль p задает функтор p* : C/Y → C/X, который имеет как левый, так и правый сопряженный функтор. Левый сопряженный функтор называется зависимой суммой и задается композицией. Правый сопряженный функтор называется зависимым произведением. Экспонента по P в C/Y может быть выражена через зависимое произведение по формуле. Причина этих названий заключается в том, что при интерпретации P как зависимого типа, функторы и соответствуют формированию типов и соответственно.
The right adjoint is called the dependent product. The exponential by P in C/Y can be expressed in terms of the dependent product by the formula
The reason for these names is because, when interpreting P as a dependent type , the functors and correspond to the type formations and respectively.