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

Материал из Википедии — свободной энциклопедии
Перейти к: навигация, поиск

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

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

Определение[править | править вики-текст]

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

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

Примеры декартово замкнутых категорий[править | править вики-текст]

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

Применение[править | править вики-текст]

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

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

Примечания[править | править вики-текст]

  1. Маклейн С. Глава 4. Сопряжённые функторы // Категории для работающего математика = Categories for the working mathematician / Пер. с англ. под ред. В. А. Артамонова. — М.: Физматлит, 2004. — С. 95—128. — 352 с. — ISBN 5-9221-0400-4.

Литература[править | править вики-текст]

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