Indukcja wzajemna

Jest jeszcze jeden rodzaj indukcji, o którym dotychczas nie mówiliśmy: indukcja wzajemna (ang. mutual induction). Bez zbędnego teoretyzowania zbadajmy sprawę na przykładzie klasyków polskiej literatury: Smok to wysuszony zmok Zmok to zmoczony smok Stanisław Lem Idea stojąca za indukcją wzajemną jest prosta: chcemy przez indukcję zdefiniować jednocześnie dwa obiekty, które mogą się nawzajem do siebie odwoływać. W owym definiowaniu nie mamy rzecz jasna pełnej swobody — obowiązują te same kryteria co w przypadku zwykłych, "pojedynczych" definicji typów induktywnych. Wobec tego zauważyć należy, że definicja słowa "smok" podana przez Lema jest według Coqowych standardów nieakceptowalna, gdyż jeżeli w definicji smoka rozwiniemy definicję zmoka, to otrzymamy Smok to wysuszony zmoczony smok Widać gołym okiem, iż próba zredukowania (czyli obliczenia) obiektu smok nigdy się nie skończy. Jak już wiemy, niekończące się obliczenia w logice odpowiadają sprzeczności, a zatem ani smoki, ani zmoki w Coqowym świecie nie istnieją. Nie znaczy to bynajmniej, że wszystkie definicje przez indukcję wzajemną są w Coqu niepoprawne, choć należy przyznać, że są dość rzadko używane. Czas jednak abyśmy ujrzeli pierwszy prawdziwy przkład indukcji wzajemnej.

Aby zrozumieć tę definicję, zestawmy ją z naszą definicją parzystości z sekcji Induktywne predykaty. Zdefiniowaliśmy tam predykat bycia liczbą parzystą tak:

• 0 jest parzyste
• jeżeli n jest parzyste, to n + 2 też jest parzyste

Tym razem jednak nie definiujemy jedynie predykatu "jest liczbą parzystą". Definiujemy jednocześnie dwa predykaty: "jest liczbą parzystą" oraz "jest liczbą nieparzystą", które odwołują się do siebi nawzajm. Definicja brzmi tak:

• 0 jest parzyste
• jeżeli n jest nieparzyste, to n + 1 jest parzyste
• jeżeli n jest parzyste, to n + 1 jest nieparzyste

Czy definicja taka rzeczywiście ma sens? Sprawdźmy to:

• 0 jest parzyste na mocy definicji
• jeżeli 0 jest parzyste (a jest), to 1 jest nieparzyste
• jeżeli 1 jest nieparzyste (a jest), to 2 jest parzyste
• i tak dalej, ad infinitum

Jak widać, za pomocą naszej wzajemnie induktywnej definicji even można wygenerować wszystkie liczby parzyste (i tylko je), tak więc nowe even jest równoważne staremu even z sekcji Induktywne predykaty. Podobnie odd może wygenerować wszystkie liczby nieparzyste i tylko je.

Ćwiczenie (upewniające)

Upewnij się, że powyższy akapit nie kłamie.

Ćwiczenie (właściwości even i odd)

Udowodnij podstawowe właściwości even i odd.

Jeśli poległeś przy ostatnim zadaniu — nie przejmuj się. Specjalnie dobrałem złośliwy przykład. W tym momencie należy sobie zadać pytanie: jak dowodzić właściwości typów wzajemnie induktywnych? Aby udzielić odpowiedzi, spróbujmy udowodnić even_plus za pomocą indukcji po n, a potem prześledźmy, co poszło nie tak.

Nasza indukcja po n zawiodła, gdyż nasza hipoteza indukcyjna ma w konkluzji even (n + m), podczas gdy nasz cel jest postaci odd (n + m). Zauważmy, że teoretycznie cel powinno dać się udowodnić, jako że mamy hipotezy even m oraz odd n, a suma liczby parzystej i nieparzystej jest nieparzysta. Nie zrażajmy się jednak i spróbujmy indukcji po dowodzie even n.

Nasza indukcja po dowodzie hipotezy even n zawiodła, i to z kretesem, gdyż w kontekście nie mamy nawet żadnej hipotezy indukcyjnej! Co właściwie się stało?

Jak widać, w naszej hipotezie "indukcyjnej" wygenerowanej przez Coqa w ogóle nie ma żadnej indukcji. Jest tam jedynie odwołanie do predykatu odd... Zauważmy jednak, że naszym celem znów było odd (n + m), a hipotezy odd n oraz even m sprawiają, że w teorii powinno dać się ten cel udowodnić, gdyż suma liczby parzystej i nieparzystej jest nieparzysta. Mogłoby się zdawać, że cierpimy na niedopasowanie (próba 1) lub brak (próba 2) hipotez indukcyjnych. Wydaje się też, że skoro w obydwu próbach zatrzymaliśmy się na celu odd (n + m), to pomocne mogłoby okazać się poniższe twierdzenie.

Niestety — nie dla psa kiełbasa, gdyż natykamy się na problemy bliźniaczo podobne do tych, które napotkaliśmy w poprzednim twierdzeniu: nasza hipoteza indukcyjna ma w konkluzji odd (n + m), podczas gdy nasz cel jest postaci even (n + m). Próba przepchnięcia lematu za pomocą indukcji po dowodzie hipotezy odd n także nie zadziała, z tych samych powodów dla których indukcja po even n nie pozwoliła nam udowodnić even_plus. Zauważmy jednak, że cel jest udowadnialny, gdyż jako hipotezy mamy even n oraz even m, a suma dwóch liczb parzystych jest parzysta. Wydaje się, że wpadliśmy w błędne koło i jesteśmy w matni, bez wyjścia, bez nadziei, bez krzty szans na powodzenie: w dowodzie even_plus potrzebujemy lematu odd_even_plus, ale nie możemy go udowodnić, gdyż w dowodzie odd_even_plus wymagane jest użycie lematu even_plus. Ehhh, gdybyśmy tak mogli udowodnić oba te twierdzenia na raz... Eureka! Zauważ, że w naszych dotychczasowych dowodach przez indukcję posługiwaliśmy się zwykłą, "pojedynczą" indukcją. Była ona wystarczająca, gdyż mieliśmy do czynienia jedynie ze zwykłymi typami induktywnymi. Tym razem jednak jest inaczej: w ostatnich trzech dowodach chcieliśmy użyć "pojedynczej" indukcji do udowodnienia czegoś na temat predykatów wzajemnie induktywnych. Jest to ogromny zgrzyt. Do dowodzenia właściwości typów wzajemnie induktywnych powinniśmy użyć... o zgrozo, jak mogliśmy to przeoczyć, przecież to takie oczywiste... indukcji wzajemnej! Najprostszy sposób przeprowadzenia tego dowodu wygląda tak:

Co tu się właściwie stało? Pierwsze dwie linijki są takie same jak poprzednio: stwierdzamy, że będziemy dowodzić twierdzenia o podanej nazwie i postaci. Następnie mamy słowo kluczowe with, które pełni tu rolę podobną jak w definicjach przez indukcję wzajemną: podając po nim nazwę i postać twierdzenia mówimy Coqowi, że chcemy dowodzić tego twierdzenia (odd_even_plus) jednocześnie z poprzednim (even_plus). Dotychczas po rozpoczęciu dowodu ukazywał nam się jeden cel. Tym razem, jako że dowodzimy dwóch twierdzeń jednocześnie, mamy przed sobą dwa cele. W kontekście mamy też od razu dwie hipotezy indukcyjne. Musimy na nie bardzo uważać: dotychczas hipotezy indukcyjne pojawiały się dopiero w kroku indukcyjnym i sposób ich użycia był oczywisty. Tym razem jest inaczej — jako, że mamy je od samego początku, możemy natychmiast użyć ich do "udowodnienia" naszych twierdzeń. Niestety, takie "udowodnienie" odpowiada wywołaniu rekurencyjnemu na argumencie, który nie jest strukturalnie mniejszy (coś jak f x := f x). Fakt ten obrazuje wiadomość o błędzie, jaką Coq daje nam po tej próbie:

Zaczynamy dowód od nowa, tym razem już bez oszukiwania. Musimy udowodnić każdy z naszych celów osobno, ale możemy korzystać z obydwu hipotez indukcyjnych. W obydwu celach zaczynamy od analizy przypadków, czyli rozbicia n, i rozwiązania przypadku bazowego. Rozbicie n dało nam n', które jest strukturalnie mniejsze od n, a zatem możemy bez obaw użyć naszej hipotezy indukcyjnej. Reszta jest trywialna.

Reguły indukcji dla typów wzajemnych (TODO)

Indukcja wzajemna pozwala definiować na raz wiele typów, które mogą odwoływać się do siebie nawzajem. Cytując klasyków: smok to wysuszony zmok, zmok to zmoczony smok.

Reguła niezależnej analizy przypadków dla Smoka wygląda banalnie: jeżeli ze Zmoka potrafimy wyprodukować S, to ze Smoka też. Dla Zmoka jest analogicznie.

Implementacja jest banalna.

Typ rekursora jest jednak nieco bardziej zaawansowany. Żeby zdefiniować funkcję typu Smok -> S, musimy mieć nie tylko rzeczy w kształcie konstruktorów Smoka, ale także w kształcie konstruktorów Zmoka, gdyż rekurencyjna struktura obu typów jest ze sobą nierozerwalnie związana.

Implementacja wymaga rekursji wzajemnej, ale poza nie jest jakoś wybitnie groźna.

Mając rekursor, napisanie typu reguły indukcji jest banalne, podobnie jak jego implementacja.