Interested Article - Декартово замкнутая категория
- 2021-11-19
- 1
Декартово замкнутая категория — категория , допускающая каррирование , то есть содержащая для каждого класса морфизмов некоторый объект , представляющий его. Декартово замкнутые категории занимают в некотором смысле промежуточное положение между абстрактными категориями и множествами , так как позволяют корректно оперировать с функциями , но не позволяют, к примеру, оперировать с подобъектами.
С точки зрения программирования декартово замкнутые категории реализуют инкапсуляцию аргументов функций — каждый аргумент представляется объектом категории и используется как чёрный ящик . Вместе с тем выразительности декартово замкнутых категорий вполне достаточно, чтобы оперировать с функциями способом, принятым в λ-исчислении . Это делает их естественными категорными моделями типизированного λ-исчисления .
Определение
Категория C называется декартово замкнутой , если она удовлетворяет трём условиям:
- в C имеется терминальный объект ;
- любые два объекта X , Y в C имеют произведение X × Y ;
- любые два объекта Y , Z в C имеют экспоненциал Z Y .
Категория, такая, что для любого её объекта категория объектов над ним декартово замкнута, называется локально декартово замкнутой .
Примеры декартово замкнутых категорий
- Категория множеств естественным образом представляет собой декартово замкнутую категорию, так как функции из одного множества в другое являются множеством, и, следовательно, объектом. Также в ней существуют произведения ( декартовы произведения ) и терминальные объекты — синглетоны .
- Категория Cat всех малых категорий (и функторов в качестве морфизмов) декартово замкнута; экспоненциал C D — это категория функторов из D в C с естественными преобразованиями в качестве морфизмов. Также существует категория произведения и терминальный объект — категория 1 из одного объекта и одного морфизма.
- Элементарный топос является декартово замкнутой категорией по определению.
- ( англ. ) также является стандартным примером декартово замкнутой категории. Так как булева алгебра является её частным случаем, она тоже всегда декартово замкнута.
Применение
В декартово замкнутой категории «функция двух переменных» (морфизм f : X × Y → Z ) всегда может быть представлена как «функция одной переменной» (морфизм λ f : X → Z Y ). В программировании эта операция известна как каррирование ; это позволяет интерпретировать просто типизированное лямбда-исчисление в любой декартово замкнутой категории. Декартово замкнутые категории служат категорной моделью для типизированного -исчисления и комбинаторной логики .
Соответствие Карри — Ховарда предоставляет изоморфизм между интуиционистской логикой, просто типизированным лямбда-исчислением и декартово замкнутыми категориями. Определённые декартово замкнутые категории ( топосы ) предлагались как основные объекты альтернативных оснований математики вместо традиционной теории множеств .
Примечания
- Маклейн С. Глава 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.
- 2021-11-19
- 1