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 .
En kategori C kallas kartesisk stängd [1] om den uppfyller tre villkor:
En kategori så att för något av dess objekt kategorin objekt över den är kartesisk stängd kallas lokalt kartesisk stängd .
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 .