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.

Teraz następuje mały twist. Udowodnienie, że każdy argument spełnia fD będzie piekielnie trudne i będziemy w związku z tym potrzebować charakteryzacji funkcji f'. Zaczynamy więc od udowodnienia, że dla n <= 100 wynikiem jest 91. Najpierw robimy to na wykresie, bo tak jest łatwiej, a potem transferujemy wynik na funkcję. Charakteryzację dla 100 < n dostajemy wprost z definicji.

Dowód jest przez indukcję dobrze ufundowaną po n, a relacja dobrze ufundowana, której używamy, to fun n m : nat => 101 - n < 101 - m. Dlaczego akurat taka? Przypomnijmy sobie, jak dokładnie oblicza się funkcja f, np. dla 95: f 95 = f (f 106) = f 96 = f (f 107) = f 97 = f (f 108) = f 98 = f (f 109) = f 99 = f (f 110) = f 100 = f (f 111) = f 101 = 91. Jak więc widać, im dalej w las, tym bardziej zbliżamy się do magicznej liczby 101. Wyrażenie 101 - n mówi nam, jak blisko przekroczenia 101 jesteśmy, a więc 101 - n < 101 - m oznacza, że każde wywołanie rekurencyjne musi być bliżej 101 niż poprzednie wywołanie. Oczywiście zamiast 101 może być dowolna większa liczba - jeżeli zbliżamy się do 101, to zbliżamy się także do 1234567890. Dowód dobrego ufundowania jest banalny, ale tylko pod warunkiem, że zrobiłeś wcześniej odpowiednie ćwiczenie. Jeszcze jedna uwaga: jak wymyślić relację dobrze ufundowaną, jeżeli jest nam potrzebna przy dowodzie takim jak ten? Mógłbym ci tutaj naopowiadać frazesów o... w sumie nie wiem o czym, ale prawda jest taka, że nie wiem, jak się je wymyśla. Tej powyższej wcale nie wymyśliłem sam - znalazłem ją w świerszczyku dla bystrzaków. Dobra, teraz właściwa część dowodu. Zaczynamy od analizy przypadków. Drugi przypadek, gdy 100 < n, jest bardzo łatwy. W pierwszym zaś przypadku z hipotezy indukcyjnej dostajemy fD (n + 11), tzn. n + 11 należy do dziedziny. Skoro tak, to używamy konstruktora fD_le100, a jako r (czyli wynik wywołania rekurencyjnego) dajemy mu f' d. Dwa podcele zachodzą na mocy założenia, a jedna wynika z twierdzenia o poprawności. Pozostaje nam zatem pokazać, że f' d także należy do dziedziny. W tym celu po raz kolejny używamy hipotezy indukcyjnej. Na zakończenie robimy analizę przypadków po d, używamy charakteryzacji f' do uproszczenia celu i kończymy rozumowaniami arytmetycznymi.

Teraz możemy zdefiniować oryginalne f. Niestety, funkcja f się nie oblicza i nie wiem nawet dlaczego.

Twierdzenia o poprawności i pełności oraz charakteryzacja dla f wynikają za darmo z odpowiednich twierdzeń dla f'.

Reguły indukcji wykresowej dowodzimy tak samo jak poprzednio, czyli za pomocą twierdzeń o pełności i poprawności.

Na koniec również mały twist, gdyż równanie rekurencyjne najprościej jest udowodnić za pomocą właściwości wykresu funkcji f - jeśli nie wierzysz, to sprawdź (ale będzie to bardzo bolesne sprawdzenie). Podsumowując: zarówno oryginalna metoda induktywnej dziedziny jak i komenda Function nie radzą sobie z zagnieżdżonymi wywołaniami rekurencyjmi, czyli takimi, w których argumentem jest wynik innego wywołania rekurencyjnego. Możemy jednak poradzić sobie z tym problemem za pomocą ulepszonej metody induktywnej dziedziny, w której funkcję w definicji predykatu dziedziny reprezentujemy za pomocą jej induktywnie zdefiniowanego wykresu.

Ćwiczenie

Przyjrzyjmy się poniższej fikuśnej definicji funkcji:

Wytłumacz, dlaczego Coq nie akceptuje tej definicji. Następnie wymyśl twierdzenie charakteryzujące tę funkcję, a na koniec zdefiniuj ją za pomocą metody zaprezentowanej w tym podrozdziale.