W tym rozdziale zajmiemy się badaniem relacji. Poznamy podstawowe rodzaje relacji, ich właściwości, a także zależności i przekształcenia między nimi. Rozdział będzie raczej matematyczny.

Relacje binarne

Zacznijmy od przypomnienia klasyfikacji zdań, predykatów i relacji:

• zdania to obiekty typu Prop. Twierdzą one coś na temat świata: "niebo jest niebieskie", P -> Q etc. W uproszczeniu możemy myśleć o nich, że są prawdziwe lub fałszywe, co nie znaczy wcale, że można to automatycznie rozstrzygnąć. Udowodnienie zdania P to skonstruowanie obiektu p : P. W Coqu zdania służą nam do podawania specyfikacji programów. W celach klasyfikacyjnych możemy uznać, że są to funkcje biorące zero argumentów i zwracające Prop.
• predykaty to funkcje typu A -> Prop dla jakiegoś A : Type. Można za ich pomocą przedstawiać stwierdzenia na temat właściwości obiektów: "liczba 5 jest parzysta", odd 5. Dla niektórych argumentów zwracane przez nie zdania mogą być prawdziwe, a dla innych już nie. Dla celów klasyfikacji uznajemy je za funkcje biorące jeden argument i zwracające Prop.
• relacje to funkcje biorące dwa lub więcej argumentów, niekoniecznie o takich samych typach, i zwracające Prop. Służą one do opisywania zależności między obiektami, np. "Grażyna jest matką Karyny", Permutation (l ++ l') (l' ++ '). Niektóre kombinacje obiektów mogą być ze sobą w relacji, tzn. zdanie zwracane dla nich przez relację może być prawdziwe, a dla innych nie.

Istnieje jednak zasadnicza różnica między definiowaniem "zwykłych" funkcji oraz definiowaniem relacji: zwykłe funkcje możemy definiować jedynie przez dopasowanie do wzorca i rekurencję, zaś relacje możemy poza tymi metodami definiować także przez indukcję, dzięki czemu możemy wyrazić więcej konceptów niż za pomocą rekursji.

Najważniejszym rodzajem relacji są relacje binarne, czyli relacje biorące dwa argumenty. To właśnie im poświęcimy ten rozdział, pominiemy zaś relacje biorące trzy i więcej argumentów. Określenia "relacja binarna" będę używał zarówno na określenie relacji binarnych heterogenicznych (czyli biorących dwa argumnty różnych typów) jak i na określenie relacji binarnych homogenicznych (czyli biorących dwa argumenty tego samego typu).

Identyczność relacji

Zacznijmy od ustalenia, jakie relacje będziemy uznawać za "identyczne". Okazuje się, że używanie równości eq do porównywania zdań nie ma zbyt wiele sensu. Jest tak dlatego, że nie interesuje nas postać owych zdań, a jedynie ich logiczna zawartość. Z tego powodu właściwym dla zdań pojęciem "identyczności" jest równoważność, czyli <->. Podobnie jest w przypadku relacji: uznamy dwie relacje za identyczne, gdy dla wszystkich argumentów zwracają one równoważne zdania. Formalnie wyrazimy to nieco na około, za pomocą pojęcia subrelacji. R jest subrelacją S, jeżeli R a b implikuje S a b dla wszystkich a : A i b : B. Możemy sobie wyobrażać, że jeżeli R jest subrelacją S, to w relacji R są ze sobą tylko niektóre pary argumentów, które są w relacji S, a inne nie.

Ćwiczenie

Udowodnij, że powyższa definicja le' porządku "mniejszy lub równy" na liczbach naturalnych jest tą samą relacją, co le. Być może przyda ci się kilka lematów pomocniczych.

Uporawszy się z pojęciem "identyczności" relacji możemy przejść dalej, a mianowicie do operacji, jakie możemy wykonywać na relacjach.

Operacje na relacjach

Podobnie jak w przypadku funkcji, najważniejszą operacją jest składanie relacji, a najważniejszą relacją — równość. Składanie jest łączne, zaś równość jest elementem neutralnym tego składania. Musimy jednak zauważyć, że mówiąc o łączności relacji mamy na myśli coś innego, niż w przypadku funkcji.

Składanie funkcji jest łączne, gdyż złożenie trzech funkcji z dowolnie rozstawionymi nawiasami daje wynik identyczny w sensie eq. Składanie relacji jest łączne, gdyż złożenie trzech relacji z dowolnie rozstawionymi nawiasami daje wynik identyczny w sensie same_hrel. Podobnie sprawa ma się w przypadku stwierdzenia, że eq jest elementem nautralnym składania relacji.

Rinv to operacja, która zamienia miejscami argumenty relacji. Relację Rinv R będziemy nazywać relacją odwrotną do R.

Złożenie dwóch relacji możemy odwrócić, składając ich odwrotności w odwrotnej kolejności. Odwrotnością relacji identycznościowej jest zaś ona sama.

Pozostałe trzy operacje na relacjach odpowiadają spójnikom logicznym — mamy więc negację relacji oraz koniunkcję i dysjunkcję dwóch relacji. Zauważ, że operacje te możemy wykonywać jedynie na relacjach o takich samych typach argumentów. Sporą część naszego badania relacji przeznaczymy na sprawdzanie, jak powyższe operacj mają się do różnych specjalnych rodzajów relacji. Nim to się stanie, zbadajmy jednak właściwości samych operacji.

Zacznijmy od relacjowych odpowiedników True i False. Przydadzą się nam one do wyrażania właściwości Rand oraz Ror.

To nie wszystkie właściwości tych operacji, ale myślę, że widzisz już, dokąd to wszystko zmierza. Jako, że Rnot, Rand i Ror pochodzą bezpośrednio od spójników logicznych not, and i or, dziedziczą one po nich wszystkie ich właściwości. Fenomen ten nie jest w żaden sposób specyficzny dla relacji i operacji na nich - z pewnością spotkamy się z nim ponownie w nadchodzących rozdziałach.

Relatory, czyli więcej operacji na relacjach (TODO)

Póki co wszystkie operacje na relacjach, które widzieliśmy, pochodziły po prostu od spójników logicznych. Co jednak z operacjami na typach, takimi jak produkt, suma, opcja, typy funkcyjne, etc.? Czy żyją one w odizolowanym świecie, który nie ma zupełnie żadnego związku ze światem relacji? Oczywiście, że nie: mając relacje na jakichś typach, możemy przekształcić je na relację na produkcie czy sumie tych typów w kanoniczny sposób spełniający pewne właściwości. Operacje, które dokonują tego przekształcenia, nazywać będziemy relatorami.

Przykładem relatora jest option.

Możemy też zdefiniować pojęcia birelatora (od łacińskiego prefiksu "bi" oznaczającego "dwa"), czyli dwuargumentowy relator.

Produkty i sumy są przykładami birelatorów.

Relacje homogeniczne (TODO)

Relacje homogeniczne to takie, których wszystkie argumenty są tego samego typu. Warunek ten pozwala nam na wyrażenie całej gamy nowych właściwości, które relacje takie mogą posiadać. Uwaga terminologiczna: w innych pracach to, co nazwałem Antireflexive bywa zazwyczaj nazywane Irreflexive. Ja przyjąłem następujące reguły tworzenia nazw różnych rodzajów relacji:

• "podstawowa" własność nie ma przedrostka, np. "zwrotna", "reflexive"
• zanegowana własność ma przedrostek "nie" (lub podobny w nazwach angielskich), np. "niezwrotna", "irreflexive"
• przeciwieństwo tej właściwości ma przedrostek "anty-" (po angielsku "anti-"), np. "antyzwrotna", "antireflexive"

Relacje równoważności (TODO)

Relacje zwrotne

Relacja R jest zwrotna (ang. reflexive), jeżeli każdy x : A jest w relacji sam ze sobą. Przykładem ze świata rzeczywistego może być relacja "x jest blisko y". Jest oczywiste, że każdy jest blisko samego siebie.

Okazuje się, że wszystkie relacje na typie pustym (Empty_set) są zwrotne. Nie powinno cię to w żaden sposób zaskakiwać — jest to tzw. pusta prawda (ang. vacuous truth), zgodnie z którą wszystkie zdania kwantyfikowane uniwersalnie po typie pustym są prawdziwe. Wszyscy w pustym pokoju są debilami.

Najważniejszym przykładem relacji zwrotnej jest równość. eq jest relacją zwrotną, gdyż ma konstruktor eq_refl, który głosi, że każdy obiekt jest równy samemu sobie. Zwrotna jest też relacja RTrue, gdyż każdy obiekt jest w jej przypadku w relacji z każdym, a więc także z samym sobą. Zwrotna nie jest za to relacja RFalse na typie niepustym, gdyż tam żaden obiekt nie jest w relacji z żadnym, a więc nie może także być w relacji z samym sobą.

Równość jest "najmniejszą" relacją zwrotną w tym sensie, że jest ona subrelacją każdej relacji zwrotnej. Intuicyjnym uzasadnieniem jest fakt, że w definicji eq poza konstruktorem eq_refl, który daje zwrotność, nie ma niczego innego.

TODO: Zachodzi też twierdzenie odwrotne.

Jak widać, złożenie, odwrotność i koniunkcja relacji zwrotnych są zwrotne. Dysjunkcja posiada natomiast dużo mocniejszą właściwość: dysjunkcja dowolnej relacji z relacją zwrotną daje relację zwrotną. Tak więc dysjunkcja R z eq pozwala nam łatwo "dodać" zwrotność do R. Słownie dysjunkcja z eq odpowiada zwrotowi "lub równy", który możemy spotkać np. w wyrażeniach "mniejszy lub równy", "większy lub równy". Właściwością odwrotną do zwrotności jest antyzwrotność. Relacja antyzwrotna to taka, że żaden x : A nie jest w relacji sam ze sobą.

Typowymi przykładami relacji antyzwrotnych są nierówność <> oraz porządek "mniejszy niż" (<) na liczbach naturalnych. Ze względu na sposób działania ludzkiego mózgu antyzwrotna jest cała masa relacji znanych nam z codziennego życia: "x jest matką y", "x jest ojcem y", "x jest synem y", "x jest córką y", "x jest nad y", "x jest pod y", "x jest za y", "x jest przed y", etc.

Równość na typie niepustym nie jest antyzwrotna, gdyż jest zwrotna (wzajemne związki między tymi dwoma pojęciami zbadamy już niedługo). Antyzwrotna nie jest także relacja RTrue na typie niepustym, gdyż co najmniej jeden element jest w relacji z samym sobą. Antyzwrotna jest za to relacja pusta (RFalse).

Złożenie relacji antyzwrotnych nie musi być antyzwrotne, ale odwrotność i dysjunkcja już tak, zaś koniunkcja dowolnej relacji z relacją antyzwrotną daje nam relację antyzwrotną. Dzięki temu możemy dowolnej relacji R "zabrać" zwrotność koniunkcjując ją z <>. Kolejną właściwością jest niezwrotność. Relacja niezwrotna to taka, która nie jest zwrotna. Zauważ, że pojęcie to zasadniczo różni się od pojęcia relacji antyzwrotnej: tutaj mamy kwantyfikator exists, tam zaś forall.

Typowym przykładem relacji niezwrotnej jest nierówność x <> y. Jako, że każdy obiekt jest równy samemu sobie, to żaden obiekt nie może być nierówny samemu sobie. Zauważ jednak, że typ A musi być niepusty, gdyż w przeciwnym wypadku nie mamy czego dać kwantyfikatorowi exists. Innym przykładem relacji niezwrotnej jest porządek "większy niż" na liczbach naturalnych. Porządkami zajmiemy się już niedługo.

Równość jest zwrotna, a więc nie może być niezwrotna. Zauważ jednak, że musimy podać aż dwa osobne dowody tego faktu: jeden dla typu pustego Empty_set, a drugi dla dowolnego typu niepustego. Wynika to z tego, że nie możemy sprawdzić, czy dowolny typ A jest pusty, czy też nie.

Podobnej techniki możemy użyć, aby pokazać, że relacja pełna (RTrue) nie jest niezwrotna. Inaczej jest jednak w przypadku RFalse — na typie pustym nie jest ona niezwrotna, ale na dowolnym typie niepustym już owszem.

Złożenie relacji niezwrotnych nie musi być niezwrotne. Przyjrzyj się uważnie definicji Rcomp, a z pewnością uda ci się znaleźć jakiś kontrprzykład.

Odwrotność relacji niezwrotnej jest niezwrotna. Koniunkcja dowolnej relacji z relacją niezwrotną daje relację niezwrotną. Tak więc za pomocą koniunkcji i dysjunkcji możemy łatwo dawać i zabierać zwrotność różnym relacjom. Okazuje się też, że dysjunkcja nie zachowuje niezwrotności. Na zakończenie zbadajmy jeszcze, jakie związki zachodzą pomiędzy zwrotnością, antyzwrotnością i niezwrotnością.

Podstawowa zależność między nimi jest taka, że negacja relacji zwrotnej jest antyzwrotna, zaś negacja relacji antyzwrotnej jest zwrotna.

Każda relacja na typie pustym jest jednocześnie zwrotna i antyzwrotna, ale nie może taka być żadna relacja na typie niepustym.

Związek między niezwrotnością i antyzwrotnością jest nadzwyczaj prosty: każda relacja antyzwrotna na typie niepustym jest też niezwrotna.

Relacje symetryczne

Relacja jest symetryczna, jeżeli kolejność podawania argumentów nie ma znaczenia. Przykładami ze świata rzeczywistego mogą być np. relacje "jest blisko", "jest obok", "jest naprzeciwko".

Alterntywną charakteryzacją symetrii może być stwierdzenie, że relacja symetryczna to taka, która jest swoją własną odwrotnością.

Równość, relacja pełna i pusta są symetryczne.

Złożenie relacji symetrycznych nie musi być symetryczne.

Pozostałe operacje (odwracanie, koniunkcja, dysjunkcja, negacja) zachowują symetrię. Relacja antysymetryczna to przeciwieństwo relacji symetrycznej — jeżeli x jest w relacji z y, to y nie może być w relacji z x. Sporą klasę przykładów stanowią różne relacje służące do porównywania: "x jest wyższy od y", "x jest silniejszy od y", "x jest bogatszy od y".

Każda relacja na typie pustym jest antysymetryczna. Równość nie jest antysymetryczna, podobnie jak relacja pełna (ale tylko na typie niepustym). Relacja pusta jest antysymetryczna, gdyż przesłanka R x y występująca w definicji antysymetrii jest zawsze fałszywa.

Relacje przechodnie

Relacje równoważności

Relacje porządku (TODO)

Relacje słaboantysymetryczne

Relacje totalne

Porządki

Relacje gęste

Domknięcia (TODO)

Ogólne pojęcie domknięcia

Uwaga, najnowszy pomysł: przedstawić domknięcia w taki sposób, żeby niepostrzeżenie przywyczajały do monad.

Domknięcie zwrotne

Domknięcie symetryczne

Ćwiczenie (gorsze domknięcie symetryczne)

Przyjrzyj się poniższej alternatywnej definicji domknięcia symetrycznego. Udowodnij, że jest ona równoważna sc. Dlaczego jest ona gorsza niż sc?

Domknięcie zwrotnosymetryczne

Redukcje (TODO)

Redukacja zwrotna

Redukcja przechodnia

Redukacja zwrotno-przechodnia

Podsumowanie

Do obczajenia z biblioteki stdpp: