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

From Studia Informatyczne

Spis treści

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:

Grafika:tk-4.1.png

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:

Grafika:tk-4.2.png

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.