4 Kategorie kartezja´ nsko zamkni ete

Rachunek lambda w kategoriach kartezja´ nsko zamkni etych _,

Krzysiek Kapulkin semestr letni 2009/10

1 Kategorie, funktory i naturalne transformacje

Definicja 1. Kategorie C tworz_, a klasa obiekt´_, ow ob(C) i klasa morfizm´ow mor(C), przy czym zak ladamy, ˙ze:

1. Ka˙zdy morfizm f ∈ mor(C) posiada dziedzine dom(f ) ∈ ob(C) oraz prze-_, ciwdziedzine cod(f ) ∈ ob(C). Je´sli X = dom(f ), Y = cod(f ), to piszemy_, f : X ^//Y . Rodzine wszystkich morfizm´_, ow o dziedzinie X i przeciwdzie- dzinie Y oznaczamy hom_C(X, Y ). Je´sli f i g sa dwoma morfizmami takimi,_,

˙ze cod(f ) = dom(g), to istnieje morfizm h taki, ˙ze dom(h) = dom(f ) oraz cod(h) = cod(g) nazywany z lo˙zeniem h = g ◦ f :

A ^{h //}

fBBBBB!!B

BB C

B

g

|==|

||

||

||

2. Dla ka˙zdego X ∈ ob(C) istnieje morfizm identyczno´sciowy idX ∈ hom_C(X, X).

3. je´sli f : X ^//Y , to idY ◦ f = f ◦ id_X = f . 4. je´sli f : X ^//Y , g : Y ^//Z i h : Z ^//T , to

h ◦ (g ◦ f ) = (h ◦ g) ◦ f.

Przyk lady 1.

• 0 to kategoria pusta (ob(C) = mor(C) = ∅).

• 1 to kategoria z jednym obiektem ∗ i jednym morfizmem id_∗.

• 2 to kategoria z dwoma obiektami i jednym morfizmem nieidentyczno´sciowym miedzy nimi._,

• Sets to kategoria, kt´orej obiektami sa zbiory, a morfizmami funkcje._,

• Grp to kategoria, kt´orej obiektami sa grupy, a morfizmami homomorfizmy_, grup.

• Monoids to kategoria, kt´orej obiektami sa monoidy, a morfizmami homomor-_, fizmy monoid´ow.

• Powy˙zsze dwa przyk lady mo˙zna uog´olni´c: niech T – teoria r´owno´sciowa. W´ow- czas przez Alg(T) bedziemy oznacza´_, c kategorie T-algebr i ich homomorfizm´ow._,

• Niech M (odp. G) bedzie monoidem (odp. grup_, a). W´_, owczas M (odp. G) mo˙zemy traktowa´c jako kategorie z jednym obiektem ∗, w kt´_, orej morfizmami sa_, elementy monoidu (odp. grupy). Element neutralny pe lni role identyczno´_, sci, za´s mno˙zenie w monoidzie (odp. grupie) jest sk ladaniem morfizm´ow.

• Vect_k to kategoria przestrzeni liniowych nad ustalonym cia lem k, w kt´orej morfizmami sa przekszta lcenia liniowe._,

• Grph to kategoria graf´ow. Przez graf rozumiemy tu czw´orke_, (O, A, d : A ^//O, c : A ^//O),

gdzie O jest zbiorem wierzcho lk´ow, A zbiorem krawedzi, funkcja d przyporz_, ad-_, kowuje krawedzi jej dziedzin_, e, za´_, s c jej przeciwdziedzine. Morfizmem w kate-_, gorii graf´ow nazywamy takie przekszta lcenie

f : (O, A, d : A ^//O, c : A ^//O) ^//(O⁰, A⁰, d⁰: A^{0 //}O⁰, c⁰: A^{0 //}O⁰),

˙ze d⁰(f (a)) = f (d(a)) oraz c⁰(f (a)) = f (c(a)).

• Top to kategoria, kt´orej obiektami sa przestrzenie topologiczne, a morfizmami_, przekszta lcenia ciag le._,

• Zbi´or cze´_,sciowo uporzadkowany hP, ≤i mo˙zemy traktowa´_, c jako kategorie. Jej_, obiektami sa elementy P . Ponadto:_,

hom_C(p, p⁰) =

 {∗} je´sli p ≤ p⁰

∅ w przeciwnym przypadku

• Posets to kategoria, w kt´orej obiektami sa zbiory cz_, e´_,sciowo uporzadkowane,_, za´s morfizmami funkcje monotoniczne (zachowujace porz_, adek)._,

• CPO to kategoria, w kt´orej obiektami sa zupe lne porz_, adki cz_, e´_,sciowe, za´s morfizmami funkcje ciag le (w sensie Scotta)._,

• Niech C bedzie kategori_, a. Kategori_, a dualn_, a do C nazywamy kategori_, e C_, ^opzde- finiowana nast_, epuj_, aco: ob(C_, ^op) = ob(C), za´s homC^op(X, Y ) = hom_C(Y, X).

Powiemy, ˙ze kategoria C jest ma la, je´sli ob(C) i mor(C) sa zbiorami._, Przyk lady 2.

• Kategorie 0, 1 i 2 to kategorie ma le.

• Grupa G rozwa˙zana jako kategoria jest kategoria ma l_, a._,

• Zbi´or uporzadkowany hP, ≤i rozwa˙zany jako kategoria jest kategori_, a ma l_, a._, Definicja 2. Niech C i D bed_, a kategoriami. Funktorem F : C_, ^//D nazywamy pare przekszta lce´_, n przyporzadkowuj_, acych obiektom C obiekty D, a morfizmom C_, morfizmy D spe lniajac_, a warunki:_,

1. Je´sli f ∈ mor(C), to F (dom(f )) = dom(F (f )) oraz F (cod(f )) = cod(F (f )).

2. Dla ka˙zdego X ∈ ob(C) zachodzi F (idX) = id_{F (X)}.

3. Dladowolnej sk ladalnej pary morfizm´ow f, g ∈ mor(C) zachodzi F (g ◦ f ) = F (g) ◦ F (f ).

Przyk lady 3.

• U : Grp ^//Sets to funktor

”zapominania”. Grupie hG, e, ◦i przyporzadko-_, wujemy jej uniwersum G, a homomorfizmowi grup f : hG, e, ◦i ^//hG⁰, e⁰, ◦⁰i funkcje f : G_, ^//G⁰.

• U : CRng ^//Ab to funktor cze´_,sciowego zapominania z kategorii pier´scieni w kategorie grup abelowych. Pier´_, scieniowi hR, 0, +, ·i przyporzadkowujemy_, jego grupe addytywn_, a hR, 0, +i._,

• ab : Grp ^//Ab to funktor abelianizacji przyporzadkowuj_, acy grupie jej abe-_, lianizacje._,

• i : Grp ^//Monoids to w lo˙zenie kategorii grup w kategorie monoid´_, ow.

• i : Sets_{f in} ^//Sets to w lo˙zenie kategorii zbior´ow sko´nczonych w kategorie_, wszystkich zbior´ow.

• F : Sets ^//Grp to funktor przyporzadkowuj_, acy zbiorowi X grup_, e woln_, a_, na zbiorze wolnych generator´ow X. Z definicji grupy wolnej (przez w lasno´s´c uniwersalna) mamy, ˙ze w´_, owczas ka˙zda funkcja f : X ^//Y rozszerza sie je-_, dnoznacznie do homomorfizmu grup F (f ) : F (X) ^//F (Y ).

• X × (−) : Sets ^//Sets to funktor mno˙zenia kartezja´nskiego przez ustalony zbi´or X ∈ Sets. Obiektowi A ∈ Sets przyporzadkowujemy zbi´_, or X × A, za´s funkcji f : A ^//B funkcje (id_, X, f ) : X ×A ^//X ×B taka, ˙ze (id_, X, f )(x, a) = (x, f (a)).

• U : Top ^//Sets to funktor zapominania przypisujacy przestrzeni topologicz-_, nej (X, O(X)) zbi´or X, a przekszta lceniu ciag lemu f : (X, O(X))_, ^//(Y, O(Y )) funkcje f : X_, ^//Y .

• D : Sets ^//Top to funktor przyporzadkowuj_, acy zbiorowi X przestrze´_, n to- pologiczna (X, O(X)), gdzie O(X) jest topologi_, a dyskretn_, a na X tj. ka˙zdy_, zbi´or jest otwarty. W´owczas ka˙zda funkcja f : X ^//Y mo˙ze by´c traktowana jako przekszta lcenie ciag le f : (X, O(X))_, ^//(Y, O(Y )).

Funktor z kategorii C^op do kategorii D nazywamy czesto funktorem kontrawariant-_, nym z C do D. Wtedy o”zwyk lym” funktorze m´owimy, ˙ze jest kowariantny.

• P : Sets ^//Sets funktor zbioru potegowego jest funktorem kontrawariant-_, nym. Przyporzadkowuje on zbiorowi X ∈ Sets jego zbi´_, or potegowy P(X)._, Niech f : X ^//Y bedzie funkcj_, a. W´_, owczas P(f ) : P(Y ) ^//P(X) jest funk- cja przeciwobrazu, tj. dla A ∈ P(Y ) mamy: P(f )(A) = f_, ⁻¹(A).

Mo˙zemy zdefiniowa´c kategorie Cat nast_, epuj_, aco:_,

• jej obiektami bed_, a wszystkie ma le kategorie._,

• jej morfizmami b

ed, a funktory._,

Definicja 3. Niech C, D bed_, a kategoriami, za´_, s F, G : C ^//D funktorami. Natu- ralna transformacj_, a τ : F_, ^//G nazywamy rodzine morfizm´_, ow w D indeksowana_, obiektami C tj.

τ = {τ_C: F (C) ^//G(C)}_C∈ob(C)

taka, ˙ze dla dowolnego morfizmu f : C_, ^//D kwadrat F (C) ^{τC //}

F (f )



G(C)

G(f )



F (D) _τ

D

//G(D)

jest przemienny.

Przyk lady 4.

• Niech F : C ^//D bedzie funktorem. Definiujemy transformacj_, e identyczno´_, s- ciowa id_{, F}: F ^//F jako id_F = {id_{F (C)}: F (C) ^//F (C)}_C∈ob(C). Przemien- no´s´c kwadratu:

F (C) ^{idF (C)//}

F (f )



F (C)

F (f )



F (D)

id_{F (D)}//F (D) wynika bezpo´srednio z definicji kategorii.

• Niech X × (−), Y × (−) : Sets ^//Sets bed_, a funktorami mno˙zenia kartezja´_, n- skiego. W´owczas dowolna funkcja f : X ^//Y indukuje naturalna transfor-_, macje τ_, f tych funktor´ow. Mamy bowiem τf = {τA: X × A ^//Y × A}A∈Sets, gdzie τA= f × idA. Niech a : A ^//B bedzie funkcj_, a. W´_, owczas przemienno´s´c kwadratu:

X × A ^{f ×idA//}

idX×a



Y × A

idY×a



X × B _{f ×id}

B

//Y × B jest oczywista.

• Niech 1_Sets: Sets ^//Sets to funktor identyczno´sciowy, za´s P : Sets ^//Sets niech bedzie funktorem pot_, egowym. Okre´_, slamy w´owczas naturalna transfor-_, macje τ : 1_, Sets //P jako τ = {τ_X: X ^//P(X)}_X∈Sets, gdzie τX(x) = {x}.

• Niech id_Vectk, (−)^∗∗: Vectk //Vectkbed_, a odpowiednio funktorem identycz-_, no´sciowym i funktorem przyporzadkowuj_, acym przestrzeni liniowej jej drug_, a_, przestrze´n sprze˙zon_, a (tj. V_, ^∗∗ = hom(hom(V, k), k)). Okre´slamy naturalna_, transformacje ev : id_{, Vectk} ^//(−)^∗∗ jako: ev = {ev_V : V ^//V^∗∗}_{V ∈Vectk}, gdzie evV(v)(f ) = f (v) dla v ∈ V i f ∈ hom(V, k).

2 W lasno´ sci morfizm´ ow

Niech f : C ^//D bedzie morfizmem w kategorii C. Powiemy, ˙ze f jest:_,

• monomorfizmem, je´sli dla dowolnych morfizm´ow g, h : B ^//C mamy:

f ◦ g = f ◦ h ⇒ g = h;

• epimorfizmem, je´sli dla dowolnych morfizm´ow g, h : D ^//E mamy:

g ◦ f = h ◦ f ⇒ g = h;

• retrakcja, je´_, sli istnieje taki morfizm g : D ^//C, ˙ze f ◦ g = idD;

• sekcj

a, je´, sli istnieje taki morfizm g : D ^//C, ˙ze g ◦ f = id_C.

• izomorfizmem, je´sli istnieje morfizm g : D ^//C taki, ˙ze f ◦ g = id_D oraz g ◦ f = id_C.

Latwo zauwa˙zy´c, ˙ze pojecia monomorfizmu i epimorfizmu, jak r´_, ownie˙z retrakcji i sek- cji sa poj_, eciami dualnymi, tzn. monomorfizm (retrakcja) w C jest epimorfizmem_, (odp. sekcja) w C_, ^op i na odwr´ot: epimorfizm (sekcja) w C jest monomorfizmem (odp. retrakcja) w C_, ^op.

Przyk lady 5.

• Monomorfizmy w Sets to funkcje r´o˙znowarto´sciowe. Epimorfizmy w Sets to funkcje

”na”. Izomorfizmy w Sets to bijekcje.

• W og´olno´sci, morfizm, kt´ory jest mono i epimorfizmem, nie musi by´c izo- morfizmem. Jako przyk lad mo˙zemy wzia´_,c w lo˙zenie i : N ^//Z w kategorii Monoids.

3 Konstrukcje w kategoriach

Niech C bedzie kategori_, a. Obiekt 1 ∈ C (0 ∈ C) nazywamy obiektem ko´_, ncowym (odp. obiektem poczatkowym), je´_, sli dla ka˙zdego obiektu C ∈ C istnieje dok ladnie jeden morfizm ! : C ^//1 (odp. ! : 0 ^//C).

Latwo zauwa˙zy´c, ˙ze obiekt ko´ncowy (poczatkowy), je´_, sli istnieje, to jest wyzna- czony jednoznacznie z dok ladno´scia do izomorfizmu. Mianowicie, przypu´_, s´cmy, ˙ze X i Y sa dwoma obiektami ko´_, ncowymi (poczatkowymi) w C. W´owczas istnieje_, dok ladnie jeden morfizm f : X ^//Y oraz dok ladnie jeden morfizm g : Y ^//X.

Oczywi´scie, f ◦ g = idY oraz g ◦ f = idX, stad X i Y s_, a izomorficzne._,

Mo˙zna te˙z zauwa˙zy´c, ˙ze obiekt ko´ncowy w C jest obiektem poczatkowym w C_, ^op i na odwr´ot: obiekt poczatkowy w C jest obiektem ko´_, ncowym w C^op.

Przyk lady 6.

• Obiektem poczatkowym w kategorii zbior´_, ow Sets jest zbi´or pusty ∅. Obiektem ko´ncowym w Sets jest dowolny singleton {∗}.

• Obiektem poczatkowym i ko´_, ncowym w kategorii grup Grp jest grupa jedno- elementowa {∗}.

• W kategorii cia l Fields nie istnieje obiekt ko´ncowy. Wynika to bezpo´srednio z faktu, ˙ze w´sr´od aksomat´ow cia la zak ladamy: 0 6= 1. W kategorii tej nie istnieje r´ownie˙z obiekt poczatkowy, bowiem cia la mog_, a mie´_, c r´o˙zne charakte- rystyki.

• Rozwa˙zmy dowolna kategori_, e zbudowan_, a na posecie P = hP, ≤i. W´_, owczas obiektem ko´ncowym (odp. poczatkowym) w P jest element najwi_, ekszy (odp._, najmniejszy) w P , o ile taki element istnieje. W przeciwnym przypadku P nie posiada obiektu ko´ncowego (odp. poczatkowego)_,

Niech C bedzie kategori_, a. Produktem binarnym obiekt´_, ow X, Y ∈ C nazywamy obiekt oznaczany X × Y , kt´ory wraz z morfizmami π_X: X × Y ^//X i π_Y : X × Y ^//Y ma nastepuj_, ac_, a w lasno´_, s´c:

Dla ka˙zdego obiektu Z oraz morfizm´ow fX: Z ^//X i fY : Z ^//Y istnieje dok lad- nie jeden morfizm f : Z ^//X ×Y spe lniajacy warunki f_{, X} = π_X◦f oraz f_Y = π_Y◦f tzn. uprzemienniajacy oba tr´_, ojkaty w poni˙zszym diagramie:_,

X ^{oo πX} X × Y ^{πY //}Y

Z

fX

ddIIII

IIIIII ^fY

v::v vv vv vv vv

hf_X,fYi

OO

Niech C bedzie kategori_, a. Koproduktem binarnym obiekt´_, ow X, Y ∈ C nazywamy obiekt oznaczany X + Y , wraz z morfizmami iX: X ^//X + Y i iY: Y ^//X + Y , kt´ory spe lnia nastepuj_, acy warunek:_,

Dla ka˙zdego obiektu Z oraz morfizm´ow f_X: X ^//Z i f_Y : Y ^//Z istnieje do- k ladnie jeden morfizm f : X + Y ^//Z o w lasno´sciach f_X = f ◦ i_X oraz f_Y = f ◦ i_Y tzn. uprzemienniajacy oba tr´_, ojkaty w poni˙zszym diagramie:_,

X ^{iX //}

fIXIIIII$$I II

I X + Y

hf_X,fYi



iY Y

oo

fX

zzvvvvvvvvvv

Z

Analogicznie jak powy˙zej mo˙zemy stwierdzi´c, ˙ze produkt i koprodukt binarny wy- znaczone sa z dok ladno´_, scia do izomorfizmu (proste sprawdzenie pozostawiamy Czy-_, telnikowi). Ponadto sa poj_, eciami dualnymi, tj. produkt w C jest koproduktem_, w C^op oraz koprodukt w C jest produktem w C^op.

Przyk lady 7.

• W kategorii zbior´ow Sets produkt binarny to iloczyn kartezja´nski dw´och zbio- r´ow, za´s koprodukt binarny to suma roz laczna, czyli zbi´_, or {0} × X ∪ {1} × Y .

• W kategorii grup abelowych Ab produkt i koprodukt binarny to iloczyn kar- tezja´nski grup, z dzia laniami wykonywanymi po wsp´o lrzednych._,

• W kategorii definiowanej przez zbi´or cze´_,sciowo uporzadkowany P = hP, ≤i_, produkty dane sa przez operacj_, e kresu g´_, ornego u, za´s koprodukty przez kresy dolne t.

• W kategorii cia l Fields nie istnieja produkty, bowiem w ka˙zdym ciele zachodzi:_, a · b = 0 =⇒ a = 0 lub b = 0.

Jednak w produkcie cia l mieliby´smy dwa niezerowe elementy: (1, 0) i (0, 1), kt´orych iloczyn dawa lby 0 w wyniku.

Niech teraz C bedzie dowoln_, a kategori_, a z produktami binarnymi. Powiemy, ˙ze C ma_, obiekty wyk ladnicze, je´sli dla dowolnej pary obiekt´ow A, B ∈ ob(C) istnieje obiekt B^A ∈ ob(C) wraz z morfizmami evalA,B: B^A× A ^//B (tworzacymi naturaln_, a_, transformacje) o tej w lasno´_, sci, ˙ze dla dowolnego f : C × A ^//B istnieje dok ladnie jeden morfizm curry(f ) : C ^//B^A, kt´ory uprzemiennia poni˙zszy diagram:

B^A B^A× A ^{eval //}B

C

curry(f )

OO

C × A

curry(f )×1A

OO

f

x;;x xx xx xx xx xx xx xx xx x

Przyk lady 8.

• W kategorii Sets obiektem wyk ladniczym Y^X jest zbi´or wszystkich funkcji o dziedzinie X i przeciwdziedzinie Y .

• Kategoria Cat ma obiekty wyk ladnicze: D^Cmo˙zemy zdefiniowa´c jako kategorie_, funktor´ow F : C ^//D, w kt´orej morfizmami sa naturalne transformacje._,

• Algebra Heytinga rozpatrywana jako kategoria ma obiekty wyk ladnicze dane przez a → b. Istotnie, patrzac na algebry Heytinga z punktu widzenia logiki,_, eval mo ˙zemy zinterpretowa´c jako regu le eliminacji implikacji (modus ponens),_, za´s curry wyra˙za regu le wprowadzania implikacji._,

• W CPO obiektami wyk ladniczymi s

a przestrzenie funkcji ci, ag lych [D ⇒ E],_, z uporzadkowaniem_,

”po wsp´o lrzednych”._,

4 Kategorie kartezja´ nsko zamkni ete

Kategorie nazywamy kartezja´_, nsko zamkniet_, a, je´_, sli ma:

1. produkty binarne, 2. obiekt ko´ncowy, 3. obiekty wyk ladnicze.

Przyk lady 9.

• Kategoria Sets jest kategoria kartezja´_, nsko zamkniet_, a._,

• Kategoria Posets jest kategori

a kartezja´, nsko zamkniet_, a._,

• Kategoria CPO jest kartezja´nsko zamknieta._,

• Kategoria Cat jest kategoria kartezja´_, nsko zamkniet_, a._,

• (Giuseppe Rosolini). Kategoria PERs, kt´orej obiektami sa pary: zbi´_, or z cze´_,sciowa relacj_, a r´_, ownowa˙zno´sci (tj. relacja, kt´_, ora jest symetryczna i prze- chodnia, ale niekoniecznie zwrotna), za´s morfizmami funkcje zachowujace rela-_, cje, jest kategoria kartezja´_, nsko zamkniet_, a. Obiektem wyk ladniczym dla pary_, obiekt´ow: hA, Ri, hB, Si jest zbi´or wszystkich funkcji z A do B z relacja_, [R ^//S], gdzie f [R ^//S]g wtedy i tylko wtedy, gdy f i g indukuja te_, same funkcje na klasach abstrakcji A/R ^//B/S.

5 Sk ladnia rachunku lambda z typami prostymi

Typy. Zak ladamy, ˙ze dany jest zbi´or symboli typ´ow S. Nad S definiujemy zbi´or typ´ow jako najmniejszy zbi´or taki, ˙ze

1. ka˙zdy symbol typu jest typem.

2. je´sli T₁ i T₂ sa typami, to T_{, 1} ^//T₂ te˙z jest typem.

Termy. Nastepnie definujemy zbi´_, or term´ow nad zbiorem sta lych C. Ka˙zdy term jest etykietowany: napis t : T oznacza, ˙ze term t jest typu T . Ka˙zdy term t : T posiada te˙z zbi´or zmiennych wolnych F V (t).

Zbi´or term´ow to najmniejszy zbi´or taki, ˙ze:

1. (sta le) ka˙zda sta la z C, c : C jest termem; przy tym F V (c) = ∅;

2. (zmienne) dla ka˙zdego typu T mamy przeliczalny zbi´or zmiennych typu T : x₁: T, x₂: T, . . .; dla zmiennych F V (x_i) = {x_i: T };

3. (aplikacje) je´sli t : (T1 //T2) i s : T1 sa termami to (ts) : T_, 2 te˙z jest termem;

okre´slamy F V (ts) = F V (t) ∪ F V (s);

4. (λ-abstrakcje) je´sli t : T2 jest termem a x : T1 zmienna to λx.t : T_, 1 //T2 te˙z jest termem; przyjmujemy F V (λx.t) = F V (t) \ {x : T1}.

Termy rachunku λ uto˙zsamiamy zawsze, gdy r´o˙znia si_, e tylko zmiennymi zwi_, azanymi_, (α-konwersja). W szczeg´olno´sci, termy λx.xy i λx⁰.x⁰y uwa˙zamy za r´owne, za´s termy λx.xy i λx.xy⁰ za r´o˙zne.

Podstawienie. Definujemy podstawienie t[s/x] : T2

termu s : T₁ na zmienna woln_, a x : T_{, 1} w termie t : T₂. Jest to

”wstawienie” termu s : T1 we wszystkie wystapienia wolne zmiennej x : T_, 1, ale tak, by zmienne z s : T1

nie zosta ly przy tym zwiazane. Dok ladniej:_,

t[s/x] =















s gdy t : T₂ jest zmienna x : T_{, 1},

t gdy t : T2 jest zmienna r´_, o˙zna od x : T_, 1, t₁[s/x]t₂[s/x] gdy t = t₁t₂: T₂,

t gdy t = λx.t₁: T₂,

λy.t1[s/x] gdy t = λy.t1: T2 oraz y 6∈ F V (s).

Poniewa˙z uto˙zsamiamy dwa termy, je´sli r´o˙znia si_, e tylko zmiennymi zwi_, azanymi,_, zawsze mo˙zemy tak dobra´c term t₁ i zmienna y, by t = λy.t_{, 1}: T₂oraz by y 6∈ F V (s).

Podobnie mo˙zemy zdefiniowa´c jednoczesne podstawienie t[s₁/x₁, . . . , s_n/x_n] : T

term´ow s₁: T₁, . . . , s_n: T_n, na zmienne x₁: T₁, . . . , x_n: T_n w termie t : T .

6 Semantyka rachunku lambda

Interpretacje. Poka˙zemy, ˙ze kategorie kartezja´nsko zamkniete s_, a_,

”dostatecznie bogatymi uniwersami”, by mo˙zna w nich by lo interpretowa´c rachunek lambda.

Niech C bedzie kategori_, a kartezja´_, nsko zamknieta. Zak ladamy teraz, ˙ze w C_, mamy ustalone: obiekt ko´ncowy 1, produkty binarne i obiekty wyk ladnicze.

Interpretacja jezyka przyporz_, adkowuje ka˙zdemu symbolowi typu S obiekt [[S]]._, Interpretacje rozszerzamy do interpretacji wszystkich typ´ow w ten spos´ob, by

[[T1 //T2]] = [[T2]]^[[T1]]. Ponadto dla ka˙zdej sta lej c : T , wybieramy morfizm

[[c]] : 1 ^//[[T ]].

Interpretacja ta rozszerza sie do interpretacji wszystkich term´_, ow w nastepuj_, acy spo-_, s´ob. Dla zbioru zmiennych Γ = {x₁: T₁, . . . , x_n: T_n} okre´slamy

[[Γ]] = [[T1]] × . . . × [[Tn]]

Interpretacja termu t : T b_, edzie morfizm:_,

[[t]] : [[F V (t)]] ^//[[T ]]

zdefiniowany nastepuj_, aco:_,

1. [[x]] jest identyczno´scia na [[T ]] dla dowolnej zmiennej x : T ;_,

2. je´sli [[t]] : [[F V (t)]] ^//[[T₂]]^[[T1]] oraz [[s]] : [[F V (s)]] ^//[[T₁]], to morfizm [[ts]] : [[F V (ts)]] ^//[[T2]]

jest z lo˙zeniem

eval_{[[T1]],[[T2]]}◦ h[[t]] ◦ π_t, [[s]] ◦ π_si : [[F V (ts)]] ^//[[T₂]]^[[T1]]× [[T₁]] ^//[[T₂]], gdzie πsi πtsa rzutowaniami z [[F V (ts)]] odpowiednio na [[F V (s)]] oraz [[F V (t)]];_, 3. dla [[t]] : [[F V (t)]] ^//[[T₂]] oraz zmiennej x : T₁, okre´slamy interpretacje λx.t_,

jako morfizm

[[λx.t]] = curry[[t]] : [[F V (t) \ {x : T₁}]] ^//[[T₂]]^[[T1]].

Podstawienie. Niech Γ = hx₁:S₁, x₂:S₂, . . . , x_n:S_ni, ∆ = hy₁:T₁, y₂:T₂, . . . , y_k:T_ki bed_, a kontekstami. Jednoczesnym podstawieniem nazywamy n-tk_, e σ = ht_{, 1}, t₂, . . . , t_ki o tej w lasno´sci, ˙ze dla dowolnego 1 ≤ i ≤ k zachodzi Γ ` ti: Ti. Interpretacja takiego_, podstawienia jest morfizm:

[[σ]] = h[[t1]], [[t2]], . . . , [[t_k]]i,

za´s interpretacja wyniku podstawienia t[σ] = t[t_, 1/y1, t2/y2, . . . , tk/yk] : T, jest z lo˙ze- nie morfizm´ow:

[[t]] ◦ [[σ]] : [[∆]] ^//[[Γ]] ^//[[T ]].

Twierdzenie 1. (o poprawno´sci). Semantyka rachunku lambda w kategoriach kartezja´nsko zamknietych ma takie w lasno´_, sci:

(β) Je´sli Γ, x : T1` t : T<sub>2</sub> oraz Γ ` s : T1, to [[(λx.t)s]] = [[t[s/x]]].

(η) Je´sli Γ ` T₁ ^//T₂, to [[λx.tx]] = [[t]].

Dow´od: Zaczniemy od β-r´ownowa˙zno´sci. Mamy nastepuj_, acy ci_, ag r´_, owno´sci:

[[(λx.t)s]] = eval_{[[T1]],[[T2]]}◦ hcurry([[t]]), [[s]]i = (produkt)

= eval_{[[T1]],[[T2]]}◦ (curry([[t]]) × 1_[[T1]]) ◦ h1_[[Γ]], [[s]]i = (eval)

= [[t]] ◦ h1_[[Γ]], [[s]]i = (podstawienie)

= [[t]] ◦ [[h−→x , si]] = (podstawienie)

= [[t[s/x]]]

By pokaza´c, ˙ze η-r´ownowa˙zne termy sa nierozr´_, o˙znialne przy interpretacji w kate- goriach kartezja´nsko zamknietych, rozpatrzmy nast_, epuj_, acy ci_, ag r´_, owno´sci:

[[λx.tx]] = curry([[tx]]) = (definicja eval)

= curry(eval_{[[T1]],[[T2]]}◦ ([[t]] × 1_[[T1]])) =

= [[t]] 

Prawdziwe jest r´ownie˙z twierdzenie odwrotne (o pe lno´sci), stwierdzajace, ˙ze je´_, sli dana r´owno´s´c zachodzi w dowolnej kategorii kartezja´nsko zamknietej, to jest do-_, wodliwa syntaktycznie. Podobnie jak w klasycznej teorii modeli, dow´od polega na zbudowaniu odpowiedniej konstrukcji z term´ow (modulo β- i η-r´ownowa˙zno´s´c), zwa- nej kategoria syntaktyczn_, a lub klasyfikuj_, ac_, a. Obiektami takiej kategorii s_, a konteksty,_, za´s morfizmami podstawienia. Latwo sprawdzi´c, ˙ze taka kategoria jest kartezja´nsko zamknieta, a jako konstrukcja z term´_, ow spe lnia tylko niezbedne r´_, owno´sci.