Rekursja dobrze ufundowana

Typy induktywne są jak domino - każdy term to jedna kostka, indukcja i rekursja odpowiadają zaś temu co tygryski lubią najbardziej, czyli reakcji łańcuchowej przewracającej wszystkie kostki. Typ unit to jedna biedna kostka, zaś bool to już dwie biedne kostki - true i false. W obu przypadkach nie dzieje się nic ciekawego - żeby wszystkie kostki się przewróciły, musimy pchnąć palcem każdą z osobna. Typ nat jest już ciekawszy - są dwa rodzaje kostek, 0 i S, a jeżeli pchniemy kostkę 0 i między kolejnymi kostkami jest odpowiedni odstęp, to równy szlaczek kolejnych kostek przewracać się będzie do końca świata. Podobnie dla typu list A mamy dwa rodzaje kostek - nil i cons, ale kostki rodzaju cons mają różne kolory - są nimi elementy typu A. Podobnie jak dla nat, jeżeli pchniemy kostkę nil i odstępy między kolejnymi kostkami są odpowiednie, to kostki będą przewracać się w nieskończoność. Tym razem jednak zamiast jednego szaroburego szlaczka będzie multum kolorowych szlaczków o wspólnych początkach (no chyba, że A = unit - wtedy dostaniemy taki sam bury szlaczek jak dla nat). Powyższe malownicze opisy przewracających się kostek domina bardziej przywodzą na myśl indukcję, niż rekursję, chociaż wiemy już, że jest to w sumie to samo. Przyjmują one perspektywę "od przodu" - jeżeli przewrócimy początkową kostkę i niczego nie spartaczyliśmy, kolejne kostki będą przewracać się już same. Co to znaczy, że niczego nie spartaczyliśmy, pytasz? Tutaj przydaje się spojrzenie na nasze domino "od tyłu". Żeby kostka domina się przewróciła, muszą przewrócić się na nią wszystkie bezpośrednio poprzedzające ją kostki, a żeby one się przewróciły, to przewrócić muszą się wszystkie poprzedzające je kostki i tak dalej. W związku z tym możemy powiedzieć, że kostka jest dostępna, jeżeli dostępne są wszystkie kostki ją poprzedzające. Jeszcze jeden drobny detal: kiedy dostępne są kostki, które nie mają żadnych poprzedzających kostek? Odpowiedź: zawsze, a dowodem na to jest nasz palec, który je przewraca. W ten oto wesoły sposób udało nam się uzyskać definicję elementu dostępnego oraz relacji dobrze ufundowanej.

Kostki domina reprezentuje typ A, zaś relacja R to sposób ułożenia kostek, a x to pewna konkretna kostka domina. Konstruktor Acc_intro mówi, że kostka x jest dostępna w układzie domina R, jezeli każda kostka y, która poprzedza ją w układzie R, również jest dostępna. Mniej poetycko: element x : A jest R-dostępny, jeżeli każdy R-mniejszy od niego element y : A również jest R-dostępny.

Układ kostek reprezentowany przez R jest niespartaczony, jeżeli każda kostka domina jest dostępna. Mniej poetycko: relacja R jest dobrze ufundowana, jeżeli każde x : A jest R-dostępne. Uwaga: typem naszego układu kostek nie jest A -> A -> Prop, lecz A -> A -> Type, a zatem R jest tak naprawdę indeksowaną rodziną typów, a nie relacją. Różnica między relacją i rodziną typów jest taka, że relacja, gdy dostanie argumenty, zwraca zdanie, czyli coś typu Prop, a rodzina typów, gdy dostanie argumenty, zwraca typ, czyli coś typu Type. Tak więc pojęcie rodziny typów jest ogólniejsze niż pojęcie relacji. Ta ogólność przyda się nam za kilka chwil aby nie musieć pisać wszystkiego dwa razy.

Ćwiczenie

Sprawdź, czy relacje <=, < są dobrze ufundowane.

Ćwiczenie

Pokaż, że relacja dobrze ufundowana jest antyzwrotna oraz zinterpretuj ten fakt (tzn. powiedz, o co tak naprawdę chodzi w tym stwierdzeniu).

Ćwiczenie

Sprawdź, czy dobrze ufundowana jest następująca relacja porządku: wszystkie liczby parzyste są mniejsze niż wszystkie liczby nieparzyste, zaś dwie liczby o tej samej parzystości porównujemy według zwykłego porządku <.

Ćwiczenie

Sprawdź, czy dobrze ufundowana jest następująca relacja porządku (mam nadzieję, że obrazek jest zrozumiały): 0 < 1 < ... < ω < ω + 1 < ... < 2 * ω Oczywiście najpierw musisz wymyślić, w jaki sposób zdefiniować taką relację. Uwaga: istnieje bardzo sprytne rozwiązanie.

Nasza bajka powoli zbliża się do końca. Czas udowodnić ostateczne twierdzenie, do którego dążyliśmy: jeżeli układ kostek R jest niespartaczony (czyli gdy każda kostka jest dostępna), to każda kostka się przewraca.

Podobnie jak poprzednio, A to typ kostek domina, R to układ kostek, zaś wf : well_founded R to dowód na to, że układ jest niespartaczony. P : A -> Type to dowolna rodzina typów indeksowana przez A, ale możemy myśleć, że P x znaczy "kostka x się przewraca". Mamy jeszcze hipotezę, która głosi, że kostka x przewraca się, gdy przewraca się każda kostka, która poprzedza ją w układzie R. Dowód jest banalny. Zaczynamy od wprowadzenia zmiennych i hipotez do kontekstu. Następnie odwijamy definicję well_founded. Teraz hipoteza wf głosi, że każde x : A jest dostępne. Skoro tak, to specjalizujemy ją dla naszego konkretnego x, które mamy w kontekście. Wiemy już zatem, że x jest dostępne. Jest to kluczowy fakt, gdyż oznacza to, że wszystkie kostki domina poprzedzające x również są dostępne. Co więcej, Acc jest zdefiniowane induktywnie, więc możemy pokazać, że x się przewraca, właśnie przez indukcję po dowodzie dostępności x. Przypadek jest jeden (co nie znaczy, że nie ma przypadków bazowych - są nimi kostki domina, których nic nie poprzedza): musimy pokazać, że x się przewraca przy założeniu, że wszystkie poprzedzające je kostki również się przewracają. To, że x się przewraca, wynika z hipotezy H. Pozostaje nam jedynie pokazać, że przewraca się wszystko, co jest przed nim, ale to jest faktem na mocy hipotezy indukcyjnej IH.

Poprzednie twierdzenie, czyli well_founded_rect, to twierdzenie o rekursji dobrze ufundowanej. Powyższe, czyli well_founded_ind, które jest jego specjalizacją dla relacji binarnych (czyli bytów o typie A -> A -> Prop), możemy nazwać twierdzeniem o indukcji dobrze ufundowanej. Upewnij się, że dobrze rozumiesz oba twierdzenia, a także pojęcia dostępności i dobrego ufundowania, gdyż są one bardzo ważne przy rozwiązywaniu poważniejszych problemów. Co to są "poważniejsze problemy"? Mam oczywiście na myśli dowodzenie twierdzeń i definiowanie funkcji, którego nie da się zrobić za pomocą prostej indukcji albo banalnego dopasowania do wzorca. W tego typu sytuacjach nieodzowne będzie skorzystanie z indukcji i rekursji dobrze ufundowanej, o czym przekonamy się już natychmiast zaraz.

Poważniejszym problemem jest bowiem definicja dzielenia, z którą borykamy się od samiuśkiego początku niniejszego rozdziału. Powyższy kawałek kodu jest (nieudaną, jak się okaże) próbą uporania się z tym problemem. Definiować będziemy w trybie dowodzenia, gdyż przy posługiwaniu się rekursją dobrze ufundowaną zazwyczaj tak jest dużo łatwiej. Zaczynamy od zaaplikowania reguły rekursji dobrze ufundowanej dla typu nat i porządku < (no i rzecz jasna wf_lt, czyli dowodu na to, że lt jest dobrze ufundowany - bez tego ani rusz). Po typach widać, że rekursja będzie się odbywać po pierwszym argumencie. Wprowadzamy też zmienne do kontekstu.

Następnie musimy sprawdzić, czy dzielna (czyli n) jest mniejsza od dzielnika (czyli S m - zauważ, że definiujemy tutaj "sprytną" wersję dzielenia, tzn. div n m = n/(m + 1), żeby uniknąć problemów z dzieleniem przez 0). Jeżeli tak, wynikiem jest 0. Jeżeli nie, wynikiem jest wynik wywołania rekurencyjnego na argumencie n - S m powiększony o 1. Na koniec musimy jeszcze tylko pokazać, że argument wywołania rekurencyjnego, czyli n - S m, jest mniejszy od argumentu obecnego wywołania, czyli n. Żeby za bardzo nie pobrudzić sobie rąk arytmetyką, zostawiamy ten cel taktyce lia, ale zawijamy jej użycie w kombinator abstract, który zapobiega "wylaniu się" rozumowania taktyki lia do definicji.

Mówiąc wprost, taktyka abstract lia zamiast wstawiać do definicji całe rozumowanie, tak jak zrobiłaby to taktyka lia, dowodzi sobie na boku odpowiedni lemat arytmetyczny, nazywa go div_subproof i dowodzi celu za jego pomocą.

Jak widać, definicja przechodzi bez problemu, a nasza funkcja elegancko się oblicza (pamiętaj, że div 5 2 to tak naprawdę 5/3, więc wynikiem faktycznie powinno być 1). Jednak nie samymi definicjami żyje człowiek - czas trochę podowodzić. Spodziewamy się wszakże, że nasze dzielenie spełnia wszystkie właściwości, których się po nim spodziewamy, prawda?

Niestety jednak, jak to w życiu, nie ma kolorowo. Powyższy lemat głosi, że n/1 = n. Ponieważ div jest zdefiniowane za pomocą rekursji dobrze ufundowanej, to dowodzić będziemy oczywiście za pomocą indukcji dobrze ufundowanej. Tak, będziemy dowodzić, hmmm... cóż... tylko jak? Sytuacja wygląda beznadziejnie. Nie żeby lemat był nieprawdziwy - co to, to nie. Po prostu próba odwinięcia definicji i policzenia czegokolwiek daje inny wynik, niż byśmy chcieli - część definicji ukryta dotychczas w div_subproof wylewa się i zaśmieca nam ekran. Problem nie pochodzi jednak od taktyki lia (ani od abstract lia). Jest on dużo ogólniejszy i polega na tym, że wewnątrz definicji funkcji pojawiają się dowody, które są wymagane przez well_founded_rect, ale które zaorywują jej obliczeniową harmonię. Nie jesteśmy jednak (jeszcze) skazani na porażkę. Spróbujemy uporać się z tą przeszkodą dzięki równaniu rekurencyjnemu. Równanie rekurencyjne to lemat, którego treść wygląda dokładnie tak, jak pożądana przez nas definicja funkcji, ale która nie może służyć jako definicja z różnych powodów, np. dlatego że nie jest strukturalnie rekurencyjna. Dzięki równaniu rekurencyjnemu możemy użyć taktyki rewrite do przepisania wystąpień funkcji div do pożądanej postaci zamiast rozwijać je za pomocą taktyki unfold lub obliczać za pomocą cbn.

Powyższe równanie dokładnie opisuje, jak powinna zachowywać się funkcja div, ale za definicję służyć nie może, gdyż Coq nie byłby w stanie rozpoznać, że n - S m jest podtermem n. Zauważ, że używamy tu <? (czyli ltb) zamiast le_lt_dec. Możemy sobie na to pozwolić, gdyż użycie le_lt_dec w faktycznej definicji wynikało jedynie z tego, że potrzebowaliśmy dowodu odpowiedniego faktu arytmetycznego, żeby użyć go jako argumentu wywołania rekurencyjnego. Niestety próba udowodnienia tego równania rekurencyjnego musi skończyć się taką samą porażką, jak próba udowodnienia div_0_r. Przyczyna jest taka sama jak ostatnio. Zresztą, naiwnym byłoby spodziewać się, że nam się uda - zarówno div_0_r, jak i div_eq to nietrywialne właściwości funkcji div, więc gdybyśmy potrafili udowodnić równanie rekurencyjne, to z dowodem div_0_r również poradzilibyśmy sobie bez problemu. Żeby jednak przekonać się o użyteczności równania rekurencyjnego, jego "dowód" kończymy za pomocą komendy Admitted, która przerywa dowód i zamienia twierdzenie w aksjomat. Dzięki temu za chwilę zobaczymy, ile moglibyśmy zdziałać, mając równanie rekurencyjne.

Jak widać, dzięki równaniu rekurencyjnemu dowody przebiegają dość gładko. W powyższym zaczynamy od indukcji dobrze ufundowanej po n (przy użyciu relacji < i dowodu wf_lt), wprowadzamy zmienne do kontekstu, po czym przepisujemy równanie rekurencyjne. Po przeprowadzeniu analizy przypadków kończymy za pomocą rozumowań arytmetycznych, używając być może hipotezy indukcyjnej.

Ćwiczenie

Zgadnij, jakie jest polecenie tego ćwiczenia, a następnie wykonaj je.

Ćwiczenie

Sprawdź, czy dobrze ufundowane są relacje le' i lt'. Uwaga: pierwsze zadanie jest bardzo łatwe, drugie jest piekielnie trudne. Jeżeli nie potrafisz rozwiązać go formalnie w Coqu, zrób to na kartce nieformalnie - będzie dużo łatwiej.

Ćwiczenie

Niech B : Type i niech R : B -> B -> Prop będzie relacją dobrze ufundowaną. Zdefiniuj po współrzędnych relację porządku na funkcjach o typie A -> B i rozstrzygnij, czy relacja ta jest dobrze ufundowana. Uwaga: w zależności od okoliczności to zadanie może być trudne lub łatwe.

Ćwiczenie

Pokaż, że jeżeli kodziedzina funkcji f : A -> B jest dobrze ufundowana za pomocą relacji R : B -> B -> Prop, to jej dziedzina również jest dobrze ufundowana.