W tym rozdziale zapoznamy się z najważniejszymi rodzajami funkcji. Trzeba przyznać na wstępie, że rozdział będzie raczej matematyczny (co wcale nie powinno cię odstraszać - matematyka jest świetna, a najbardziej praktyczną rzeczą w kosmosie jest dobra teoria).

Funkcje

Potrafisz już posługiwać się funkcjami. Mimo tego zróbmy krótkie przypomnienie. Typ funkcji (niezależnych) z A w B oznaczamy przez A -> B. W Coqu funkcje możemy konstruować za pomocą abstrakcji (np. fun n : nat => n + n) albo za pomocą rekursji strukturalnej. Eliminować zaś możemy je za pomocą aplikacji: jeżeli f : A -> B oraz x : A, to f x : B. Funkcje wyrażają ideę przyporządkowania: każdemu elementowi dziedziny funkcja przyporządkowuje element przeciwdziedziny. Jednak status dziedziny i przeciwdziedziny nie jest taki sam: każdemu elementowi dziedziny coś odpowiada, jednak mogą istnieć elementy przeciwdziedziny, które nie są obrazem żadnego elementu dziedziny. Co więcej, w Coqu wszystkie funkcje są konstruktywne, tzn. mogą zostać obliczone. Jest to coś, co bardzo mocno odróżnia Coqa oraz rachunek konstrukcji (jego teoretyczną podstawę) od innych systemów formalnych.

Najważniejszą rzeczą, jaką możemy zrobić z funkcją, jest zaaplikowanie jej do argumentu. Jest to tak częsta operacja, że zdefiniujemy sobie dwie notacje, które pozwolą nam zaoszczędzić kilka stuknięć w klawiaturę. Notacja $ (pożyczona z języka Haskell) będzie nam służyć do niepisania nawiasów: jeżeli argumentami funkcji będą skomplikowane termy, zamiast pisać wokół nich parę nawiasów, będziemy mogli wstawić tylko jeden symbol dolara "$". Dzięki temu zamiast 2n nawiasów napiszemy tylko n znaków "$" (choć trzeba przyznać, że będziemy musieli pisać więcej spacji). Notacja |> (pożyczona z języka F#) umożliwi nam pisanie aplikacji w odwrotnej kolejności. Dzięki temu będziemy mogli np. pomijać nawiasy w abstrakcji. Jako, że nie da się zrobić notacji w stylu "x f", jest to najlepsze dostępne nam rozwiązanie.

Drugą najważniejszą operacją, jaką możemy wykonywać na funkcjach, jest składanie. Jedynym warunkiem jest aby przeciwdziedzina pierwszej funkcji była taka sama, jak dziedzina drugiej funkcji.

Składanie funkcji jest łączne. Zagadka: czy jest przemienne? Uwaga techniczna: jeżeli prezentuję jakieś twierdzenie bez dowodu, to znaczy, że dowód jest ćwiczeniem.

Najważniejszą funkcją w całym kosmosie jest identyczność. Jest to funkcja, która nie robi zupełnie nic. Jej waga jest w tym, że jest ona elementem neutralnym składania funkcji.

Funkcja stała to funkcja, która ignoruje swój drugi argument i zawsze zwraca pierwszy argument.

flip to całkiem przydatny kombinator (funkcja wyższego rzędu), który zamienia miejscami argumenty funkcji dwuargumentowej.

Ostatnim przydatnim kombinatorem jest iter. Służy on do składania funkcji samej ze sobą n razy. Oczywiście funkcja, aby można ją było złożyć ze sobą, musi mieć identyczną dziedzinę i przeciwdziedzinę.

Aksjomat ekstensjonalności

Ważną kwestią jest ustalenie, kiedy dwie funkcje są równe. Zacznijmy od tego, że istnieją dwie koncepcje równości:

• intensjonalna — funkcje są zdefiniowane przez identyczne (czyli konwertowalne) wyrażenia
• ekstensjonalna — wartości funkcji dla każdego argumentu są równe

Podstawowym i domyślnym rodzajem równości w Coqu jest równość intensjonalna, której właściwości już znasz. Każda funkcja, na mocy konstruktora eq_refl, jest równa samej sobie. Prawdą jest też mniej oczywisty fakt: każda funkcja jest równa swojej η-ekspansji.

η-ekspansja funkcji f to nic innego, jak funkcja anonimowa, która bierze x i zwraca f x. Nazwa pochodzi od greckiej litery η (eta). Powyższe twierdzenie jest trywialne, gdyż równość zachodzi na mocy konwersji. Warto podkreślić, że jego prawdziwość nie zależy od żadnych aksjomatów. Stwierdzenie to możemy zweryfikować za pomocą komendy Print Assumptions, która wyświetla listę aksjomatów, które zostały wykorzystane w definicji danego termu. Napis "Closed under the global context" oznacza, że żadnego aksjomatu nie użyto.

Równość intensjonalna ma jednak swoje wady. Główną z nich jest to, że jest ona bardzo restrykcyjna. Widać to dobrze na powyższym przykładzie: nie jesteśmy w stanie udowodnić, że funkcje fun n : nat => 1 + n oraz fun n : nat => n + 1 są równe, gdyż zostały zdefiniowane za pomocą innych termów. Mimo, że termy te są równe, to nie są konwertowalne, a zatem funkcje też nie są konwertowalne. Nie znaczy to jednak, że nie są równe — po prostu nie jesteśmy w stanie w żaden sposób pokazać, że są.

Z tarapatów wybawić nas może jedynie aksjomat ekstensjonalności dla funkcji, zwany w Coqu functional_extensionality (dla funkcji, które nie są zależne) lub functional_extensionality_dep (dla funkcji zależnych). Aksjomat ten głosi, że f i g są równe, jeżeli są równe dla wszystkich argumentów. Jest on bardzo użyteczny, a przy tym nie ma żadnych smutnych konsekwencji i jest kompatybilny z wieloma innymi aksjomatami. Z tych właśnie powodów jest on jednym z najczęściej używanych w Coqu aksjomatów. My też będziemy go wykorzystywać.

Sposób użycia aksjomatu jest banalnie prosty. Jeżeli mamy cel postaci f = g, to taktyka extensionality x przekształca go w cel postaci f x = g x, o ile tylko nazwa x nie jest już wykorzystana na coś innego. Dzięki zastosowaniu aksjomatu nie musimy już polegać na konwertowalności termów definiujących funkcje. Wystarczy udowodnić, że są one równe. W tym przypadku robimy to za pomocą twierdzenia plus_comm.

Ćwiczenie

Użyj aksjomatu ekstensjonalności, żeby pokazać, że dwie funkcje binarne są równe wtedy i tylko wtedy, gdy ich wartości dla wszystkich argumentów są równe.

Odwrotności i izomorfizmy (TODO)

W tym podrozdziale zajmiemy się pojęciem funkcji odwrotnej i płynącą z niego mądrością.

Intuicja jest dość prosta: wiemy ze szkoły, że na liczbach całkowitych odejmowanie jest odwrotnością dodawania (np. a + b - b = a), tzn. jeżeli do a dodamy b, a potem odejmiemy b, to znowu mamy a. Podobnie w liczbach rzeczywistych mnożenie przez liczbę niezerową ma odwrotność w postaci dzielenia, np. (x * y) / y = x. Oczywiście pojęcie odwrotności dotyczy nie tylko działań na liczbach, ale także dowolnych funkcji - g jest odwrotnością f, gdy odwraca ono działanie f dla dowolnego argumentu a, tzn. najpierw mamy a, potem aplikujemy f i mamy f a, zaś na koniec aplikujemy g i znów mamy a, czyli g (f a) = a. To właśnie jest napisane w definicji has_postinverse. No właśnie - powyższy opis jest opisem postodwrotności. Nazwa wynika z kolejności - g jest postodwrotnością f, gdy najpierw aplikujemy f, a potem odwracamy jego działanie za pomocą g (po łacinie "post" znaczy "po", np. "post meridiem" znaczy "po południu"). Analogicznie, choć może nieco mniej intuicyjnie, prezentuje się definicja preodwrotności (po łacinie "prae" znaczy "przed"). g jest preodwrotnością f, gdy f jest postodwrotnością g. Innymi słowy: f ma preodwrotność, jeżeli odwraca ono działanie jakiejś funkcji. Dobra, wystarczy gadania. Czas na ćwiczenia.

Ćwiczenie

Pokaż, że odjęcie n jest postodwrotnością dodania n. Czy jest także preodwrotnością?

Zauważ, że sortem has_preinverse i has_postinverse jest Type, nie zaś Prop. Jest tak dlatego, że o ile stwierdzenie "f jest pre/post odwrotnością g" jest zdaniem, to posiadanie odwrotności już nie, gdyż dana funkcja może mieć wiele różnych odwrotności.

Ćwiczenie

Rozważmy funkcję app [1; 2; 3], która dokleja na początek listy liczb naturalnych listę [1; 2; 3]. Znajdź dwie różne jej postodwrotności (nie musisz formalnie dowodzić, że są różne - wystarczy nieformalny argument). Czy funkcja ta ma preodwrotność?

Ćwiczenie

Czasem funkcja może mieć naprawdę dużo odwrotności. Pokaż, że funkcja cons x dla x : A ma ich nieskończenie wiele. Nie musisz dowodzić, że odwrotności są różne (ani że jest ich dużo), jeżeli widać to na pierwszy rzut oka.

Ćwiczenie

Dla listowych funkcji widzieliśmy postodwrotności, ale nie widzieliśmy preodwrotności. Może więc preodwrotności nie istnieją? Otóż nie tym razem! Dla jakich n funkcja cycle n ma (pre/post)odwrotność?

Skracalność (TODO)

Injekcje

Objaśnienia zacznijmy od nazwy. Po łacinie "iacere" znaczy "rzucać", zaś "in" znaczy "w, do". W językach romańskich samo słowo "injekcja" oznacza zaś zastrzyk. Bliższym matematycznemu znaczeniu byłoby jednak tłumaczenie "wstrzyknięcie". Jeżeli funkcja jest injekcją, to możemy też powiedzieć, że jest "injektywna". Inną nazwą jest "funkcja różnowartościowa". Na wiki można zapoznać się z obrazkami poglądowymi: https://en.wikipedia.org/wiki/Bijection,%20injection%20and%20surjection Podstawowa idea jest prosta: jeżeli funkcja jest injekcją, to identyczne jej wartości pochodzą od równych argumentów. Przekonajmy się na przykładzie.

Funkcja fun n : nat => 2 + n, czyli dodanie 2 z lewej strony, jest injekcją, gdyż jeżeli 2 + n = 2 + n', to rozwiązując równanie dostajemy n = n'. Jeżeli wartości funkcji są równe, to argumenty również muszą być równe. Zobaczmy też kontrprzykład.

Funkcja f(n) = n^2 - n nie jest injekcją, gdyż mamy zarówno f(0) = 0 jak i f(1) = 0. Innymi słowy: są dwa nierówne argumenty (0 i 1), dla których wartość funkcji jest taka sama (0). A oto alternatywna definicja.

Głosi ona, że funkcja injektywna to funkcja, która dla różnych argumentów przyjmuje różne wartości. Innymi słowy, injekcja to funkcja, która zachowuje relację <>. Przykład 1 możemy sparafrazować następująco: jeżeli n jest różn od n', to wtedy 2 + n jest różne od 2 + n'. Definicja ta jest równoważna poprzedniej, ale tylko pod warunkiem, że przyjmiemy logikę klasyczną. W logice konstruktywnej pierwsza definicja jest lepsza od drugiej.

Ćwiczenie

Pokaż, że injective jest mocniejsze od injective'. Pokaż też, że w logice klasycznej są one równoważne.

Udowodnij, że różne funkcje są lub nie są injektywne.

Jedną z ważnych właściwości injekcji jest to, że są składalne: złożenie dwóch injekcji daje injekcję.

Ta właściwość jest dziwna. Być może kiedyś wymyślę dla niej jakąś bajkę.

Na zakończenie należy dodać do naszej interpretacji pojęcia "injekcja" jeszcze jedną ideę. Mianowicie jeżeli istnieje injekcja f : A -> B, to ilość elementów typu A jest mniejsza lub równa liczbie elementów typu B, a więc typ A jest w pewien sposób mniejszy od B. f musi przyporządkować każdemu elementowi A jakiś element B. Gdy elementów A jest więcej niż B, to z konieczności któryś z elementów B będzie obrazem dwóch lub więcej elementów A. Wobec powyższego stwierdzenie "złożenie injekcji jest injekcją" możemy zinterpretować po prostu jako stwierdzenie, że relacja porządku, jaką jest istnienie injekcji, jest przechodnia. (TODO: to wymagałoby relacji jako prerekwizytu).

Ćwiczenie

Udowodnij, że nie istnieje injekcja z bool w unit. Znaczy to, że bool ma więcej elementów, czyli jest większy, niż unit.

Pokaż, że istnieje injekcja z typu pustego w każdy inny. Znaczy to, że Empty_set ma nie więcej elementów, niż każdy inny typ (co nie powinno nas dziwić, gdyż Empty_set nie ma żadnych elementów).

Surjekcje

Drugim ważnym rodzajem funkcji są surjekcje.

I znów zacznijmy od nazwy. Po francusku "sur" znaczy "na", zaś słowo "iacere" już znamy (po łac. "rzucać"). Słowo "surjekcja" moglibyśmy więc przetłumaczyć jako "pokrycie". Tym bowiem w istocie jest surjekcja — jest to funkcja, która "pokrywa" całą swoją przeciwdziedzinę. Owo "pokrywanie" w definicji wyraziliśmy w ten sposób: dla każdego elementu b przeciwdziedziny B istnieje taki element a dziedziny A, że f a = b. Zobaczmy przykład i kontrprzykład.

Powyższe twierdzenie głosi, że "funkcja pred jest surjekcją", czyli, parafrazując, "każda liczba naturalna jest poprzednikiem innej liczby naturalnej". Nie powinno nas to zaskakiwać, wszakże każda liczba naturalna jest poprzednikiem swojego następnika, tzn. pred (S n) = n.

Surjekcją nie jest za to konstruktor S. To również nie powinno nas dziwić: istnieje przecież liczba naturalna, która nie jest następnikiem żadnej innej. Jest nią oczywiście zero. Surjekcje cieszą się właściwościami podobnymi do tych, jakie są udziałem injekcji.

Ćwiczenie

Pokaż, że złożenie surjekcji jest surjekcją. Udowodnij też "dziwną właściwość" surjekcji.

Ćwiczenie

Zbadaj, czy wymienione funkcje są surjekcjami. Sformułuj i udowodnij odpowiednie twierdzenia. Funkcje: identyczność, dodawanie (rozważ zero osobno), odejmowanie, mnożenie (rozważ 1 osobno).

Tak jak istnienie injekcji f : A -> B oznacza, że A jest mniejszy od B, gdyż ma mniej (lub tyle samo) elementów, tak istnieje surjekcji f : A -> B oznacza, że A jest większy niż B, gdyż ma więcej (lub tyle samo) elementów. Jest tak na mocy samej definicji: każdy element przeciwdziedziny jest obrazem jakiegoś elementu dziedziny. Nie jest powiedziane, ile jest tych elementów, ale wiadomo, że co najmniej jeden. Podobnie jak w przypadku injekcji, fakt że złożenie surjekcji jest surjekcją możemy traktować jako stwierdzenie, że porządek, jakim jest istnienie surjekcji, jest przechodni. (TODO)

Ćwiczenie

Pokaż, że nie istnieje surjekcja z unit w bool. Oznacza to, że unit nie jest większy niż bool.

Pokaż, że istnieje surjekcja z każdego typu niepustego w unit. Oznacza to, że każdy typ niepusty ma co najmniej tyle samo elementów, co unit, tzn. każdy typ nie pusty ma co najmniej jeden element.

Bijekcje

Po łacinie przedrostek "bi-" oznacza "dwa". Bijekcja to funkcja, która jest zarówno injekcją, jak i surjekcją.

Pozostawię przykłady bez komentarza — są one po prostu konsekwencją tego, co już wiesz na temat injekcji i surjekcji. Ponieważ bijekcja jest surjekcją, to każdy element jej przeciwdziedziny jest obrazem jakiegoś elementu jej dziedziny (obraz elementu x to po prostu f x). Ponieważ jest injekcją, to element ten jest unikalny. Bijekcja jest więc taką funkcją, że każdy element jej przeciwdziedziny jest obrazem dokładnie jednego elementu jej dziedziny. Ten właśnie fakt wyraża poniższa definicja alternatywna. TODO: exists! nie zostało dotychczas opisane, a chyba nie powinno być opisane tutaj.

Ćwiczenie

Udowodnij, że obie definicje są równoważne.

Ćwiczenie

Funkcja unary reprezentuje liczbę naturalną n za pomocą listy zawierającej n kopii termu tt. Udowodnij, że unary jest bijekcją.

Jak już powiedzieliśmy, bijekcje dziedziczą właściwości, które mają zarówno injekcje, jak i surjekcje. Wobec tego możemy skonkludować, że złożenie bijekcji jest bijekcją. Nie mają one jednak "dziwnej własciwości". TODO UWAGA: od teraz twierdzenia, które pozostawię bez dowodu, z automatu stają się ćwiczeniami.

Bijekcje mają też interpretacje w idei rozmiaru oraz ilości elementów. Jeżeli istnieje bijekcja f : A -> B, to znaczy, że typy A oraz B mają dokładnie tyle samo elementów, czyli są "tak samo duże". Nie powinno nas zatem dziwić, że relacja istnienia bijekcji jest relacją równoważności:

• każdy typ ma tyle samo elementów, co on sam
• jeżeli typ A ma tyle samo elementów co B, to B ma tyle samo elementów, co A
• jeżeli A ma tyle samo elementów co B, a B tyle samo elementów co C, to A ma tyle samo elementów co C

Ćwiczenie

Jeżeli między A i B istnieje bijekcja, to mówimy, że A i B są równoliczne (ang. equipotent). Pokaż, że relacja równoliczności jest relacją równoważności. TODO: prerekwizyt: relacje równoważności

Równoliczność A i B będziemy oznaczać przez A ~ B. Nie należy notacji ~ mylić z notacją ~ oznaczającej negację logiczną. Ciężko jednak jest je pomylić, gdyż pierwsza zawsze bierze dwa argumenty, a druga tylko jeden.

Inwolucje

Kolejnym ważnym (choć nie aż tak ważnym) rodzajem funkcji są inwolucje. Po łacinie "volvere" znaczy "obracać się". Inwolucja to funkcja, która niczym Chuck Norris wykonuje półobrót — w tym sensie, że zaaplikowanie jej dwukrotnie daje cały obrót, a więc stan wyjściowy. Mówiąc bardziej po ludzku, inwolucja to funkcja, która jest swoją własną odwrotnością. Spotkaliśmy się już z przykładami inwolucji: najbardziej trywialnym z nich jest funkcja identycznościowa, bardziej oświecającym zaś funkcja rev, która odwraca listę — odwrócenie listy dwukrotnie daje wyjściową listę. Inwolucją jest też negb.

Żeby nie odgrzewać starych kotletów, przyjrzyjmy się funkcji weird.

Funkcja ta zamienia miejscami bloki elementów listy o długości dwa. Nietrudno zauważyć, że dwukrotne takie przestawienie jest identycznością. UWAGA TODO: dowód wymaga specjalnej reguły indukcyjnej.

Inwolucją jest też kombinator flip, który poznaliśmy na początku rozdziału. Przypomnijmy, że zamienia on miejscami argumenty funkcji binarnej. Nie dziwota, że dwukrotna taka zamiana daje oryginalną funkcję.

Okazuje się, że złożenie inwolucji wcale nie musi być inwolucją. Wynika to z faktu, że funcje weird i rev są w pewien sposób niekompatybilne — pierwsze wywołanie każdej z nich przeszkadza drugiemu wywołaniu drugiej z nich odwrócić efekt pierwszego wywołania.

Kryterium to jest rozstrzygające — jeżeli inwolucje komutują ze sobą (czyli są "kompatybilne", f .> g = g .> f), to ich złożenie również jest inwolucją.

Ponieważ każda inwolucja ma odwrotność (którą jest ona sama), każda inwolucja jest z automatu bijekcją.

Ćwiczenie

Rozważmy funkcje rzeczywiste f(x) = ax^n, f(x) = ax^(-n), f(x) = sin(x), f(x) = cos(x), f(x) = a/x, f(x) = a - x, f(x) = e^x. Które z nich są inwolucjami?

Uogólnione inwolucje

Pojęcie inwolucji można nieco uogólnić. Żeby to zrobić, przeformułujmy najpierw definicję inwolucji.

Nowa definicja głosi, że inwolucja to taka funkcja, że jej złożenie ze sobą jest identycznością. Jeżeli funkcje f .> f i id A zaaplikujemy do argumentu x, otrzymamy oryginalną definicję. Nowa definicja jest równoważna starej na mocy aksjomatu ekstensjonalności dla funkcji.

Pójdźmy o krok dalej. Zamiast składania .> użyjmy kombinatora iter 2, który ma taki sam efekt.

Droga do uogólnienia została już prawie przebyta. Nasze dotychczasowe inwolucje nazwiemy uogólnionymi inwolucjami rzędu 2. Definicję uogólnionej inwolucji otrzymamy, zastępując w definicji 2 przez n.

Nie żeby pojęcie to było jakoś szczególnie często spotykane lub nawet przydatne — wymyśliłem je na poczekaniu. Spróbujmy znaleźć jakąś uogólnioną inwolucję o rzędzie większym niż 2.

Idempotencja

Kolejnym rodzajem funkcji są funkcje idempotente. Po łacinie "idem" znaczy "taki sam", zaś "potentia" oznacza "moc". Funkcja idempotentna to taka, której wynik jest taki sam niezależnie od tego, ile razy zostanie zaaplikowana. Przykłady można mnożyć. Idempotentne jest wciśnięcie guzika w windzie — jeżeli np. wciśniemy "2", to po wjechaniu na drugi piętro kolejne wciśnięcia guzika "2" nie będą miały żadnego efektu. Idempotentne jest również sortowanie. Jeżeli posortujemy listę, to jest ona posortowana i kolejne sortowania niczego w niej nie zmienią. Problemem sortowania zajmiemy się w przyszłych rozdziałach.

Identyczność jest idempotentna — niezrobienie niczego dowolną ilość razy jest wszakże ciągle niezrobieniem niczego. Podobnież funkcja stała jest idempotentna — zwracanie tej samej wartości daje zawsze ten sam efekt, niezależnie od ilości powtórzeń. Ciekawszym przykładem, który jednak nie powinien cię zaskoczyć, jest funkcja take dla dowolnego n : nat. Wzięcie n elementów z listy l daje nam listę mającą co najwyżej n elementów. Próba wzięcia n elementów z takiej listy niczego nie zmieni, gdyż jej długość jest mniejsza lub równa ilości elementów, które chcemy wziąć.

Jeżeli chodzi o składanie funkcji idempotentnych, sytuacja jest podobna do tej, jaka jest udziałem inwolucji.

Skracalność (TODO)

Tutaj o lewej i prawej skracalności, czyli mono- i epi- morfizmy.