Kartesisk sluten kategori
En kartesisk sluten kategori är en kategori som tillåter currying , d.v.s. innehåller för varje klass av morfismer något objekt som representerar den. Kartesiska slutna kategorier upptar på sätt och vis en mellanposition mellan abstrakta kategorier och uppsättningar , eftersom de tillåter dig att korrekt arbeta med funktioner , men inte tillåter till exempel att arbeta med subobjekt.
Ur programmeringssynpunkt implementerar kartesiska slutna kategorier inkapsling av funktionsargument - varje argument representeras av ett kategoriobjekt och används som en svart låda . Samtidigt är uttrycksförmågan hos kartesiska slutna kategorier tillräckligt för att arbeta med funktioner på det sätt som antagits i λ-kalkylen . Detta gör dem till naturliga kategoriska modeller av den typade λ-kalkylen .
Definition
En kategori C kallas kartesisk stängd [1] om den uppfyller tre villkor:
- C har ett terminalobjekt ;
- alla två objekt X , Y i C har produkten X × Y ;
- vilka två objekt som helst Y , Z i C har exponentiell Z Y .
En kategori så att för något av dess objekt kategorin objekt över den är kartesisk stängd kallas lokalt kartesisk stängd .
Exempel på kartesiska stängda kategorier
- Kategorin av mängder är naturligtvis en kartesisk sluten kategori, eftersom funktioner från en mängd till en annan är en mängd, och därmed ett objekt. Den innehåller också produkter ( kartesiska produkter ) och terminalobjekt- singlar .
- Kategorin Cat av alla små kategorier (och fungerar som morfismer) är kartesisk sluten; den exponentiella C D är kategorin av funktioner från D till C med naturliga transformationer som morfismer. Det finns också en produktkategori och ett terminalobjekt - kategori 1 av ett objekt och en morfism.
- En elementär topos är per definition en kartesisk sluten kategori.
- Heyting- algebra är också ett standardexempel på en kartesisk sluten kategori. Eftersom boolesk algebra är ett specialfall av det är den också alltid kartesisk stängd.
Applikation
I en kartesisk sluten kategori kan en "funktion av två variabler" (morfism f : X × Y → Z ) alltid representeras som en "funktion av en variabel" (morfism λ f : X → Z Y ). Vid programmering är denna operation känd som currying ; detta gör att den enkelt skrivna lambdakalkylen kan tolkas i vilken kartesisk sluten kategori som helst. Kartesiska slutna kategorier fungerar som en kategorimodell för maskinskriven kalkyl och kombinatorisk logik .
Curry-Howard-korrespondensen ger en isomorfism mellan intuitionistisk logik, den enkelt skrivna lambdakalkylen och kartesiska slutna kategorier. Vissa kartesiska slutna kategorier ( topoi ) har föreslagits som huvudobjekten för alternativa grunder för matematik istället för traditionell mängdteori .
Anteckningar
- ↑ McLane S. Kapitel 4. Adjoint functors // Kategorier för den arbetande matematikern / Per. från engelska. ed. V. A. Artamonova. - M . : Fizmatlit, 2004. - S. 95-128. — 352 sid. — 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.