Categoria închisă carteziană

O categorie închisă carteziană  este o categorie care admite currying , adică conține pentru fiecare clasă de morfisme un obiect care o reprezintă. Categoriile închise carteziene ocupă, într-un fel, o poziție intermediară între categorii abstracte și mulțimi , deoarece vă permit să operați corect cu funcții , dar nu permit, de exemplu, să operați cu subobiecte.

Din punct de vedere al programării , categoriile carteziene închise implementează încapsularea argumentelor funcției - fiecare argument este reprezentat de un obiect categorie și este folosit ca o cutie neagră . În același timp, expresivitatea categoriilor închise carteziene este suficientă pentru a opera cu funcții în maniera adoptată în calculul λ . Acest lucru le face modele categorice naturale ale calculului λ tipizat .

Definiție

O categorie C se numește carteziană închisă [1] dacă îndeplinește trei condiții:

• C are un obiect terminal ;
• oricare două obiecte X , Y din C au produsul X × Y ;
• oricare două obiecte Y , Z din C au exponenţial Z Y .

O categorie astfel încât pentru oricare dintre obiectele sale categoria de obiecte de peste el este carteziană închisă se numește local carteziană închisă .

Exemple de categorii carteziene închise

• Categoria mulțimilor este în mod natural o categorie carteziană închisă, deoarece funcțiile de la o mulțime la alta sunt o mulțime și, prin urmare, un obiect. Conține, de asemenea, produse (produse carteziene ) și obiecte terminale - singletons .

• Categoria Cat din toate categoriile mici (și functorii ca morfisme) este carteziană închisă; exponenţialul C D  este categoria functorilor de la D la C cu transformări naturale ca morfisme. Există, de asemenea, o categorie de produse și un obiect terminal - categoria 1 a unui obiect și un morfism.

• Un topos elementar este o categorie închisă carteziană prin definiție.

• Algebra Heyting este , de asemenea, un  exemplu standard de categorie închisă carteziană. Deoarece algebra booleană este un caz special al acesteia, este întotdeauna închisă carteziană.

Aplicație

Într-o categorie închisă carteziană, o „funcție a două variabile” (morfismul f : X × Y → Z ) poate fi întotdeauna reprezentată ca o „funcție a unei variabile” (morfismul λ f : X → Z Y ). În programare, această operație este cunoscută sub numele de curry ; aceasta permite ca calculul lambda tip simplu să fie interpretat în orice categorie închisă carteziană. Categoriile carteziene închise servesc ca model de categorie pentru calculul tipizat și logica combinatorie .

Corespondența Curry-Howard oferă un izomorfism între logica intuiționistă, calculul lambda tip simplu și categoriile închise carteziene. Anumite categorii carteziene închise ( topoi ) au fost propuse ca obiecte principale ale fundamentelor alternative ale matematicii în locul teoriei tradiționale a mulțimilor .

Note

1. ↑ McLane S. Capitolul 4. Functori adjuncți // Categorii pentru matematicianul de lucru / Per. din engleza. ed. V. A. Artamonova. - M . : Fizmatlit, 2004. - S. 95-128. — 352 p. — ISBN 5-9221-0400-4 .

Literatură

• Curien P.-L. Logica combinatorie categorica.-- LNCS, 194, 1985, pp.~139-151.
• Roy L. Crole , Categorii pentru tipuri, Cambridge University Press, 1994.