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.

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ą.

Funkcja Ackermanna

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.

Scalanie posortowanych list

Ć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.