Wstęp (TODO)

Po powtórce nadszedł czas nowości. Zacznijmy od nazwy, która jest iście kretyńska: indukcja-indukcja. Każdy rozsądny człowiek zgodzi się, że dużo lepszą nazwą byłoby coś w stylu "indukcja wzajemna indeksowana". Ta alternatywna nazwa rzuca sporo światła: indukcja-indukcja to połączenie i uogólnienie mechanizmów definiowania typów wzajemnie induktywnych oraz indeksowanych typów induktywnych. Typy wzajemnie induktywne mogą odnosić się do siebie nawzajem, ale co to dokładnie znaczy? Ano to, że konstruktory każdego typu mogą brać argumenty wszystkch innych typów definiowanych jednocześnie z nim. To jest clou całej sprawy: konstruktory. A co to ma do typów indeksowanych? Ano, zastanówmy się, co by się stało, gdybyśmy chcieli zdefiniować przez wzajemną indukcję typ A oraz rodzinę typów B : A -> Type. Otóż nie da się: konstruktory A mogą odnosić się do B i vice-versa, ale A nie może być indeksem B. Indukcja-indukcja to coś, co... tam taram tam tam... pozwala właśnie na to: możemy jednocześnie zdefiniować typ i indeksowaną nim rodzinę typów. I wszystko to ukryte pod taką smutną nazwą... lobby teoriotypowe nie chciało, żebyś się o tym dowiedział. Czas na przykład!

Listy posortowane

Jako się już wcześniej rzekło, indukcja-indukcja nie jest wspierana przez Coqa - powyższa definicja kończy się informacją o błędzie: Coq nie widzi slist kiedy czyta indeksy ok właśnie dlatego, że nie dopuszcza on możliwości jednoczesnego definiowania rodziny (w tym wypadku relacji) ok wraz z jednym z jej indeksów, slist. Będziemy zatem musieli poradzić sobie z przykładem jakoś inaczej - po prostu damy go sobie za pomocą aksjomatów. Zanim jednak to zrobimy, omówimy go dokładniej, gdyż deklarowanie aksjomatów jest niebezpieczne i nie chcemy się pomylić. Zamysłem powyższego przykładu było zdefiniowanie typu list posortowanych slist R, gdzie R pełni rolę relacji porządku, jednocześnie z relacją ok : A -> slist R -> Prop, gdzie ok x l wyraża, że dostawienie x na początek listy posortowanej l daje listę posortowaną. Przykład jest oczywiście dość bezsensowny, bo dokładnie to samo można osiągnąć bez używania indukcji-indukcji - wystarczy najpierw zdefiniować listy, a potem relację bycia listą posortowaną, a na koniec zapakować wszystko razem. Nie będziemy się tym jednak przejmować. Definicja slist R jest następująca:

• snil to lista pusta
• scons robi posortowaną listę z głowy h i ogona t pod warunkiem, że dostanie też dowód zdania ok h t mówiącego, że można dostawić h na początek listy t

Definicja ok też jest banalna:

• każdy x : A może być dostawiony do pustej listy
• jeżeli mamy listę scons h t p oraz element x, o którym wiemy, że jest mniejszy od h, tzn. R x h, to x może zostać dostawiony do listy scons h t p

Jak powinny wyglądać reguły rekursji oraz indukcji? Na szczęście wciąż działają schematy, które wypracowaliśmy dotychczas. Reguła rekursji mówi, że jeżeli znajdziemy w typie P coś o kształcie slist R, a w relacji Q coś o kształcie ok, to możemy zdefiniować funkcję slist R -> P oraz forall (x : A) (l : slist R), ok x l -> Q. Regułe indukcji można uzyskać dodając tyle zależności, ile tylko zdołamy unieść. Zobaczmy więc, jak zrealizować to wszystko za pomocą aksjomatów.

Najpierw musimy zadeklarować slist, gdyż wymaga tego typ ok. Obie definicje wyglądają dokładnie tak, jak nagłówki w powyższej definicji odrzuconej przez Coqa. Widać też, że gdybyśmy chcieli zdefiniować rodziny A i B, które są nawzajem swoimi indeksami, to nie moglibyśmy tego zrobić nawet za pomocą aksjomatów. Rodzi to pytanie o to, które dokładnie definicje przez indukcję-indukcję są legalne. Odpowiedź brzmi: nie wiem, ale może kiedyś się dowiem.

Następnie definiujemy konstruktory: najpierw konstruktory slist, a potem ok. Musimy to zrobić w tej kolejności, bo konstruktor ok_snil odnosi się do snil, a ok_scons do scons. Znowu widzimy, że gdyby konstruktory obu typów odnosiły się do siebie nawzajem, to nie moglibyśmy zdefiniować takiego typu aksjomatycznie.

Ugh, co za potfur. Spróbujmy rozłożyć go na czynniki pierwsze. Przede wszystkim, żeby za dużo nie pisać, zobaczymy tylko regułę indukcji. Teoretycznie powinny to być dwie reguły (tak jak w przypadku Smoka i Zmoka) - jedna dla slist i jedna dla ok, ale żeby za dużo nie pisać, możemy zapisać je razem. Typ A i relacja R są parametrami obu definicji, więc skwantyfikowane są na samym początku. Nasza reguła pozwala nam zdefiniować przez wzajemną rekursję dwie funkcje, f : forall l : slist R, P l oraz g : forall (h : A) (t : slist R) (p : ok h t), Q h t p. Tak więc P to kodziedzina f, a Q - g. Teraz potrzebujemy rozważyć wszystkie możliwe przypadki - tak jak przy dopasowaniu do wzorca. Przypadek snil jest dość banalny. Przypadek scons jest trochę cięższy. Przede wszystkim chcemy, żeby konkluzja była postaci P (scons h t p), ale jak powinny wyglądać hipotezy indukcyjne? Jedyna słuszna odpowiedź brzmi: odpowiadają one typom wszystkich możliwych wywołań rekurencyjnych f i g na strukturalnych podtermach scons h t p. Jedynymi typami spełniającymi te warunki są P t oraz Q h t p, więc dajemy je sobie jako hipotezy indukcyjne. Przypadki dla Q wyglądają podobnie: ok_snil jest banalne, a dla ok_scons konkluzja musi być jedynej słusznej postaci, a hipotezami indukcyjnymi jest wszystko, co pasuje. W efekcie otrzymujemy dwie funkcje, f i g. Tym razem następuje jednak mały twist: ponieważ nasza definicja jest aksjomatyczna, zagwarantować musimy sobie także reguły obliczania, które dotychczas były zamilaczne, bo wynikały z definicji przez dopasowanie do wzorca. Teraz wszystkie te "dopasowania" musimy napisać ręcznie w postaci odpowiednio skwantyfikowanych równań. Widzimy więc, że Psnil, Pscons, Qok_snil i Qok_scons odpowiadają klauzulom w dopasowaniu do wzorca. Ufff... udało się. Tak spreparowaną definicją aksjomatyczną możemy się jako-tako posługiwać:

Możemy na przykład dość łatwo zdefiniować niezależny rekursor tylko dla slist, nie odnoszący się w żaden sposób do ok. Widzimy jednak, że "programowanie" w taki aksjomatyczny sposób jest dość ciężkie - zamiast eleganckich dopasowań do wzorca musimy ręcznie wpisywać argumenty do reguły indukcyjnej.

Używanie takiego rekursora jest już dużo prostsze, co ilustruje powyższy przykład funkcji, która zapomina o tym, że lista jest posortowana i daje nam zwykłą listę. Przykładowe posortowane listy wyglądają tak:

Niezbyt piękna, prawda?

Utrapieniem jest też to, że nasza funkcja się nie oblicza. Jest tak, bo została zdefiniowana za pomocą reguły indukcji, która jest aksjomatem. Aksjomaty zaś, jak wiadomo, nie obliczają się. Wyniku powyższego wywołania nie będę nawet wklejał, gdyż jest naprawdę ohydny.

Najlepsze, co możemy osiągnąć, mając taką definicję, to udowodnienie, że jej wynik faktycznie jest taki, jak się spodziewamy.

Ćwiczenie

Zdefiniuj dla list posortowanych funkcję slen, która liczy ich długość. Udowodnij oczywiste twierdzenie wiążące ze sobą slen, toList oraz length.

Przykład był bez sensu... (TODO)

Ćwiczenie

Udowodnij, że przykład faktycznie jest bez sensu: zdefiniuje relację sorted : (A -> A -> Prop) -> list A -> Prop, gdzie sorted R l oznacza, że lista l jest posortowana według porządku R. Używając sorted zdefiniuj typ list posortowanych slist' R, a następnie znajdź dwie funkcje f : slist R -> slist' R i f : slist' R -> slist R, które są swoimi odwrotnościami.

Ćwiczenie

Żeby przekonać się, że przykład był naprawdę bezsensowny, zdefiniuj rodzinę typów blist : (A -> A -> Prop) -> A -> Type, gdzie elementami blist R x są listy posortowane, których elementy są R-większe od x. Użyj blist do zdefiniowania typu slist'' R, a następnie udowodnij, że slist R i slist'' R są sobie równoważne.

Teoria typów w teorii typów za pomocą indukcji-indukcji

Na koniec wypadałoby jeszcze wspomnieć, do czego tak naprawdę można w praktyce użyć indukcji-indukcji (definiowanie list posortowanych nie jest jedną z tych rzeczy, o czym przekonałeś się w ćwiczeniach). Otóż najciekawszym przykładem wydaje się być formalizacja teorii typów, czyli, parafrazując, implementacja Coqa w Coqu. Żeby się za to zabrać, musimy zdefiniować konteksty, typy i termy, a także relacje konwertowalności dla typów i termów. Są tutaj możliwe dwa podejścia:

• Curry'ego (ang. Curry style lub mądrzej extrinsic style) - staramy się definiować wszystko osobno, a potem zdefiniować relacje "term x jest typu A w kontekście Γ", "typ A jest poprawnie sformowany w kontekście Γ" etc. Najważniejszą cechą tego sposobu jest to, że możemy tworzyć termy, którym nie da się przypisać żadnego typu oraz typy, które nie są poprawnie sformowane w żadnym kontekście.
• Churcha (ang. Church style lub mądrzej intrinsic style) - definiujemy wszystko na raz w jednej wielkiej wzajemnej indukcji. Zamiastów typów definiujemy od razu predykat "typ A jest poprawnie sformowany w kontekście Γ", a zamiast termów definiujemy od razu relację "term x ma typ A w kontekście Γ". Parafrazując - wszystkie termy, które jesteśmy w stanie skonstruować, są poprawnie typowane (a wszystkie typy poprawnie sformowane w swoich kontekstach).

Zamiast tyle gadać zobaczmy, jak mogłoby to wyglądać w Coqu. Oczywiście będą to same nagłówki, bo podanie tutaj pełnej definicji byłoby mocno zaciemniającym przegięciem.

Nagłówki w tej definicji powinniśmy interpretować tak:

• Ctx to typ reprezentujący konteksty.
• Ty ma reprezentować typy, ale nie jest to typ, lecz rodzina typów indeksowana kontekstami - każdy typ jest typem w jakimś kontekście, np. list A jest typem w kontekście zawierającym A : Type, ale nie jest typem w pustym kontekście.
• Term ma reprezentować termy, ale nie jest to typ, lecz rodzina typów indeksowana kontekstami i typami - każdy term ma jakiś typ, a typy, jak już się rzekło, zawsze są typami w jakimś kontekście. Przykład: jeżeli x jest zmienną, to cons x nil jest typu list A w kontekście, w którym x jest typu A, ale nie ma żadnego typu (i nie jest nawet poprawnym termem) w kontekście pustym ani w żadnym, w którym nie występuje x.
• TyConv Γ A B zachodzi, gdy typy A i B są konwertowalne, czyli obliczają się do tego samego (relacja taka jest potrzebna, gdyż w Coqu i ogólnie w teorii typów występować mogą takie typy jak if true then nat else bool, który jest konwertowalny z nat). Jako się rzekło, typy zawsze występują w kontekście, więc konwertowalne mogą być też tylko w kontekście.
• TermConv Γ A x y znaczy, że termy x i y są konwertowalne, np. if true then 42 else 0 jest konwertowalne z 42. Ponieważ każdy term ciągnie za sobą swój typ, TermConv ma jako indeks typ A, a ponieważ typ ciągnie za sobą kontekst, indeksem TermConv jest także Γ.

Jak widać, indukcji-indukcji jest w powyższym przykładzie na pęczki - jest ona wręcz teleskopowa, gdyż Ctx jest indeksem Ty, Ctx i Ty są indeksami Term, a Ctx, Ty i Term są indeksami TermConv. Cóż, to by było na tyle w tym temacie. Ława oburzonych wyraża w tym momencie swoje najwyższe oburzenie na brak indukcji-indukcji w Coqu. Jednak uszy do góry - istnieją już języki, które jakoś sobie radzą z indukcją-indukcją. Jednym z nich jest wspomniana we wstępie Agda.

Sterty binarne

Ćwiczenie

Typ stert binarnych BHeap R, gdzie R : A -> A -> Prop jest relacją porządku, składa się z drzew, które mogą być albo puste, albo być węzłem przechowującym wartość v : A wraz z dwoma poddrzewami l r : BHeap R, przy czym v musi być R-większe od wszystkich elementów l oraz r. Użyj indukcji-indukcji, żeby zdefiniować jednocześnie typ BHeap R oraz relację ok, gdzie ok v h zachodzi, gdy v jest R-większe od wszystkich elementów h. Najpierw napisz pseudodefinicję, a potem przetłumacz ją na odpowiedni zestaw aksjomatów. Następnie użyj swojej aksjomatycznej definicji, aby zdefiniować funkcję mirror, która tworzy lustrzane odbicie sterty h : BHeap R. Wskazówka: prawdopodobnie nie uda ci się zdefiniować mirror. Zastanów się, dlaczego jest tak trudno.

Drzewa wyszukiwań binarnych (TODO)

Ćwiczenie

Typ drzew wyszukiwań binarnych BST R, gdzie R : A -> A -> Prop jest relacją porządku, składa się z drzew, które mogą być albo puste, albo być węzłem przechowującym wartość v : A wraz z dwoma poddrzewami l r : BST R, przy czym v musi być R-większe od wszystkich elemtnów l oraz R-mniejsze od wszystkich elementów r. Użyj indukcji-indukcji, żeby zdefiniować jednocześnie typ BST R wraz z odpowiednimi relacjami zapewniającymi poprawność konstrukcji węzła. Wypróbuj trzy podejścia:

• jest jedna relacja, oklr, gdzie oklr v l r oznacza, że z v, l i r można zrobić węzeł
• są dwie relacje, okl i okr, gdzie okl v l oznacza, że v jest R-większe od wszystkich elementów l, zaś okr v r, że v jest R-mniejsze od wszystkich elementów r
• jest jedna relacja, ok, gdzie ok v t oznacza, że v jest R-mniejsze od wszystkich elementów t

Najpierw napisz pseudodefinicję, a potem przetłumacz ją na odpowiedni zestaw aksjomatów. Następnie użyj swojej aksjomatycznej definicji, aby zdefiniować funkcję mirror, która tworzy lustrzane odbicie drzewa t : BST R. Wskazówka: dość możliwe, że ci się nie uda.