Uwaga: ten rozdział jest póki co posklejany z fragmentów innych rozdziałów. Czytając go, weź na to poprawkę. W szczególności zawiera on zadania, których nie będziesz w stanie zrobić, bo niezbędny do tego materiał jest póki co w kolejnym rozdziale. Możesz więc przeczytać część teoretyczną, a zadania pominąć (albo w ogóle pominąć cały ten rozdział).

Typy i termy

Czym są termy? Są to twory o naturze syntaktycznej (składniowej), reprezentujące funkcje, typy, zdania logiczne, predykaty, relacje etc. Polskim słowem o najbliższym znaczeniu jest słowo "wyrażenie". Zamiast prób definiowania termów, co byłoby problematyczne, zobaczmy przykłady:

• 2 — stałe są termami
• P — zmienne są termami
• Prop — typy są termami
• fun x : nat => x + 2 — λ-abstrakcje (funkcje) są termami
• f x — aplikacje funkcji do argumentu są termami
• if true then 5 else 2 — konstrukcja if-then-else jest termem

Nie są to wszystkie występujące w Coqu rodzaje termów — jest ich nieco więcej. Kolejnym fundamentalnym pojęciem jest pojęcie typu. W Coqu każdy term ma dokładnie jeden, niezmienny typ. Czym są typy? Intuicyjnie można powiedzieć, że typ to rodzaj metki, która dostarcza nam informacji dotyczących danego termu. Dla przykładu, stwierdzenie x : nat informuje nas, że x jest liczbą naturalną, dzięki czemu wiemy, że możemy użyć go jako argumentu dodawania: term x + 1 jest poprawnie typowany (ang. well-typed), tzn. x + 1 : nat, a więc możemy skonkludować, że x + 1 również jest liczbą naturalną. Innym przykładem niech będzie stwierdzenie f : nat -> nat, które mówi nam, że f jest funkcją, która bierze liczbę naturalną i zwraca liczbę naturalną. Dzięki temu wiemy, że term f 2 jest poprawnie typowany i jest liczbą naturalną, tzn. f 2 : nat, zaś term f f nie jest poprawnie typowany, a więc próba jego użycia, a nawet napisania byłaby błędem. Typy są tworami absolutnie kluczowymi. Informują nas, z jakimi obiektami mamy do czynienia i co możemy z nimi zrobić, a Coq pilnuje ścisłego przestrzegania tych reguł. Dzięki temu wykluczona zostaje możliwość popełnienia całej gamy różnych błędów, które występują w językach nietypowanych, takich jak dodanie liczby do ciągu znaków. Co więcej, system typów Coqa jest jednym z najsilniejszych, jakie dotychczas wymyślono, dzięki czemu umożliwia nam wiele rzeczy, których prawie żaden inny język programowania nie potrafi, jak np. reprezentowanie skomplikowanych obiektów matematycznych i dowodzenie twierdzeń.

Typy i termy, kanoniczność i uzasadnienie reguł eliminacji

Co to są termy? Po polsku: wyrażenia. Są to napisy zbudowane według pewnych reguł (które będziemy chcieli poznać), które mogą oznaczać przeróżne rzeczy: zdania logiczne i ich dowody, programy i ich specyfikacje, obiekty matematyczne takie jak liczby czy funkcje, struktury danych takie jak napisy czy listy. Najważniejszym, co wiemy o każdym termie, jest jego typ. Co to jest typ? To taki klasyfikator, który mówi, czego możemy się po termie spodziewać - można liczyć za pomocą liczb, ale nie za pomocą wartości logicznych. Można dowodzić zdań, ale nie napisów. Można skleić ze sobą dwa napisy, ale nie napis i funkcję etc. Każdy term ma tylko jeden typ, więc każdy typ możemy sobie wyobrazić jako wielki worek z termami. Dla przykładu, typ nat, czyli typ liczb naturalnych, to worek, w którym są takie wyrażenia, jak:

• 42
• 2 + 2
• 10 * 10
• jeżeli słowo "dupa" zawiera "i", to 123, a w przeciwnym wypadku 765
• długość listy [a, b, c, d, e]

Najważniejsze termy są nazywane elementami. Dla nat są to 0, 1, 2, 3, 4, 5 i tak dalej. Elementy wyróżnia to, że są w postaci normalnej (zwanej też postacią kanoniczną). Znaczy to intuicyjnie, że są one ostatecznymi wynikami obliczeń, np.:

• obliczenie 42 daje 42
• obliczenie 2 + 2 daje 4
• obliczenie 10 * 10 daje 100
• obliczenie ... daje 765
• obliczenie długości listy daje 5

Czym dokładnie są obliczenia, dowiemy się później. Na razie wystarczy nam wiedzieć, że każdy term zamknięty, czyli taki, o którym wiadomo wystarczająco dużo, oblicza się do postaci normalnej, np. 5 + 1 oblicza się do 6. Jeżeli jednak czegoś nie wiadomo, to term się nie oblicza, np. n + 1 nie wiadomo ile wynosi, jeżeli nie wiadomo, co oznacza n. Podsumowując, każdy element jest termem, a każdy term oblicza się do postaci normalnej, czyli do elementu.

Typy a zbiory

Z filozoficznego punktu widzenia należy stanowczo odróżnić typy od zbiorów, znanych chociażby z teorii zbiorów ZF, która jest najpowszechniej używaną podstawą współczesnej matematyki:

• zbiory są materialne, podczas gdy typy są strukturalne. Dla przykładu, zbiory {1, 2} oraz {2, 3} mają przecięcie równe {2}, które to przecięcie jest podzbiorem każdego z nich. W przypadku typów jest inaczej — dwa różne typy są zawsze rozłączne i żaden typ nie jest podtypem innego
• relacja "x ∈ A" jest semantyczna, tzn. jest zdaniem logicznym i wymaga dowodu. Relacja "x : A" jest syntaktyczna, a więc nie jest zdaniem logicznym i nie wymaga dowodu — Coq jest w stanie sprawdzić automatycznie (bez pomocy użytkownika), czy dany term jest danego typu, a często także wywnioskować z kontekstu, jakiego typu jest dany term
• zbiór to kolekcja obiektów, do której można włożyć cokolwiek. Nowe zbiory mogą być formowane ze starych w sposób niemal dowolny (aksjomaty są dość liberalne). Typ to kolekcja obiektów o takiej samej wewnętrznej naturze. Zasady formowania nowych typów ze starych są bardzo ścisłe
• teoria zbiorów mówi, jakie obiekty istnieją (np. aksjomat zbioru potęgowego mówi, że dla każdego zbioru istnieje zbiór wszystkich jego podzbiorów). Teoria typów mówi, w jaki sposób obiekty mogą być konstruowane — różnica być może ciężko dostrzegalna dla niewprawionego oka, ale znaczna

Uniwersa

Jeżeli przeczytałeś uważnie sekcję "Typy i termy" z rozdziału o logice, zauważyłeś zapewne stwierdzenie, że typy są termami. W połączeniu ze stwierdzeniem, że każdy term ma swój typ, zrodzić musi się pytanie: jakiego typu są typy? Zacznijmy od tego, że żeby uniknąć używania mało poetyckiego określenia "typy typów", typy typów nazywamy uniwersami. Czasami używa się też nazwy "sort", bo określenie "jest sortu" jest znacznie krótsze, niż "należy do uniwersum" albo "żyje w uniwersum". Prop, jak już wiesz, jest uniwersum zdań logicznych. Jeżeli x : A oraz A : Prop (tzn. A jest sortu Prop), to typ A możemy interpretować jako zdanie logiczne, a term x jako jego dowód. Na przykład I jest dowodem zdania True, tzn. I : True, zaś term 42 nie jest dowodem True, gdyż 42 : nat.

O ile jednak każde zdanie logiczne jest typem, nie każdy typ jest zdaniem — przykładem niech będą liczby naturalne nat. Sortem nat jest Set. Niech nie zmyli cię ta nazwa: Set nie ma nic wspólnego ze zbiorami znanymi choćby z teorii zbiorów ZF. Set jest uniwersum, w którym żyją specyfikacje. Jeżeli x : A oraz A : Set (tzn. sortem A jest Set), to A możemy interpretować jako specyfikację pewnej klasy programów, a term x jako program, który tę specyfikację spełnia (implementuje). Na przykład 2 + 2 jest programem, ktory spełnia specyfikację nat, tzn. 2 + 2 : nat, zaś fun n : nat => n nie spełnia specyfikacji nat, gdyż fun n : nat => n : nat -> nat.

Oczywiście w przypadku typu nat mówiene o specyfikacji jest trochę na wyrost, gdyż określenie "specyfikacja" kojarzy nam się z czymś, co określa właściwości, jakie powinien mieć spełniający ją program. O takich specyfikacjach dowiemy się więcej w kolejnych rozdziałach. Choć każda specyfikacja jest typem, to rzecz jasna nie każdy typ jest specyfikacją — niektóre typy są przecież zdaniami. Jeżeli czytasz uważnie, to pewnie wciąż czujesz niedosyt — wszakże uniwersa, jako typy, także są termami. Jakiego zatem typu są uniwersa? Przekonajmy się.

Prop oraz Set są sortu Type. To stwierdzenie wciąż jednak pewnie nie zaspakaja twojej ciekawości. Pójdźmy więc po nitce do kłębka.

Zdaje się, że osiągnęliśmy kłębek i że Type jest typu Type. Rzeczywistość jest jednak o wiele ciekawsza. Gdyby rzeczywiście zachodziło Type : Type, doszłoby do paradoksu znanego jako paradoks Girarda (którego omówienie jednak pominiemy). Prawda jest inna.

Uwaga: powyższa komenda zadziała jedynie w konsoli (program coqtop). Aby osiągnąć ten sam efekt w CoqIDE, zaznacz opcję View > Display universe levels.

Co oznacza ten dziwny napis? Otóż w Coqu mamy do czynienia nie z jednym, ale z wieloma (a nawet nieskończenie wieloma) uniwersami. Uniwersa te są numerowane liczbami naturalnymi: najniższe uniwersum ma numer 0, a każde kolejne o jeden większy. Wobec tego hierarchia uniwersów wygląda tak (użyta notacja nie jest tą, której używa Coq; została wymyślona ad hoc):

• Set żyje w uniwersum Type(0)
• Type(0) żyje w uniwersum Type(1)
• w ogólności, Type(i) żyje w uniwersum Type(i + 1)

Aby uniknąć paradoksu, definicje odnoszące się do typów żyjących na różnych poziomach hierarchii muszą same bytować w uniwersum na poziomie wyższym niż każdy z tych, do których się odwołują. Aby to zapewnić, Coq musi pamiętać, na którym poziomie znajduje każde użycie Type i odpowiednio dopasowywać poziom hierarchii, do którego wrzucone zostaną nowe definicje. Co więcej, w poprzednim rozdziale dopuściłem się drobnego kłamstewka twierdząc, że każdy term ma dokładnie jeden typ. W pewnym sensie nie jest tak, gdyż powyższa hierarcha jest kumulatywna — znaczy to, że jeśli A : Type(i), to także A : Type(j) dla i < j. Tak więc każdy typ, którego sortem jest Type, nie tylko nie ma unikalnego typu/sortu, ale ma ich nieskończenie wiele. Brawo! Czytając tę sekcję, dotarłeś do króliczej nory i posiadłeś wiedzę tajemną, której prawie na pewno nigdy ani nigdzie nie użyjesz. Możemy zatem przejść do meritum.

Pięć rodzajów reguł

Być może jeszcze tego nie zauważyłeś, ale większość logiki konstruktywnej, programowania funkcyjnego, a przede wszystkim teorii typów kręci się wokół pięciu rodzajów reguł. Są to reguły:

• formowania (ang. formation rules)
• wprowadzania (ang. introduction rules)
• eliminacji (ang. elimination rules)
• obliczania (ang. computation rules)
• unikalności (ang. uniqueness principles)

W tym podrozdziale przyjrzymy się wszystkim pięciu typom reguł. Zobaczymy jak wyglądają, skąd się biorą i do czego służą. Podrozdział będzie miał charakter mocno teoretyczny.

Reguły formowania

Reguły formowania mówią nam, jak tworzyć typy (termy sortów Set i Type) oraz zdania (termy sortu Prop). Większość z nich pochodzi z nagłówków definicji induktywnych. Reguła dla typu bool wygląda tak:

Ten mistyczny zapis pochodzi z publikacji dotyczących teorii typów. Nad kreską znajdują się przesłanki reguły, a pod kreską znajduje się konkluzja reguły. Regułę tę możemy odczytać: bool jest typem sortu Set. Postać tej reguły wynika wprost z definicji typu bool.

Powyższej regule formowania odpowiada tutaj fragment Inductive bool : Set, który stwierdza po prostu, że bool jest typem sortu Set. Nie zawsze jednak reguły formowania są aż tak proste. Reguła dla produktu wygląda tak:

Reguła formowania dla prod głosi: jeżeli A jest typem sortu Type oraz B jest typem sortu Type, to prod A B jest typem sortu Type. Jest ona rzecz jasna konsekwencją definicji produktu.

Regule odpowiada fragment Inductive prod (A B : Type) : Type. To, co w regule jest nad kreską (A : Type i B : Type), tutaj występuje przed dwukropkiem, po prostu jako argumentu typu prod. Jak widać, nagłówek typu induktywnego jest po prostu skompresowaną formą reguły formowania. Należy zauważyć, że nie wszystkie reguły formowania pochodzą z definicji induktywnych. Tak wygląda reguła formowania dla funkcji (między typami sortu Type):

Reguła nie pochodzi z definicji induktywnej, gdyż typ funkcji A -> B jest typem wbudowanym i nie jest zdefiniowany indukcyjnie.

Ćwiczenie

Napisz, bez podglądania, jak wyglądają reguły formowania dla option, nat oraz list. Następnie zweryfikuj swoje odpowiedzi za pomocą komendy Print.

Reguły wprowadzania

Reguły wprowadzania mówią nam, w jaki sposób formować termy danego typu. Większość z nich pochodzi od konstruktorów typów induktywnych. Dla typu bool reguły wprowadzania wyglądają tak:

Reguły te stwierdzają po prostu, że true jest termem typu bool oraz że false jest termem typu bool. Wynikają one wprost z definicji typu bool — każda z nich odpowiada jednemu konstruktorowi. Wobec powyższego nie powinna zaskoczyć cię reguła wprowadzania dla produktu:

Jeżeli jednak zaskoczyła cię obecność w regule A : Type i B : Type, przyjrzyj się dokładnie typowi konstruktora pair:

Widać tutaj jak na dłoni, że pair jest funkcją zależną biorącą cztery argumenty i zwracają wynik, którego typ jest produktem jej dwóch pierwszych argumentów. Podobnie jak w przypadku reguł formowania, nie wszystkie reguły wprowadzania pochodzą od konstruktorów typów induktywnych. W przypadku funkcji reguła wygląda mniej więcej tak:

Pojawiło się tu kilka nowych rzeczy: litera Γ oznacza kontekst, zaś zapis Γ |- j, że osąd j zachodzi w kontekście Γ. Zapis Γ; j oznacza rozszerzenie kontekstu Γ poprzez dodanie do niego osądu j. Regułę możemy odczytać tak: jeżeli A -> B jest typem sortu Type w kontekście Γ i y jest termem typu B w kontekście Γ rozszerzonym o osąd x : T, to fun x => y jest termem typu A -> B w kontekście Γ. Powyższa reguła nazywana jest "lambda abstrakcją" (gdyż zazwyczaj jest zapisywana przy użyciu symbolu λ zamiast słowa kluczowego fun, jak w Coqu). Nie przejmuj się, jeżeli jej. Znajomość reguł wprowadzania nie jest nam potrzebna, by skutecznie posługiwać się Coqiem. Należy też dodać, że reguła ta jest nieco uproszczona. Pełniejszy opis teoretyczny induktywnego rachunku konstrukcji można znaleźć w manualu.

Ćwiczenie

Napisz (bez podglądania) jak wyglądają reguły wprowadzania dla option, nat oraz list. Następnie zweryfikuj swoje odpowiedzi za pomocą komendy Print.

Reguły eliminacji

Reguły eliminacji są w pewien sposób dualne do reguł wprowadzania. Tak jak reguły wprowadzania dla typu T służą do konstruowania termów typu T z innych termów, tak reguły eliminacji dla typu T mówią nam, jak z termów typu T skonstruować termy innych typów. Zobaczmy, jak wygląda jedna z reguł eliminacji dla typu bool.

Reguła ta mówi nam, że jeżeli mamy typ A oraz dwie wartości x i y typu A, a także term b typu bool, to możemy skonstruować inną wartość typu A, mianowicie if b then x else y. Reguła ta jest dość prosta. W szczególności nie jest ona zależna, tzn. obie gałęzie ifa muszą być tego samego typu. Przyjrzyjmy się nieco bardziej ogólnej regule.

Reguła ta mówi nam, że jeżeli mamy rodzinę typów P : bool -> Type oraz termy x typu P true i y typu P false, a także term b typu bool, to możemy skonstruować term bool_rect P x y b typu P b. Spójrzmy na tę regułę z nieco innej strony:

Widzimy, że reguły eliminacji dla typu induktywnego T służą do konstruowania funkcji, których dziedziną jest T, a więc mówią nam, jak "wyeliminować" term typu T, aby uzyskać term innego typu. Reguły eliminacji występują w wielu wariantach:

• zależnym i niezależnym — w zależności od tego, czy służą do definiowania funkcji zależnych, czy nie.
• rekurencyjnym i nierekurencyjnym — te druge służą jedynie do przeprowadzania rozumowań przez przypadki oraz definiowania funkcji przez dopasowanie do wzorca, ale bez rekurencji. Niektóre typy nie mają rekurencyjnych reguł eliminacji.
• pierwotne i wtórne — dla typu induktywnego T Coq generuje regułę T_rect, którą będziemy zwać regułą pierwotną. Jej postać wynika wprost z definicji typu T. Reguły dla typów nieinduktywnych (np. funkcji) również będziemy uważać za pierwotne. Jednak nie wszystkie reguły są pierwotne — przekonamy się o tym w przyszłości, tworząc własne reguły indukcyjne.

Zgodnie z zaprezentowaną klasyfikacją, pierwsza z naszych reguł jest:

• niezależna, gdyż obie gałęzie ifa są tego samego typu. Innymi słowy, definiujemy term typu A, który nie jest zależny
• nierekurencyjna, gdyż typ bool nie jest rekurencyjny i wobec tego może posiadać jedynie reguły nierekurencyjne
• wtórna — regułą pierwotną dla bool jest bool_rect

Druga z naszych reguł jest:

• zależna, gdyż definiujemy term typu zależnego P b
• nierekurencyjna z tych samych powodów, co reguła pierwsza
• pierwotna — Coq wygenerował ją dla nas automatycznie

W zależności od kombinacji powyższych cech reguły eliminacji mogą występować pod różnymi nazwami:

• reguły indukcyjne są zależne i rekurencyjne. Służą do definiowania funkcji, których przeciwdziedzina jest sortu Prop, a więc do dowodzenia zdań przez indukcję
• rekursory to rekurencyjne reguły eliminacji, które służą do definiowania funkcji, których przeciwdziedzina jest sortu Set lub Type

Nie przejmuj się natłokiem nazw ani rozróżnień. Powyższą klasyfikację wymyśliłem na poczekaniu i nie ma ona w praktyce żadnego znaczenia. Zauważmy, że podobnie jak nie wszystkie reguły formowania i wprowadzania pochodzą od typów induktywnych, tak i nie wszystkie reguły eliminacji od nich pochodzą. Kontrprzykładem niech będzie reguła eliminacji dla funkcji (niezależnych):

Reguła ta mówi nam, że jeżeli mamy funkcję f typu A -> B oraz argument x typu A, to aplikacja funkcji f do argumentu x jest typu B. Zauważmy też, że mimo iż reguły wprowadzania i eliminacji są w pewien sposób dualne, to istnieją między nimi różnice. Przede wszystkim, poza regułami wbudowanymi, obowiązuje prosta zasada: jeden konstruktor typu induktywnego — jedna reguła wprowadzania. Innymi słowy, reguły wprowadzania dla typów induktywnych pochodzą bezpośrednio od konstruktorów i nie możemy w żaden sposób dodać nowych. Są one w pewien sposób pierwotne i nie mamy nad nimi (bezpośredniej) kontroli. Jeżeli chodzi o reguły eliminacji, to są one, poza niewielką ilością reguł pierwotnych, w pewnym sensie wtórne — możemy budować je z dopasowania do wzorca i rekursji strukturalnej i to właśnie te dwie ostatnie idee są w Coqu ideami pierwotnymi. Jeżeli chodzi o kontrolę, to możemy swobodnie dodawać nowe reguły eliminacji za pomocą twierdzeń lub definiując je bezpośrednio. Działanie takie jest, w przypadku nieco bardziej zaawansowanych twierdzeń niż dotychczas widzieliśmy, bardzo częste. Ba! Częste jest także tworzenie reguł eliminacji dla każdej funkcji z osobna, perfekcyjnie dopasowanych do kształtu jej rekursji. Jest to nawet bardzo wygodne, gdyż Coq potrafi automatycznie wygenerować dla nas takie reguły. Przykładem niestandardowej reguły może być reguła eliminacji dla list działająca "od tyłu":

Póki co wydaje mi się, że udowodnienie słuszności tej reguły będzie dla nas za trudne. W przyszłości na pewno napiszę coś więcej na temat reguł eliminacji, gdyż ze względu na swój "otwarty" charakter są one z punktu widzenia praktyki najważniejsze. Tymczasem na otarcie łez zajmijmy się inną, niestandardową regułą dla list.

Ćwiczenie

Udowodnij, że reguła dla list "co dwa" jest słuszna. Zauważ, że komenda Fixpoint może służyć do podawania definicji rekurencyjnych nie tylko "ręcznie", ale także za pomocą taktyk. Wskazówka: użycie hipotezy indukcyjnej list_ind_2 zbyt wcześnie ma podobne skutki co wywołanie rekurencyjne na argumencie, który nie jest strukturalnie mniejszy.

Ćwiczenie

Napisz funkcję apply, odpowiadającą regule eliminacji dla funkcji (niezależnych). Udowodnij jej specyfikację. Uwaga: notacja "$" na oznaczenie aplikacji funkcji pochodzi z języka Haskell i jest tam bardzo często stosowana, gdyż pozwala zaoszczędzić stawiania zbędnych nawiasów.

Reguły obliczania

Poznawszy reguły wprowadzania i eliminacji możemy zadać sobie pytanie: jakie są między nimi związki? Jedną z odpowiedzi na to pytanie dają reguły obliczania, które określają, w jaki sposób reguły eliminacji działają na obiekty stworzone za pomocą reguł wprowadzania. Zobaczmy o co chodzi na przykładzie.

Powyższa reguła nazywa się "redukcja beta". Mówi ona, jaki efekt ma aplikacja funkcji zrobionej za pomocą lambda abstrakcji do argumentu, przy czym aplikacja jest regułą eliminacji dla funkcji, a lambda abstrakcja — regułą wprowadzania. Możemy odczytać ją tak: jeżeli A i B są typami, zaś e termem typu B, w którym występuje zmienna wolna x typu A, to wyrażenie (fun x : A => e) t redukuje się (symbol ≡) do e, w którym w miejsce zmiennej x podstawiono term t. Zauważ, że zarówno symbol ≡ jak i notacja e{x/t} są tylko nieformalnymi zapisami i nie mają żadnego znaczenia w Coqu. Nie jest tak, że dla każdego typu jest tylko jedna reguła obliczania. Jako, że reguły obliczania pokazują związek między regułami eliminacji i wprowadzania, ich ilość można przybliżyć prostym wzorem: # reguł obliczania = # reguł eliminacji * # reguł wprowadzania, gdzie # to nieformalny symbol oznaczający "ilość". W Coqowej praktyce zazwyczaj oznacza to, że reguł obliczania jest nieskończenie wiele, gdyż możemy wymyślić sobie nieskończenie wiele reguł eliminacji. Przykładem typu, który ma więcej niż jedną regułę obliczania dla danej reguły eliminacji, jest bool:

Typ bool ma dwie reguły wprowadzania pochodzące od dwóch konstruktorów, a zatem ich związki z regułą eliminacji bool_rect będą opisywać dwie reguły obliczania. Pierwsza z nich mówi, że bool_rect P x y true redukuje się do x, a druga, że bool_rect P x y false redukuje się do y. Gdyby zastąpić w nich regułe bool_rect przez nieco prostszą regułę, w której nie występują typy zależne, to można by powyższe reguły zapisać tak:

Wygląda dużo bardziej znajomo, prawda? Na zakończenie wypadałoby napisać, skąd biorą się reguły obliczania. W nieco mniej formalnych pracach teoretycznych na temat teorii typów są one zazwyczaj uznawane za byty podstawowe, z których następnie wywodzi się reguły obliczania takich konstrukcji, jak np. match. W Coqu jest na odwrót. Tak jak reguły eliminacji pochodzą od dopasowania do wzorca i rekursji, tak reguły obliczania pochdzą od opisanych już wcześniej reguł redukcji (beta, delta, jota i zeta), a także konwersji alfa.

Ćwiczenie

Napisz reguły obliczania dla liczb naturalnych oraz list (dla reguł eliminacji nat_ind oraz list_ind).

Reguły unikalności

Kolejną odpowiedzią na pytanie o związki między regułami wprowadzania i eliminacji są reguły unikalności. Są one dualne do reguł obliczania i określają, w jaki sposób reguły wprowadzania działają na obiekty pochodzące od reguł eliminacji. Przyjrzyjmy się przykładowi.

Powyższa reguła unikalności dla funkcji jest nazywana "redukcją eta". Stwierdza ona, że funkcja stworzona za pomocą abstrakcji fun x : A, której ciałem jest aplikacja f x jest definicyjnie równa funkcji f. Regułą wprowadzania dla funkcji jest oczywiście abstrakcja, a regułą eliminacji — aplikacja. Reguły unikalności różnią się jednak dość mocno od reguł obliczania, gdyż zamiast równości definicyjnej ≡ mogą czasem używać standardowej, zdaniowej równości Coqa, czyli =. Nie do końca pasuje też do nich stwierdzenie, że określają działanie reguł wprowadzania na reguły eliminacji, gdyż zamiast reguł eliminacji mogą w nich występować inne byty, zdefiniowane jednak za pomocą reguł eliminacji. Zobaczmy o co chodzi na przykładzie.

Powyższa reguła głosi, że para, której pierwszym elementem jest pierwszy element pary p, a drugim elementem — drugi element pary p, jest w istocie równa parze p. W Coqu możemy ją wyrazić (i udowodnić) tak:

Podsumowując, reguły unikalności występują w dwóch rodzajach:

• dane nam z góry, niemożliwe do wyrażenia bezpośrednio w Coqu i używające równości definicyjnej, jak w przypadku redukcji eta dla funkcji
• możliwe do wyrażenia i udowodnienia w Coqu, używające zwykłej równości, jak dla produktów i w ogólności dla typów induktywnych

Ćwiczenie

Sformułuj reguły unikalności dla funkcji zależnych (forall), sum zależnych (sigT) i unit (zapisz je w notacji z poziomą kreską). Zdecyduj, gdzie w powyższej klasyfikacji mieszczą się te reguły. Jeżeli to możliwe, wyraź je i udowodnij w Coqu.

Metateoria

Zbliżamy się powoli do końca rozdziału. Z jednej strony sporo się nauczyliśmy, ale z drugiej strony fakt ten może budzić dość spory niepkój. No bo niby skąd mamy wiedzieć, że cała ta logika (i teoria typów też) to nie są zupełne bzdury? Pisząc ściślej: skąd np. mamy pewność, że logika konstruktywna nie jest sprzeczna, tzn. nie można w niej udowodnić False? A jakim sposobem ustalić, czy przypadkiem nie zrobiłem cię w konia pisząc, że nie da się udowodnić prawa wyłączonego środka? W niniejszym podrozdziale spróbujemy udzielić krótkiej i zwięzłej (a co za tym idzie, bardzo zgrubnej i średnio precyzyjnej) odpowiedzi na te pytania. Zacznijmy od paru kluczowych uwag.

Preliminaria

Najpierw będziemy chcieli udowodnić, że logika konstruktywna jest niesprzeczna. Co w tym przypadku oznacza słowo "udowodnić"? Aż do teraz dowodziliśmy twierdzeń w Coqu/w logice konstruktywnej, ale teraz będziemy chcieli coś udowodnić o Coqu/o logice konstruktywnej. Ta różnica jest bardzo istotna: jeżeli chcemy udowodnić coś o Coqu, to nie możemy zrobić tego w Coqu. Wynika to z jednego z twierdzeń Gödla, które w uproszczeniu mówi, że jeżeli dany system logiczny potrafi wyrazić arytmetykę liczb naturalnych (no wiesz, dodawanie, mnożenie i takie tam), to system ten nie może udowodnić swojej własnej niesprzeczności. Jeżeli przeraża cię powyższy akapit, to... taś taś ptaszku, będzie dobrze. Parafrazując: żeby udowodnić, że system logiczny nie jest sprzeczny, musimy to zrobić w systemie logicznym, który jest od niego silniejszy. Oczywiście wnikliwy umysł wnet dostrzeże tutaj pewien problem. Gdy już udowodnimy w silniejszym systemie, że słabszy system jest niesprzeczny, to jak mamy się upewnić, czy nasze twierdzenie nie jest przypadkiem gówno warte, np. dlatego, że silniejszy system jest sprzeczny? W tym celu wypadałoby udowodnić również niesprzeczność silniejszego systemu. Zgodnie z powyższym rozumowaniem trzeba w tym celu mieć jeszcze silniejszy system i on również powinien być niesprzeczny, bo inaczej z absolutnej matematycznej pewności nici. Myślę, że widzisz już, dokąd to wszystko zmierza. Tego typu problem w filozofii nazywa się regressus ad infinitum, co po naszemu znaczy po prostu "cofanie się w nieskończoność". Niestety w naszym logicznym kontekście nie ma on żadnego rozwiązania. Trochę terminologii: słabszy system (ten, którego niesprzeczności chcemy dowieść), bywa zazwyczaj nazywany "teorią" lub "językiem", a silniejszy (ten, w którym dowodzimy) to "metateoria" lub "metajęzyk". Dla zmylenia przeciwnika określeniem "metateoria" określa się także zbiór właściwości tego słabszego systemu (a zatem np. niesprzeczność logiki konstruktywnej jest jej właściwością metateoretyczną). Uwaga: nie bój się terminologii i żargonu, one nie gryzą. W praktyce kiedy poważni matematycy (a raczej informatycy i logicy, bo matematycy sensu stricto to straszne miernoty w kwestii logiki) chcą udowodnić niesprzeczność jakiegoś systemu formalnego, to po prostu nie przejmują się niesprzecznością metateorii, w której dowodzą. Zazwyczaj taki dowód i tak nie jest sformalizowany, więc zwykłe błędy w rozumowaniu są większym problemem, niż sprzeczność metateorii. Praktycznym uzasadnieniem na sensowność takiego postępowania może być to, że w ulubionej metateorii dowodzącego od dawna nie znaleziono sprzeczności (np. w teorii zbiorów ZFC, której używa się w takich przypadkach najcześciej, nie znaleziono jej przez 100 lat, więc wydaje się być dość bezpieczna). Teoretycznie, co z tego wychodzi, to względny dowód niesprzeczności, czyli twierdzenie postaci "jeżeli metateoria jest niesprzeczna, to teoria jest niesprzeczna", które w praktyce traktuje się jako absolutny dowód niesprzeczności. Dobra, wystarczy już tego ględzenia. W naszym przypadku po prostu zignorujemy problemy filozoficzne i przyjrzymy się nieformalnemu dowodowi na to, że logika konstruktywna jest niesprzeczna.

Niesprzeczność

Dowód jest banalnie prosty. Załóżmy, że istnieje jakiś dowód fałszu. Przypomnijmy sobie, że Coq jest językiem silnie normalizowalnym. Znaczy to, że wszystkie termy obliczają się do postaci normalnej, czyli termu, który jest ostatecznym wynikiem obliczeń i nie może zostać "jeszcze bardziej obliczony". Ponieważ zdania są typami, to ich certyfikaty również podlegają prawom rządzącym obliczeniami. Jak wyglądają certyfikaty na False? Cóż, teoretycznie mogą być postaci np. f x, gdzie f : P -> False, zaś x : P. Prawdziwe pytanie brzmi jednak: jak wyglądają postacie normalne certyfikatów na False? Przypomnijmy, że dla większości typów (a zatem także dla zdań) termy w postaci normalnej to te, które pojawiają się w regułach wprowadzania i nie inaczej jest dla False, a ponieważ False nie ma reguły wprowadzania, to nie ma żadnego certyfikatu na False, który byłby w postaci normalnej. Ale zaraz! Zgodnie z początkowym założeniem mamy jakiś ceryfikat na False, a zatem na mocy silnej normalizowalności oblicza się on do certyfikatu na False w postaci normalnej, a to oznacza sprzeczność. Wobec tego początkowe założenie było błędne i nie może istnieć żaden certyfikat na False. Słowem: nie da się udowodnić fałszu, a zatem logika konstruktywna jest niesprzeczna.

Niedowodliwość prawa wyłączonego środka

Podobnie przebiega dowód na niedowodliwość prawa wyłączonego środka. Zacznijmy od założenia a contrario, że mamy certyfikat na prawo wyłączonego środka, czyli LEM : forall P : Prop, P \/ ~ P. Ponieważ Coq jest silnie normalizowalny, to nasz certyfikat oblicza się do certyfikatu w postaci normalnej. Jak wygląda postać normalna dla naszego certyfikatu? Postacie normalne certyfikatów na kwantyfikację uniwersalną forall x : P, Q (a zatem także na implikację P -> Q) są postaci fun p : P => q, a certyfikatów na dysjunkcję P \/ Q są postaci or_introl p lub or_intror q. Czy powyższe fakty wystarczą, by określić, jak wygląda postać normalna certyfikatu na prawo wyłączonego środka? Jeszcze nie. Przecież mamy do dyspozycji zdanie P, więc być może da się wycisnąć z niego trochę użytecznych informacji, które pozwolą nam zadecydować, czy pójść w lewo, czy w prawo, czyż nie? Otóż nie - Coqowa teoria typów zabrania wykonywania na typach i zdaniach dopasowań do wzorca i wszelkich innych operacji, które pozwalałyby podejmować decyzje jedynie na podstawie samego typu. Więcej na ten temat dowiemy się pod koniec tego rozdziału, gdy będziemy zajmować się parametrycznością. Teraz możemy już wywnioskować, że nasz certyfikat na prawo wyłączonego środka może mieć jedną z dwóch postaci: fun P : Prop => or_introl p, gdzie p : P to certyfikat na p, lub fun P : Prop => or_intror np, gdzie np : ~ P to certyfikat na ~ P. Rozważmy dwa przypadki. Jeżeli LEM ma pierwszą z tych dwóch postaci, to oznacza to w zasadzie, że wszystkie zdania są prawdziwe! No bo patrz: jeżeli przyjrzymy się LEM False, to widzimy, że przyjmuje on postać or_introl p, gdzie p jest certyfikatem na False, ale wiemy już, że False nie da się udowodnić. Podobnie gdy LEM ma drugą z tych postaci. Wtedy LEM True jest postaci or_intror p, gdzie p to certyfikat na True -> False, a zatem p I to certyfikat na False, ale znów - fałszu nie da się udowodnić! Ponieważ w obu przypadkach uzyskaliśmy sprzeczność, a LEM nie może być żadnej innej postaci, konkluzja jest oczywista: początkowe założenie było błędne i certyfikat na prawo wyłączonego środka nie istnieje.

Konkluzja

Silna normalizowalność jest jedną z kluczowych metateoretycznych właściwości logik i języków programowania. Wynikają z niej nie tylko inne metateoretyczne właściwości tradycyjnie uznawane za ważniejsze, jak niesprzeczność, ale także bardziej ciekawostkowe, jak niedowodliwość prawa wyłączonego środka. Nie przejmuj się, jeżeli nie do końca rozumiesz (albo wcale nie rozumiesz) powyższe wywody (szczególnie preliminaria) lub dowody. Ich rozumienie nie jest niezbędne do skutecznego dowodzenia ani programowania. Ba! Wydaje mi się, że jest całkiem na odwrót: żeby zrozumieć je na intuicyjnym poziomie, potrzeba sporo praktycznego doświadczenia w programowaniu i dowodzeniu. Jeżeli go nabędziesz, powyższe wywody i dowody nagle staną się łatwe, miłe i przyjemne (i puszyste i mięciutkie!). Wróć do nich za jakiś, żeby się o tym przekonać.

Parametryczność