Kartézská uzavřená kategorie

Kartézská uzavřená kategorie  je kategorie , která připouští currying , tj. obsahuje pro každou třídu morfismů nějaký objekt , který ji reprezentuje. Kartézské uzavřené kategorie zaujímají v jistém smyslu mezistupeň mezi abstraktními kategoriemi a množinami , protože umožňují správně pracovat s funkcemi , ale neumožňují například operovat s podobjekty.

Z hlediska programování kartézské uzavřené kategorie implementují zapouzdření argumentů funkcí – každý argument je reprezentován objektem kategorie a je použit jako černá skříňka . Zároveň je expresivita kartézských uzavřených kategorií dostačující k tomu, aby fungovaly s funkcemi způsobem přijatým v λ-kalkulu . To z nich dělá přirozené kategorické modely typovaného λ-kalkulu .

Definice

Kategorie C se nazývá kartézská uzavřená [1] , pokud splňuje tři podmínky:

• C má terminálový objekt ;
• libovolné dva objekty X , Y v C mají součin X × Y ;
• libovolné dva objekty Y , Z v C mají exponenciální Z Y.

Kategorie taková, že pro kterýkoli z jejích objektů je kategorie objektů nad ní kartézsky uzavřená, se nazývá lokálně kartézská uzavřená .

Příklady kartézských uzavřených kategorií

• Kategorie množin je přirozeně kartézskou uzavřenou kategorií, protože funkce z jedné množiny do druhé jsou množinou, a tedy objektem. Dále obsahuje součiny ( kartézské součiny ) a koncové objekty - singletony .

• Kategorie Cat všech malých kategorií (a funktorů jako morfismů) je kartézsky uzavřená; exponenciála C D  je kategorie funktorů od D do C s přirozenými transformacemi jako morfismy. Dále existuje kategorie produktu a koncový objekt - kategorie 1 jednoho objektu a jednoho morfismu.

• Elementární topos je podle definice kartézská uzavřená kategorie.

• Heytingova algebra je také  standardním příkladem kartézské uzavřené kategorie. Protože booleovská algebra je jejím speciálním případem, je také vždy kartézská uzavřená.

Aplikace

V kartézské uzavřené kategorii lze „funkci dvou proměnných“ (morfismus f : X × Y → Z ) vždy reprezentovat jako „funkci jedné proměnné“ (morfismus λ f : X → Z Y ). V programování je tato operace známá jako currying ; to umožňuje jednoduše zadaný počet lambda interpretovat v jakékoli kartézské uzavřené kategorii. Kartézské uzavřené kategorie slouží jako model kategorií pro typizovaný počet a kombinatorickou logiku .

Curry-Howardova korespondence poskytuje izomorfismus mezi intuicionistickou logikou, jednoduše napsaným lambda kalkulem a karteziánskými uzavřenými kategoriemi. Určité kartézské uzavřené kategorie ( topoi ) byly navrženy jako hlavní předměty alternativních základů matematiky namísto tradiční teorie množin .

Poznámky

1. ↑ McLane S. Kapitola 4. Adjungované funktory // Kategorie pro pracujícího matematika / Per. z angličtiny. vyd. V. A. Artamonová. - M .: Fizmatlit, 2004. - S. 95-128. — 352 s. — ISBN 5-9221-0400-4 .

Literatura

• Curien P.-L. Kategorická kombinatorická logika.-- LNCS, 194, 1985, s.~139-151.
• Roy L. Crole , Kategorie pro typy, Cambridge University Press, 1994.