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

18.12.2020

Декартово замкнутая категория — категория, допускающая каррирование, то есть содержащая для каждого класса морфизмов A → B {displaystyle A o B} некоторый объект A ⇒ B {displaystyle ARightarrow B} , представляющий его. Декартово замкнутые категории занимают в некотором смысле промежуточное положение между абстрактными категориями и множествами, так как позволяют корректно оперировать с функциями, но не позволяют, к примеру, оперировать с подобъектами.

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

Определение

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

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

Категория, такая, что для любого её объекта категория объектов над ним декартово замкнута, называется локально декартово замкнутой.

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

  • Категория множеств естественным образом представляет собой декартово замкнутую категорию, так как функции из одного множества в другое являются множеством, и, следовательно, объектом. Также в ней существуют произведения (декартовы произведения) и терминальные объекты — синглетоны.
  • Категория Cat всех малых категорий (и функторов в качестве морфизмов) декартово замкнута; экспоненциал CD — это категория функторов из D в C с естественными преобразованиями в качестве морфизмов. Также существует категория произведения и терминальный объект — категория 1 из одного объекта и одного морфизма.
  • Элементарный топос является декартово замкнутой категорией по определению.
  • Алгебра Гейтинга (англ. Heyting algebra) также является стандартным примером декартово замкнутой категории. Так как булева алгебра является её частным случаем, она тоже всегда декартово замкнута.

Применение

В декартово замкнутой категории «функция двух переменных» (морфизм f:X×YZ) всегда может быть представлена как «функция одной переменной» (морфизм λf:XZY). В программировании эта операция известна как каррирование; это позволяет интерпретировать просто типизированное лямбда-исчисление в любой декартово замкнутой категории. Декартово замкнутые категории служат категорной моделью для типизированного λ {displaystyle lambda } -исчислении и комбинаторной логики.

Соответствие Карри — Ховарда предоставляет изоморфизм между интуиционистской логикой, просто типизированным лямбда-исчислением и декартово замкнутыми категориями. Определённые декартово замкнутые категории (топосы) предлагались как основные объекты альтернативных оснований математики вместо традиционной теории множеств.



Имя:*
E-Mail:
Комментарий: