UWAGA: ten rozdział właśnie ulega konceptualnemu przeobrażeinu i może być nie na miejscu, tzn. zawierać rzeczy, o których jeszcze nie było mowy.

Różnice między bool, Prop i SProp

Rozstrzygalność

Próba udowodnienia tego twierdzenia pokazuje nam zasadniczą różnicę między logiką konstruktywną, która jest domyślną logiką Coqa, oraz logiką klasyczną, najpowszechniej znanym i używanym rodzajem logiki. Każde zdanie jest, w pewnym "filozoficznym" sensie, prawdziwe lub fałszywe i to właśnie powyższe zdanie oznacza w logice klasycznej. Logika konstruktywna jednak, jak już wiemy, nie jest logiką prawdy, lecz logiką udowadnialności i ma swoją interpretację obliczeniową. Powyższe zdanie w logice konstruktywnej oznacza: program komputerowy exluded_middle rozstrzyga, czy dowolne zdanie jest prawdziwe, czy fałszywe. Skonstruowanie programu o takim typie jest w ogólności niemożliwe, gdyż dysponujemy zbyt małą ilością informacji: nie wiemy czym jest zdanie P, a nie posiadamy żadnego ogólnego sposobu dowodzenia lub obalania zdań o nieznanej nam postaci. Nie możemy np. użyć indukcji, gdyż nie wiemy, czy zdanie P zostało zdefiniowane induktywnie, czy też nie. W Coqu jedynym sposobem uzyskania termu o typie forall P : Prop, P \/ ~ P jest przyjęcie go jako aksjomat.

Powyższe dywagacje nie przeszkadzają nam jednak w udowadnianiu, że reguła wyłączonego środka zachodzi dla pewnych konkretnych zdań. Zdanie takie będziemy nazywać zdaniami rozstrzygalnymi (ang. decidable). O pozostałych zdaniach będziemy mówić, że są nierozstrzygalne (ang. undecidable). Ponieważ w Coqu wszystkie funkcje są rekurencyjne, a dowody to programy, to możemy powyższą definicję rozumieć tak: zdanie jest rozstrzygalne, jeżeli istnieje funkcja rekurencyjna o przeciwdzidzinie bool, która sprawdza, czy jest ono prawdziwe, czy fałszywe. Przykładami zdań, predykatów czy problemów rozstrzygalnych są:

• sprawdzanie, czy lista jest niepusta
• sprawdzanie, czy liczba naturalna jest parzysta
• sprawdzanie, czy dwie liczby naturalne są równe

Przykładem problemów nierozstrzygalnych są:

• dla funkcji f g : nat -> nat sprawdzenie, czy forall n : nat, f n = g n — jest to w ogólności niemożliwe, gdyż wymaga wykonania nieskończonej ilości porównań (co nie znaczy, że nie da się rozwiązać tego problemu dla niektórych funkcji)
• sprawdzenie, czy słowo o nieskończonej długości jest palindromem

Ćwiczenie

Techniczne apekty rozstrzygalności

Podsumowując powyższe rozważania, moglibyśmy stwierdzić: zdanie P jest rozstrzygalne, jeżeli istnieje term typu P \/ ~ P. Stwierdzenie takie nie zamyka jednak sprawy, gdyż bywa czasem mocno bezużyteczne. Żeby to zobrazować, spróbujmy użyć twierdzenia eq_nat_dec do napisania funkcji, która sprawdza, czy liczna naturalna n występuje na liście liczb naturalnych l:

Coq nie akceptuje powyższego kodu, racząc nas informacją o błędzie:

Nasza porażka wynika z faktu, że do zdefiniowania funkcji, która jest programem (jej dziedzina i przeciwdziedzina są sortu Type) próbowaliśmy użyć termu eq_nat_dec n h, który jest dowodem (konkluzją eq_nat_dec jest równość, która jest sortu Prop). Mimo korespondencji Curry'ego-Howarda, która odpowiada za olbrzymie podobieństwo specyfikacji i zdań, programów i dowodów, sortu Type i sortu Prop, są one rozróżniane i niesie to za sobą konsekwencje: podczas gdy programów możemy używać wszędzie, dowodów możemy używać jedynie do konstruowania innych dowodów. Praktycznie oznacza to, że mimo iż równość liczb naturalnych jest rozstrzygalna, pisząc program nie mamy możliwości jej rozstrzygania za pomocą eq_nat_dec. To właśnie miałem na myśli pisząc, że termy typu P \/ ~ P są mocno bezużyteczne. Uszy do góry: nie wszystko stracone! Jest to tylko drobna przeszkoda, którą bardzo łatwo ominąć:

Typ sumbool jest niemal dokładną kopią or, jednak nie żyje on w Prop, lecz w Type. Ta drobna sztuczka, że termy typu sumbool A B formalnie są programami, mimo że ich naturalna interpretacja jest taka sama jak or, a więc jako dowodu dysjunkcji.

Ćwiczenie

Udowodnij twierdzenie eq_nat_dec' o rozstrzygalności = na liczbach naturalnych. Użyj typu sumbool. Następnie napisz funkcję inb_nat, która sprawdza, czy liczba naturalna n jest obecna na liście l.

Kiedy nie warto rozstrzygać? (TODO)

Tutaj coś w stylu n < m \/ n = m \/ n > m

Rozstrzygalność jako pułapka na negacjonistów (TODO)

Techniczne aspekty rozstrzygalności 2 (TODO)

Ślepota boolowska (TODO)

Reflekcja w małej skali (TODO)

Poradnik hodowcy, czyli jak nie rozmnażać definicji (TODO)