Karteesinen suljettu luokka

Karteesinen suljettu luokka on luokka , joka sallii curryingin , ts. sisältää kullekin morfismiluokalle jonkin sitä edustavan objektin . Karteesiset suljetut kategoriat ovat tietyssä mielessä väliasemassa abstraktien luokkien ja joukkojen välillä , koska ne mahdollistavat oikean käytön funktioiden kanssa , mutta eivät esimerkiksi aliobjektien kanssa. $A:sta B:hen$ $A\Nuoli oikealle B$

Ohjelmoinnin näkökulmasta karteesiset suljetut luokat toteuttavat funktion argumenttien kapseloinnin - jokaista argumenttia edustaa luokkaobjekti ja sitä käytetään mustana laatikkona . Samalla karteesisten suljettujen kategorioiden ilmeisyys riittää toimimaan funktioiden kanssa λ-laskennassa omaksutulla tavalla . Tämä tekee niistä luonnollisia kategoriallisia malleja tyypitetystä λ-laskusta .

Määritelmä

Luokkaa C kutsutaan karteesiseksi suljetuksi [1] , jos se täyttää kolme ehtoa:

C : llä on pääteobjekti ;
kahdella C : n objektilla X , Y on tulo X × Y ;
kahdella C : n objektilla Y , Z on eksponentiaalinen Z Y .

Sellaista luokkaa, jonka minkä tahansa objektin objektiluokka on suorakulmainen suljettu, kutsutaan paikallisesti karteesiseksi suljetuksi .

Esimerkkejä karteesisista suljetuista luokista

Joukkojen luokka on luonnollisesti karteesinen suljettu luokka, koska joukosta toiseen tulevat funktiot ovat joukko ja siten objekti. Se sisältää myös tuotteita ( suorakulmaisia tuotteita ) ja pääteobjekteja - singletoneja .

Kaikkien pienten kategorioiden (ja funktionaalisten funktioiden morfismeina) luokka Cat on suorakulmainen suljettu; eksponentiaalinen C D on funktioiden luokka D :stä C : hen , joissa luonnolliset muunnokset ovat morfismeja. Siellä on myös tuoteluokka ja pääteobjekti - yhden objektin ja yhden morfismin luokka 1 .

Alkeistopos on määritelmän mukaan karteesinen suljettu luokka.

Heyting - algebra on myös vakioesimerkki karteesisesta suljetusta kategoriasta. Koska Boolen algebra on sen erikoistapaus, se on myös aina karteesinen suljettu.

Sovellus

Karteesisessa suljetussa kategoriassa "kahden muuttujan funktio" (morfismi f : X × Y → Z ) voidaan aina esittää "yhden muuttujan funktiona" (morfismi λ f : X → Z Y ). Ohjelmoinnissa tämä operaatio tunnetaan nimellä currying ; tämä mahdollistaa yksinkertaisesti kirjoitetun lambda -laskennan tulkinnan missä tahansa karteesisessa suljetussa kategoriassa. Karteesiset suljetut kategoriat toimivat tyyppimallin ja kombinatorisen logiikan luokkamallina . $\lambda$

Curry-Howard-kirjeenvaihto tarjoaa isomorfismin intuitionistisen logiikan, yksinkertaisesti kirjoitetun lambda-laskennan ja karteesisten suljettujen kategorioiden välillä. Matematiikan vaihtoehtoisten perusteiden pääkohteiksi on ehdotettu tiettyjä karteesisia suljettuja kategorioita ( topoi ) perinteisen joukkoteorian sijaan .

Muistiinpanot

↑ McLane S. Luku 4. Liitäntäfunktiot // Kategoriat työskentelevälle matemaatikolle / Per. englannista. toim. V. A. Artamonova. - M . : Fizmatlit, 2004. - S. 95-128. — 352 s. — ISBN 5-9221-0400-4 .

Kirjallisuus

Curien P.-L. Kategorinen kombinatorinen logiikka. - LNCS, 194, 1985, s. ~139-151.
Roy L. Crole , Categories for Types, Cambridge University Press, 1994.