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

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania

Eksponent

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

     (4.1)

Rzeczywiście, dowolnej funkcji przyporządkowujemy funkcję jako: . Operacja , nazywana kuryfikacją, jest szukaną bijekcją. Sens tej bijekcji możemy odczytać w następujący sposób - mając dane: funkcję i dwa elementy , , wartość powstaje albo przez bezpośrednią aplikację funkcji do pary argumentów , albo poprzez aplikację funkcji do argumentu i potem ewaluację tak powstałej funkcji na argumencie . Innymi słowy, poniższy diagram komutuje:

Tk-4.1.png

gdzie jest ewaluacją definiowaną jako . Rzeczywiście:

albo w końcu:

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


Definicja 4.1 [eksponent]

Niech będzie kategorią z produktami. Eksponentem obiektów i w jest obiekt wraz ze strzałką , nazywaną ewaluacją, taką że dla dowolnego obiektu i strzałki istnieje dokładnie jedna strzałka spełniająca równanie:

wyrażone na diagramie jako:

Tk-4.2.png

Uwaga techniczna: często w dowodach pojawiają się naraz ewaluacje różnych typów; wygodnie wtedy oznaczyć jako .

Zauważmy, że dla dowolnej strzałki możemy zdefiniować jej odwrotność jako

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

oraz dla dowolnej komutowanie powyższego diagramu natychmiast implikuje, że:

Pokazaliśmy więc izomorfizm:

,      (4.2)

który uogólnia izomorfizm (4.1) dla .

Kategorie kartezjańsko zamknięte

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


Definicja 4.2

Kategoria jest kartezjańsko zamknięta, jeśli posiada obiekt końcowy, produkty binarne i eksponenty.


Oto przykłady:

  • jest kartezjańsko zamknięta. Podobnie , gdyż konstrukcje są takie same, jak dla , a eksponent dla zbiorów skończonych jest zbiorem skończonym.
  • Kategoria jest kartezjańsko zamknięta. Produkt dwóch posetów definiuje się jako produkt zbiorów wraz z relacją częściowego porządku po współrzędnych: wtedy i tylko wtedy, gdy wraz z naturalnymi projekcjami i . Jako eksponent bierzemy zbiór wszystkich funkcji monotonicznych typu wraz z porządkiem po współrzędnych: Ewaluacja i kuryfikacja są definiowane tak jak w , wystarczy więc sprawdzić, że są monotoniczne. Jeśli w , to a zatem ewaluacja jest monotoniczna. Natomiast dla , , mamy co świadczy o tym, że , czyli że kuryfikacja jest monotoniczna dla każdej funkcji .
  • Dwie ważne dla semantyki języków programowania kategorie kartezjańsko zamknięte: kategorię posetów zupełnych i kategorię bc-dziedzin omawiamy oddzielnie w Wykładzie 13.
  • Poset z elementem najmniejszym jako kategoria jest kartezjańsko zamknięty wtedy i tylko wtedy, gdy jest algebrą Heytinga, zobacz podrozdział nt. algebr Heytinga.
  • - kategoria wszystkich małych kategorii - jest kartezjańsko zamknięta.
  • Dla dowolnej małej kategorii kategoria funktorów jest kartezjańsko zamknięta. Do tego przykładu wrócimy w Wykładach 7 i 8.
  • Kartezjańsko zamknięte nie są: , , , , ... z różnych przyczyn.

Algebry Heytinga

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

Stwierdzenie 4.3

Niech będzie zbiorem z operacjami:

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

dla dowolnych . Wówczas jest kratą, gdzie definiujemy jako

lub równoważnie:

Oczywiście twierdzenie odwrotne też zachodzi.

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

Definicja 4.4

Kratę nazywamy dystrybutywną, jeśli dla dowolnych zachodzi

Fakt 4.5

Powyższa równość w definicji implikuje równość dualną:


Definicja 4.6

Elementem przeciwnym do w kracie nazywamy element taki, że i .


Fakt 4.7

W kracie dystrybutywnej element przeciwny do jest jedyny. Oznaczamy go wówczas jako .


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 ma element przeciwny.


Fakt 4.9

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

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ę z elementem najmniejszym , elementem największym i operacją definiowaną dla każdej pary elementów jako:

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ę 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 , końcowym , produktami (infima binarne: ) i koproduktami (suprema: ). Krata taka jest algebrą Heytinga wtedy i tylko wtedy, gdy istnieje operacja taka, że

dla każdego . Ta definicja da się przepisać następująco:

co w terminach kategoryjnych oznacza, ze istnieje bijekcja pomiędzy strzałkami i strzałkami . A ten warunek jest dokładnie warunkiem uniwersalnym dla elementu 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:


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


Fakt 4.12

W dowolnej algebrze Heytinga , jeśli dla istnieje , to musi być .


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:


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 traktujemy elementy jako zmienne, jako syntaktyczną relację dedukcji , , jako stałe fałsz i prawda, zaś operacje jako spójniki zdaniowe. Wówczas taki system jest rachunkiem zdaniowym logiki intuicjonistycznej.

Odwrotnie, załóżmy, że mamy dany język zdaniowy, intuicjonistyczny, , składający się ze zmiennych zdaniowych , z których za pomocą spójników i stałych tworzymy w znany sposób zdania oraz z syntaktycznej relacji dedukcji podlegającej aksjomatom:

  • jest zwrotna i przechodnia,
  • ,
  • ,
  • i wtedy i tylko wtedy, gdy ,
  • i wtedy i tylko wtedy, gdy ,
  • wtedy i tylko wtedy, gdy .

Wówczas z tworzymy algebrę , tzw. algebrę Lindenbauma - Tarskiego składającą się z klas abstrakcji relacji równoważności danej przez

Algebra jest częściowym porządkiem:

z elementem największym i najmniejszym . Operacje algebry są zadane jako: , i tak samo dla oraz . Tak utworzona algebra jest algebrą Heytinga, która - co więcej - ma tę własność, że zdanie można udowodnić w wtedy i tylko wtedy, gdy w .

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 ? 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 -rachunek są dwiema manifestacjami tej samej struktury matematycznej. Poniżej spróbujemy wykazać tą tezę w kilku krokach:

  • Po pierwsze, pokażmy, że dla -rachunku kategoria , 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 dla typów , zaś ewaluacja i odwrotność kuryfikacji są zdefiniowane, jak następuje:

gdzie . Wtedy - pamiętając, że

mamy:

Naszkicowaliśmy zatem dowód, że jest kategorią kartezjańsko zamkniętą.

  • Odwrotnie, mając daną kategorię kartezjańsko zamkniętą , definiujemy język jak następuje: typy to obiekty ; termy typu to strzałki typu ; termy proste typu to strzałki typu ; równania języka to znane równania w , m.in. te wynikające z kartezjańskiej zamkniętości, np.:

i tak dalej.

  • Dwie opisane powyżej konstrukcje są w ścisłym sensie odwrotne do siebie, ponieważ możemy udowodnić, że , tzn. kategorie i są izmorficzne oraz że języki i 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.