You are currently browsing the category archive for the ‘Coq’ category.

MathTextOntology-pasek

Rozważmy abstrakcyjny graf G. Nieformalnie abstrakcyjny graf matematyczny to obiekt złożony ze zbioru wierzchołków oraz zbioru krawędzi łączących wierzchołki. Wierzchołki połączone wspólną krawędzią nazwiemy sąsiadującymi.

W zastosowaniach zwykle wierzchołki posiadają jakieś konkretne cechy ( i zwykle mają etykietki ), zaś fakt łączenia wierzchołków krawędzią, zwykle ma jakąś interpretację. W ramach rozlicznych interpretacji, możemy mówić o posiadaniu przez wierzchołek określonej własności X. X będziemy tu traktowali jako predykat o dziedzinie w zbiorze wierzchołków, a wartościach w zbiorze {T,F} reprezentującym prawdę i fałsz. Tym samym jeśli wybierzemy pewien wierzchołek v grafu G, to możemy zapytać jaka jest wartość X(v), oraz powiemy że v ma własność X jeśli X(v) = T lub krócej będziemy pisać że X(v).

Przy takiej dosyć prostej terminologii, możemy sformułować w miarę oczywistą zasadę indukcji na grafie.

    Zasada indukcji na grafie.

Dany jest graf nieskierowany G, z jedna składową spójną. Załóżmy że zachodzą następujące własności:

  1. dla każdego wierzchołka v grafu G z tego że X(v) wynika, że X zachodzi dla każdego wierzchołka sąsiadującego z v.
  2. dla pewnego wierzchołka a zachodzi własność X

    Teza: X jest prawdziwe dla wszystkich wierzchołków grafu G.

Dowód ( niewprost):

Załóżmy że spełnione jest założenie (2), to znaczy istnieje wierzchołek a dla którego zachodzi X, oraz spełniona jest zasada (1), że z faktu że X zachodzi dla pewnego wierzchołka wynika ze zachodzi dla wszystkich połączonych z nim wierzchołków.  Mimo to twierdzimy że twierdzenie nie jest prawdziwe, to znaczy że  istnieje pewien wierzchołek d dla którego X nie jest prawdziwe.

Załóżmy że istnieje pewien wierzchołek s sąsiadujący z d dla którego X(s). Wówczas z (1) wynika że d ma cechę X podczas gdy w poprzednik kroku założyliśmy że d nie posiada cechy X. Sprzeczność. Wynika z tego że żaden wierzchołek sąsiadujący z d nie może posiadać cechy X.

Wierzchołki sąsiadujące z nimi także itp, itd.

Oznaczmy przez U zbiór wierzchołków które nie posiadają cechy X. Zbiór U jest niepusty bo zawiera co najmniej wierzchołek d, a także  wierzchołki sąsiadujące z d, wierzchołki sąsiadujące z tymi wierzchołkami itd. Innymi słowy zbiór U to składowa spójna grafu zawierająca d.

Jednak z założenia graf jest grafem spójnym, posiada więc jedna składową spójna.

W takim razie A należy do U.

Ale dla A zachodzi X.
Sprzeczność.
Co prawda zasada wydaje się w miarę oczywista, ale nie znalazłem jej w google ;-)

Po drugie, oczywista to ona pewnie jest dla grafów skończonych, ale z dowodu wydaje się wynikać, ze dla nieskończonych także, co więcej, prosty dowód nie narzuca jakichś ograniczeń na moce zbiorów wierzchołków…

    W poprzednim odcinku:
„Po zatwierdzeniu dostaniemy komunikat: next_weekday (next_weekday saturday) = tuesdayŁał, jak oni to zrobili!?Qed.<- ;-) ładny koniec dowodu.

    W tym odcinku nastąpi obiecany przykład nieco bardzie skomplikowanego dowodu. Obawiam się żę wpis ten będzie najbardziej bałaganiarski ze wszystkich, i najtrudniejszy w odbiorze, a to z powodu sporej ilości komentarzy/kodu. Na spodzie wpisu znajdziecie kod omawiany w tekście bez zbędnych dodatków – można kopiować i wkleić. W zasadzie chyba samo czytanie nie ma sensu – proszę samemu pobawic się Coq.
    Zanim pokażemy coś większego, pobawimy się w kilka definicji i powiemy coś o definiowaniu własnych modułów. Aby definiować własne obiekty, celowe może być odcięcie się od „biblioteki” Coq by nie powodować konfliktów nazw czy definicji. W tym celu użyjemy komendy:

Module PierwszeKotyZaPloty.

    Od tego momentu wszystkie poniższe komendy aż do sekwencji End PierwszeKotyZaPloty. maja ograniczony zasięg leksykalny i nie powodują konfliktów z podobnymi typami zdefiniowanymi w domyślnej bibliotece Coq. Dalsze działania rozpoczniemy od zdefiniowania liczb naturalnych posługując się pomysłem z teorii Peano:

Inductive nat: Set :=
| O:nat
| S:nat->nat.

    Proszę zauważyć, że nie musieliśmy w żaden szczególny sposób określać funkcji S ( a jest to funkcja ma bowiem typ nat->nat). Funkcja ta pełni oczywiście rolę następnika.

    Kolejną definicją będzie funkcja poprzednika:

Definition pred (n:nat): nat :=
match n with
| O => O
|S m => m
end.

    Działa to tak: funkcja pred wymaga jednego argumentu w postaci liczby naturalnej. Jeśli argument ten to „O” wówczas funkcja zwraca „O” jako swoją wartość. Jeśli jednak argument jest różny od „O” to musi on być postaci „S m”, a wówczas opuszczamy „S” i mamy poprzednik liczby „S m” czyli zwracamy „m”. Co by się stało gdybyśmy popełnili błąd i zamiast „S m” twierdzili że możliwe argumenty mają inną postać?

Definition pred (n:nat): nat :=
match n with
| O => O
| S ( S m) => m
end.

    Proszę sprawdzić!
    Sprawdźmy teraz jak zdefiniowane funkcje działają w praktyce. Sprawdźmy jak Coq zrozumiał definicję funkcji S.

Check S (S ( S O)).
    daje w wyniku: S(S(S(O)) : nat

    Jak widać system rozpoznaje że obiekt S (S ( S O)) jest typu nat.

Eval simpl in ( pred ( S (S ( S O)))).

    Widzimy, że funkcja pred rzeczywiście wylicza n-1…

End PierwszeKotyZaPloty.

    W tym miejscu możemy zamknąć nasz moduł, który utworzyliśmy w celach dydaktycznych i zaczytać do środowiska bibliotekę Arith w której, w identyczny jak powyżej sposób, zdefiniowane sa liczby naturalne. Wykonujemy to komendą:

Require Import Arith.

    Sprawdźmy co da nam komenda analogiczna do wykonanej wcześniej:

Check S (S ( S O)).

    wynik to: 3:nat .

    Twórcy Coq wprowadzili „ułatwienie” w operowaniu liczbami w postaci ich standardowej graficznej reprezentacji. Jednak posługując sie biblioteką Arith w istocie operujemy na typach zdefiniowanych za pomocą wcześniejszych definicji. Aby się o tym przekonać poprośmy Coq o wypisanie definicji funkcji S (Coq wypisze co o niej wie):

Print S.
    Wynik to: Inductive nat: Set :=O: nat | S: nat->nat For S: Argument scope is [nat scope].

Print PierwszeKotyZaPloty.S.
    Wynik to: Inductive PierwszeKotyZaPloty.nat: Set :=O: PierwszeKotyZaPloty.nat | S: PierwszeKotyZaPloty.nat->PierwszeKotyZaPloty.nat

    Jak widać elementy zbioru który zdefiniowaliśmy sa innego typu niż elementy ze standardowej biblioteki co pozwala operować na nich jednocześnie bez popadania w konflikt. Jeszcze raz podkreślę, że powyższe definicje, poza „przestrzenią leksykalną” niczym się nie różnią, zaś w plikach definiujących bibliotekę Arith można znaleźć definicję zbioru nat wyglądająca dokładnie jak nasza definicja w module PierwszeKotyZaPloty.

    Skoro mamy zdefiniowane liczby naturalne, możemy budować na ich funkcje. Spróbujmy zatem zdefiniować sumę pierwszych n liczb naturalnych. Definicja będzie rekurencyjna:

Fixpoint sum_n(n:nat):nat :=
match n with
|O=> O
|S m => S m + sum_n m
end.

    Sprawdźmy czy to działa.

Eval simpl in sum_n 5.
    Wynik to: 15:nat. Wygląda dobrze.

    W dalszej kolejności będziemy dowodzić Twierdzenia w postaci: Theorem Gauss_suma: forall n:nat, 2*sum_n n = n* (n+1). czyli wzoru na sumę n początkowych liczb naturalnych, której wyliczenie przypisuje się młodemu Gaussowi podczas zajęć szkolnych. Zanim jednak tego dokonamy zdefiniujemy kilka lematów. Tak naprawdę lematy powstały podczas nieudanych prób dowodu podczas interakcji z systemem. Usiłowałem wymyślać dowód operując różnymi taktykami i definiowałem własności których mi brakło dla zakończenia dowodu. Oczywiście w wersji finalnej wstawimy Lematy tak, że znajdą się elegancko przed samym twierdzeniem i jego dowodem co skutecznie ukryje ich pochodzenie ;-). W komentowanym kodzie zdecydowałem się jednak jeden z nich zostawić w środku dowodu aby pokazać że może on tam się znajdować.
    Dodatkowa uwaga zanim zaczniemy jest taka: aby zrozumieć co się dzieje należy odpalić CoqIde lub ProofWeb. Treść skryptu poniżej nie zawiera bardzo ważnej informacji – wyniku operacji jakie podaje Coq – czyli stanu systemu. Bez tej informacji zrozumienie tego o co chodzi może być bardzo trudne.
    Zacznijmy od prostego lematu dotyczącego własności następnika:

Lemma nastepnik: forall n:nat, S n = n+1.

    Przykład ten jest interesujący bowiem posłużymy się w celu dowodu taktyką induction względem liczby n.

Lemma nastepnik: forall n:nat, S n = n+1.
Proof.
induction n.

    Tutaj komentarz: w wyniku użycia taktyki induction n dostajemy rozbicie tezy na dwa cele do dowiedzenia. Oto wynik jaki wypisuje Coq:

2 subgoals
============================
1 = 0 + 1

subgoal 2 is:
S (S n) = S n + 1

    Wszystko to jest możliwe dzięki indukcyjnej definicji zbioru obiektów nat. Wiadomo jakie są możliwe przypadki ( z definicji typu nat wiemy że albo O albo S n). W istocie w sensie praktycznym taktyka induction dokonuje analizy możliwych przypadków w oparciu o definicję obiektów którymi operujemy ( i przypomina tym samym taktykę destruct, która wcale indukcją nie jest!). Jednak oczywiście sama zasada indukcji nie jest tak prosta. Aby sprawdzić jak wygląda zasada indukcji zapisana w Coq do liczb naturalnych sprawdźmy jak jest zdefiniowany schemat ind_nat. Możemy to zrobić nie przerywając dowodu ( po prostu sprawdzamy definicje przez co nie ingerujemy w treść dowodu twierdzenia):

Check nat_ind.

    Otrzymamy jako wynik:

nat_ind : forall P : nat -> Prop, P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n

    Jak widać jest to schemat indukcji zapisany dla liczb naturalnych zdefiniowanych za pomocą elementu „O” i operacji następnika „S” co nie powinno dziwić. Warto nadmienić, że taktyka induction to mniej więcej to samo, w odróżnieniu jednak od nat_ind nie ma ona zapewne tak prostej definicji. Opieram się tu na przypuszczeniach które należałoby sprawdzić czytając kod Coq i na komentarzach z manuala Coq. Wydaje się że można rzecz wyjaśnić tak: taktyka induction jest taktyką ogólna, działająca dla dowolnych typów, zbiorów i definicji predykatów ( na przykład także dla typu bool, gdzie mamy tylko 2 możliwe przypadki). W pewnym sensie w porównaniu z nat_ind jest to raczej metataktyka która bierze pod uwagę definicje obiektów na których działa – i która w wypadku liczb naturalnych jak wyżej redukuje sie do nat_ind. Ważną wiadomością tutaj jest, ze definiując własne typy danych ( powiedzmy drzewa, listy, bagi – czyli zbiory zbiorów itp. struktury rekurencyjne) możemy dla nich zdefiniować własne taktyki indukcji – i w ten sposób rozszerzyć możliwości Coq. Są to jednak rozważania przekraczające moją wiedzę. Aby nie być całkowicie gołosłownym poniżej pokażę jednak przykład własnoręcznie zdefiniowanej prostej taktyki – do własnej indukcji stąd daleko ale …

    Wracając do naszego dowodu zapiszmy jeszcze raz całość bez zbędnych komentarzy:

Lemma nastepnik: forall n:nat, S n = n+1.
Proof.
induction n.
trivial.
(*simpl;reflexivity.*)
simpl.
rewrite IHn.
reflexivity.
Qed.

    Po taktyce induction n nastąpiła taktyka trivial która w tym przypadku oznacza to samo co wykomentowany ciąg simpl;reflexivity. Taktyka trivial dowodzi tych twierdzeń które sprowadzają się do wyliczenia wartości i sprawdzenia równości. W tym kroku dowiedliśmy prawdziwości twierdzenia dla wartości początkowej „O”. Następnie przeszliśmy do kolejnego zadania – wykonania kroku indukcyjnego od n do n+1. Po uproszczeniu simpl otrzymujemy do dowiedzenia równanie postaci S (S n) = S (n + 1) przy założeniu że IHn : S n = n + 1. IHn oznacza tu hipotezę indukcyjną po n. Jeśli w konkluzji skorzystać z tej hipotezy – dostaniemy to co nas interesuje – dokonujemy tego przez użycie taktyki rewrite IHn. – przepisujemy tezę używając przesłanki. I mamy koniec dowodu.

    Zdefiniujmy następny lemat dotyczący rozdzielności mnożenia względem dodawania:

Lemma mult_distributive: forall n m l:nat, n*(m+l)= n*m +n*l.
Proof. intros. ring. Qed.

    Tym razem (leniwie) użyliśmy taktyki ring odwołującej się do własności pierścienia liczb naturalnych – taktyka ta może być użyta z dowolnymi obiektami o strukturze pierścienia.

    Teraz gotowi do dowiedzenia naszego twierdzenia. Poniższy dowód nie jest ani ładny, ani najprostszy, ani szczególnie pomysłowy – jest barokowy. Moim celem było użycie tak wielu elementów języka jak tylko się uda, przy czym zawsze przedkładałem jawne wyliczanie tego i owego nad użycie samograjów w rodzaju ring – które jeśli je tu zastosować w odpowiednim miejscu – proszę spróbować – przyspiesza dowód. Poniżej komentarze do linii oznaczonych numerami:

Theorem Gauss_suma: forall n:nat, 2*sum_n n = n* (n+1).
Proof.
induction n.
simpl;trivial.
Ltac UFx x:= unfold x;fold x. (* 0*)
UFx sum_n. (*1*)
(*unfold sum_n. *)
(*fold sum_n.*)

Lemma mult_distributive’: forall n m l:nat, (m+l)*n= m*n +l*n. (* 2 *)
Proof. (*początek dowodu lematu*)
intros.
ring.
Qed. (*koniec dowodu lematu*)

rewrite mult_distributive.
rewrite IHn.
rewrite <-nastepnik. (*3*)
rewrite <-mult_distributive’.
(*rewrite nastepnik.*)
SearchRewrite( _ * _ ). (* 4*)
rewrite plus_comm.(*5*)
rewrite mult_comm.(*6*)
rewrite nastepnik.
(*ring*) (*7*)
rewrite mult_plus_distr_r.(*8*)
rewrite mult_plus_distr_l.(*9*)
simpl.
ring.
Qed.

    Teraz komentarze dotyczące dowodu.
(*0*) (*1*) – chyba najciekawsza część dywagacji – definicja własnej taktyki poleceniem Ltac. Taktyka UFx pobiera argument x i wykonuje kolejno unfold x po czym fold x. Jak widać Coq dysponuje „podjęzykiem” definicji taktyk, podany przykład jest w pewnym sensie banalny bo sprowadza się do bezpośredniego wykonania dwu innych taktyk jedna po drugiej, przykłady które można znaleźć w rozmaitych materiałach o Coq służą do automatyzacji dowodów i w istocie są dosyć skomplikowanymi „podprogramami” analizującymi możliwe przypadki i wyniki zastosowanych taktyk, dopasowujące wzorce itp. Polecam materiały pana Adama Chlipala wymienione poniżej jeśli kogoś to interesuje.
(*2*) – w trakcie dowodu wprowadzamy lemat. Coq nie zakłada a priori przemienności działań więc dowodzimy sobie potrzebnej tożsamości.
(*3*) – dokonujemy przepisania tezy za pomocą lematu następnik dowiedzionego wcześniej., Tym razem jednak przepisujemy równość tam występująca od prawej do lewej co sygnalizuje znak <- ( można także użyć -> i przepisać od lewej do prawej co jest zresztą domyślnym trybem stosowania równości).
(*4*) (5*) (*6*) – tak naprawdę to dowodzenie lematu dla zamienionej kolejności wyrażeń w możeniu nie było konieczne. W bibliotece Coq znajdują się stosowne twierdzenia dotyczące przemienności dodawania i mnożenia. SearchRewrite( wzorzec ) pozwala na znalezienie wszystkich zdefiniowanych twierdzeń które odpowiadają wzorcowi _ * _ gdzie podkreślenie oznacza dowolne wyrażenie. Znalezione w ten sposób lematy/twierdzenia wykorzystujemy w dowodzie.
(*7*) (*8*) (*9*) – poprzedni krok przekształcił całe rozumowanie w działanie z zakresu algebry które można rozwiązać po prostu wyliczając wartości po obydwu stronach równości za pomocą taktyki ring. Ja jednak proponuję użyć – głównie po to by podać ich nazwy – lematów dotyczących rozdzielności mnożenia względem dodawania lewostronnie i prawostronnie.

    Na zakończenie podam kilka poleceń które wypisują definicje obiektów z których korzystaliśmy:

Print nat.
Print mult_distributive.
Print Gauss_suma.

    Pierwsza definicja pokazuje sposób a jaki skonstruowaliśmy zbiór nat. Druga pokazuje konstrukcję lematu mult_dystributive, trzecia twierdzenia Gauss_suma. Dwa ostatnie obiekty to nazwy twierdzeń/lematów. W wypadku twierdzenia Gauss_suma zwracany przez Coq wynik, to dosyć koszmarna i bardzo nieczytelna funkcja która jako argument pobiera liczbę naturalną ( Gauss_suma = fun n:nat=> … ) a zwraca dowód twierdzenia które wypisaliśmy powyżej. Nie posiadam szczególnie głębokiej wiedzy na ten temat, jednak z jednej strony podana funkcja realizuje jawnie zależność opisaną tutaj, jako interpretację BHK dla dowodu twierdzenia z kwantyfikatorem ogólnym, a zarazem jest praktyczną realizacją izomorfizmu Curryego-Howarda jak opisano tu. Jeśli znajdę czas na pisanie kolejnego 4-tego odcinka tego cyklu – bedzie on poświęcony właśnie tym zagadnieniom.

    Dla zainteresowanych którzy zdadzą pytanie: czy to wszystko ma jakieś znaczenie praktyczne, dodaję na koniec przykład którego nie rozumiem, i nie umiem skomentować bo moja motywacja jest raczej matematyczna i teoretyczna. Tu jednak coś dla praktyków. Coq potrafi generować kod źródłowy programów w Ocamlu, Haskell lub Scheme. Oto przykład który znalazłem gdzieś na grupach dyskusyjnych ( nie jest kompletny, nie udało mi się go wykonać w całości z powodu niezgodności bibliotek, wyraźnie jednak widać że „coś” zwraca ;-)

Fixpoint fact_body (a n : nat) : nat :=
match n with
| 0 => a
| S m => fact_body (a*n) m
end.

Definition fact : nat -> nat := fact_body 1.
Extraction Language Scheme. (*lub Ocaml, lub Haskell*)
Extract Inlined Constant plus => „(+)”.
Extract Inlined Constant mult => „(*)”.
Extraction fact_body.
Extraction fact.

    Zgodnie z opisami jakie znalazłem tu i tam, taka generacja kodu ma służyć wytwarzaniu certyfikowanych programów komputerowych w realnych językach programowania.
——————————-

    Podczas przygotowywania tych wpisów korzystałem z wielu źródeł które wymienię tu w przypadkowej kolejności. Wszystkie kody uruchamiałem za pomocą CoqIde, niektóre sprawdzałem w ProofWeb.

  • Podstawowym źródłem informacji jest oczywiście strona domowa projektu Coq: http://coq.inria.fr na która powoływałem się na początku. W sekcjach zawierających dokumentację można znaleźć zarówno formalną specyfikację języka Gallina jak i manual do samego narzędzia. W szczególności znajduje tam indeks taktyk.
  • Podstawowe źródło wiedzy o Coq jakie użyłem podczas tej prezentacji to: „Software Foundations” Benjamin C. Pierce, Chris Casinghino, Michael Greenberg, Vilhelm Sjöberg, Brent Yorgey, with Andrew W. Appel, Arthur Chargueraud, Anthony Cowley, Jeffrey Foster, Michael Hicks, Ranjit Jhala, Greg Morrisett, Chung-chieh Shan, Leonid Spesivtsev, and Andrew Tolmach. http://www.cis.upenn.edu/~bcpierce/sf/ Polecam wszystkim zainteresowanym zwłaszcza zagadnieniami dowodzenia poprawności programów. Jest to kompletne źródło z którego można się nauczyć używać Coq, podobno także w praktyce programistycznej.
  • Kilka przykładów zaczerpnąłem ze strony kursu „Interactive Computer Theorem Proving „ Adam Chlipala http://adam.chlipala.net/itp/ Kolejne samodzielne źródło informacji na temat systemu Coq. Bardzo dobre.

    Różne pomysły i koncepcje, słowem trivia lub przypadki szczególne ( ale kształcące):

——————————-

    I to już wszystko moi drodzy. W zasadzie wyczerpałem swoją wiedzę ;-) w omawianym temacie. W planach miał być jeszcze jakiś bardziej skomplikowany dowód ale pisanie kodu w Buzz jest niezbyt przyjemne. Najbardziej skomplikowaną rzeczą z jaką w Coq spotkałem próbując ją zrozumieć choć trochę były prace Vladimira Voyevodskyego na temat Univalent Fundations of Mathematics ( tu mozna oglądnąć video z wykładu Vladimira – bardzo ładne ale trudne ). Musze przyznać że zgadzam się z jego opinią – używanie proof czeckerów w matematyce jest nieuniknione. Zaufanie jakie możemy pokładać w systemach takich jak Coq jest wcale nie mniejsze niż to kŧóre pokładamy w grupie recenzentów z czasopism. Voyevodsky w którymś ze swoich wykładów wspomniał że ma prace która leży nieopublikowana od 2 lat – recenzenci sprawdzają… Z drugiej strony on sam jako recenzent – tez niektóre artykuły sprawdza już całkiem długo. Kolejnym zagadnieniem jest zabawa amatora. Każda osoba która zada sobie trud zrozumienia podstaw Coq i zechce sformalizować swoje pomysły uzyskuje dostęp do „niezmordowanego krytyka” który potrafi sprawdzić poprawność twierdzeń dowodów a nawet pomóc w znalezieniu dowodu. Oczywiście tym co zniechęca jest ilość pracy jakiej to wymaga. Z jednej strony język Coq jest bardzo ekspresywny i można w nim wyrazić bardzo wiele stosunkowo niewielkim nakładem pracy. Z drugiej strony będąc świadomym jak wygląda nawet prosty ale nietrywialny dowód typowego twierdzenia ( np. usiłując sobie wyobrazić jak mogłaby przebiegać formalizacja dowodu który przedstawił tutaj +Artur Popławski) widać, że to jest praca na wiele wiele wieczorów… Na zakończenie odrobina statystyki: w pracy http://r6.ca/Goedel/goedel1.html o tytule „Essential Incompleteness of Arithmetic Verified by Coq” dokonano formalizacji dowodu znanego tw. Goedla. Na końcu autor zawarł sekcję o podtytule „statistics” która pozwolę sobie tu zacytować:

    „My proof, excluding standard libraries and the library for Pocklington’s criterion, consists of 46 source files, 7 036 lines of specifications, 37 906 lines of proof, and 1 267 747 total characters. The size of the gzipped tarball (gzip -9) of all the source files is 146 008 bytes, which is an estimate of the information content of my proof. „

    Życzę powodzenia – a jeśli komuś się spodobało – i będzie używał – proszę o dzielenie się wynikami.

———–Cały Kod————–
Require Import Arith.
Check S (S ( S O)).
Print S.

Check pred ( S (S ( S O))).
Eval simpl in S(S(S(S O))).

Fixpoint sum_n(n:nat):nat :=
match n with
|O=> O
|S m => S m + sum_n m
end.

Eval simpl in sum_n 5.

Lemma nastepnik: forall n:nat, S n = n+1.
Proof.
induction n.
(*simpl;reflexivity.*)
trivial.
simpl.
rewrite IHn.
reflexivity.
Qed.

Lemma mult_distributive: forall n m l:nat, n*(m+l)= n*m +n*l.
Proof.
intros.
ring.
Qed.
Lemma mult_distributive’: forall n m l:nat, (m+l)*n= m*n +l*n.
Proof.
intros.
ring.
Qed.

Lemma nastepnik’: forall n:nat, S n = 1+n.
intros.
induction n. trivial. simpl. rewrite IHn. trivial. Qed.

Ltac UFx x:= unfold x;fold x.

Theorem Gauss_suma: forall n:nat, 2*sum_n n = n* (n+1).
Proof.
induction n.
simpl;trivial.
(*Ltac UFx x:= unfold x;fold x.*)
UFx sum_n.
(*unfold sum_n.*)
(*fold sum_n.*)
rewrite mult_distributive.
rewrite IHn.
rewrite <-nastepnik.
rewrite <-mult_distributive’.
(*rewrite nastepnik.*)
SearchRewrite(_*_).
rewrite plus_comm.
rewrite mult_comm.
rewrite nastepnik.
(*ring.*)
(*SearchRewrite(_*_).*)
rewrite mult_plus_distr_r.
rewrite mult_plus_distr_l.
simpl.
symmetry.
rewrite mult_plus_distr_r.
rewrite mult_plus_distr_l.
simpl.
ring.
Qed.
Check nat_ind.

Print nat.
Print mult_distributive.
Print Gauss_suma.

Fixpoint fact_body (a n : nat) : nat :=
match n with
| 0 => a
| S m => fact_body (a*n) m
end.
Definition fact : nat -> nat := fact_body 1.
Extraction Language Haskell.
Extract Inlined Constant plus => „(+)”.
Extract Inlined Constant mult => „(*)”.
Extraction fact_body.
Extraction fact.
———–Koniec Cały Kod————–

      Poprzednie rozważania naprowadziły nas na trop dowodzenia twierdzeń za pomocą sprytnie pomyślanych regułek przekształcających jedne napisy w inne, wychodząc od rzeczy uznanych za oczywiste, aż osiągnie się to co chcemy dowieść, lub sprytniej wychodząc od zaprzeczenia tego co chcemy dowieść, tymi samymi regułkami do sprzeczności we wszystkich możliwych przypadkach. Zapewne wielu ludzi wpadło na pomysł że skoro metody te sa algorytmiczne, to można je używać nie tylko na papierze, ale i za pomocą maszyny. Jak widzieliśmy juz w latach 50-tych posiadano dostateczne narzędzia i motywację by budować theorem proovers i dowodzić nimi realne twierdzenia ( np te z ‚Principia Mathematica” Russella i Whiteheada).

    W dalszej części wpisu chciałbym się skupić na Coq. Nie oznacza to bynajmniej że uważam go za najciekawszy czy najlepszy proover. Słynny i nadal chyba najdoskonalszy Mizar – dzieło Andrzej Trybulca ( posiada największą bibliotekę gotowych sformalizowanych teorii na świecie), prosty i ciekawy Mace4/Prover9 bardzo efektywnie wynajdujący kontrprzykłady dla podanych twierdzeń, Isabele, HOL, i wiele innych są przykładami bardzo ciekawych narzędzi. Coq wyróżnia się jednak „niewielkimi kosztami wejścia” i wydaje mi się, że stromą krzywą uczenia. W odróżnieniu np. od Mizara który potrafi sprawdzić dowód zapisany w syntetycznym, lecz bliskim naturalnemu, języku, czym przypomina prace z gołym kompilatorem, Coq oferuje pewną dozę interaktywności. Kiedy mamy do dowiedzenia twierdzenie, to po stosownej formalizacji – czyli po zdefiniowaniu stosownych pojęć i zapisaniu twierdzenia w odpowiednim języku Coq oferuje wybór taktyk dowodowych, przekształceń i reguł inferencji pozwalających na dowodzenie do pewnego stopnia wręcz na chybił-trafił. Oczywiście taka bezmyślna taktyka nadaje się do dowodzenia tylko bardzo prostych twierdzeń, z drugiej strony skoro czasami nie wiadomo od czego zacząć….

    Coq składa się z środowiska obliczeniowego Coq który jest narzędziem pracującym w linii komend i przypomina interaktywne środowiska programistyczne znane np. z pythona czy języków funkcyjnych, lub z tekstowych sesji matlaba. W tym trybie pracy możliwe jest zaczytanie wcześniej przygotowanego zestawu skryptów, ich „kompilacja” i uzyskanie odpowiedzi czy skrypty sa poprawne.
Praca w trybie tekstowym z pewnością jest bardzo użyteczną umiejętnością, zwłaszcza dla osób profesjonalnie użytkujących Coq, pozwala bowiem pracować z naprawdę sporymi teoriami o wielkiej liczbie twierdzeń itp. zapisanych w setkach plików. Dla osoby początkującej z pewnością znacznie ciekawszym sa środowiska interaktywne z interfejsem graficznym, wyposażone w menu z podpowiedziami i tym podobne ułatwienia. Środowiska takie nadają się także do prowadzenia dydaktyki – sądząc po sporej ilości kursów opartych na Coq jest to bynajmniej nie banalna część jego zastosowań.
     Wspomnę tu o trzech takich narzędziach – nadmieniając jedynie, że język programowania Coq nazywa się Gallina:

  • ProofWeb  którego autorem jest Cezary Kaliszyk i zespół programistów – działa świetnie i umożliwia zapoznanie się z systemem Coq bez potrzeby instalacji czegokolwiek – całość działa w przeglądarce – proszę sprawdzić! W szczególności polecam – jeśli ktoś chce sprawdzić przykłady które tu zostaną podane do posłużenia się tym środowiskiem. Warto wspomnieć że strona zawiera także kurs logiki oraz przygotowane skrypty z ćwiczeniami – warto spróbować! Uwaga – ProofWeb posiada własną bibliotekę regułek inferencji i taktyk dowodowych – ja zaś posługiwać się będę czystym Coq bez żadnych dodatków. Pomimo że poniżej używam kilku przykładów zaczerpniętych z materiałów ProofWeb, ich dowody sa poprowadzone inaczej – aby byly kompatybilne z „gołym Coq”. Te same przykłady mają swoje dowody w ProofWeb ( proszę poszukać;-) – jednak ich przeprowadzenie w Coq wymaga zaczytania biblioteki ProofWeb z której ja staram się tu nie korzystać.
  • ProofGeneral – to środowisko przygotowane do pracy z Emacsem. Osobiście używałem raz – nie lubię Emacsa. Jednak dla osób lubiących ten system operacyjny – środowisko to może okazać się bardzo produktywne, zwłaszcza, że nie jest ono ograniczone do wspierania jedynie Coq, i pozwala używać kilka rozmaitych systemów stosowanych w informatyce teoretycznej i matematyce jak Isabele, HOL, ACL2 itp.

    Coq wraz z CoqIde można ściągnąć za darmo ze strony http://coq.inria.fr/download . Coq jest systemem opensource, dystrybuowanym na podstawie licencji GNU Lesser General Public Licence Version 2.1 (LGPL). Coq został napisany głównie w Objective Caml. Prace nad jego stworzeniem rozpoczęto w roku 1984, autorami są Thierry Coquand and Gérard Huet którzy zaczęli prace, oraz Christine Paulin. Oczywiście lista autorów jest znacznie dłuższa. Coq powstał w instytucie INRIA we Francji.
     Instalacja pod Linuxem jest prosta i sprowadza się do użycia standardowych narzędzi dostępnych w dystrybucji, np. w wypadku Ubuntu wystarczy użyć: apt-get install coqide, dla Fedory: yum install coqide, i zgodzić się na pociągnięcie zależności. W wypadku Windows musimy ściągnąć stosowny instalator ze strony podanej powyżej i zainstalować program własnoręcznie. Dostępne są także wersję dla Mac OS oraz źródła programu.

    Pominiemy kwestię użycia interfejsu tekstowego, i przejdziemy do użycia CoqIde. Po uruchomieniu środowiska dostajemy okienko z trzema sekcjami:

1. okno w którym wprowadzamy komendy
2. okienko z komunikatami błędów i ostrzeżeniami
3. okienko w którym oglądamy wyniki naszych prac ( niejako standardowe wyjście programu).

    Jak na poniższym obrazku:

    Aby przejść od słów do czynów, wpiszmy pierwsze komendy w okienko komend (1). Proponuję aby poniższe sekwencje wpisać np. w ProfWeb który swoim wyglądem imituje CoqIde:

Na początek prosty przykład definicji typu wyliczeniowego ( czyli zbioru skończonego):

Inductive day : Type :=
| monday : day
| tuesday : day
| wednesday : day
| thursday : day
| friday : day
| saturday : day
| sunday : day.
     Po wpisaniu powyższego w pole (1) należy zatwierdzić to co się wprowadziło naciskając strzałkę w dół ( co spowoduje analizę wpisu i przejście do następnej komendy). Można także użyć wygodnej sekwencji ctrl-alt-down ( klawisz strzałki) – co niestety u mnie pod Ubuntu nie działa…
     Po zatwierdzeniu system zwraca nam komunikat który możemy odczytać w oknie (2) :

day is defined
dayrect is defined
dayind is defined
dayrec is defined

    Następnie definiujemy prostą funkcję pobierająca jako argument zmienną o type „day” i zwracającą wynik o tym samym typie:

Definition nextweekday (d:day) : day :=
match d with
| monday => tuesday
| tuesday => wednesday
| wednesday => thursday
| thursday => friday
| friday => monday
| saturday => monday
| sunday => monday
end.

     Po zatwierdzeniu system upewnia nas że „next_weekday is defined”
     Spróbujmy wyliczyć nasza funkcję dla kilku argumentów:

Eval simpl in (nextweekday friday).
Eval simpl in (nextweekday (nextweekday saturday)).

Co wyszło? Możemy teraz zapisać pierwsze twierdzenie dotyczące zdefiniowanej funkcji:

Example testnextweekday:
(nextweekday (nextweekday saturday)) = tuesday.

    Po zatwierdzeniu dostaniemy komunikat:

1 subgoal

============================
nextweekday (nextweekday saturday) = tuesday

    jak widać system nie przyjął równości na wiarę i oczekuje od nas uzupełnienia podanej zależności dowodem. Mamy konkluzję do dowiedzenia, i jest ono napisane pod kreską, nad kreska znajdują się zas dane przesłanki – w tym wypadku ich zbiór jest pusty. Jeśli teraz będziemy chcieli bawić się w dalsze definiowanie bez dostarczenia dowodu, system zaprotestuje pouczając nas że znajdujemy się w proof mode. Działania systemu zostały niejako wstrzymane do momentu w którym dowiedziemy naszej tezy. No to dowodzimy:

Proof. <- rozpoczynamy dowód. Nie trzeba tego robić, ale jak ładnie wygląda!
unfold nextweekday._ <- rozpiszmy definicję naszej funkcji. jak widać jawne wyliczenie prowadzi do oczywistej równości…
reflexivity. <- …którą uważamy za prawdziwą na mocy prawa zwrotności relacji równości
Qed. <- ;-) ładny koniec dowodu.

    Kilka słów komentarza. W powyższym „dowodzie” użyliśmy dwu tak zwanych taktyk dowodowych. Pierwsza nosi nazwę unfold, jej składnia to unfold nazwaobiektu_ i polega na wpisaniu w miejsce nazwy obiektu jego definicji. W naszym przypadku takie postępowanie pozwoliło od razu na wyliczenie wartości funkcji nextweekday z definicji. Wynikiem zastosowania tej taktyki była równość ( proszę sprawdzić!) w postaci tuesday = tuesday Wynik ten jest kolejnym twierdzeniem które musimy dowieść! Kolejnym krokiem było zastosowanie taktyki reflexivity czyli powołanie się na własność relacji równości. Ten sam dowód mógłby byc zapisany w nieco mniej wyrafinowany sposób: Proof. simpl. reflexivity. Qed. ( w jednej linii). Tym razem stosujemy taktykę simpl która sprowadza się do uproszenia wyrażeń przez wyliczanie tego co da się wyliczyć wprost.

    Taktyki o których tu mowa, to przykłady reguł inferencji, o jakich była mowa poprzednio, o mniej lub bardziej wymyślnych formach. Taktyki proste, jak te które sprowadzają się do rozpisania definicji funkcji są dosyć oczywiste, należy jednak wiedzieć, że Coq dostarcza taktyk w liczbie około 200 przy czym są wśród nich tak „proste” jak unfold czy simpl , skomplikowane jak induction realizująca indukcję matematyczną (postaram się o przykład w następnym wpisie), praktyczne jak taauto która umie dowieść skomplikowane tautologie logiczne, czy pochodna do niej intuition , są taktyki operujące po stronie przesłanek jak i taktyki operujące na konkluzjach. Można za ich pomocą eliminować implikacje, kwantyfikatory, dodawać dodatkowe założenia i budować lematy. Użytkownik może także samodzielnie budować własne taktyki, nazwać je i stosować kiedy mu to potrzebne. Spis gotowych taktyk wraz z opisem można znaleźć tu: http://coq.inria.fr/doc/tactic-index.html

    Podam teraz przykłady z klasycznego rachunku zdań:
Variables A B C D : Prop.

Theorem example01 : A /\ B -> B /\ A._
Proof. <- mamy dowieść implikacji A /\ B -> B /\ A.
intros. <- rozbijamy implikację na hipotezę H: A /\ B i konkluzję B /\ A.
destruct H. <- destruct to taktyka która sprawdza możliwe przypadki, w naszym przypadku hipoteza H zostaje rozbita na przesłanki H:A i H0:B. Obie przesłanki muszą być spełnione.
split. <-tym razem rozbijamy konkluzję na możliwe przypadki – w naszym wypadku mamy dowieść konkluzję 1. A i 2. B
assumption. <- konkluzja 1. wynika z założenia H.
assumption. <- konkluzja 2. wynika z założenia H0.
Qed. <- dowiedliśmy tezy.

(* komentarz w kodzie Coq tworzymy tak jak tu)
(Kontynuujmy wprowadzanie dalszych taktyk*)

Theorem example04 : A \/ B -> B \/ A._
Proof.
intros.
destruct H.
right.
assumption.
left.
assumption.
Qed.

    Po standardowym początku w którym pozbyliśmy sie implikacji, dokonaliśmy rozbicia na przypadki zostawiając tylko jeden ( z powodu obecności alternatywy). Tym razem pojawiły sie taktyki dotyczące alternatywy left i right które zostawiają z alternatywy odpowiednio lewy i prawy czynnik konkluzji. W każdym przypadku prawdziwość wynika z spostrzeżenia że konkluzja pojawia się w przesłankach.

    W następnym odcinku będą trochę bardziej złożone konstrukcje, a potem, na koniec postaram się uzupełnić wpisy o uwagi na temat Dependent Type Theory i Izomorfizmu Curryego-Howarda.

   

    Systemy dedukcji

    Chciałbym napisać coś o Coq. temat jest jak rzeka, ale nie brak tez materiałów w necie a nawet książek wśród których, co ciekawa, a dla mnie przyznam zaskakujące, pojawiają się polskie nazwiska. Pomyślałem jednak że warto na początku podzielić się trochę historyczną wiedzą, zwłaszcza, że jak jej nie zapiszę to i tak mi z głowy zniknie;-) W zasadzie celem poniższego jest skierowanie czytelnika do przeglądnięcia metody tabel analitycznych oraz pokazania jakiegokolwiek systemu dedukcji naturalnej. Wszystko to w celu zwrócenia uwagi, że systemy automatycznego dowodzenia twierdzeń nie sa cudem ale przemyślnie skonstruowanymi programami, i że jest to dziedzina posiadająca obecnie długa historię sięgająca co najmniej lat 50-tych a może i początków wieku XX. Autor, czyli ja, jest laikiem i amatorem, rad więc przyjmie;-) komentarze i uwagi, zwłaszcza od chcących podzielić się wiedzą, byle nie na temat ortografii;-)

    Początek wieku XX był czasem burzliwego rozwoju logiki. Koniec XIX wieku przyniósł sporo zmian i zamieszania po pracach Fregego i Cantora. Frege dokonał reformy logiki tworząc ją taką jaką znamy obecnie – wprowadził większość znanej nam symboliki, ustalił znaczenie pojęć, podał podstawowe definicje. Cantor tworząc teorię mnogości określił język dla uprawiania matematyki jednak uznanie zostało poprzedzone wielkim zamieszaniem u podstaw samej matematyki – bowiem teoria mnogości wydawała z początku się paradoksalna i niespójna, nie została przyjęta ze zrozumieniem. Można wręcz zasugerować, choć to pewnie kontrowersyjna ocena, że w dużej mierze burzliwy rozwój matematyki w tym przełomowym okresie był próbą wprowadzenia ładu w teorie Fregego i Cantora, okazały się one bowiem tak istotne i wpływowe że zatrzęsły podstawami matematyki. Istotną rolę w rozwoju logiki w tamtych czasach odegrały prace Hilberta nad teorią dowodu, siłą rzeczy zahaczające o logikę i będące próbą formalizacji wnioskowania matematycznego.

    Hilbert starał się wdrożyć potężny program uporządkowania podstaw matematyki w celu przezwyciężenia trudności wynikających z rozlicznych paradoksów odziedziczonych po pracach o których mowa. Okres ten można by podsumować omawiając prace Russella i Witheheada „Principia Mathematica” będącą próbą sprowadzenia matematyki do logiki Fregego i całej matematyki – prąd ten nazywamy logicyzmem ( współcześnie uważa się raczej zgodnie że była to próba nieudana). Można by to dzieło nazwać łabędzim śpiewem logicyzmu, pozostała jednak po niej teoria typów, rozwijana współcześnie w ramach informatyki w zupełnie innym kontekście i z innych powodów. Następne przyszły prace Goedla i Tarskiego niejako zamykające pewien etap, w znaczeniu – ustalające pewien kanon ścisłości i metod opisu w rozwoju logiki. W zasadzie wąsko rozumiany program Hilberta, podobnie jak logicyzm, upadł – prace Goedla przypieczętowały koniec marzeń o absolutnych i obiektywnych podstawach matematyki – jednak z tą opinią nie zgadza siwe zdecydowana większość matematyków;-) Jak było tak było, co wygrało to wygrało, ale wypracowane rozwiązania i metody okazały sie bardzo owocne i przetrwały niejako w nowej roli – stworzono teorię modeli, nowoczesną semantykę, teorię prawdy, ugruntowano pojęcie teorii formalnej.

    Mniej więcej pośrodku tego okresu podjęto próbę formalizacji teorii dowodu i wnioskowania matematycznego. Opisano wówczas tak zwane systemy dedukcji.

    Systemy dedukcji zostały formalnie opisane po praz pierwszy w pracach G.Gentzen  i S.Jaśkowskiego  Warto nadmienić, że jakkolwiek popularność zdobyły prace Gentzen i to one stały się motorem rozwoju tej dziedziny logiki, to wikipedia przyznaje pierwszeństwo otwarcia tematyki badań Jaśkowskiemu. Systemy te, nieco zapomniane i mam wrażenie wyparte z kursów matematyki uniwersyteckiej wydają się co najmniej od lat 60-tych zdobywać na znaczeniu za sprawą rozwoju metod automatycznego dowodzenia twierdzeń. Prace Gentzen i Jaśkowskiego miały jednak motywację czysto teoretyczną i można przypuszczać, że np. Gentzen starał się częściowo być może realizować program Hilberta którego był asystentem.

    Systemy dedukcji w myśl prac Gentzen składają się z dwu elementów (za „Małą Encyklopedią logiki” ): „Każdy system dedukcyjny może być określony jako para (A,R) gdzie A jest zbiorem aksjomatów, zaś R zbiorem reguł dedukcyjnych.”

    Jeśli zbiór aksjomatów jest niepusty, mamy do czynienia z systemem logicystycznym i odpowiada to klasycznym sformułowaniom teorii matematycznych, kiedy zaś zbiór aksjomatów jest zbiorem pustym – mamy do czynienia z systemem dedukcji naturalnej. Co ciekawe systemy dedukcji naturalnej opisano dopiero w latach 30-tych ubiegłego stulecia – wcześniejsze systemy to systemy logicystyczne mające swoje pochodzenie w tradycji logiki i matematyki. Dla porządku, za „Małą Encyklopedią logiki” podam tu przykład dla zestawu reguł dla systemu Naturalnej Dedukcji Klasycznej:

operator: reguła prowadzania: reguła opuszczania:
     
(\land)  \frac{A B} {A \land B}  \frac{A \land B}{A}; \frac{A \land B}{B}
     
(\lor)  \frac{A}{A \lor B};\frac{A}{A \lor B}  \frac{A \lor B, A \vdash C, B \vdash C}{C}
     
(\lnot)  \frac{A \vdash 0 }{ \lnot A}  \frac{A \lnot A}{0};\frac{ \lnot \lnot A }{A}
     
(\to)  \frac{A \vdash B}{A \to B }  \frac{A,A \to B}{B}
     
(\forall)  \frac{B(a)}{(x)B(x)}  \frac{(x)B(x)}{B(a)}
     
(\exists)  \frac{B(a)}{(Ex)B(x)}  \frac{(Ex)B(x),B(a) \vdash A}{A}
     

    oraz reguła dodatkowa: { \frac{0}{A} }

    Rozszyfrujmy powyższe reguły. Każda z nich ma postać „ułamka” w którym nad kreską znajdują się przesłanki, a pod kreską konkluzja. Są to reguły wnioskowania lub inaczej inferencji i należy przez to rozumieć, że jeśli dla przykładu w regule wprowadzania {(\land)} mamy jako przesłanki prawdziwe zdanie A oraz prawdziwe zdanie B, to należy przyjąć że prawdziwe jest także zdanie {"(A \land B)"}. Ciekawa jest reguła (v) w której pojawia się symbol odwróconej litery T. Oznacza on wynikanie – A T C oznacza, że z A logicznie wynika C. Jest to wynikanie logiczne w odróżnieniu od implikacji która jest zdefiniowana jako {p \rightarrow q = \lnot (p \land \lnot q)} bądź za pomocą znanej tabelki z 0 i 1-kami. Kolejny ciekawy szczegół to druga reguła opuszczania {( \lnot )} zwana regułą wyłączonego środka. Jej usunięcie z przytoczonego zestawu prowadzi do innego, nierównoważnego zestawu reguł dedukcji związanego z systemami intuicjonistycznymi – i jest podstawą logiki intuicjonistycznej. Logika ta jest używana w wielu systemach komputerowych dowodów w tym w systemie Coq, o którym będzie ( być może;-) mowa. Reguła opuszczania dla {(\rightarrow)} to oczywiście modus poens czyli reguła odrywania. Reguły {( \forall )} i {( \exists)} dotyczą kwantyfikatorów i pozwalają od zdania kwantyfikowanego przejść do szczególnego przypadku ( „skoro prawdą jest że dla każdego x B(x) to mogę za x wstawić jakąś stała a i opuścić kwantyfikator”, „skoro prawda jest że dla dowolnej stałej B(a), to prawda jest że dla każdego x, B(x)” itp.) Nie ma potrzeby wnikać tutaj dalej w szczegóły. Systemy Gentzen są ciekawe z wielu powodów, teoretycznych związanych z teorią dowodu i praktycznych sa bowiem podstawą automatycznego generowania – a przez to dowodzenia, twierdzeń. Wychodząc od znanych przesłanek, w ramach systemu dedukcyjnego opisanego regułami jak powyżej ( lub innymi) możemy generować kolejne konkluzje będące przesłankami dla następnych konkluzji itp. Oczywiście jeśli zbudujemy ciąg prowadzący od uznanych przesłanek, a zakończony interesującym nas zdaniem – otrzymamy dowód wprost zdania nas interesującego. Jeśli przesłanki są aksjomatami ( co w systemach dedukcji naturalnej nie jest konieczne) – otrzymamy klasyczny dowód wprost zgodnie z definicją twierdzenia w teorii aksjomatycznej.

    Systemy dowodzenia wprost jakkolwiek mają wielkie znaczenie teoretyczne – sa trudne do stosowania w praktyce. Aby dowodzić zadane twierdzenia należałoby kolejno stosować możliwe kombinacje reguł az znajdziemy stosowną i uzyskamy tezę. Oczywiście liczba możliwości rośnie błyskawicznie wraz ze stopniem komplikacji twierdzenia, i metoda staje się niepraktyczna. Z tego a także z wielu innych powodów w badaniach teoretycznych systemów formalnych ogranicza się zwykle liczbę reguł inferencji do modus poens, często przy tym rozbudowując aksjomaty. Warto jednak pamiętać, że rachunek oparty na systemach reguł jak powyżej jest w stanie generować automatycznie twierdzenia wychodząc z zadanych przesłanek. Jest on także bardzo ważnym narzędziem teoretycznym w teorii dowodu zwłaszcza kiedy doda się do niego tak zwaną regułę cięcia ( cut), która pozwala zdziałać cuda, miedzy innymi pozwoliła Gentzen na dowód niesprzeczność arytmetyki Peano bez schematu indukcji, niesprzeczność rachunku kwantyfikatorów i wiele innych. Utorowała także drogę do metody tablic analitycznych która jest kolejną, podstawową techniką mechanicznego dowodzenia twierdzeń. Twórcami metody tablic analitycznych są holenderski logik Beth (1956)  i Fin Hintikka (1955). Nie będę się tu wgłębiał w szczegóły metody, w skrócie odpowiada ona dowodowi niewprost czyli przez zaprzeczenie tezy i doprowadzenie do sprzeczności. W metodzie mechanicznej zaprzeczamy tezie i badamy kolejno wszystkie możliwe implikacje tego działania – tworzy się w ten sposób rodzaj drzewa zawierającego w gałęziach formuły logiczne. Sprzeczności – czyli jednoczesne pojawienie sie na jednej gałęzi p i ~p – ograniczają wzrost drzewa. Jeśli twierdzenie jest prawdziwe, każda z gałęzi zawiera sprzeczność – mówimy że drzewo jest zamknięte. Jeśli twierdzenie jest fałszywe – gałąź niezawierająca sprzeczności daje jednocześnie kontrprzykład – przynajmniej w wypadku klasycznego rachunku zdań. Klasyczny rachunek zdań jest rozstrzygalny, to znaczy dla każdego zdania jesteśmy w stanie w skończonej liczbie kroków podać czy jest prawdziwe. Odpowiada to skończonemu drzewu w ramach metody tablic analitycznych. Dobre przedstawienie metody po polsku zawiera podręcznik Kazimierza Trzęsickiego „Logika i teoria mnogości Ujęcie systematyczno-historyczne” – polecam. W wypadku użycia kwantyfikatorów, a wiadomo że taki przypadek nas interesuje, z wyżej podanych reguł inferencji wynika, że ich eliminacja kwantyfikatora wymaga wprowadzania kolejnych stałych. Liczba tych stałych szybko rośnie, de facto uniemożliwiając skuteczne dowodzenie dowolnych twierdzeń – jak wiemy rachunek logiczny kwantyfikatorów nie jest rozstrzygalny. Współczesny kształt metodzie nadał znany logik Smullayan, jego wpływ był tak wielki że w zasadzie mówi się współcześnie o tablicach jako o jego metodzie. Najpewniej należy przypisać temu, że nie tyle mamy do czynienia z jedną metoda a raczej z ich całą rodziną, i że Smullyan opracował i usystematyzował efektywną i praktyczną metodę dla klasycznego rachunku logiki pierwszego rzędu. Smullyan jest także autorem kilkunastu książek popularyzujących logikę napisanych w całkowicie brawurowy sposób.

    Ciekawym aspektem metody tablic analitycznych jest kolejny polski trop. Otóż jak pisze Melvin Fitting w ‚Introduction” w „Handbook of Tableau Methods” M.D’Agostino, D. M. Gabbay, R. Hahnle and J. Posegga, eds. „Notational simplification was the essential next step in the development of tableaus and, just as with the preceding stage, it was taken independently by two people: Zbigniew Lis and Raymond Smullyan. Lis published his paper [Lis, 1960] in 1960, but in Polish (with Russian and English summaries), in Studia Logica. At that time there was a great gulf fixed between the East and the West in Europe, and Lis’s ideas did not become generally known. They were subsequently rediscovered and extended by Smullyan, culminating in his 1968 book [Smullyan, 1968]. The work of Lis himself only came to general attention in the last few years. […] It is through Smullyan’s 1968 book First-Order Logic [1968] that tableaus became widely known. They also appeared in the 1967 textbook [Jeffrey, 1967], which was directed at beginning logic students. Smullyan’s book was preceded by [Smullyan, 1963; Smullyan, 1965; Smullyan, 1966] in which the still unknown contributions of Lis were rediscovered, deepened, and extended.”

    Metody tablic analitycznych zostały wymyślone od podstaw w celu automatyzacji technik dowodu. Poniżej ciekawy cytat z tego samego artykułu: „In 1957–58, Dag Prawitz, Prawitz, and Neri Voghera developed a tableau-based a system that was implemented on a Facit EDB [Prawitz et al., 1960]. At approximately the same time, the summer of 1958, Hao Wang proposed a family of theorem provers based on the sequent calculus, which he then implemented on an IBM 704 [Wang, 1960]. The first of Wang’s programs, for classical propositional logic, proved all the approximately 220 propositional theorems of Russell and Whitehead’s Principia Mathematica in 3 minutes! This was quite a remarkable achievement for 1958.”

Komentarze ( z buzz):

Marcin Rzeźnicki – Świetny post. Moje gratulacje. Dobrze napisane. Wspomniał bym jeszcze o Heytingu i semantyce Heytinga jako o „dynamicznym”, funkcjonalnym obrazie logiki w celu uzupełnienia przykładu o prawie wyłączonego środka – to może być ciekawe dla „komputerowców”. Polecam książkę Girarda „Proofs and Types” – do ściągnięcia za free z: http://www.paultaylor.eu/stable/Proofs+Types (w tym ujęciu a or not a polegało by na znalezieniu dowodu dla a lub funkcji mapującej dowód a -> 0 co, jak wiemy, nie zawsze jest możliwe). Podobnie z eliminacją podwójnej negacji. a potem pewnie izomorfizm Curryego-Howarda, ale to pewnie masz w zanadrzu na potem. Czekam z niecierpliwością !!8/6

Kazimierz Kurz – @Marcin Rzeźnicki dziękuję, jest mi bardzo miło. Obawiam się jednak że przeceniasz moje możliwości i aż tak kompetentnie tematu nie opiszę – onieśmieliłeś mnie ;-). Chciałem tylko pokazać system dedukcyjny na papierze, i pokazałem jego definicję żeby było jasne że nie od komputerów się zaczęło. O tw. Curryego-Howarda rzeczywiście trzeba będzie wspomnieć, ale jednak celem raczej jest pokazanie samego Coq, a nie „Wprowadzenie do komputerowych metod dowodu – ujęcie historyczne” ;-) bo zwyczajnie nie mam do tego stosownej wiedzy i kwalifikacji, choć chciałbym mieć. Marcin – a może uzupełnisz to co napisałem? Dodaj co uważasz za stosowne – będzie cykl wpisów;-). Mam juz za sobą niedokończone obietnice na temat grupy renormalizacji – tam tez nie powstała najbardziej techniczna część tematu – za co ze wstydem przepraszam – poległem jednak na diagramatyce – aby coś w tej teorii pola porachować trzeba mieć diagramy Feynmanna a to mnie wyraźnie przerosło. Z drugiej strony taki jest ten Web2.0 – jak człowiek się zleniwi a motywacja uleci – cudne plany idą w odstawkę. Tym razem Mój Sprytny Plan ;-) jest taki, że chciałbym napisać takie wpisy -systemy dedukcji (*zrobione, ew do uzupełnienia) -opis narzędzia -Prosty dowód -Nieco skomplikowany dowód Pisząc toto spostrzegłem jak niewiele wiem;-) i jak wiele trzeba by się dowiedzieć by wyjaśniać komuś kto, zakładam, wie jeszcze mniej. BTW. szalenie żałuję, że nie ma tu nigdzie Wlodzimierza Holsztyńskiego – jego uwagi merytoryczne i biograficzne mogłyby być tu znacznie bardziej wartościowe niż sam mój wpis, gdyby zechciał toto skomentować. Jeszce raz dziękuję.
    W następnym wpisie postaram się napisać coś o Coq.

Enter your email address to follow this blog and receive notifications of new posts by email.

Dołącz do 256 obserwujących.

%d bloggers like this: