Cartesisk lukket kategori
En kartesisk lukket kategori er en kategori , der tillader currying , dvs. indeholder for hver klasse af morfismer et eller andet objekt, der repræsenterer det. Kartesiske lukkede kategorier indtager på en måde en mellemposition mellem abstrakte kategorier og mængder , da de giver dig mulighed for korrekt at operere med funktioner , men ikke tillader for eksempel at operere med subobjekter.
Fra et programmeringssynspunkt implementerer kartesiske lukkede kategorier indkapsling af funktionsargumenter - hvert argument er repræsenteret af et kategoriobjekt og bruges som en sort boks . Samtidig er ekspressiviteten af kartesiske lukkede kategorier ganske nok til at fungere med funktioner på den måde, der er vedtaget i λ-regningen . Dette gør dem til naturlige kategoriske modeller af den typebestemte λ-regning .
Definition
En kategori C kaldes kartesisk lukket [1] , hvis den opfylder tre betingelser:
- C har et terminalobjekt ;
- to vilkårlige objekter X , Y i C har produktet X × Y ;
- to vilkårlige objekter Y , Z i C har eksponentiel Z Y .
En kategori, således at for enhver af dens objekter kategorien af objekter over den er kartesisk lukket, kaldes lokalt kartesisk lukket .
Eksempler på kartesiske lukkede kategorier
- Kategorien af mængder er naturligvis en kartesisk lukket kategori, da funktioner fra et sæt til et andet er et sæt og dermed et objekt. Den indeholder også produkter ( kartesiske produkter ) og terminalobjekter - singletons .
- Kategorien Kat af alle små kategorier (og fungerer som morfismer) er kartesisk lukket; den eksponentielle C D er kategorien af funktorer fra D til C med naturlige transformationer som morfismer. Der er også en produktkategori og et terminalobjekt - kategori 1 af et objekt og en morfisme.
- En elementær topos er per definition en kartesisk lukket kategori.
- Heyting- algebraen er også et standardeksempel på en kartesisk lukket kategori. Da boolsk algebra er et specialtilfælde af det, er den også altid kartesisk lukket.
Ansøgning
I en kartesisk lukket kategori kan en "funktion af to variable" (morfi f : X × Y → Z ) altid repræsenteres som en "funktion af en variabel" (morfi λ f : X → Z Y ). I programmering er denne operation kendt som currying ; dette gør det muligt at fortolke den enkelt indtastede lambdaregning i enhver kartesisk lukket kategori. Cartesiske lukkede kategorier tjener som en kategorimodel for maskinskrevet calculus og kombinatorisk logik .
Curry-Howard-korrespondancen giver en isomorfisme mellem intuitionistisk logik, den enkelt indtastede lambdaregning og kartesiske lukkede kategorier. Visse kartesiske lukkede kategorier ( topoi ) er blevet foreslået som hovedobjekterne for alternative grundlag for matematik i stedet for traditionel mængdeteori .
Noter
- ↑ McLane S. Kapitel 4. Adjoint functors // Kategorier for den arbejdende matematiker / Pr. fra engelsk. udg. V. A. Artamonova. - M . : Fizmatlit, 2004. - S. 95-128. — 352 s. — ISBN 5-9221-0400-4 .
Litteratur
- Curien P.-L. Kategorisk kombinatorisk logik.-- LNCS, 194, 1985, s.~139-151.
- Roy L. Crole , Categories for Types, Cambridge University Press, 1994.