W poprzednim rozdziale dość dogłębnie zapoznaliśmy się z mechanizmem definiowania induktywnych typów i rodzin typów. Nauczyliśmy się też definiować funkcje operujące na ich elementach za pomocą dopasowania do wzorca oraz rekursji. Indukcja i rekursja są ze sobą bardzo ściśle powiązane. Obie opierają się na autoreferencji, czyli odnoszeniu się do samego siebie:

• liczba naturalna to zero lub następnik liczby naturalnej
• długość listy złożonej z głowy i ogona to jeden plus długość ogona

Można użyć nawet mocniejszego stwierdzenia: indukcja i rekursja są dokładnie tym samym zjawiskiem. Skoro tak, dlaczego używamy na jego opisanie dwóch różnych słów? Cóż, jest to zaszłość historyczna, jak wiele innych, które napotkaliśmy. Rozróżniamy zdania i typy/specyfikacje, relacje i rodziny typów, dowody i termy/programy etc., choć te pierwsze są specjalnymi przypadkami tych drugich. Podobnie indukcja pojawiła się po raz pierwszy jako technika dowodzenia faktów o liczbach naturalnych, zaś rekursja jako technika pisania programów. Dla jasności, terminów tych będziemy używać w następujący sposób:

• indukcja będzie oznaczać metodę definiowania typów oraz metodę dowodzenia
• rekursja będzie oznaczać metodę definiowania funkcji

W tym rozdziale zbadamy dokładniej rekursję: poznamy różne jej rodzaje, zobaczymy w jaki sposób za jej pomocą można zrobić własne niestandardowe reguły indukcyjne, poznamy rekursję (i indukcję) dobrze ufundowaną oraz zobaczymy, w jaki sposób połączyć indukcję i rekursję, by móc dowodzić poprawności pisanych przez nas funkcji wciśnięciem jednego przycisku (no, prawie). Zanim jednak to nastąpi, rzućmy okiem na rekursję z dwóch odmiennych perspektyw.

Rekursja jako najlepszość

Znamy już podstawowe typy induktywne, jak liczby naturalne oraz listy elementów typu A. Wiemy też, że ich induktywność objawia się głównie w tym, że możemy definiować funkcje przez rekursję strukturalną po argumentach tych typów oraz dowodzić przez indukcję. W takim podejściu indukcja i sama induktywność typów induktywnych wydają się być czymś w rodzaju domina - wystarczy popchnąć pierwsze kilka kostek (przypadki bazowe) i zapewnić, że pozostałe kostki są dobrze ułożone (przypadki rekurencyjne), aby zainicjować reakcję łańcuchową, która będzie przewracać kostki w nieskończoność. Nie jest to jednak jedyny sposób patrzenia na typy induktywne. W tym podrozdziale spróbuję przedstawić inny sposób patrzenia, w którym typ induktywny to najlepszy typ do robienia termów o pewnym kształcie, a rekursja to zmiana kształtu z lepszego na gorszy, ale bardziej użyteczny. Żeby móc patrzeć z tej perspektywy musimy najpierw ustalić, czym jest kształt. Uwaga: "kształt" nie jest pojęciem technicznym i nie ma ścisłej definicji - używam tego słowa, żeby ułatwić pracę twojej wyobraźni. Czym jest kształt termu? Najprościej rzecz ujmując każdy term jest drzewkiem, którego korzeniem jest jakiś konstrukt językowy (stała, konstruktor, uprzednio zdefiniowana funkcja, dopasowanie do wzorca, let, lub cokolwiek innego), a jego poddrzewa to argumenty tego konstruktu. Dla przykładu, termy typu nat mogą mieć takie kształty:

• 0 - stała
• S (S (S 0)) - konstruktor
• plus 0 5, mult 0 5 - uprzednio zdefiniowana funkcja
• if andb false false then 42 else S 42 - if
• match 0 with | 0 => 666 | S _ => 123 - dopasowanie do wzorca
• length [true; false] - uprzednio zdefiniowana funkcja
• let x := Prop in 16 - let
• ... i wiele, wiele innych!

Tak wiele różnych sposobów robienia termów to niesamowite bogactwo, więc żeby zgodnie z przysłowiem od tego przybytku nie rozbolała nas głowa, musimy pomyśleć o nich w nieco bardziej jednorodny sposób. Rozwiązanie jest na szczęście bajecznie proste: zauważ, że wszystkie powyższe konstrukty językowe można po prostu zawinąć w funkcję, która bierze pewną liczbę argumentów (być może zero) i zwraca coś typu nat. To jednak nie w pełni mityguje przyszły-niedoszły ból głowy. O ile mamy teraz jednorodny sposób myślenia o kształtach termów, to i tak kształtów tych mogą być olbrzymie ilości. Z tego powodu dokonamy samoograniczenia i zamiast o wszystkich możliwych kształtach termów będziemy wybiórczo skupiać naszą uwagę tylko na tych kształtach, które akurat będą nas interesować. Dla przykładu, możemy interesować się termami typu nat zrobionymi wyłącznie za pomocą:

• konstruktorów 0 i S
• konstruktora 0, stałej 1 oraz funkcji plus 2
• funkcji plus i stałych 5 oraz 42
• funkcji mult i stałej 1
• funkcji length : list nat -> nat

Ćwiczenie

Narysuj jakieś nietrywialne termy typu nat o takich kształtach.

Ćwiczenie

Liczbę n da się wyrazić za pomocą termu t, jeżeli t oblicza się do n, tzn. komenda Compute t daje w wyniku n. Pytanie: termy o których z powyższych kształtów mogą wyrazić wszystkie liczby naturalne?

Ćwiczenie

Liczba n ma unikalną reprezentację za pomocą termów o danym kształcie, gdy jest tylko jeden term t, który reprezentuje n. Pytanie: które z powyższych sposobów unikalnie reprezentują wszystkie liczby naturalne? Sporo już osiągnęliśmy w wyklarowywaniu pojęcia kształtu, ale zatrzymajmy się na chwilę i zastanówmy się, czy jest ono zgodne z naszymi intuicjami. Okazuje się, że otóż nie do końca, bo w naszej obecnej formulacji kształty (0, plus) oraz (1, mult) są różne, podczas gdy obrazki (narysuj je!) jasno pokazują nam, że np. plus 0 (plus 0 0) oraz mult 1 (mult 1 1) wyglądają bardzo podobnie, tylko nazwy są różne. Dlatego też modyfikujemy nasze pojęcie kształtu - teraz kształtem zamiast stałych i funkcji, jak 0 i plus, nazywać będziemy typy tych stałych i funkcji. Tak więc kształtem termów zrobionych z 0 i plus będzie nat (bo 0 : nat) i nat -> nat -> nat (bo plus : nat -> nat -> nat). Teraz jest już jasne, że 1 i mult dają dokładnie ten sam kształt, bo typem 1 jest nat, zaś typem mult jest nat -> nat -> nat. Zauważmy, że można nasze pojęcie kształtu jeszcze troszkę uprościć:

• po pierwsze, każdą stałą można traktować jako funkcję biorącą argument typu unit, np. możemy 0 : nat reprezentować za pomocą funkcji Z : unit -> nat zdefiniowanej jako Z := fun _ : unit => 0
• po drugie, funkcje biorące wiele argumentów możemy reprezentować za pomocą funkcji biorących jeden argument, np. plus : nat -> nat -> nat możemy reprezentować za pomocą plus' : nat * nat -> nat, który jest zdefiniowany jako plus' := fun '(n, m) => plus n m
• po trzecie, ponieważ kodziedzina wszystkich funkcji jest taka sama (w naszym przypadku nat), możemy połączyć wiele funkcji w jedną, np. 0 i plus możemy razem reprezentować jako Zplus : unit + nat * nat -> nat, zdefiniowaną jako Zplus := fun x => match x with | inl _ => 0 | inr (n, m) => plus n m end

Dzięki tym uproszczeniom (albo utrudnieniom, zależy kogo spytacie) możemy teraz jako kształt traktować nie funkcje albo same ich typy, lecz tylko jeden typ, który jest dziedziną takiej połączonej funkcji. Tak więc zarówno (0, plus) jak i (1, mult) są kształtu unit + nat * nat. Ma to sporo sensu: drzewa reprezentujące te termy są albo liściem (reprezentowanym przez unit), albo węzłem, który rozgałęzia się na dwa poddrzewa (reprezentowanym przez nat * nat). Ale to jeszcze nie wszystko. Przecież nat to nie jedyny typ, w którym można robić termy o kształcie unit + nat * nat. Jeżeli przyjrzymy się, jak wyglądają termy zrobione za pomocą (true, andb) albo (false, orb), to okaże się, że... mają one dokładnie ten sam kształt, mimo że według naszej definicji ich kształt to unit + bool * bool, czyli niby coś innego. Ostatnim stadium ewolucji naszego pojęcia kształtu jest taki oto zestaw definicji:

• kształt to funkcja F : Type -> Type
• realizacją kształtu F jest typ X oraz funkcja f : F X -> X

Widzimy teraz, że (0, plus), (1, mult), (true, andb) oraz (false, orb) nie są kształtami, lecz realizacjami kształtu F := fun X : Type => 1 + X * X. Pora powoli zmierzać ku konkluzji. Na początku powiedzieliśmy, że typ induktywny to najlepszy typ do robienia termów o pewnym kształcie. Jakim kształcie, zapytasz pewnie, i jak objawia się owa najlepszość? Czas się tego dowiedzieć. Definiując typ induktywny podajemy jego konstruktory, a całą resztę, czyli możliwość definiowania przez dopasowanie do wzorca i rekursję, reguły eliminacji etc. dostajemy za darmo. Nie dziwota więc, że to właśnie konstruktory są realizacją kształtu, którego dany typ jest najlepszym przykładem. Napiszmy to jeszcze raz, dla jasności: typ induktywny to najlepszy sposób robienia termów o kształcie realizowanym przez jego konstruktory. W naszym natowym przykładzie oznacza to, że nat jest najlepszym sposobem robienia termów o kształcie F := fun X => unit + X, czyli termów w kształcie "sznurków" (konstruktor S to taki supełek na sznurku, a 0 reprezentuje koniec sznurka). Są też inne realizacje tego sznurkowego kształtu, jak np. stała 42 : nat i funkcja plus 8 : nat -> nat albo stała true : bool i funkcja negb : bool -> bool, albo nawet zdanie False : Prop oraz negacja not : Prop -> Prop, ale żadna z nich nie jest najlepsza. Jak objawia się najlepszość typu induktywnego? Ano, dwojako:

• po pierwsze, objawia się w postaci rekursora, który bierze jako argument docelową realizację danego kształtu i przerabia term typu induktywnego, podmieniając najlepszą realizację na docelową
• po drugie, rekursor jest unikalny, czyli powyższa podmiana realizacji odbywa się w jedyny słuszny sposób

Żeby nie być gołosłownym, zobaczmy przykłady:

Tak wygląda rekursor dla liczb naturalnych. Widzimy, że "zmiana realizacji" termu o danym kształcie intuicyjnie polega na tym, że bierzemy term i zamieniamy 0 na z, a S na s, czyli dla przykładu liczba 4 (czyli S (S (S (S 0)))) zostanie zamieniona na s (s (s (s z))). Jeszcze konkretniejszy przykład: nat_rec' true negb zamieni liczbę S (S (S (S 0))) w negb (negb (negb (negb true))). Oczywiście term ten następnie oblicza się do true.

Ćwiczenie

Mamy nat_rec' true negb : nat -> bool, a zatem zmiana realizacji sznurka z (0, S) na (true, negb) odpowiada sprawdzeniu jakiejś właściwości liczb naturalnych. Jakiej? Pisząc wprost: zdefiniuj bezpośrednio przez rekursję taką funkcję f : nat -> bool, że forall n : nat, nat_rec' true negb n = f n (oczywiście musisz udowodnić, że wszystko się zgadza).

Uwaga: Coq domyślnie generuje dla typu "rekursor", ale ma on na myśli coś innego, niż my:

Coqowe nat_rec to w zasadzie to samo, co nat_ind, czyli reguła indukcji, tyle że kodziedziną motywu nie jest Prop, lecz Set (możesz myśleć, że Set to to samo co Type). Podobieństwo naszego nat_rec' oraz reguły indukcji nie jest przypadkowe - myślenie o typach induktywnych w przedstawiony wyżej sposób jest najlepszym sposobem na spamiętanie wszystkich możliwych reguł rekursji, indukcji i tympodobnych. A robi się to tak (naszym przykładem tym razem będzie typ list A). Krok pierwszy: każda lista to albo nil : list A albo cons : A -> list A -> list A zaaplikowany do głowy h : A i ogona t : list A. Krok drugi: skoro tak, to list A jest najlepszym sposobem na robienie termów w kształcie (nil, cons). Krok trzeci: wobec tego mamy (a raczej musimy sobie zrobić) rekursor list_rec', który, gdy damy mu inną realizację kształtu F := fun X => unit + A * X, to podmieni on nil i consy w dowolnej liście l na tą inną realizację. Jego typ wygląda tak:

Krócej można ten typ zapisać tak:

Implementacja jest banalna:

Krok czwarty: żeby uzyskać regułę indukcji, bierzemy rekursor i zamieniamy P : Type na P : list A -> Prop. Żeby uzyskać najbardziej ogólną regułę eliminacji, używamy P : list A -> Type.

Oczywiście musimy też dostosować typy argumentów. Może to prowadzić do pojawienia się nowych argumentów. c w rekursorze miało typ A -> P -> P. Pierwszy argument typu A musimy nazwać h, żeby móc go potem użyć. Ostatnie P to konkluzja, która musi być postaci P (cons h t), ale t : list A nigdzie nie ma, więc je dodajemy. Pierwsze P zmienia się w hipotezę indukcyjną P t. Krok piąty: definicja reguły indukcji jest prawie taka sama jak poprzednio (musimy uwzględnić pojawienie się t : list A jako argumentu w c. Poza tym drobnym detalem zmieniają się tylko typy:

Włala, mamy regułę indukcji. Na sam koniec wypadałoby jeszcze opisać drobne detale dotyczące najlepszości. Czy skoro nat jest najlepszym typem do robienia termów w kształcie sznurków, to znaczy, że inne realizacje tego kształtu są gorsze? I w jaki sposób objawia się ich gorszość? Odpowiedź na pierwsze pytanie jest skomplikowańsza niż bym chciał: nat jest najlepsze, ale inne typy też mogą być najlepsze. Rozważmy poniższy typ:

Jako, że nat' jest typem induktywnym, to jest najlepszym sposobem robienia termów w kształcie F := fun X => unit + X. Ale jak to? Przecież najlepsze dla tego kształtu jest nat! Tak, to prawda. Czy zatem nat' jest gorsze? Nie: oba te typy, nat i nat', są najlepsze. Wynika stąd ciekawa konkluzja: nat' to w zasadzie to samo co nat, tylko inaczej nazwane. Fakt ten łatwo jest udowodnić: mając natowy sznurek możemy za pomocą nat_rec' przerobić go na nat'owy sznurek. Podobnie nat'owy sznurek można za pomocą nat'_rec' przerobić na natowy sznurek. Widać na oko, że obie te funkcje są swoimi odwrotnościami, a zatem typy nat i nat' są izomorficzne, czyli mają takie same elementy i takie same właściwości.

Ćwiczenie

Zdefiniuj funkcje f : nat -> nat' i g : nat -> nat', które spełniają forall n : nat, g (f n) = n oraz forall n : nat', f (g n) = n. Nie musisz w tym celu używać nat_rec' ani nat'_rec' (no chyba, że chcesz).

Drugie pytanie brzmiało: w czym objawia się brak najlepszości innych realizacji danego kształtu? Odpowiedź jest prosta: skoro najlepszość to unikalny rekursor, to brak najlepszości oznacza brak unikalnego rekursora. Przeżyjmy to na przykładzie: Używając rekursora dla nat możemy podmienić S na negację, a 0 na false, i otrzymać dzięki temu funkcję sprawdzającą, czy długość sznurka (czyli liczby naturalnej) jest nieparzysta. Czy dla innych realizacji tego samego kształtu też możemy tak zrobić? Nie zawsze. Rozważmy typ unit wraz ze stałą tt i funkcją f := fun _ => tt, które realizują ten sam kształt co nat, 0 i S. Zauważmy, że tt = f tt, a zatem różne sznurki obliczają się do tej samej wartości. Jest to sytuacja zgoła odmienna od natowej - różne ilości Sów dają różne liczby naturalne. Gdybyśmy mieli dla tej realizacji rekursor podmieniający f na jakąś funkcję g, zaś tt na stałą x, to niechybnie doszłoby do katastrofy. Dla przykładu, gdybyśmy próbowali tak jak wyżej sprawdzić, czy długość sznurka jest nieparzysta, zamieniając tt na false, zaś f na negb, to wynikiem zamiany dla tt byłoby false, zaś dla f tt byłoby to negb false = true. To jednak prowadzi do sprzeczności, bo tt = f tt. Wyniki podmiany dla sznurków obliczających się do równych wartości musza być takie same. Oczywiście unit, tt i f to bardzo patologiczna realizacja sznurkowego kształtu. Czy są jakieś mniej patologiczne realizacje, które umożliwiają podmiankę, która pozwala sprawdzić nieparzystość długości sznurka? Tak. Przykładem takiej realizacji jest... bool, false i negb (a rzeczona podmianka, to w tym przypadku po prostu funkcja identycznościowa). Czy znaczy to, że bool, false i negb to najlepsza realizacja sznurkowego kształtu? Nie - da się znaleźć całą masę podmianek, które nat umożliwia, a bool, false i negb - nie (joł, sprawdź to - wcale nie kłamię). Cóż, to by było na tyle. W ramach pożegnania z tym spojrzeniem na typy induktywne napiszę jeszcze tylko, że nie jest ono skuteczne zawsze i wszędzie. Działa jedynie dla prostych typów zrobionych z enumeracji, rekurencji i parametrów. Żeby myśleć w ten sposób np. o indeksowanych rodzinach typów trzeba mieć nieco mocniejszą wyobraźnię.

Ćwiczenie

Rozważmy poniższe typy:

• unit
• bool
• option A
• A * B
• A + B
• exists x : A, P x
• nat
• list A

Dla każdego z nich:

• znajdź kształt, którego jest on najlepszą realizacją
• napisz typ rekursora
• zaimplementuj rekursor
• zaimplementuj bezpośrednio za pomocą rekursora jakąś ciekawą funkcję
• z typu rekursora wyprowadź typ reguły indukcji (oczywiście bez podglądania za pomocą komendy Print... nie myśl też o białym niedźwiedziu)
• zaimplementuj regułę indukcji
• spróbuj bezpośrednio użyć reguły indukcji, by udowodnić jakiś fakt na temat zaimplementowanej uprzednio za pomocą rekursora funkcji

Reguły eliminacji (TODO)

Jak działa taktyka induction (TODO)

Rodzaje rekursji

Funkcja może w swej definicji odwoływać się do samej siebie na różne sposoby. Najważniejszą klasyfikacją jest klasyfikacja ze względu na dozwolone argumenty w wywołaniu rekurencyjnym:

• Rekursja strukturalna to taka, w której funkcja wywołuje siebie na argumentach będących podtermami argumentów z obecnego wywołania.
• W szczególności rekursja prymitywna to taka, w której funkcja wywołuje siebie jedynie na bezpośrednich podtermach argumentu głównego z obecnego wywołania.
• Rekursja dobrze ufundowana to taka, w której funkcja wywołuje siebie jedynie na argumentach "mniejszych", gdzie o tym, które argumenty są mniejsze, a które większe, decyduje pewna relacja dobrze ufundowana. Intuicyjnie relacja dobrze ufundowana jest jak drabina: schodząc po drabinie w dół kiedyś musimy schodzenie zakończyć. Nie możemy schodzić w nieskończoność.

Mniej ważną klasyfikacją jest klasyfikacja ze względu na... cóż, nie wiem jak to ładnie nazwać:

• Rekursja bezpośrednia to taka, w której funkcja f wywołuje siebie samą bezpośrednio.
• Rekursja pośrednia to taka, w której funkcja f wywołuje jakąś inną funkcję g, która wywołuje f. To, że f nie wywołuje samej siebie bezpośrednio nie oznacza wcale, że nie jest rekurencyjna.
• W szczególności, rekursja wzajemna to taka, w której funkcja f wywołuje funkcję g, a g wywołuje f.
• Rzecz jasna rekursję pośrednią oraz wzajemną można uogólnić na dowolną ilość funkcji.

Oczywiście powyższe dwie klasyfikacje to tylko wierzchołek góry lodowej, której nie ma sensu zdobywać, gdyż naszym celem jest posługiwanie się rekursją w praktyce, a nie dzielenie włosa na czworo. Wobec tego wszystkie inne rodzaje rekursji (albo nawet wszystkie możliwe rodzaje w ogóle) będziemy nazywać rekursją ogólną. Z rekursją wzajemną zapoznaliśmy się już przy okazji badania indukcji wzajemnej w poprzednim rozdziale. W innych funkcyjnych językach programowania używa się jej zazwyczaj ze względów estetycznych, by móc elegancko i czytelnie pisać kod, ale jak widzieliśmy w Coqu jest ona bardzo upierdliwa, więc raczej nie będziemy jej używać. Skupmy się zatem na badaniu rekursji strukturalnej, dobrze ufundowanej i ogólnej.

Ćwiczenie

Przypomnij sobie podrozdział o indukcji wzajemnej. Następnie wytłumacz, jak przetłumaczyć definicję funkcji za pomocą rekursji wzajemnej na definicję, która nie używa rekursji wzajemnej.

Rekursja prymitywna (TODO)

Wiemy już, że rekursja ogólna prowadzi do sprzeczności, a jedyną legalną formą rekursji jest rekursja prymitywna (i niektóre formy rekursji strukturalnej, o czym dowiemy się później). Funkcje rekurencyjne, które dotychczas pisaliśmy, były prymitywnie rekurencyjne, więc potrafisz już całkiem sprawnie posługiwać się tym rodzajem rekursji. Pozostaje nam zatem jedynie zbadać techniczne detale dotyczące sposobu realizacji rekursji prymitywnej w Coqu. W tym celu przyjrzyjmy się ponownie definicji dodawania:

Możemy zaobserwować parę rzeczy. Pierwsza, techniczna sprawa: po = widzimy nieznany nam konstrukt fix. Pozwala on tworzyć anonimowe funkcje rekruencyjne, tak jak fun pozwala tworzyć anonimowe funkcje nierekurencyjne. Funkcje zdefiniowane komendami Fixpoint i Definition są w jęzku termów Coqa reprezentowane odpowiednio za pomocą fix i fun. Po drugie: za listą argumentów, a przed zwracanym typem, występuje adnotacja {struct n}. Wskazuje ona, który z argumentów funkcji jest argumentem głównym. Dotychczas gdy definiowaliśmy funkcje rekurencyjne nigdy nie musieliśmy jej pisać, bo Coq zawsze domyślał się, który argument ma być główny. W poetyckiej polszczyźnie argument główny możemy wskazać mówiąc np., że "funkcja plus zdefiniowana jest przez rekursję po pierwszym argumencie" albo "funkcja plus zdefinowana jest przez rekursję po n". Czym jest argument główny? Spróbuję wyjasnić to w sposób operacyjny:

• jako argument główny możemy wskazać dowolny argument, którego typ jest induktywny
• Coq wymusza na nas, aby argumentem głównym wywołania rekurencyjnego był podterm argumentu głównego z obecnego wywołania

Dlaczego taki zabieg chroni nas przed sprzecznością? Przypomnij sobie, że termy typów induktywnych muszą być skończone. Parafrazując: są to drzewa o skończonej wysokości. Ich podtermy są od nich mniejsze, więc w kolejnych wywołaniach rekurencyjnych argument główny będzie malał, aż w końcu jego rozmiar skurczy się do zera. Wtedy rekursja zatrzyma się, bo nie będzie już żadnych podtermów, na których można by zrobić wywołanie rekurencyjne. Żeby lepiej zrozumieć ten mechanizm, zbadajmy najpierw relację bycia podtermem dla typów induktywnych. Relację tę opisują dwie proste zasady:

• po pierwsze, jeżeli dany term został zrobiony jakimś konstruktorem, to jego podtermami są rekurencyjne argumenty tego konstruktora. Przykład: 0 jest podtermem S 0, zaś nil podtermem cons 42 nil.
• po drugie, jeżeli t1 jest podtermem t2, a t2 podtermem t3, to t1 jest podtermem t3 — własność ta nazywa się przechodniością. Przykład: S 0 jest podtermem S (S 0), a zatem 0 jest podtermem S (S 0). Podobnie nil jest podtermem cons 666 (cons 42 nil)

Ćwiczenie

Zdefiniuj relacje bycia podtermem dla liczb naturalnych i list.

Udowodnij, że przytoczone wyżej przykłady nie są oszustwem. Komenda Goal jest wygodna, gdyż używając jej nie musimy nadawać twierdzeniu nazwy. Użycie Qed zapisze twierdzenie jako Unnamed_thm, Unnamed_thm0, Unnamed_thm1 etc.

Ćwiczenie

Udowodnij, że relacje subterm_nat oraz subterm_list są antyzwrotne i przechodnie. Uwaga: to może być całkiem trudne.

Jak widać, podtermy liczby naturalnej to liczby naturalne, które są od niej mniejsze, zaś podtermy listy to jej ogon, ogon ogona i tak dalej. Zero i lista pusta nie mają podtermów, gdyż są to przypadki bazowe, pochodzące od konstruktorów, które nie mają argumentów rekurencyjnych. Dla każdego typu induktywnego możemy zdefiniować relację bycia podtermem podobną do tych dla liczb naturalnych i list. Zauważmy jednak, że nie możemy za jednym zamachem zdefiniować relacji bycia podtermem dla wszystkich typów induktywnych, gdyż nie możemy w Coqu powiedzieć czegoś w stylu "dla wszystkich typów induktywnych". Możemy powiedzieć jedynie "dla wszystkich typów". Coq nie generuje jednak automatycznie takiej relacji, gdy definiujemy nowy typ induktywny. W jaki zatem sposób Coq sprawdza, czy jeden term jest podtermem drugiego? Otóż... w sumie, to nie sprawdza. Rzućmy okiem na następujący przykład:

Definicja zdaje się być poprawna: 0 to przypadek bazowy, a gdy n jest postaci S n', wywołujemy funkcję rekurencyjnie na argumencie 0. 0 jest podtermem S n', a zatem wszystko powinno być dobrze. Dostajemy jednak następujący komunikat o błędzie:

Komunikat ten głosi, że argumentem głównym wywołania rekurencyjnego jest 0, podczas gdy powinno być nim n'. Wynika stąd jasno i wyraźnie, że jedynymi legalnymi argumentami w wywołaniu rekurencyjnym są te podtermy argumentu głównego, które zostają ujawnione w wyniku dopasowania do wzorca. Coq nie jest jednak głupi - jest głupszy, niż ci się wydaje, o czym świadczy poniższy przykład.

Funkcja ta próbuje policzyć n-tą liczbę Fibonacciego: https://en.wikipedia.org/wiki/Fibonacci_number, ale słabo jej to wychodzi, gdyż dostajemy następujący błąd:

Mimo, że S n' jest podtermem S (S n'), który pochodzi z dopasowania do wzorca, to Coq nie jest w stanie zauważyć tego faktu. W komunikacie o błędzie pojawia się za to tajemnicza zmienna n0, której w naszym kodzie nigdzie nie ma. Sposobem na poradzenie sobie z problemem jest pokazanie Coqowi palcem, o co nam chodzi:

Tym razem Coq widzi, że S n' jest podtermem S (S n'), gdyż explicite nadaliśmy temu termowi nazwę n'', używając do tego klauzli as. Ufff... udało nam się przebrnąć przez techniczne detale działania rekursji strukturalnej. Mogłoby się wydawać, że jest ona mechanizmem bardzo upośledzonym, ale z doświadczenia wiesz już, że w praktyce omówione wyżej problemy występują raczej rzadko. Mogłoby się też wydawać, że skoro wywołania rekurencyjne możemy robić tylko na bezpośrednich podtermach dopasowanych we wzorcu, to nie da się zdefiniować prawie żadnej ciekawej funkcji. Jak zobaczymy w kolejnych podrozdziałach, wcale tak nie jest. Dzięki pewnej sztuczce za pomocą rekursji strukturalnej można wyrazić rekursję dobrze ufundowaną, która na pierwszy rzut oka jest dużo potężniejsza i daje nam wiele możliwości definiowania różnych ciekawych funkcji.

Ćwiczenie (dzielenie)

Zdefiniuj funkcję div, która implementuje dzielenie całkowitoliczbowe. Żeby uniknąć problemów z dzieleniem przez 0, div n m będziemy interpretować jako n podzielone przez S m, czyli np. div n 0 to n/1, div n 1 to n/2 etc. Uwaga: to ćwiczenie pojawia się właśnie w tym miejscu nieprzypadkowo.

Rekursja monotoniczna

Czas na omówienie pewnej ciekawej, ale średnio użytecznej formy rekursji (z pamięci nie jestem w stanie przytoczyć więcej niż dwóch sztampowych przykładów jej użycia), a jest nią rekursja monotoniczna (zwana też czasem rekursją zagnieżdżoną, ale nie będziemy używać tej nazwy, gdyż dotychczas używaliśmy jej na określenie rekursji, w której arguemntem wywołania rekurencyjnego jest wynik innego wywołania rekurencyjnego). Cóż to za zwierzątko, rekursja monotoniczna? Żeby się tego dowiedzieć, przypomnijmy sobie najpierw, jak technicznie w Coqu zrealizowana jest rekursja strukturalna.

Tak oto definicja funkcji plus, lecz zapisana nieco inaczej, niż gdy widzieliśmy ją ostatnim razem. Tym razem prezentujemy ją jako funkcję biorącą jeden argument typu nat i zwracającą funkcję z typu nat w typ nat.

Ale komenda Fixpoint jest jedynie cukrem syntaktycznym - funkcję plus możemy równie dobrze zdefiniować bez niej, posługując się jedynie komendą Definition, a wyrażeniem, które nam to umożliwia, jest fix. fix działa podobnie jak fun, ale pozwala dodatkowo nadać definiowanej przez siebie funkcji nazwę, dzięki czemu możemy robić wywołania rekurencyjne. Czym więc jest rekursja monotoniczna? Z rekursją monotoniczną mamy do czynienia, gdy za pomocą fixa (czyli przez rekursję) definiujemy funkcję, która zwraca inną funkcję, i ta zwracana funkcja także jest zdefiniowana za pomocą fixa (czyli przez rekursję). Oczywiście to tylko pierwszy krok - wynikowa funkcja również może zwracać funkcję, która jest zdefiniowana za pomocą fixa i tak dalej. Widać zatem jak na dłoni, że plus ani plus' nie są przykładami rekursji monotonicznej. Wprawdzie definiują one za pomocą fixa (lub komendy Fixpoint) funkcję, która zwraca inną funkcję, ale ta zwracana funkcja nie jest zdefiniowana za pomocą fixa, lecz za pomocą fun, a więc nie jest rekurencyjna. Podsumowując: rekursja jest monotoniczna, jeżeli w definicji funkcji pojawiają się co najmniej dwa wystąpienia fix, jedno wewnątrz drugiego (przy czym rzecz jasna Fixpoint też liczy się jako fix). No to skoro już wiemy, czas zobaczyć przykład jakiejś funkcji, która jest zdefiniowana przez rekursję monotoniczną.

Powyższa funkcja zwana jest funkcją Ackermanna, gdyż wymyślił ją... zgadnij kto. Jest ona całkiem sławna, choć z zupełnie innych powodów niż te, dla których my się jej przyglądamy. Nie oblicza ona niczego specjalnie użytecznego - jej wynikami są po prostu bardzo duże liczby. Jeżeli nie wierzysz, spróbuj policzyć ręcznie ack 4 2 - zdziwisz się. Jak widać, Coq nie akceptuje powyższej definicji. Winny temu jest rzecz jasna kształt rekursji. Dla n równego 0 zwracamy S m, co jest ok. Dla n postaci S n' i m równego 0 robimy wywołanie rekurencyjne na n' i 1, co również jest ok. Jednak jeżeli n i m odpowednio są postaci S n' i S m', to robimy wywołanie rekurencyjne postaci ack n' (ack (S n') m'). W wewnętrznym wywołaniu rekurencyjnym pierwszy argument jest taki sam jak obecny. Gdyby argumentem głównym był drugi argument, to jest tym bardziej źle, gdyż w zewnętrznym wywołaniu rekurencyjnym nie jest nim m', lecz ack (S n') m'. Nie ma się więc co dziwić, że Coq nie może zgadnąć, który argument ma być argumentem głównym. Mimo, że Coq nie akceptuje tej definicji, to wydaje się ona być całkiem spoko. Żaden z argumentów nie może wprawdzie posłużyć nam za argument główny, ale jeżeli rozważymy ich zachowanie jako całość, to okazuje się, że w każdym wywołaniu rekurencyjnym mamy dwie możliwości:

• albo pierwszy argument się zmniejsza
• albo pierwszy argument się nie zmienia, ale drugi argument się zmniejsza

Możemy z tego wywnioskować, że jeżeli wywołamy ack na argumentach n i m, to w ogólności najpierw m będzie się zmniejszał, ale ponieważ musi kiedyś spaść do zera, to wtedy n będzie musiał się zmniejszyć. Oczywiście wtedy w kolejnym wywołaniu zaczynamy znowu z jakimś m, które potem się zmniejsza, aż w końcu znowu zmniejszy się n i tak dalej, aż do chwili, gdy n spadnie do zera. Wtedy rekursja musi się skończyć. Jednym z typowych zastosowań rekursji zagnieżdżonej jest radzenie sobie z takimi właśnie przypadkami, w których mamy ciąg argumentów i pierwszy maleje, lub pierwszy stoi w miejscu a drugi maleje i tak dalej. Zobaczmy więc, jak techniki tej można użyć do zdefiniowania funkcji Ackermanna.

Zauważmy przede wszystkim, że nieco zmienia się wygląd typu naszej funkcji. Jest on wprawdzie dokładnie taki sam (nat -> nat -> nat), ale zapisujemy go inaczej. Robimy to by podkreslić, że wynikiem ack jest funkcja. W przypadku gdy n jest postaci S n' zdefiniowana jest ona za pomocą fixa tak, jak wyglądają dwie ostatnie klauzule dopasowania z oryginalnej definicji, ale z wywołaniem ack (S n') m' zastąpionym przez ack' m'. Tak więc funkcja ack' reprezentuje częściową aplikację ack n.

Ćwiczenie

Zdefiniuj funkcję merge o typie forall (A : Type) (cmp : A -> A -> bool), list A -> list A -> list A, która scala dwie listy posortowane według porządku wyznaczanego przez cmp w jedną posortowaną listę. Jeżeli któraś z list posortowana nie jest, wynik może być dowolny. Wskazówka: dlaczego niby to ćwiczenie pojawia się w podrozdziale o rekursji zagnieżdżonej?

Obie listy są posortowane według leb, więc wynik też jest.

Pierwsza lista nie jest posortowana według leb, więc wynik jest z dupy.

Ćwiczenie

Skoro już udało ci się zdefiniować merge, to udowodnij jeszcze parę lematów, cobyś nie miał za dużo wolnego czasu.

Rekursja polimorficzna

Rząd rżnie głupa, czyli o pierwszym i wyższym rzędzie (TODO)

Rekursja wyższego rzędu (TODO)

Pozostaje kwestia rekursji wyższego rzędu. Co to takiego? Ano dotychczas wszystkie nasze wywołania rekurencyjne były konkretne, czyli zaaplikowane do argumentów. Mogłoby się wydawać, że jest to jedyny możliwy sposób robienia wywołań rekurencyjnych, jednak nie jest tak. Wywołania rekurencyjne mogą mieć również inną, wyższorzędową postać, a mianowicie - możemy przekazać funkcję, którą właśnie definiujemy, jako argument do innej funkcji. Dlaczego jest to wywołanie rekurencyjne, skoro nie wywołujemy naszej funkcji? Ano dlatego, że tamta funkcja, która dostaje naszą jako argument, dostaje niejako możliwość robienia wywołań rekurencyjnych. W zależności od tego, co robi ta funkcja, wszystko może być ok (np. gdy ignoruje ona naszą funkcję i w ogóle jej nie używa) lub śmiertelnie niebezpieczne (gdy próbuje zrobić wywołanie rekurencyjne na strukturalnie większym argumencie). Sztoby za dużo nie godoć, bajszpil:

Tree to typ drzew niepustych, które mogą mieć dowolną (ale skończoną) ilość poddrzew. Spróbujmy zdefiniować funkcję, która zwraca lustrzane odbicie drzewa.

Nie jest to zbyt trudne. Rekurencyjnie odbijamy wszystkie poddrzewa za pomocą map mirror, a następnie odwracamy kolejność poddrzew z użyciem rev. Chociaż poszło gładko, to mamy tu do czynienia z czymś, czego wcześniej nie widzieliśmy. Nie ma tu żadnego wywołania rekurencyjnego, a mimo to funkcja działa ok. Dlaczego? Właśnie dlatego, że wywołania rekurencyjne są robione przez funkcję map. Mamy więc do czynienia z rekursją wyższego rzędu.

Inny przykład:

Tym razem mamy drzewo, które może mieć naprawdę dowolną ilość poddrzew, ale jego poddrzewa są nieuporządkowane.

Rekursja strukturalna (TODO)

Rekursja ogólna

W Coqu rekursja ogólna nie jest dozwolona. Powód jest banalny: prowadzi ona do sprzeczności. W celu zobrazowania spróbujmy zdefiniować za pomocą taktyk następującą funkcję rekurencyjną:

Przyjrzyjmy się uważnie definicji funkcji loop. Mimo, że udało nam się ujrzeć znajomy napis "No more subgoals", próba użycia komendy Qed kończy się błędem. Fakt, że konstruujemy funkcję za pomocą taktyk, nie ma tu żadnego znaczenia, lecz służy jedynie lepszemu zobrazowaniu, dlaczego rekursja ogólna jest grzechem. Dokładnie to samo stałoby się, gdybyśmy próbowali zdefiniować loop ręcznie:

Gdyby tak się nie stało, możliwe byłoby skonstruowanie dowodu False:

Aby chronić nas przed tą katastrofą, Coq nakłada na rekurencję ograniczenie: argument główny wywołania rekurencyjnego musi być strukturalnym podtermem argumentu głównego obecnego wywołania. Innymi słowy, dozwolona jest jedynie rekursja strukturalna. To właśnie napisane jest w komunikacie o błędzie, który dostajemy, próbując przeforsować powyższe definicje:

Wywołanie rekurencyjne loop jest nielegalne, gdyż jego argumentem jest u, podczas gdy powinien być nim jakiś podterm u. Zanim jednak dowiemy się, czym jest argument główny, czym są podtermy i jak dokładnie Coq weryfikuje poprawność naszych definicji funkcji rekurencyjnych, wróćmy na chwilę do indukcji. Jak się zaraz okaże, nielegalność rekursji ogólnej wymusza również pewne ograniczenia w definicjach induktywnych.

Ćwiczenie

Ograniczenia nakładane przez Coqa sprawiają, że wszystkie napisane przez nas funkcje rekurencyjne muszą się kiedyś zatrzymać i zwrócić ostateczny wynik swojego działania. Tak więc nie możemy w Coqu pisać funkcji nieterminujących, czyli takich, które się nie zatrzymują. Rozważ bardzo interesujące pytanie filozoficzne: czy funkcje, które nigdy się nie zatrzymują (lub nie zatrzymują się tylko dla niektórych argumentów) mogą być w ogóle do czegokolwiek przydatne? Nie daj się wpuścić w maliny.

Rekursja po paliwie

Rekursja dobrze ufundowana to sirius byznys, więc zanim się nią zajmiemy wypadałoby nauczyć się robić robotę na odwal, byle działało. Jakkolwiek nie brzmi to zbyt profesjonalnie, dobrze jest mieć tego typu narzędzie w zanadrzu, choćby w celu szybkiego prototypowania. Czasem zdarza się też, że tego typu luźne podejście do problemu jest jedynym możliwym, bo nikt nie wie, jak to zrobić porządnie. Narzędziem, o którym mowa, jest coś, co ja nazywam "rekursją po paliwie". Pozwala ona zasymulować definicję dowolnej funkcji o typie A1 -> ... -> An -> B (w tym nawet częściowej czy nieterminującej, co już samo w sobie jest ciekawe) za pomocą funkcji o typie nat -> A1 -> ... -> An -> option B. Trik jest dość banalny: argument typu nat jest argumentem głównym, po którym robimy rekursję. Jest on naszym "paliwem", które spalamy przy każdym wywołaniu rekurencyjnym. Jeżeli paliwo się nam skończy, zwracamy None. Jeżeli jeszcze starcza paliwa, możemy zdefiniować funkcję tak jak zamierzaliśmy, ale mamy też obowiązki biurokratyczne związane ze sprawdzaniem, czy wyniki wywołań rekurencyjnych to None czy Some. Coby za dużo nie godoć, przykład.

Będą nam potrzebne notacje dla list oraz funkcja even, która sprawdza, czy liczba naturalna jest parzysta. Będziemy chcieli zdefiniować funkcję Collatza. Gdyby Coq wspierał rekursję ogólną, jej definicja wyglądałaby tak:

Jest to bardzo wesoła funkcja. Przypadki bazowe to 0 i 1 - zwracamy wtedy po prostu listę z jednym elementem, odpowiednio [0] lub [1]. Ciekawiej jest dla n większego od 1. n zostaje głową listy, zaś w kwestii ogona mamy dwa przypadki. Jeżeli n jest parzyste, to argumentem wywołania rekurencyjnego jest n podzielone przez 2, zaś w przeciwnym przypadku jest to 1 + 3 * n. Funkcja ta nie ma żadnego ukrytego celu. Została wymyślona dla zabawy, a przyświecające jej pytanie to: czy funkcja ta kończy pracę dla każdego argumentu, czy może jest jakiś, dla którego się ona zapętla? O ile funkcja jest prosta, o tyle odpowiedź jest bardzo skomplikowana i dotychczas nikt nie potrafił jej udzielić. Sprawdzono ręcznie (czyli za pomocą komputerów) bardzo dużo liczb i funkcja ta zawsze kończyła pracę, ale nikt nie umie udowodnić, że dzieje się tak dla wszystkich liczb.

Definicja funkcji collatz za pomocą rekursji po paliwie wygląda dość groźnie, ale tak naprawdę jest całkiem banalna. Ponieważ oryginalna funkcja była typu nat -> list nat, to ta nowa musi być typu nat -> nat -> option (list nat). Tym razem zamiast dopasowywać n musimy dopasować paliwo, czyli fuel. Dla 0 zwracamy None, a gdy zostało jeszcze trochę paliwa, przechodzimy do właściwej części definicji. W przypadkach bazowych zwracamy [n], ale musimy zawinąć je w Some. W pozostałych przypadkach sprawdzamy, czy n jest parzyste, a następnie doklejamy odpowiedni ogon, ale musimy dopasować wywołania rekurencyjne żeby sprawdzić, czy zwracają one None czy Some.

Zaimplementowana za pomocą rekursji po paliwie funkcja oblicza się bez problemu, oczywiście o ile wystarczy jej paliwa. W powyższych przykładach 10 jednostek paliwa wystarcza, by obliczyć wynik dla 5, ale 2 jednostki paliwa to za mało. Jak więc widać, ilość potrzebnego paliwa zależy od konkretnej wartości na wejściu. Interpretacja tego, czym tak naprawdę jest paliwo, nie jest zbyt trudna. Jest to maksymalna głębokość rekursji, na jaką może pozwolić sobie funkcja. Czym jest głębokość rekursji? Możemy wyobrazić sobie drzewo, którego korzeniem jest obecne wywołanie, a poddrzewami są drzewa dla wywołań rekurencyjnych. Głębokość rekursji jest po prostu głębokością (czyli wysokością) takiego drzewa. W przypadku funkcji collatz głębokość rekursji jest równa długości zwróconej listy (gdy funkcja zwraca Some) lub większa niż ilość paliwa (gdy funkcja zwraca None). Powyższe rozważania prowadzą nas do techniki, która pozwala z funkcji zrobionej rekursją po paliwie zrobić normalną, pełnoprawną funkcję. Wystarczy znaleźć "funkcję tankującą" fill_tank : A1 -> ... -> An -> nat, która oblicza, ile paliwa potrzeba dla danych argumentów wejściowych. Funkcja ta powinna mieć tę własność, że gdy nalejemy tyle paliwa, ile ona każe (lub więcej), zawsze w wyniku dostaniemy Some. Trudnością, z którą nikt dotychczas w przypadku funkcji collatz nie potrafił się uporać, jest właśnie znalezienie funkcji tankującej. Jak więc widać, rekursja po paliwie nie zawsze jest fuszerką czy środkiem prototypowania, lecz czasem bywa faktycznie przydatna do reprezentowania funkcji, których inaczej zaimplementować się nie da.

Ćwiczenie

Zdefiniuj za pomocą rekursji po paliwie funkcję divFuel, która jest implementacją dzielenia (takiego zwykłego, a nie sprytnego jak ostatnio, tzn. divFuel fuel n 0 jest niezdefiniowane).

Ćwiczenie

Sporą zaletą rekursji po paliwie jest to, że definicje zrobionych za jej pomocą funkcji są jasne i czytelne (przynajmniej w porównaniu do rekursji dobrze ufundowanej, o czym już niedługo się przekonamy). To z kolei pozwala nam w dość łatwy sposób dowodzić interesujących nas właściwości tych funkcji. Udowodnij kilka oczywistych właściwości dzielenia:

• divFuel ? n 1 = Some n, tzn. n/1 = n. Ile potrzeba paliwa?
• divFuel ? n n = Some 1, tzn. n/n = 1. Ile potrzeba paliwa?
• przy dzieleniu przez 0 nigdy nie starcza paliwa.

Ćwiczenie (lemat o tankowaniu)

Pokaż, że jeżeli wystarcza nam paliwa do obliczenia wyniku, ale zatankujemy jeszcze trochę, to dalej będzie nam wystarczać. Wniosek: tankującemu nie dzieje się krzywda.

Ćwiczenie

Udowodnij, że funkcji collatz dla wejść o postaci pow 2 n (czyli potęg dwójki) wystarczy S n jednostek paliwa. Uwaga (trochę złośliwa): jeśli napotkasz trudności w trakcie dowodzenia (a moje uwagi przecież nie biorą się znikąd), to pamiętaj, że mają one charakter arytmetyczny, tzn. są związane z użyciem w definicji funkcji takich jak pow czy div2, nie są zaś spowodowane jakimiś problemami z samą techniką, jaką jest rekursja po paliwie.

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.

Indukcja wykresowa

Skoro nie dla psa kiełbasa, to musimy znaleźć jakiś sposób na udowodnienie równania rekurencyjnego dla div. Zamiast jednak głowić się nad równaniami rekurencyjnymi albo nad funkcją div, zastanówmy się w pełnej ogólności: jak dowodzić właściwości funkcji rekurencyjnych? No przez indukcję, czy to nie oczywiste? Jasne, ale jak dokładnie owa indukcja ma wyglądać? Odpowiedź jest prostsza niż można się spodziewać. Otóż gdy kupujesz but, ma on pasować do twojej stopy, zaś gdy kupujesz gacie, mają one pasować do twojej dupy. Podobnie jest z indukcją: jej kształt ma pasować do kształtu rekursji, za pomocą której zdefiniowana została funkcja. Czym jest "kształt" rekursji (i indukcji)? Jest to raczej poetyckie pojęcie, które odnosi się do tego, jak zdefiniowano funkcję - ile jest przypadków, podprzypadków, podpodprzypadków etc., w jaki sposób są w sobie zagnieżdżone, gdzie są wywołania rekurencyjne, ile ich jest i na jakich argumentach etc. Dowiedziawszy się, czym jest kształt rekursji i indukcji, powinniśmy zacząć szukać sposobu na dopasowanie kształtu indukcji w naszych dowodach do kształtu rekursji funkcji. Dotychczas indukcję zawsze robiliśmy po argumencie głównym, zaś z potencjalnymi niedopasowaniami kształtów radziliśmy sobie robiąc ad hoc analizy przypadków, które uznaliśmy za stosowne. I tutaj przyda nam się nieco konceptualnej spostrzegawczości. Zauważyć nam bowiem trzeba, że robiąc indukcję po argumencie głównym, kształt indukcji odpowiada kształtowi typu argumentu głównego. Skoro zaś mamy dopasować go do kształtu rekursji funkcji, to nasuwa nam się oczywiste pytanie: czy da się zdefiniować typ, który ma taki sam kształt, jak definicja danej funkcji? Odpowiedź brzmi: nie, ale da się zdefiniować rodzinę typów (a konkretniej pisząc, rodzinę zdań, czyli relację) o takiej właściwości. Owa relacja zwie się wykresem funkcji. Jaki ma to związek z bazgrołami znanymi ci ze szkoły (zakładam, że wiesz, że wykresem funkcji liniowej jest prosta, wykresem funkcji kwadratowej jest parabola, a wykresy sinusa i cosinusa to takie wesołe szlaczki)? To, co w szkole nazywa się wykresem funkcji, jest jedynie graficznym przedstawieniem prawdziwego wykresu, czyli relacji. Samo słowo "wykres", wywodzące się w oczywisty sposób od kreślenia, sugeruje, że myślenie o wykresie jak o obrazku było pierwsze, a koncepcja wykresu jako relacji jest późniejsza. W ramach ciekawostki być może warto napisać, że w dawnych czasach matematycy silnie utożsamiali funkcję z jej wykresem (w sensie obrazka) i przez to byty, których wykresu nie dało się narysować, nie były uznawane za funkcje. W nieco późniejszym czasie zaszły jednak niemałe zmiany i obecnie panującym zabobonem jest utożsamianie funkcji z wykresem (w sensie relacji), przez co za funkcje uznawane są także byty, których nie da się obliczyć lub nikt nie potrafi pokazać, że terminują (takich jak np. "funkcja" Collatza). Gdybyś zgłupiał od powyższych czterech akapitów, to przypominam, że dla nas zawarte w nich pojęcia oznaczają to:

• Funkcja to byt, którego typem jest A -> B lub forall x : A, B x. Można dać jej coś na wejściu i uzyskać wynik na wyjściu, tzn. można ją obliczyć. W Coqu wszystkie funkcje prędzej czy później kończą się obliczać.
• Wykres funkcji to relacja opisująca związek argumentu funkcji z jej wynikiem. Każda funkcja ma wykres, ale nie każda relacja jest wykresem jakiejś funkcji.
• Jeżeli typy A i B da się jakoś sensownie narysować, to możemy narysować obrazek przedstawiający wykres funkcji.

Żeby było nam raźniej, tak wygląda formalna definicja stwierdzenia, że relacja R jest wykresem funkcji f. Uwaga: jeżeli funkcja bierze więcej niż jeden argument (tzn. ma typ A1 -> ... -> An -> B), to wtedy do powyższej definicji musimy wrzucić jej zmodyfikowaną wersję o typie A1 * ... * An -> B.

Ćwiczenie

Zdefiniuj funkcję graph_of, która każdej funkcji przyporządkowuje jej wykres. Następnie udowodnij, że faktycznie jest to wykres tej funkcji.

Ćwiczenie

Wymyśl typy A i B oraz relację o typie A -> B -> Prop, która nie jest wykresem żadnej funkcji. Następnie udowodnij formalnie, że nie mylisz się.

Ćwiczenie

Pokaż, że wszystkie wykresy danej funkcji są równoważne w poniższym sensie.

Skoro już wiemy czym są wykresy funkcji, czas nauczyć się definiować induktywne wykresy o kształtach odpowiednich dla naszych niecnych celów.

Zwróćmy tylko uwagę na fakt, że mówiąc o kształcie rekursji (lub po prostu o kształcie definicji) div nie mamy na myśli faktycznej definicji, która używa rekursji dobrze ufundowanej i jak już wiemy, jest dość problematyczna, lecz "docelowej" definicji, którą wyraża między innymi równanie rekurencyjne.

div jest funkcją typu nat -> nat -> nat, więc jej wykres to relacja typu nat -> nat -> nat -> Prop. Dwa pierwsze argumenty relacji reprezentują wejście, zaś ostatni argument reprezentuje wyjście, tzn. chcemy, żeby divG n m r było równoważne div n m = r. Z równania rekurencyjnego widać, że mamy dwa przypadki, czyli konstruktory też będą dwa. Jeden odpowiada przypadkowi, gdy n < S m, tzn. dzielna jest mniejsza niż dzielnik (pamiętaj, że div n m oznacza n/(m + 1), żeby uniknąć problemów z dzieleniem przez zero). Konkluzją jest wtedy divG n m 0, tzn. argumentami są n i m, zaś wynikiem jest 0. Drugi przypadek to przyadek rekurencyjny. Jeżeli n >= S m, tzn. dzielna jest większa lub równa od dzielnika, to konkluzją jest divG n m (S r), tzn. argumentami są n i m, zaś wynikiem dzielenia jest S r. Czym jest r? Jest ono skwantyfikowane w tym konstruktorze i pojawia się w przesłance divG (n - S m) m r, która mówi, że wynikiem dzielenia n - S m przez m jest r. Przesłanka ta jest wykresowym odpowiednikiem wywołania rekurencyjnego.

Ćwiczenie

Mimo, że wszystkie wykresy danej funkcji są równoważne, to zdefiniować można je na wiele różnych sposobów. W zależności od sposobu definicja może być użyteczna lub nie, np. przy definicjach induktywnych dostajemy za darmo regułę indukcji. Podaj inną definicję wykresu funkcji div, która nie używa typów induktywnych (ani nie odwołuje się do samej funkcji div - to byłoby za łatwe). Użyj kwantyfikatora egzystencjalnego, mnożenia, dodawania oraz relacji równości (i niczego więcej). Nazwij ją divG'. Na razie nie musisz dowodzić, że wykres faktycznie jest wykresem div (póki co jest to za trudne), co oczywiście nie znaczy, że wolno ci się mylić - uzasadnij nieformalnie, że wykres faktycznie opisuje funkcję div. Do dowodu formalnego wrócimy później.

Mamy wykres. Fajnie, ale co możemy z nim zrobić? Jeszcze ważniejsze pytanie brzmi zaś: co powinniśmy z nim zrobić?

Pierwsza czynność po zdefiniowaniu wykresu, którą powinniśmy wykonać, to sprawdzenie, czy ów wykres jest relacją deterministyczną. Relacja deterministyczna to taka, której ostatni argument jest zdeterminowany przez poprzednie. Jeżeli wykres jest deterministyczny to dobrze, a jeżeli nie, to definicja na pewno jest błędna, bo wykres ma opisywać funkcję, a żadna funkcja nie może dla tych samych argumentów dawać dwóch różnych wyników. Relacjom deterministycznym (i nie tylko) przyjrzymy się dokładniej w rozdziale o relacjach. Dowód nie jest zbyt trudny. Robimy indukcję po dowodzie hipotezy divG n m r1, ale musimy pamiętać, żeby wcześniej zgeneralizować r2, bo w przeciwnym przypadku nasza hipoteza indukcyjna będzie za mało ogólna.

Kolejna rzecz do udowodnienia to twierdzenie o poprawności, które mówi, że divG faktycznie jest wykresem div. Zauważ, że moglibyśmy równie dobrze sformułować je za pomocą is_graph, ale tak jak wyżej będzie praktyczniej. Dowód zaczynamy od indukcji dobrze ufundowanej, po czym wprowadzamy zmienne do kontekstu i... aj waj, cóż to takiego? Używamy równania rekurencyjnego do rozpisania div, po czym kończymy przez rozważenie przypadków. Ten dowód pokazuje, że nie udało nam się osiągnąć celu, który sobie postawiliśmy, czyli udowodnienia div_eq za pomocą specjalnej reguły indukcji. Niestety, bez równania rekurencyjnego nie da się udowodnić twierdzenia o poprawności. Nie powinniśmy jednak za bardzo się tym przejmować - uszy do góry. Póki co dokończmy poszukiwań ostatecznej reguły indukcji, a tym nieszczęsnym równaniem rekurencyjnym zajmiemy się później.

Kolejną, ostatnią już rzeczą, którą powinniśmy zrobić z wykresem, jest udowodnienie twierdzenia o pełności, które głosi, że jeżeli argumentom n i m odpowiada na wykresie wynik r, to r jest równe div n m. Dowód jest banalny i wynika wprost z twierdzeń o determinizmie i poprawności. I po co nam to było? Ano wszystkie fikołki, które zrobiliśmy, posłużą nam jako lematy do udowodnienia reguły indukcji wykresowej dla div. Co to za reguła, jak wygląda i skąd ją wziąć?

Pierwowzorem reguły indukcji wykresowej dla danej funkcji jest reguła indukcji jej wykresu. Reguła indukcji dla div to w sumie to samo co powyższa reguła, ale z r wyspecjalizowanym do div n m. Chcemy też pozbyć się niepotrzebnej przesłanki divG n m r (po podstawieniu za r ma ona postać divG n m (div n m)), gdyż nie jest potrzebna - jest zawsze prawdziwa na mocy twierdzenia divG_correct.

Przydałaby się jednak także i filozoficzna interpretacja reguły. Pozwoli nam ona dowodzić zdań, które zależą od n m : nat i wyniku dzielenia, czyli div n m. Są dwa przypadki, jak w docelowej definicji div. Gdy n < S m, czyli dzielna jest mniejsza od dzielnika, wystarczy udowodnić P n m 0, bo wtedy div n m wynosi 0. W drugim przypadku, czyli gdy n >= S m, wystarczy udowodnić P n m (S (div (n - S m) m)) (bo taki jest wynik div n m dla n >= S m) przy założeniu, że P zachodzi dla n - S m, m oraz div (n - S m) m, bo takie są argumenty oraz wynik wywołania rekurencyjnego. Dowód jest prosty. Wprowadzamy zmienne do kontekstu, a następnie za pomocą zwykłego apply używamy reguły indukcji divG_ind - jako rzekło się powyżej, reguła div_ind nie jest niczym innym, niż lekką przeróbką divG_ind. Mamy trzy podcele. Pierwszy odpowiada przesłance Hlt. Drugi to przesłanka Hge, ale musimy wszędzie podstawić div (n' - S m') m' za r - posłuży nam do tego twierdzenie o pełności. Trzeci to zbędna przesłanka divG n m (div n m), którą załatwiamy za pomocą twierdzenia o poprawności. Włala (lub bardziej wykwintnie: voilà)! Mamy regułę indukcji wykresowej dla div. Zobaczmy, co i jak można za jej pomocą udowodnić.

Ćwiczenie

Udowodnij twierdzenie div_le za pomocą indukcji dobrze ufundowanej i równania rekurencyjnego, czyli bez użycia indukcji wykresowej. Jak trudny jest ten dowód w porównaniu do powyższego?

Ćwiczenie

Udowodnij za pomocą indukcji wykresowej, że twój alternatywny wykres funkcji div z jednego z poprzednich ćwiczeń faktycznie jest wykresem div. Następnie udowodnij to samo za pomocą indukcji dobrze ufundowanej i równania rekurencyjnego. Która metoda dowodzenia jest lepsza (nie, to pytanie nie jest subiektywne - masz udzielić jedynej słusznej odpowiedzi).

Ćwiczenie

Napisz funkcję split o sygnaturze split (n : nat) {A : Type} (l : list A) : option (list A * list A), która rozdziela listę l na blok o długości n i resztę listy, lub zwraca None gdy lista jest za krótka. Następnie udowodnij dla tej funkcji regułę indukcji wykresowej i użyj jej do udowodnienia kilku lematów. Wszystkie te rzeczy przydadzą się nam w jednym z kolejnych zadań.

Metoda induktywnej dziedziny

Póki co nie jest źle - udało nam się wszakże wymyślić jedyną słuszną metodę dowodzenia właściwości funkcji rekurencyjnych. Jednak nasza implementacja kuleje przez to nieszczęsne równanie rekurencyjne. Jak możemy udowodnić je bez używania indukcji wykresowej? Żeby znaleźć odpowiedź na to pytanie, znowu przyda się nam trochę konceptualnej jasności. Na czym tak naprawdę polega problem? Jak pamiętamy, problem wynika z tego, że definiując div przez rekursję dobrze ufundowaną musieliśmy jednocześnie dowodzić, że wywołania rekurencyjne odbywają się na argumencie mniejszym od argumentu obecnego wywołania. Tak więc problemem jest połączenie w jednej definicji dwóch dość luźno powiązanych rzeczy, którymi są:

• Docelowa definicja, która określa obliczeniowe zachowanie funkcji. Jej manifestacją jest nasze nieszczęsne równanie rekurencyjne. Bywa ona czasem nazywana aspektem obliczeniowym (albo algorytmicznym) funkcji.
• Dowód terminacji, który zapewnia, że definicja docelowa jest legalna i nie prowadzi do sprzeczności. Jego manifestacją są występujące w definicji div dowody na to, że wywołanie rekurencyjne ma argument mniejszy od obecnego wywołania. Bywa on czasem nazywany aspektem logicznym funkcji.

Pani doktur, mamy diagnozę! Tylko co z nią zrobić? Czy jest jakaś metoda, żeby rozdzielić obliczeniowy i logiczny aspekt danej funkcji, a potem poskładać je do kupy? Pomyślmy najpierw nad aspektem obliczeniowym. Czy da się zdefiniować funkcję bezpośrednio za pomocą jej definicji docelowej, czyli równania rekurencyjnego? Żeby to zrobić, musielibyśmy mieć możliwość robienia rekursji o dokładnie takim kształcie, jaki ma mieć ta funkcja... Eureka! Przecież mamy coś, co pozwala nam na rekursję o dokładnie takim kształcie, a mianowicie induktywny wykres! Ale przecież wykres wiąże ze sobą argumenty i wynik, a my chcemy dopiero zdefiniować coś, co ów wynik obliczy... czyli nie eureka? Nie do końca. Możemy zmodyfikować definicję wykresu, wyrzucając z niej wszystkie wzmianki o wyniku, uzyskując w ten sposób predykat będący induktywną charakteryzacją dziedziny naszej funkcji. Dzięki niemu możemy zdefiniować zmodyfikowaną wersję funkcji, w której dodatkowym argumentem jest dowód na to, że argumenty należą do dziedziny. Logiczny aspekt funkcji, czyli dowód terminacji, sprowadza się w takiej sytuacji do pokazania, że wszystkie argumenty należą do dziedziny (czyli spełniają predykat dziedziny). Żeby zdefiniować oryginalną funkcję, wystarczy jedynie poskładać oba aspekty do kupy, czyli wstawić dowód terminacji do zmodyfikowanej funkcji. Żeby nie utonąć w ogólnościach, zobaczmy, jak nasz wspaniały wynalazek radzi sobie z dzieleniem.

Tak wygląda predykat dziedziny dla dzielenia. Zauważmy, że tak naprawdę to nie jest to predykat, bo bierze dwa argumenty i co więcej nie zwraca Prop, lecz Type. Nie będziemy się tym jednak przejmować - dla nas divD będzie "predykatem dziedziny". Zauważmy też, że nie jest to predykat dziedziny dla div, lecz dla div', czyli zupełnie nowej funkcji, którą zamierzamy zdefiniować. Ok, przejdźmy do konkretów. div' ma mieć typ nat -> nat -> nat, a zatem divD ma dwa indeksy odpowiadające dwóm argumentom div'. Pierwszy konstruktor głosi, że jeżeli n < S m, to oba te argumenty należą do dziedziny (bo będziemy chcieli w tym przypadku zwrócić 0). Drugi konstruktor głosi, że jeżeli n >= S m, to para argumentów n i m należy do dziedziny pod warunkiem, że para argumentów n - S m i m należy do dziedziny. Jest tak, gdyż w tym przypadku będziemy chcieli zrobić wywołanie rekurencyjne właśnie na n - S m oraz m.

Dzięki divD możemy zdefiniować funkcję div'_aux, której typem jest forall n m : nat, divD n m -> nat. Jest to funkcja pomocnicza, która posłuży nam do zdefiniowania właściwej funkcji div'. Ponieważ divD jest zdefiniowane induktywnie, docelowa definicja div' jest strukturalnie rekurencyjna po argumencie H : divD n m, mimo że nie jest strukturalnie rekurencyjna po n ani m. To właśnie jest magia stojąca za metodą induktywnej dziedziny - możemy sprawić, żeby każda (no, prawie), nawet najdziwniejsza rekursja była strukturalnie rekurencyjna po dowodzie należenia do dziedziny. Definicja jest banalna. Gdy natrafimy na konstruktor divD_lt, zwracamy 0 (bo wiemy, że jednym z argumentów divD_lt jest dowód na to, że n < S m). Jeżeli trafimy na divD_ge, to wiemy, że n >= S m, więc robimy wywołanie rekurencyjne na H' : divD (n - S m) m i dorzucamy do wyniku S. W ten sposób zdefiniowaliśmy obliczeniową część div', zupełnie nie przejmując się kwestią terminacji.

Dowód terminacji jest bliźniaczo podobny do naszej pierwszej definicji div. Zaczynamy przez rekursję dobrze ufundowaną z porządkiem lt (i dowodem wf_lt na to, że lt jest dobrze ufundowany), wprowadzamy zmienne do kontekstu, po czym sprawdzamy, który z przypadków zachodzi. Jeżeli n >= S m, używamy konstruktora divD_ge. n >= S m zachodzi na mocy założenia, zaś n - S m i m należą do dziedziny na mocy hipotezy indukcyjnej. Gdy n < S m, n i m należą do dziedziny na mocy założenia.

A oto i ostateczna definicja - wstawiamy dowód divD_all do funkcji pomocniczej div'_aux i uzyskujemy pełnoprawną funkcję dzielącą div' : nat -> nat -> nat.

Jak widać, wynik oblicza się bez problemu. Po raz kolejny przypominam, że div' n m oblicza n/(m + 1), nie zaś n/m. Przypominam też, że dowód divD_all koniecznie musimy zakończyć za pomocą komendy Defined, a nie jak zazwyczaj Qed, gdyż w przeciwnym przypadku funkcja div' nie mogłaby niczego obliczyć.

Żeby udowodnić regułę indukcji wykresowej, będziemy potrzebowali tego samego co poprzednio, czyli twierdzeń o poprawności i pełności funkcji div' względem wykresu divG. Dowody są jednak dużo prostsze niż ostatnim razem. Najpierw dowodzimy, że funkcja pomocnicza div'_aux oblicza taki wynik, jakiego spodziewa się wykres divG. Dowód jest banalny, bo indukcja po d : divD n m ma dokładnie taki kształt, jakiego nam potrzeba. Właściwy dowód dla div' uzyskujemy przez wyspecjalizowanie divG_div'_aux do div'.

Dowód pełności i dowód reguły indukcji wykresowej są dokładnie takie same jak poprzednio. Zauważ, że tym razem zupełnie zbędne okazało się równanie rekurencyjne, bez którego nie mogliśmy obyć się ostatnim razem. Jednak jeżeli chcemy, możemy bez problemu je udowodnić, i to nawet na dwa sposoby.

Pierwszy, trudniejszy sposób, to zgeneralizowanie divD_all n m do dowolnego d oraz indukcja po d (to tak, jakbyśmy najpierw udowodnili tę regułę dla div'_aux, a potem wyspecjalizowali do div'). Drugi, łatwiejszy sposób, realizuje nasz początkowy pomysł, od którego wszystko się zaczęło: dowodzimy równania rekurencyjnego za pomocą reguły indukcji wykresowej.

Ćwiczenie

Zdefiniuj funkcję rot, która bierze liczbę n oraz listę i zwraca listę, w której bloki o długości dokładnie n + 1 zostały odwrócone, np. rot 0 [1; 2; 3; 4; 5; 6; 7] = [1; 2; 3; 4; 5; 6; 7] rot 1 [1; 2; 3; 4; 5; 6; 7] = [2; 1; 4; 3; 6; 5; 7] rot 2 [1; 2; 3; 4; 5; 6; 7] = [3; 2; 1; 6; 5; 4; 7] Wskazówka: rzecz jasna użyj metody induktywnej dziedziny. Nie bez przyczyny także w jednym z poprzednich zadań kazałem ci zdefiniować funkcję split, która odkraja od listy blok o odpowiedniej długości. Następnie zdefiniuj wykres funkcji rot i udowodnij jej regułę indukcji wykresowej oraz równanie rekurencyjne. Użyj jej, żeby pokazać, że rot jest inwolucją dla dowolnego n, tzn. rot n (rot n l) = l. Uwaga: potrzebne będzie trochę lematów.

Ćwiczenie

Zdefiniuj funkcję Eratosthenes : nat -> list nat, która dla danego n znajduje listę wszystkich liczb pierwszych, które są mniejsze lub równe n. Jako funkcję pomocniczą zaimplementuj sito Eratosthenesa. Sito to funkcja sieve : list nat -> list nat, która działa tak:

• jeżeli wejście jest puste, zwróć listę pustą
• jeżeli wejście ma głowę h i ogon t, to wstaw h na początek wyniku i wywołaj się rekurencyjnie na ogonie t z odfiltrowanymi wszystkimi wielokrotnościami głowy h

Jeżeli jako argument sieve podamy listę wszystkich liczb poczynając od pewnej liczby pierwszej p aż do n, to otrzymamy listę liczb pierwszych między p i n. Żeby sprawnie rozwiązać to zadanie, zgeneralizuj funkcję sieve na dowolny typ A i funkcję porównującą cmp : A -> A -> bool (tak będzie łatwiej) i użyj metody induktywnej dziedziny.

Komenda Function

Odkryliśmy uniwersalną metodę definiowania funkcji i dowodzenia ich właściwości. Czego chcieć więcej? Po pierwsze, metoda definiowania nie jest uniwersalna (jeszcze), o czym przekonamy się w kolejnych podrozdziałach. Po drugie, mimo że metoda dowodzenia faktycznie jest uniwersalna, to komu normalnemu chciałoby się przy każdej funkcji tyle pisać? Jakieś wykresy, dziedziny, lematy, reguły indukcji, co to ma być? Czy w celu sprawnego definiowania i dowodzenia właściwości funkcji trzeba zoutsourcować cały proces i zatrudnić milion Hindusów? Na szczęście nie, gdyż bóg dał nam komendę Function.

Komenda ta żyje w module Recdef, którego nazwa jest skrótem od słów "recydywista defraudator"... dobra, koniec żartów.

Definicja zaczyna się od słowa kluczowego Function, następnie mamy nazwę funkcji i argumenty, tak jak w zwykłych definicjach za pomocą Definition czy Fixpoint, a później tajemniczą klauzulę {measure id n}, do której zaraz wrócimy, i zwracany typ. Ciało definicji wygląda dokładnie jak docelowa definicja. Jednak po kropce definicja nie kończy się - zamiast tego Coq każe nam udowodnić, że wywołanie rekurencyjne div'' odbywa się na argumencie mniejszym niż n. Po zakończeniu dowodu funkcja zostaje zaakceptowana przez Coqa. To jednak nie koniec. Komenda Function nie tylko pozwala bezboleśnie zdefiniować div'', ale też generuje dla nas całą masę różnych rzeczy:

• div''_tcc to lemat, który mówi, że wszystkie wywołania rekurencyjne są na argumencie mniejszym od obecnego
• div''_terminate to dowód tego, że funkcja terminuje (czyli że się nie zapętla). Jeżeli przyjrzysz się jego typowi, to zobaczysz, że jest podobny zupełnie do niczego. Wynika to z faktu, że komenda Function tak naprawdę nie używa metody induktywnej dziedziny, ale pewnej innej metody definiowania funkcji ogólnie rekurencyjnych. Nie powinno nas to jednak martwić - ważne, że działa.
• div''_ind to reguła indukcji wykresowej dla div''. Jest też jej wariant div''_rect, czyli "rekursja wykresowa", służąca raczej do definiowania niż dowodzenia.
• R_div'' to induktywnie zdefiniowany wykres funkcji div''. Zauważ jednak, że nie jest on relacją, a rodziną typów - nie wiem po co i nie ma co wnikać w takie detale.
• R_div''_correct to twierdzenie o poprawności wykresu.
• R_div''_complete to twierdzenie o pełności wykresu.
• div''_equation to równanie rekurencyjne

Jak więc widać, nastąpił cud automatyzacji i wszystko robi się samo. To jednak nie koniec udogodnień. Zobaczmy, jak możemy udowodnić jakiś fakt o div''.

Dowodzenie właściwości funkcji zdefiniowanych za pomocą Function jest bajecznie proste. Jeżeli wszystkie argumenty funkcji znajdują się w kontekście, to możemy użyć taktyki functional induction (nazwa_funkcji argument_1 ... argument_n), która odpala indukcję wykresową dla tej funkcji. Z powodu nazwy tej taktyki indukcja wykresowa bywa też nazywana indukcją funkcyjną. Wujek Dobra Rada: nigdy nie odwijaj definicji funkcji zdefiniowanych za pomocą Function ani nie próbuj ręcznie aplikować reguły indukcji wykresowej, bo skończy się to jedynie bólem i zgrzytaniem zębów. Na koniec wypadałoby jedynie dodać, że wcale nie złapaliśmy pana boga za nogi i komenda Function nie rozwiązuje wszystkich problemów pierwszego świata. W szczególności niektóre funkcje mogą być tak upierdliwe, że komenda Function odmówi współpracy z nimi. Radzeniu sobie z takimi ciężkimi przypadkami poświęcimy kolejne podrozdziały.

Ćwiczenie

Zdefiniuj funkcję rot (i wszystkie funkcje pomocnicze) jeszcze raz, tym razem za pomocą komendy Function. Porównaj swoje definicje wykresu oraz reguły indukcji z tymi automatycznie wygenerowanymi. Użyj taktyki functional induction, żeby jeszcze raz udowodnić, że rot jest inwolucją. Policz, ile pisania udało ci się dzięki temu zaoszczędzić. Czy w twoim rozwiązaniu są lematy, w których użycie indukcji funkcyjnej znacznie utrudnia przeprowadzenie dowodu? W moim poprzednim rozwiązaniu był jeden taki, ale wynikał z głupoty i już go nie ma.

Rekursja zagnieżdżona

Jakież to diabelstwo może być tak diabelskie, by przeciwstawić się metodzie induktywnej dziedziny oraz komendzie Function? Ano ano, rekursja zagnieżdżona - wywołanie rekurencyjne jest zagnieżdżone, jeżeli jego argumentem jest wynik innego wywołania rekurencyjnego.

Ta funkcja jest podobna zupełnie do niczego, co dotychczas widzieliśmy. Działa ona następująco:

• jeżeli n jest większe od 100, to zwróć n - 10
• w przeciwnym wypadku wywołaj rekurencyjnie f na n + 11, a następnie wywołaj f na wyniku tamtego wywołania.

Taka rekursja jest oczywiście nielegalna: n + 11 nie jest strukturalnym podtermem n, gdyż jest od niego większe, zaś f (n + 11) w ogóle nie wiadomo a priori, jak się ma do n. Nie dziwota więc, że Coq odrzuca powyższą definicję. Być może wobec tego taka "funkcja" w ogóle nie jest funkcją, a definicja jest wadliwa? Otóż nie tym razem. Okazuje się bowiem, że istnieje funkcja zachowująca się zgodnie z zawartym w definicji równaniem. Żebyśmy mogli w to uwierzyć, zastanówmy się, ile wynosi f 100. f 100 = f (f 111) = f 101 = 101 - 10 = 91 - poszło gładko. A co z 99? Mamy f 99 = f (f 110) = f 100 = 91 - znowu 91, czyżby spiseg? Dalej: f 98 = f (f 109) = f 99 = 91 - tak, to na pewno spiseg. Teraz możemy zwerbalizować nasze domysły: jeżeli n <= 100, to f n = 91. Jak widać, nieprzypadkowo funkcja ta bywa też nazywana "funkcją 91 McCarthy'ego". Czy da się tę funkcję zaimplementować w Coqu? Jeszcze jak!

Ehhh... nie tego się spodziewałeś, prawda? f_troll jest wprawdzie implementacją opisanej powyżej nieformalnie funkcji f, ale definicja opiera się na tym, że z góry wiemy, jaki jest wynik f dla dowolnego argumentu. Nie trzeba chyba tłumaczyć, że dla żadnej ciekawej funkcji nie będziemy posiadać takiej wiedzy (a sama funkcja McCarthy'ego nie jest ciekawa, bo jest sztuczna, ot co!). Czy więc da się zaimplementować f bezpośrednio, tzn. w sposób dokładnie oddający definicję nieformalną? Otóż tak, da się i to w sumie niewielkim kosztem: wystarczy jedynie nieco zmodyfikować naszą metodę induktywnej dziedziny. Zanim jednak to zrobimy, zobaczmy, dlaczego nie obejdzie się bez modyfikacji.

A oto i źródło całego problemu. Jeżeli n <= 100, to chcemy zrobić dwa wywołania rekurencyjne: jedno na n + 11, a drugie na f (n + 11). Wobec tego należenie tych dwóch argumentów do dziedziny jest warunkiem należenia n do dziedziny i stąd postać całego konstruktora. Niestety, definicja jest zła - f (n + 11) nie jest poprawnym termem, gdyż f nie jest jeszcze zdefiniowane. Mamy więc błędne koło: żeby zdefiniować f, musimy zdefiniować predykat dziedziny fD, ale żeby zdefiniować fD, musimy zdefiniować f. Jak wyrwać się z tego błędnego koła? Ratunek przychodzi ze strony być może nieoczekiwanej, ale za to już bardzo dobrze przez nas poznanej, a jest nim induktywna definicja wykresu. Tak tak - w definicji fD możemy (a nawet musimy) zastąpić wystąpienia f przez wystąpienia wykresu f. Hej ho, po przykład by się szło.

Tak wygląda wykres funkcji f. Wywołanie rekurencyjne f (f (n + 11) możemy zareprezentować jako dwa argumenty, mianowicie fG (n + 11) r1 i fG r1 r2. Dosłownie odpowiada to wywołaniu rekurencyjnemu w stylu let r1 := f (n + 11) in let r2 := f r1 in r2.

Po zdefiniowaniu wykresu dowodzimy, podobnie łatwo jak poprzednio, że jest on relacją deterministyczną.

A tak wygląda definicja predykatu dziedziny. Zamiast fD (f (n + 11)) mamy fD r, gdyż r na mocy argumentu fG (n + 11) r reprezentuje wynik wywołania rekurencyjnego f (n + 11).

Definicja funkcji pomocniczej f' może być nieco zaskakująca: gdzie podziało się zagnieżdżone wywołanie rekurencyjne? Nie możemy jednak dać się zmylić przeciwnikowi. Ostatnią klauzulę dopasowania do wzorca możemy zapisać jako | fD_le100 n r H g d1 d2 => f' d2. Widzimy, że d2 jest typu fD r, ale g : fG (n + 11) r, więc możemy myśleć, że r to tak naprawdę f (n + 11), a zatem d2 tak naprawdę jest typu fD (f (n + 11)). Jeżeli dodatkowo napiszemy wprost domyślny argument f', to wywołanie rekurencyjne miałoby postać @f' (@f' (n + 11) d1) d2, a więc wszystko się zgadza. Żeby jednak nie rzucać słów na wiatr, udowodnijmy to.

Dowód twierdzenia o poprawności jest tylko odrobinkę trudniejszy niż ostatnio, gdyż w przypadku wystąpienia w kontekście dwóch hipotez o typie fG (n + 11) _ musimy użyć twierdzenia o determinizmie wykresu.

Dowód twierdzenia o pełności pozostaje bez zmian.