Teoria kategorii dla informatyków/Wykład 4: Zaawansowane konstrukcje uniwersalne

Eksponent

Mając dane dwa zbiory $A$ i $B$, możemy stworzyć- zgodnie z aksjomatyką teorii mnogości - zbiór wszystkich funkcji typu $A\to B$ oznaczany $B^{A}$. W języku kategoryjnym powiedzielibyśmy, że dla danych dwóch obiektów $A,B\in \mathbf {Set} _{0}$, istnieje zawsze inny obiekt $B^{A}$, który nazwiemy tu eksponentem. Jeszcze krócej tę samą myśl wypowiemy tak: $\mathbf {Set}$ ma eksponenty. Spróbujmy zbadać, jaką własnością uniwersalną charakteryzują się eksponenty w $\mathbf {Set}$. Oto nieformalny tok rozumowania: skoro $B^{A}$, który łatwo będzie nam też zapisywać w miarę potrzeby jako $[A,B]$, jest pewnym specjalnym obiektem $\mathbf {Set}$, to muszą z nim być związane strzałki, które go dekonstruują, czyli rozkładają na czynniki $A$, $B$, z których powstał. (Tak było na przykład w przypadku produktu $A\times B$, gdzie destruktorami są projekcje.) Teoria mnogości wspomaga nas tutaj twierdzeniem, że istnieje izmorfizm

$\mathbf {Set} (Z\times A,B)\cong \mathbf {Set} (Z,B^{A}).$      (4.1)

Rzeczywiście, dowolnej funkcji $f\colon Z\times A\to B$ przyporządkowujemy funkcję $\mathrm {curry} (f)\colon Z\to B^{A}$ jako: $\mathrm {curry} (f)(z):=f(z,-)$. Operacja $\mathrm {curry}$, nazywana kuryfikacją, jest szukaną bijekcją. Sens tej bijekcji możemy odczytać w następujący sposób - mając dane: funkcję $f\colon Z\times A\to B$ i dwa elementy $z\in Z$, $a\in A$, wartość $f(z,a)$ powstaje albo przez bezpośrednią aplikację funkcji $f$ do pary argumentów $(z,a)$, albo poprzez aplikację funkcji $\mathrm {curry} (f)$ do argumentu $z$ i potem ewaluację tak powstałej funkcji na argumencie $a$. Innymi słowy, poniższy diagram komutuje:

gdzie $\mathrm {ev} \colon B^{A}\times A\to B$ jest ewaluacją definiowaną jako $\mathrm {ev} (f,a):=f(a)$. Rzeczywiście:

$(\mathrm {ev} \circ (\mathrm {curry} (f)\times 1_{A}))(z,a)=\mathrm {ev} (\mathrm {curry} (f)(z),a)=\mathrm {ev} (f(z,-),a)=f(z,a)$

albo w końcu:

$\mathrm {ev} \circ (\mathrm {curry} (f)\times 1_{A})=f.$

Powyższe rozważania mają sens nie tylko w $\mathbf {Set}$, ale i w każdej kategorii z produktami. Otrzymujemy więc następującą definicję:

Definicja 4.1 [eksponent]

Niech $\mathbf {C}$ będzie kategorią z produktami. Eksponentem obiektów $A$ i $B$ w $\mathbf {C}$ jest obiekt $[A,B]\in \mathbf {C} _{0}$ wraz ze strzałką $\mathrm {ev} \colon [A,B]\times A\to B$, nazywaną ewaluacją, taką że dla dowolnego obiektu $Z\in \mathbf {C} _{0}$ i strzałki $f\colon Z\times A\to B$ istnieje dokładnie jedna strzałka $\mathrm {curry} (f)\colon Z\to [A,B]$ spełniająca równanie:

$\mathrm {ev} \circ (\mathrm {curry} (f)\times 1_{A})=f$

wyrażone na diagramie jako:

Uwaga techniczna: często w dowodach pojawiają się naraz ewaluacje różnych typów; wygodnie wtedy $\mathrm {ev} \colon [A,B]\times A\to B$ oznaczyć jako $\mathrm {ev} _{A,B}$.

Zauważmy, że dla dowolnej strzałki $g\colon Z\to [A,B]$ możemy zdefiniować jej odwrotność jako

$\mathrm {uncurry} (g):=\mathrm {ev} \circ (g\times 1_{A})\colon Z\times A\to B.$

Wtedy własność uniwersalna z powyższej definicji daje nam:

$\mathrm {curry} (\mathrm {uncurry} (g))=g$

oraz dla dowolnej $f\colon Z\times A\to B$ komutowanie powyższego diagramu natychmiast implikuje, że:

$\mathrm {uncurry} (\mathrm {curry} (f))=f.$

Pokazaliśmy więc izomorfizm:

$\mathrm {Hom} _{\mathbf {C} }(Z\times A,B)\cong \mathrm {Hom} _{\mathbf {C} }(Z,[A,B])$,      (4.2)

który uogólnia izomorfizm (4.1) dla $\mathbf {Set}$.

Kategorie kartezjańsko zamknięte

Kategorie, w których istnieją eksponenty zasługują na wyróżnienie:

Definicja 4.2

Kategoria $\mathbf {C}$ jest kartezjańsko zamknięta, jeśli posiada obiekt końcowy, produkty binarne i eksponenty.

Oto przykłady:

• $\mathbf {Set}$ jest kartezjańsko zamknięta. Podobnie $\mathbf {Set} _{fin}$, gdyż konstrukcje są takie same, jak dla $\mathbf {Set}$, a eksponent $[A,B]$ dla zbiorów skończonych jest zbiorem skończonym.
• Kategoria $\mathbf {Pos}$ jest kartezjańsko zamknięta. Produkt dwóch posetów $(P,\leq )\times (Q,\leq )$ definiuje się jako produkt zbiorów $P\times Q$ wraz z relacją częściowego porządku po współrzędnych: $(p_{1},q_{1})\leq (p_{2},q_{2})$ wtedy i tylko wtedy, gdy $(p_{1}\leq p_{2})\wedge (q_{1}\leq q_{2})$ wraz z naturalnymi projekcjami $\pi _{P}(p,q):=p$ i $\pi _{Q}(p,q):=q$. Jako eksponent $[P,Q]$ bierzemy zbiór wszystkich funkcji monotonicznych typu $P\to Q$ wraz z porządkiem po współrzędnych: $f\sqsubseteq g\iff \forall z\in P\ (f(z)\leq g(z)).$ Ewaluacja i kuryfikacja są definiowane tak jak w $\mathbf {Set}$, wystarczy więc sprawdzić, że są monotoniczne. Jeśli $(f,p)\leq (q,r)$ w $[P,Q]\times P$, to $\mathrm {ev} (f,p)=f(p)\leq g(p)\leq g(r)=\mathrm {ev} (g,r),$ a zatem ewaluacja jest monotoniczna. Natomiast dla $f\colon Z\times P\to Q$, $z\sqsubseteq z'$, $p\in P$ mamy $\mathrm {curry} (f)(z)(p)=f(z,p)\leq f(z',p)=\mathrm {curry} (f)(z')(p),$ co świadczy o tym, że $\mathrm {curry} (f)(z)\leq \mathrm {curry} (f)(z')$, czyli że kuryfikacja jest monotoniczna dla każdej funkcji $f$.
• Dwie ważne dla semantyki języków programowania kategorie kartezjańsko zamknięte: kategorię posetów zupełnych $\mathbf {Dcpo}$ i kategorię bc-dziedzin $\mathbf {BC}$ omawiamy oddzielnie w Wykładzie 13.
• Poset $(P,\leq )$ z elementem najmniejszym $0$ jako kategoria jest kartezjańsko zamknięty wtedy i tylko wtedy, gdy jest algebrą Heytinga, zobacz podrozdział nt. algebr Heytinga.
• $\mathbf {Cat}$ - kategoria wszystkich małych kategorii - jest kartezjańsko zamknięta.
• Dla dowolnej małej kategorii $\mathbf {C}$ kategoria funktorów $[\mathbf {C} ^{op},\mathbf {Set} ]$ jest kartezjańsko zamknięta. Do tego przykładu wrócimy w Wykładach 7 i 8.
• Kartezjańsko zamknięte nie są: $\mathbf {Vect}$, $\mathbf {Ab}$, $\mathbf {Top}$, $\mathbf {Met}$, ... z różnych przyczyn.

Algebry Heytinga

Przypomnijmy najpierw - w telegraficznym skrócie -pojęcia kraty dystrybutywnej i algebry Boole'a: Niech $(L,\leq )$ będzie kratą z elementem najmniejszym $\mathbf {0}$ i elementem największym $\mathbf {1}$. Łatwo się przekonać, że kratę można również zdefiniować jako algebrę, bez relacji $\leq$, jedynie za pomocą równości i prymitywnych operacji $\wedge ,\vee ,\mathbf {0} ,\mathbf {1}$.

Stwierdzenie 4.3

Niech $L$ będzie zbiorem z operacjami: $\wedge \colon L\times L\to L$ $\vee \colon L\times L\to L$ $\mathbf {0} \colon 1\to L$ $\mathbf {1} \colon 1\to L,$

gdzie $\wedge$ i $\vee$ są łączne i przemienne oraz spełniają następujące aksjomaty:

$x\wedge x=x$ $x\vee x=x$ $\mathbf {1} \wedge x=x$ $\mathbf {0} \vee x=x$ $x\wedge (y\vee x)=x=(x\wedge y)\vee x$

dla dowolnych $x,y,z\in L$. Wówczas $(L,\leq )$ jest kratą, gdzie $\leq$ definiujemy jako

$x\leq y\iff x=x\wedge y$

lub równoważnie:

$x\leq y\iff y=x\vee y.$

Oczywiście twierdzenie odwrotne też zachodzi.

Niektóre spośród krat posiadają ciekawą własność:

Definicja 4.4

Kratę $(L,\leq )$ nazywamy dystrybutywną, jeśli dla dowolnych $x,y,z\in L$ zachodzi $x\wedge (y\vee z)=(x\wedge y)\vee (x\wedge z).$

Fakt 4.5

Powyższa równość w definicji implikuje równość dualną: $x\vee (y\wedge z)=(x\vee y)\wedge (x\vee z).$

Definicja 4.6

Elementem przeciwnym do $x$ w kracie $L$ nazywamy element $a\in L$ taki, że $x\wedge a=\mathbf {0}$ i $x\vee a=\mathbf {1}$.

Fakt 4.7

W kracie dystrybutywnej element przeciwny do $x$ jest jedyny. Oznaczamy go wówczas jako $\neg x$.

Najbardziej znanymi kratami dystrybutywnymi są niewątpliwie algebry Boole'a.

Definicja 4.8 [algebra Boole'a]

Algebrą Boole'a nazywamy kratę dystrybutywną, w której każdy element $x$ ma element przeciwny.

Fakt 4.9

W dowolnej algebrze Boole'a $L$ zachodzą równości:

$\neg (x\vee y)=\neg x\wedge \neg y$ $\neg (x\wedge y)=\neg x\vee \neg y$ $\neg \neg x=x.$

Pierwszą i drugą równość nazywamy prawami de Morgana.

Algebry Boole'a są szczególnymi przypadkami innych krat dystrybutywnych, tzw. algebr Heytinga, które omawiamy poniżej:

Definicja 4.10 [algebra Heytinga]

Algebrą Heytinga nazywamy kratę $(L,\leq )$ z elementem najmniejszym $\mathbf {0}$, elementem największym $\mathbf {1}$ i operacją $\Rightarrow \colon L\times L\to L$ definiowaną dla każdej pary elementów $x,y\in L$ jako: $x\Rightarrow y:=\bigvee \{z\in L\mid z\wedge x\leq y\}.$

Taka definicja może na pierwszy rzut oka wydawać się przypadkowa. Punkt widzenia teorii kategorii rozjaśnia wątpliwości natychmiast: Jeśli potraktujemy kratę $(L,\leq ,\mathbf {0} ,\mathbf {1} )$ jako kategorię, będzie to kategoria, w której pomiędzy dwoma dowolnymi obiektami istnieje co najwyżej jedna strzałka, z elementem początkowym $\mathbf {0}$, końcowym $\mathbf {1}$, produktami (infima binarne: $\wedge$) i koproduktami (suprema: $\vee$). Krata taka jest algebrą Heytinga wtedy i tylko wtedy, gdy istnieje operacja $\Rightarrow$ taka, że

$x\Rightarrow y=\bigvee \{z\in L\mid z\wedge x\leq y\}$

dla każdego $x,y\in L$. Ta definicja da się przepisać następująco:

$z\leq x\Rightarrow y\ \iff \ z\wedge x\leq y,$

co w terminach kategoryjnych oznacza, ze istnieje bijekcja pomiędzy strzałkami $\mathrm {Hom} _{L}(z,x\Rightarrow y)$ i strzałkami $\mathrm {Hom} (z\wedge x,y)$. A ten warunek jest dokładnie warunkiem uniwersalnym dla elementu $x\Rightarrow y$ traktowanego jako eksponent!

A zatem: algebra Heytinga to poset z elementem najmniejszym, który jako kategoria jest kartezjańsko zamknięty. Warto zapamiętać tę charakteryzację.

Ponieważ:

Fakt 4.11

W dowolnej algebrze Boole'a mamy: $z\leq (\neg x\vee y)\iff z\wedge x\leq y,$

więc każda algebra Boole'a jest algebrą Heytinga. Można też pokazać, że:

Fakt 4.12

W dowolnej algebrze Heytinga $L$, jeśli dla $x\in L$ istnieje $\neg x$, to musi być $\neg x=x\Rightarrow \mathbf {0}$.

Kartezjańska zamkniętość algebr Heytinga daje nam natychmiast następujące równości (które w innych kategoriach są izomorfizmami) i nierówności (czyli istnienie odpowiednich strzałek) - porównaj Zadanie 4.3:

Fakt 4.13

W dowolnej algebrze Heytinga zachodzą zależności: $x\leq (y\Rightarrow (x\wedge y))$ $y\wedge (y\Rightarrow x)\leq x$ $(x\Rightarrow \mathbf {1} )=\mathbf {1}$ $(\mathbf {1} \Rightarrow x)=x$ $(y\wedge z)\Rightarrow x=(z\Rightarrow (y\Rightarrow x))$ $(x\Rightarrow (y\wedge z))=(x\Rightarrow y)\wedge (x\Rightarrow z)$ $\mathbf {1} \leq x\Rightarrow x$ $\mathbf {1} \leq (x\Rightarrow (y\Rightarrow x))$ $\mathbf {1} \leq (x\Rightarrow (y\Rightarrow z))\Rightarrow ((x\Rightarrow y)\Rightarrow (x\Rightarrow z)).$

Powyższe własności doprowadzają nas do najważniejszego wniosku w tym podrozdziale: algebry Heytinga są algebraicznym odpowiednikiem rachunku intuicjonistycznej logiki zdaniowej. Naszkicujmy tę odpowiedniość w obie strony: dla danej algebry Heytinga $(L,\leq ,\mathbf {0} ,\mathbf {1} ,\wedge ,\vee ,\Rightarrow )$ traktujemy elementy $x\in L$ jako zmienne, $\leq$ jako syntaktyczną relację dedukcji $\vdash$, $\mathbf {0}$, $\mathbf {1}$ jako stałe fałsz i prawda, zaś operacje $\wedge ,\vee ,\Rightarrow$ jako spójniki zdaniowe. Wówczas taki system jest rachunkiem zdaniowym logiki intuicjonistycznej.

Odwrotnie, załóżmy, że mamy dany język zdaniowy, intuicjonistyczny, ${\mathcal {L}}$, składający się ze zmiennych zdaniowych $x,y,z,...$, z których za pomocą spójników $\wedge ,\vee ,\Rightarrow$ i stałych $\mathbf {0} ,\mathbf {1}$ tworzymy w znany sposób zdania $p,q,r,...$ oraz z syntaktycznej relacji dedukcji $\vdash$ podlegającej aksjomatom:

• $\vdash$ jest zwrotna i przechodnia,
• $p\vdash \mathbf {1}$,
• $\mathbf {0} \vdash p$,
• $p\vdash q$ i $p\vdash r$ wtedy i tylko wtedy, gdy $p\vdash q\wedge r$,
• $p\vdash r$ i $q\vdash r$ wtedy i tylko wtedy, gdy $p\vee q\vdash r$,
• $p\wedge q\vdash r$ wtedy i tylko wtedy, gdy $p\vdash q\Rightarrow r$.

Wówczas z ${\mathcal {L}}$ tworzymy algebrę $H({\mathcal {L}})$, tzw. algebrę Lindenbauma - Tarskiego składającą się z klas abstrakcji $[p]$ relacji równoważności $=$ danej przez

$[p]=[q]\ \iff \ p\dashv \vdash q.$

Algebra $H({\mathcal {L}})$ jest częściowym porządkiem:

$[p]\leq [q]\ :\iff \ p\vdash q,$

z elementem największym $[\mathbf {1} ]$ i najmniejszym $[\mathbf {0} ]$. Operacje algebry są zadane jako: $[p]\wedge [q]:=[p\wedge q]$, i tak samo dla $\vee$ oraz $\Rightarrow$. Tak utworzona algebra $H({\mathcal {L}})$ jest algebrą Heytinga, która - co więcej - ma tę własność, że zdanie $p$ można udowodnić w ${\mathcal {L}}$ wtedy i tylko wtedy, gdy $[p]=\mathbf {1}$ w $H({\mathcal {L}})$.

Kategorie kartezjańsko zamknięte a lambda rachunek

Oczywiście można i trzeba sobie zadać pytanie: skoro algebry Heytinga są algebraicznym równoważnikiem zdaniowego rachunku logiki intuicjonistycznej, to czy ten fenomen przenosi się na ogólne kategorie kartezjańsko zamknięte? Pytamy zatem: jaki język odpowiada dowolnej kategorii kartezjańsko zamkniętej $\mathbf {C}$? Nie dość, że pytanie jest dobrze postawione, co się okaże za chwilę, to jeszcze ma bardzo satysfakcjonującą odpowiedź: tym językiem jest rachunek lambda! W rzeczywistości struktury: kategorii kartezjańsko zamkniętej i lambda rachunku, są dwoma odbiciami tego samego zjawiska, czy też - jeśli ktoś woli inną poetykę - kategorie k.z. i $\lambda$-rachunek są dwiema manifestacjami tej samej struktury matematycznej. Poniżej spróbujemy wykazać tą tezę w kilku krokach:

• Po pierwsze, pokażmy, że dla $\lambda$-rachunku kategoria $\mathbf {C} (\lambda )$, zdefiniowana w Zadaniu 1.11, wzbogacona o obiekt końcowy (który zawsze łatwo dodać), jest kartezjańsko zamknięta. Widzieliśmy już w podrozdziale nt. produktów, że ta kategoria posiada produkty. Pokażemy zatem, że posiada eksponenty. Oczywiście $[A,B]:=A\to B$ dla typów $A,B$, zaś ewaluacja i odwrotność kuryfikacji są zdefiniowane, jak następuje:

$\mathrm {ev} :=\lambda z.\pi _{1}(z)\pi _{2}(z)\colon [A,B]\times A\to B$ $\mathrm {uncurry} (f):=\lambda z.\lambda x.f(z,x)\colon Z\to [A,B]$

gdzie $z:Z,x:A$. Wtedy - pamiętając, że

$g\times h=\lambda w.\langle g\pi _{1}(w),h\pi _{2}(w)\rangle ,$

mamy:

$\mathrm {ev} \circ (\mathrm {curry} (f)\times 1_{A})=\lambda v.(\lambda z.\pi _{1}(z)\pi _{2}(z))(\lambda w.\langle (\lambda y.\lambda x.f(y,x))\pi _{1}(w),(\lambda u.u)\pi _{2}(w)\rangle )v=\lambda v.(\lambda z.\pi _{1}(z)\pi _{2}(z))(\langle \lambda x.f(\pi _{1}(v),x),\pi _{2}(v)\rangle )=\lambda v.(\lambda x.f(\pi _{1}(v),x))\pi _{2}(v)=\lambda v.f(\pi _{1}(v),\pi _{2}(v))=\lambda v.fv=f.$

Naszkicowaliśmy zatem dowód, że $\mathbf {C} (\lambda )$ jest kategorią kartezjańsko zamkniętą.

• Odwrotnie, mając daną kategorię kartezjańsko zamkniętą $\mathbf {C}$, definiujemy język ${\mathcal {L}}(\mathbf {C} )$ jak następuje: typy to obiekty $\mathbf {C}$; termy typu $A\to B$ to strzałki typu $A\to B$; termy proste typu $A$ to strzałki typu $\mathbf {1} \to A$; równania języka ${\mathcal {L}}(\mathbf {C} )$ to znane równania w $\mathbf {C}$, m.in. te wynikające z kartezjańskiej zamkniętości, np.:

$\lambda x.\pi _{1}(x)=p_{1},$ $\lambda x.\pi _{2}(x)=p_{2},$ $\lambda y.f(x,y)=\mathrm {curry} (f)(x),$

i tak dalej.

• Dwie opisane powyżej konstrukcje są w ścisłym sensie odwrotne do siebie, ponieważ możemy udowodnić, że $\mathbf {C} ({\mathcal {L}}(\mathbf {C} ))\cong \mathbf {C}$, tzn. kategorie $\mathbf {C} (\lambda (\mathbf {C} ))$ i $\mathbf {C}$ są izmorficzne oraz że języki $\lambda$ i ${\mathcal {L}}(\mathbf {C} (\lambda ))$ są sobie równoważne w sensie, który jest dokładnie przedyskutowany w książce J.Lambeka i O. Scotta pt. Introduction to Higher-Order Categorical Logic, Cambridge University Press, 1986.