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

ModusPoens

W poprzednim wpisie przedstawiłem dosyć oczywisty fakt dotyczący zasady indukcji na grafie o jednej składowej spójnej. W obecnym, przejdziemy do nieco innej tematyki, wszakże wpis poprzedni nie był całkiem oderwany od dzisiejszego tematu. Mam nadzieję posługiwać się nim w przyszłości, był wiec to rodzaj przygotowania artyleryjskiego przed bitwą. Amunicji użyliśmy niewiele, a kaliber nie był zbyt wielki. Zobaczymy co dalej.

Na początek kilka słów o motywacji. W poprzednich kilku wpisach drapałem po wierzchu temat reprezentacji dowodów matematycznych jako grafu i próbowałem zdefiniować dla takich struktur grupy homologii tak by cechy dowodu ( konkretnie sprzeczność) miały jakieś homologiczne odzwierciedlenie. Niestety analizując temat dokładniej, dochodzę do wniosku ( o czym napiszę w kolejnych wpisach) że homologia nie wypali. Jest tak dlatego, ze struktura „triangulacji dowodów” jak ją nazwałem – nie jest struktura simplicjalną. Znalazłem błąd w swoim rozumowaniu, są kontrprzykłady, i trzeba stwierdzić, że tego typu podejście wygląda na skazane na daleko idące kłopoty ( co nie znaczy że homologia i logika nie dadzą się pożenić. Jestem przekonany że istnieje tu głęboki związek, np. przekonuje mnie do tego koincydencja faktu że istnieje tylko jeden rodzaj nieorientowalności rozmaitości i jeden rodzaj sprzeczności logicznej. )

Czas więc na kolejne podejście, bo sam pomysł „triangulacji dowodu” wydaje się nadal żywotny, kopie i kto wie, może coś sie z tego urodzi.

Zamierzamy pracować z dowodem matematycznym. Poniżej przedstawię ścisłą definicję tego co będę rozumiał pod tym pojęciem. Będzie ona oczywiście całkowicie klasyczna, zostanie jednak wypowiedziana w pewnej specyficznej terminologii. Aby ją wprowadzić musimy określić pewien obraz czym jest zbiór wyrażeń których ozywamy podczas dowodzenia twierdzenia matematycznego. Po pierwsze dowody powstają w ramach sformalizowanego rozumowania. Każdy dowód powstaje w ramach określonej teorii ta zaś posiada zwykle aksjomaty, operuje pewnego rodzaju obiektami pierwotnymi ( „rzeczy” o których mówi teoria, a których cechy definiują aksjomaty) oraz intensywnie czerpie z logiki określonego rodzaju ( np. logiki pierwszego rzędu FOL). Aksjomaty są relacjami które nakładamy na obiekty będące przedmiotem naszego rozumowania dowodowego, i zwykle w dowodzie nie używamy ich wszystkich, a tylko pewien podzbiór. Sytuacja ta ma prozaiczny powód – większość użytecznych teorii matematycznych posiada nieskończenie wiele aksjomatów. Jako przykład może posłużyć aksjomat indukcji, a używając prawidłowej terminologii: schemat aksjomatów indukcji. Jest to wyrażenie ( lub zdanie, wszakże w zapisie stosowanym zwykle, jest to zdanie wypowiedziane w logice wyższego rzędu niż FOL) które stwierdza, że „dla każdego zdania {T(n)} dotyczącego liczby naturalnej {n}, jeśli prawdziwe jest zdanie {T(0)} oraz {T(n) \Rightarrow T(n+1)} to prawdziwe jest {T(n)}„. Proszę zwrócić uwagę, ze schemat ów – rozwija sie na nieskończenie wiele aksjomatów, po jednym dla każdego zdania T o ile posiada ono cechy wymienione w owym schemacie aksjomatu. Oznacza to, że teoria korzystająca z owego schematu aksjomatów, w istocie posiada przeliczalną ilość aksjomatów. Rzecz jest znana i omówiona w każdym podręczniku podstaw matematyki.

W jaki sposób z schematu aksjomatów dostajemy konkretny aksjomat? Jakie jeszcze mogą lub są schematy aksjomatów?

Sprawa zwykle nie jest szczególnie drążona, wszakże stosowanie schematów aksjomatów jest powszechne. Dlaczego? W języku FOL nie jesteśmy w stanie wypowiedzieć treści kwantyfikowanej po zdaniach. Teoria matematyczna posługująca się językiem logiki pierwszego rzędu zawiera wyłącznie kwantyfikacje po obiektach, to jest po „rzeczach”. Np. w ramach teorii mnogości wypowiadamy zdania o zbiorach i elementach, ale nie o „twierdzeniach na temat zbiorów”. Tymczasem użycie tak prostej reguły jak

\displaystyle \phi \Rightarrow (\psi \Rightarrow \phi )

wymaga byśmy za {\phi} i {\psi} mogli podstawić dowolne zdania. Zwykle zapisuje się ów schemat aksjomatów systemu Hilberta, za pomocą zmiennych {\phi} i {\psi}, rozumiejąc przez to, że mamy do czynienia z nieskończenie wieloma aksjomatami, a {\phi} i {\psi} reprezentują każde możliwe zdanie. Stąd zapis takiego schematu zawiera zwykle kwantyfikator ogólny „dla każdego zdania {\phi} teorii T” {\phi \Rightarrow(\psi \Rightarrow \phi )} i można by wyobrażać sobie że mamy tu w istocie nieskończoną listę aksjomatów, po jednym dla każdego możliwego podstawienia zmiennych. W realnym rozumowaniu istnieje potrzeba użycia stosownej reguły dedukcji, pozwalającej zrealizować owo podstawienie, zasygnalizować je czytelnikowi dowodu. Zwykle ma ono postać zapisu „{\phi = q}” gdzie {q} jest juz zdaniem teorii, dotyczącym „rzeczy” i zapisanym w języku FOL.Jednak wyrażenie „{\phi=q}” nie jest prawidłowym wyrażeniem języka FOL. jest sztuczką syntaktyczną, zapisem mnemotechnicznym, odwołaniem sie do „indeksu w bazie danych aksjomatów” umyślnie oznaczonej „{\phi \Rightarrow(\psi \Rightarrow \phi )}” po to by z owej listy, wyfiltrować stosowny aksjomat dotyczący zdania „{q}„. Regułą taka, opisująca „podstawienie, oznaczmy ją chwilowo {P}, mogłaby mieć postać

\displaystyle P("\phi=q", "\phi\Rightarrow\phi") = " q \Rightarrow(\psi \Rightarrow q )"

Odczytalibyśmy ją jako „w schemacie „{\phi \Rightarrow(\psi \Rightarrow \phi )}” podstaw za {\phi} zdanie „{q}„. Zauważmy że sam symbol równości „{=}” użyty w nawiasach, nie oznacza że owo {\phi} staje się równe „{q}” na stałe a tylko mamy na myśli pewną konkretną realizację, selekcję, ze zbioru opisanego schematem aksjomatów. W terminologii informatycznej powiedzielibyśmy że zasięg leksykalny owego znaku „=” ograniczony jest wyłącznie do zapisu powyżej. Co więcej. wynik takiej operacji podstawienia nie jest zdaniem, a zaledwie kolejnym schematem który może zawierać, i zawiera w naszym przykładzie inne zmienne! Dopiero sekwencja podstawień eliminująca ze schematu wszystkie występujące w nim zmienne, daje w wyniku określone jednoznacznie przez użyte podstawienia, zdanie używanego w ramach teorii języka. Oczywiście jest wiele symbolik opisujących powyższą operację podstawienia. Wydaje mi sie jednak że zaproponowana jest w miarę wygodna i przejrzysta. Co więcej – wyrażenie „{\phi = q}” – choć nie jest zdaniem teorii ( a nawet nie jest zdaniem), będzie wprost występowało na liście wyrażeń używanych w dowodzie, podobnie jak schematy aksjomatów. Ale o tym poniżej.

Kolejnym obiektem który jest używany w procesie dowodowym sa tautologie. Przywołuje sie je czasami wprost – stwierdzając, że pewne zdanie jest prawdziwe niezależnie od prawdziwości występujących w nim zdań, a czasami jako schemat aksjomatów, z zmienną, jak opisano powyżej ( bo też i tautologie są nieprzebranym zbiorem „potencjalnych aksjomatów” zaś ich użycie w taki czy inny sposób jest zwykle kwestią estetyki i optymalizacji środków dowodowych). Ponieważ u podstaw prawdziwości tautologii leży sama logika, a w jej ramach najprostsza metoda sprawdzania prawdziwości – tabela wartościowania prawdy i fałszu, stwierdza sie zwykle że tautologie logiczne są konsekwencją zbioru pustego. Czyli że ich prawdziwość nie wymaga czynienia żadnych specyficznych założeń. Można by rzec, że posiadamy pewną regułę dedukcyjną T, od słowa tautologia, która pozwala nam wprowadzić do dowodu dowolne wyrażenie będące tautologią, a to poprzez wskazanie, ze jest owo wyrażenie konsekwencją zbioru pustego. Zapis wyglądałby następująco:

\displaystyle T(\emptyset ,t) \Rightarrow t

gdzie {\emptyset} to zbiór pusty zaś {t} to tautologia.

Widzimy że w takim zapisie, ze zbioru tautologii wybraliśmy zdanie {t}. Zapis ten jest w pewnym sensie patologiczny, gdyż reguła dedukcyjna dotycząca tautologii {T}, zawiera po obu stronach wyrażenia to samo zdanie {t}. Dlatego zapis ten, choć formalnie prawdziwy i zgodny z resztą terminologii ( o czym poniżej) nie będzie używany dalej zaś osiągniemy to kosztem dodania do naszego zapisu wszystkich tautologii jako dodatkowego, wyróżnionego zbioru tautologii o tym samym statusie co schematy aksjomatów. Nie musi być to od razu zbiór wszystkich tautologii używanej logiki. Wystarczy by zbiór ten zawierał te tautologie które są użyte w dowodzie który będziemy analizować.

Rozważyliśmy zatem trzy zbiory – zbiór aksjomatów A, zbiór tautologii T, oraz zbiór „indeksów”, wyrażeń postaci „{\phi=q}” oraz symbol {\emptyset}, które będę dalej nazywał zbiorem filtrów. Tutaj drobny komentarz, sygnalizujący rzecz nad którą sie zastanawiam, jednak nie umiem jej rozstrzygnąć. Zgodnie z teorią mnogości, zbiór pusty jest częścią każdego zbioru, tym samym należy też do zbiorów {T} i {A}. Być może rozsądniej byłoby rozważyć specjalny symbol na określenie tego rodzaju elementu którego konsekwencją sa tautologie, ale który sam nie jest konsekwencją żadnego rozumowania. Warto dodatkowo pamiętać, że w sensie ogólnym konsekwencją sprzecznego zbioru zdań ( np. teorii o sprzecznych aksjomatach) jest dowolne zdanie, a więc zbiór pełny zdań, a nie zbiór pusty.

Zacznijmy od formalnego przedstawienia opisanego powyżej budulca.

Mamy dany:

 

  • zbiór schematów aksjomatów {A},
  • zbiór tautologii {T},
  • zbiór filtrów {F}, który zawiera wyrażenia postaci „zmienna = zdanie”, oraz zbiór pusty {\emptyset}
  • zbiór L poprawnych syntaktycznie wyrażeń teorii

 

Definicja Zbioru Selektorów: Zbiór selektorów {S} to zbiór zawierający aksjomaty, tautologie i filtry.

Zbiór {Z = A \cup T} nazwiemy zbiorem zdań pierwotnych teorii. Element należący do zbioru selektorów {S} nazwiemy selektorem.

Chcielibyśmy nad zbiorem selektorów i zdań logiki bazowej zbudować mechanizmy umożliwiające rozumowanie dedukcyjne. Należy w tym celu zdefiniować reguły dedukcji, które w niezawodny sposób prowadzą od aksjomatów do poprawnych syntaktycznie wniosków. Pojawia się tu jednak pewien problem. Reguła dedukcji {R}, to funkcja, o 2 argumentach, która odwzorowuje zbiór selektorów {S} i zbiór zdań pierwotnych {Z} teorii, w zbiór poprawnych wyrażeń pewnego rodzaju. Nie są to jednak zdania, a jak widzieliśmy wyżej, schematy zdań, lub listy zdań, w zależności od przyjętego podejścia. Mamy zatem następującą definicję:

Reguły dedukcji: Regułą dedukcji jest to funkcja 2 argumentowa taka że, jeśli {x \in L}, {y \in S} to istnieje takie ( jednoznacznie wyznaczone) {z \in L} że

\displaystyle R(x,y) = z

Wyrażenie {x} nazywamy przesłanką, wyrażenie {y} nazwiemy selektorem, wyrażenie {z} to wniosek.

Ponieważ „nowe” zdania w teorii powstają wyłącznie w wyniku realizacji pewnej reguły dedukcji, a w powyższym wyrażeniu symbol „{=}” oznacza zwykłą równość, możemy każde wystąpienie zdania z zastąpić równoważnym wyrażeniem {R(x,y)}. Tym samym pojecie „zbiór zdań logiki bazowej” staje się czysto mnemotechnicznym wybiegiem, zaś każde zdanie teorii to po prostu odpowiednio zagnieżdżony ciąg reguł dedukcyjnych operujących na selektorach ( w pierwszym argumencie) oraz aksjomatach i tautologiach ( w drugim). Tym samym możemy stwierdzić, że zbiór zdań {L} jest zbyt duży dla naszych rozważań, zaś w tym co nastąpi będziemy rozważali wyłącznie wyniki iteracji reguł dedukcji na zbiorze {A \cup T}.

Zamiarem moim jest zbudowanie graficznej reprezentacji takich struktur, co ma też i taką zaletę, że choć wypowiadam wszystkie zdania poniżej w języku aksjomatów, dowodów itp. te same narzędzia powinny nadać sie do analiz systemów matematycznych gdzie zachodzi iteracja funkcji 2 argumentowych.

Podkreślmy w tym miejscu, że istotne cechy reguł dedukcyjnych:

 

  • reguły dedukcyjne są operacjami czysto syntaktycznymi
  • reguła dedukcyjna jest funkcją.
  • Zachodzą relacje jednoznaczności:
  • ( {R(a,b) =c} i {R(a,d) = c ) \Rightarrow b=d}
  • ( {R(a,b) =c} i {R(d,b) = c ) \Rightarrow a=d}
  • ( {R(a,b) =c} i {R(a,b) = d ) \Rightarrow c =d}
  • wynik działania reguły dedukcyjnej jest prawidłowym zdaniem języka L. Wolę jednak określić tą cechę w innych sposób. Zachodzi cecha przeniesienia typu zmiennej. Reguła dedukcyjna „przy użyciu selektora” przenosi typ z przesłanki na wniosek. Własność ta jest spełniona dla wszelkich reguł postaci modus ponens ( modus tollens itp.), zachodzi też dla wielu reguł rachunku sekwentów.

 

Uwaga – ostatnia cecha to pewnego rodzaju nadużycie. Niestety ściśle rzecz biorąc nie jest spełniona dla reguł polegających na podstawianiu czy też „filtrowaniu” jak wolałbym ten proces nazwać. W takim bowiem przypadku jako pierwszy argument występuje schemat aksjomatów, czyli lista zdań, zaś na etapie wyeliminowania wszystkich zmiennych, ostatni selektor wybiera z niej jedno zdanie, które zostaje zwrócone jako wniosek. Nie jest wykluczone, że jest to ślad czegoś ważniejszego, np. że reguły dedukcyjne powinny być odwzorowaniami zwracającymi nie tyle zdania, co całe listy zdań, zaś teoria powinna posiadać kanoniczne odwzorowanie pomiędzy jednoelementową listą zawierającą zdanie bez zmiennych a zbiorem zdań ( czyli pomiędzy jednoelementową listą i jej elementem) . Definicja taka dodałaby do teorii miłej symetrii, i miałaby sens, bowiem w wypadku podstawiania za jedną zmienną w schemacie w którym występuje ich kilka, wynik podstawienia nadal jest schematem a nie zdaniem.

W ogólności w teorii może występować więcej niż jedna reguła dedukcji, co będziemy sygnalizować przez ich ponumerowanie. Tym samym będziemy mówili o k-tej regule dedukcji {R_k}. Typowym przykładem może być tu system Hilberta gdzie mamy dwie reguły dedukcji: modus ponens i regułę podstawiania za zmienną. Istnieją systemy rachunków zdań gdzie reguł jest więcej ( lub mniej). W dalszych rozważaniach modus ponens ( zapisywana jako „mp”) i reguła podstawiania będą traktowane przeze mnie jako modelowy przykład takich reguł.

Zdefiniujmy co mamy na myśli operując pojeciem dowodu:

Definicja Dowodu: Dowód P twierdzenia t, to ciąg zdań {a_1,a_2 \cdots a_N =t}, o tej własności że dla każdego zdania {a_i} zachodzi jeden z elementów alternatywy:

  • {a_i \in A}, {a_i} jest schematem aksjomatu
  • {a_i \in T}, {a_i} jest tautologią,
  • {a_i \in F}, {a_i} jest elementem zbioru filtrów
  • ogólniej moglibyśmy napisać że {a_i \in S} – jest selektorem lub
  • istnieje liczba {p} oraz {j,k<i} takie że {a_i = R_p(a_j,a_k)} gdzie {R_p} to {p}-ta reguła dedukcji.
  • {a_N = t} nie jest filtrem.

wyrażenie t jest zdaniem ( bo nie jest filtrem) i nazywamy je tezą dowodu.

W ramach takiej definicji w dowodzie zostają zapisane jawnie wszystkie wyrażenia użyte w krokach dowodowych ( a nie tylko te które są zdaniami). Przez długość N dowodu P, rozumiemy ilość selektorów, czyli po prostu wyrażeń, które sie na niego składają.

Z powyższej definicji wynika, że dla każdego dowodu P, mamy ciąg wyrażeń będący jego reprezentacją. Każdemu wyrażeniu {a_i} w dowodzie P przyporządkujmy liczbę naturalną { \#(P,a_i)} – numer miejsca na którym wyrażenie to występuje w dowodzie P. Każdy dowód to skończony ciąg wyrażeń, więc { \#(P,a_i)} jest dobrze zdefiniowane i przybiera wartości od 1 ( dla pierwszego wyrażenia dowodu) aż po { \#(P,t) =N} gdzie {t} to teza dowodu zaś {N} to jego długość.

Dla wygody, kiedy dowód jest ustalony, opuścimy symbol P w powyższym zapisie, czyli będziemy używać wyrażeń postaci { \#(a_i) = n}. Jeśli zdanie q nie występuje w dowodzie, napiszemy \#(q) = 0 . Czasami pewnie opuścimy nawiasy pisząc sam symbol \#a_i =n

W dalszym ciągu będę używał słowa „zdania” w znaczeniu – schematy aksjomatów, tautologie lub zdania właściwe logiki bazowej teorii. Tym samym nie będziemy pedantycznie analizować zagadnień sygnalizowanych w pt. 4 cech reguł dedukcji. Proszę pamiętać jednak że zdanie może oznaczać zarówno poprawne twierdzenie teorii jak i cały schemat zdań ( a więc wyrażenie zawierające zmienne).

Dowód składa się z wyrażeń, ale nowe zdania pojawiają sie w dowodzie wyłącznie jako wynik działania reguł dedukcyjnych. Jeśli w wyniku działania {R_k(q_i,q_j) = q_s} to wykonaniu reguły dedukcyjnej {R_k} przypiszemy taki sam numer jak zdaniu {q_s}. Mamy zatem {\#(P, R_k(q_i,q_j)=q_s) = \#(P,q_s)} i definicja numeru miejsca w dowodzie {\#} zostaje rozszerzona na realizacje ( wystąpienia) reguł dedukcyjnych. O ile w wypadku wyrażeń numeracja jest ciągła, od 1 do N o tyle numeracja wystąpień reguł dedukcyjnych może zawierać luki. Prawdziwe jest jednak poniższe, oczywiste stwierdzenie:

Stwierdzenie: dla danego dowodu P, numeracja użycia reguł dedukcyjnych jest cięgiem ściśle monotonicznym.

Jest to wniosek z faktu, że numeracja zdań w dowodzie jest ściśle monotoniczna, zaś reguły dedukcyjne otrzymują te same numery co zdania, z pominięciem wyrażeń ze zbioru filtrów oraz bezpośredniego użycia aksjomatów i tautologii.

Wydaje sie że wyposażeni w takie narzędzia możemy wypisać podstawowe pojecie jakim będziemy sie zajmować w dalszym ciągu wpisów:

Definicja Triangulacji dowodu:

Triangulacja dowodu P to odwzorowanie {\mathcal{F}} dowodu P w graf skierowany G. Każde wystąpienie reguły dedukcyjnej {R(p,q)=s} jest odwzorowane na trójkąt skierowany {(pqs) = (pq) \cup (qs) \cup (ps)}

W odwzorowaniu tym każdemu zdaniu dowodu {a_i} przypisany jest wierzchołek grafu G. Różnym zdaniom przypisujemy rożne wierzchołki, tym samym zdaniom przypisujemy te same wierzchołki.

Będziemy zajmowali sie własnościami grafów które sa obrazami dowodów w odwzorowaniu {\mathcal{F}}. W następnym wpisie podam przykłady triangulacji, oraz zastanowimy się na jakie sposoby łączą się trójkąty w owej triangulacji.

 

MathTextOntology-pasek

 

 

     W tym wpisie opiszę na prostym przykładzie ;-) w jaki sposób wygenerować własny parser za pomocą antlr. Po zainstalowaniu i skonfigurowaniu zgodnie z instrukcją na stronie ( różne tam systemowe aliasy żeby wszystko się uruchamiało ze ścieżek bezszmerowo), uzyskujmy trzy elementy w systemie: zainstalowany program antlr o którym za chwilę napiszę więcej, program grun – a właściwie spreparowany alias systemowy pewnego złożonego polecenia pozwalający na uruchamianie kodu generowanego przez antlr ( o czym za chwilę) oraz oczywiście zainstalowaliśmy stosowną wersję java, jak napisano w instrukcji instalacji. Jak ktoś chce wykonać własnoręcznie to co opisałem poniżej, musi mieć zainstalowane wszystkie trzy komponenty. Nie będę opisywał tych szczegółów bo są dobrze ujęte na stronie antlr, a ponadto dla prostej nauki można użyć AntlrWorks który nie wymaga żadnych szczególnych konfiguracji i dostarcza „wszystko w jednym” i to dla rozmaitych systemów operacyjnych, a na dodatek obok tego co opisałem poniżej, sprawdza poprawności, koloruje i wyświetla diagramy składniowe dla podanej gramatyki.

    Przejdźmy do samego antlr. Wpis omawia antlr w wersji 4, czyli antlr4. W stosunku do antlr3 są spore różnice, in plus, więc kwestie antlr3 zostawmy na boku, zaznaczając tylko, że jak ktoś czyta gdziekolwiek artykuł o antlr powinien zadać sobie jako pierwsze pytanie o jakiej wersji mowa bo różnice sa spore.

    Antlr jest narzędziem które na wejściu przyjmuje definicję gramatyki języka i na jej podstawie generuje kod programu który potrafi ten język analizować. Nie będę wnikał tu zbyt głęboko w temat, ale właściwie mamy tu do czynienia z definicją gramatyki w postaci BNF zapisaną w specyficzny dla antlr sposób. Pominę także detale związane z poprawnością gramatyki i ograniczeniami jakie niesie antlr – szczegóły sa do odnalezienia w dokumentacji – antlr pozwala na gramatyki wprost lewo rekurencyjne – jak w przykłądzie poniżej, ale nie pozwala na gramatyki niejawnie lewo rekurencyjne ( generacja kodu kończy sie błędem).
Jako przykład niech posłuży nam gramatyka wyrażeń numerycznych obejmujących liczby naturalne oraz ich dodawanie, odejmowanie, mnożenie i dzielenie, oraz nawiasy. Definicja takiej gramatyki ma postać pliku .g4 który wygląda następująco ( numery na początku wierszy nie są częścią pliku):

———————-Expr.g4—————–
(1) grammar Expr;
(2) progr: (expr NEWLINE)*
(3) ;
(4) expr: expr (‚*’|’/’) expr
(5)          | expr (‚+’|’-‚) expr
(6)          | INT
(7)          | ‚(‚ expr ‚)’
(8)          | expr NEWLINE
(9) ;
(10) NEWLINE : [\n]+ ;
(11) INT : [0-9]+ ;
—————————————

    Opiszmy jaki jest cel użycia takiej gramatyki i co z nią potrafi zrobić antlr, a przy okazji wyjaśnimy znaczenie poszczególnych linii pliku. Gramatyka pokazana powyżej nazywa sie Expr, co definiuje linia (1) pliku. Opisuje ona reguły interpretacji pewnego rodzaju tekstu – czyli zespołów znaków tekstowych. Wyrażenia te, jeśli są prawidłowo zbudowane, powinny dać sie zinterpretować w kontekście tej gramatyki, dla siebie powiedzielibyśmy że jako wyrażenia arytmetyczne, a dla programu – jako zgodne z gramatyką ciągi znaków. Wyrażenie takie to progr który jest pewną liczbą wyrażeń expr zakończonych znakami NEWLINE ( linie (2)-(3) pliku). Wyrażenie expr zdefiniowane w liniach (4)-(9) składa sie z wyrażeń typu expr NEWLINE – ( mamy tu jawnie lewą rekurencję)   lub   „nawias” expr „nawias” lub INT lub expr  ( „+” lub „-„ ) expr itp. Kreski pionowe na początku linii (5) i następnych oznaczają alternatywy. Na końcu w liniach (10) i (11) zdefiniowano co znaczy NEWLINE i INT w składni przypominającej wyrażenia regularne. Przykłady bardziej – niekiedy znacznie bardziej – złożonych gramatyk można znaleźć na tej stronie. Polecam zwłaszcza zerknięcie na gramatykę jakiegoś języka programowania jak choćby java czy python, oraz gramatykę opisująca plik csv.

    Program komputerowy analizujący wyrażenie zgodne z powyższą gramatyką, na przykład „(5*(3+4) -12)/(2+3*(6-3))”, powinien prawidłowo rozpoznać elementy wyrażenia, takie jak „(3+4)”, określić ich „znaczenie” i poprawność. Nazwijmy taki program analizatorem. Proces tworzenia analizatora który będzie dokonywał interpretacji takich wyrażeń ma wiele uniwersalnych cech, niezależnych od szczegółów gramatyki zdefiniowanej powyżej. Elementy te powtarzają się zarówno przy budowie analizatorów dla wyrażeń jak „(3+4)” jak i w przypadku analizatorów języka naturalnego, języka SQL, analizatorów sprawdzających konstrukcje języka C++ lub pliki xml. Twórcy antlr stworzyli narzędzie które w oparciu o definicję gramatyki, buduje szkielet programu, w jednym z kilku dostępnych języków, który programista może zmodyfikować dostosowując je w trakcie pracy do własnych potrzeb. Antlr jest zatem programem który generuje programy ( a raczej programem który generuje źródła innych programów). Tego rodzaj programów nazywa sie generatorami kodu, a w tym konkretnie przypadku mamy do czynienia z programem generującym analizatory ( sa oczywiście inne generatory, programy mogą generować szkielety stron www, szkielety GUI, szkielety baz danych i inne. Właściwie każdy IDE który posiada pewnego rodzaju wbudowaną „automatyzację” tworzenia kodu – na przykład dopisuje szkielety klas języka itp. jest tego rodzaju generatorem. Całkiem spora część kodu jest tym samym generowana). Program wygenerowany przez antlr ( domyślnie w java), nasz analizator, składa sie z dwu podstawowych elementów logicznych. Pierwszy z nich nazywa się lekserem. Lekser to program który dzięki wbudowanej gramatyce, takiej jak ta powyżej, jest w stanie prawidłowo rozpoznać elementy języka, zwane tokenami. Tokeny w naszym przykładzie to: złożone wyrażenia progr i expr, symbole operacji logicznych „+,-,*,/”, wyrażenie INT – reprezentowane w prostym tutaj przykładzie jako dowolnej długości ciąg znaków 0,1,2…9 = [0-9]+, oraz wyrażenie NEWLINE, obejmujące znaki nowej linii [\n]+ w dowolnej ilości. Lekser przegląda zatem strumień znaków jaki program analizuje i wykrzykuje z radością – „o! expr! „, „o! progr!”, „o! nawias!”.

     Lekser rozpoznaje ciągi znaków i przekazuje je do kolejnego elementu analizatora – parsera. Parser otrzymuje od leksera, z powodów nazwijmy to technicznych, numer pozycji w wyrażeniu gdzie zaczyna i kończy się dany element języka. Wtedy parser sprawdza czy spełnione sa reguły gramatyki. Prosta gramatyka jaką tu omawiam, nie ma zbyt wielu skomplikowanych aspektów, ale jednym z śladów złożoności z jaką musi poradzić sobie parser jest kwestia poprawnego otwarcia i domknięcia nawiasów. Parser zatem dokona sprawdzenia czy zgodnie z regułami gramatyki zapisanymi w linii o numerze (7) każdy nawias który został otwarty został także prawidłowo zamknięty, czy każdy operator „+” zawiera dwa wyrażenia expr z swojej prawej i lewej strony itp. Parser mówi „nawias mówisz? a gdzie drugi?”.

    Podsumujmy – lekser rozpoznaje, parser sprawdza.

    Jak używać antlr? Zapisujemy definicje gramatyki w pliku o nazwie zgodnej z nazwą gramatyki – w naszym przypadku będzie to plik Expr.g4. Najlepiej całą operację przeprowadzić w stworzonym uprzednio katalogu, gdyż antrl wygeneruje kilka plików z kodem i katalog zapełni się plikami. Następnie generujemy pareser/lexer poleceniem
>antlr4 Expr.g4

Wykonanie tego polecania powoduje że w katalogu w którym je wykonaliśmy pojawi się sporo plików z kodem java.
Kompilujemy owe kody ( w katalogu gdzie to wszystko jest):
>javac *.java

    I już. Powstał nam prosty parser, który potrafi rozpoznać i sprawdzić poprawność wyrażeń arytmetycznych na liczbach naturalnych. Oczywiście od takiej prostej generacji do użytecznych działań daleka droga, ewentualny rozwój aplikacji ( prostego kalkulatora ?) wymagałby od nas grzebania po kodzie jaki wygenerował antlr i dostosowywania tego kodu do naszych potrzeb. W szczególności musielibyśmy napisać kod który zinterpretuje wyrażenia które rozpoznał lekser i sprawdził parser ( ale jeśli ktoś poda nam złe wyrażenie, np. nie domknie nawiasu – obsługę błędów już mamy!). Interpretacja oznacza w ostatnim zdaniu przejście od tego, że program rozumie iż (3+4) to prawidłowe wyrażenie w którym 3 i 4 to elementy INT, + to operator „+” zaś „(” i „)” to nawiasy, do użycia w miejsce + operatora dodawania zaś w miejsce 3 i 4 liczb integer. Antlr bowiem parsuje, czyli przetwarza, pliki tekstowe, i wszystko co sprawdza to znaki w takich plikach, po prostu napisy.

    Sprawdźmy jak to działa. stworzyłem plik tekstowy example.txt o następującej zawartości:

———–example.txt—————–
((2+7*(13-10/7)/8)*12 -3*(5+7))/5
((2+7*(13-10/7)/8)/12 -3*(5+7))/6
———————————————

i za pomocą polecenia:
>grun Expr prog -gui example.txt

wygenerowałem następujący obrazek:

antlr4_parse_tree

    Jak widać w ostatnim poleceniu wskazałem jawnie że wierzchołek parsowania ma postać dyrektywy progr z gramatyki ( jak się wskaże co innego drzewo wygląda inaczej – i jest błędne dla podanego przykładu – co jak rozumiem oznacza, że przykład nie spełnia założenia, czyli że jest czym innym niż elementem, progr. ), czego kod wygenerowany z antlr sam nie rozpozna.

    Antlr generuje kod w java który zawiera lekser i parser. Programy te nie tylko wykonują to co opisaliśmy powyżej – to rola leksera i parsera – ale także reprezentują dostarczony strumień znaków w postaci drzewa jakie widzimy ma obrazku powyżej – jest to tak zwane drzewo parsowania. W drzewie tym, reguły złożone gramatyki, takie jak progr i expr reprezentowane są jako korzenie drzewa, zaś tokeny proste, jak NEWLINE, INT i nawiasy – są liśćmi. Obok leksera i parsera antlr generuje także kod walkera i listenera. Walker potrafi przeglądać drzewo – od lewej do prawej, i generować zdarzenia których oczekuje lekser i potrafi je zinterpretować. Na przykład walker trafiając na wyrażenie „3+4” wygeneruje zdarzenia „wchodzę w wyrażenie „+”, końcowy liść – „3”, końcowy liść „4”, wychodzę z wyrażenia”. Listener może zinterpretować te sygnały i wykonać operację arytmetyczną na koniec wypisując „wynik: 7”, ale może także zamienić nasze wyrażenie do postaci: „wyrażenie to: trzy plus cztery”. Oba te zachowania, i wiele innych, są możliwe, relatywnie łatwe do wykonania, wymagają jednak modyfikacji kodu czego nie będę tu pokazywał – odsyłam do strony antlr. Warto wszakże zwrócić uwagę, że choć z ludzkiego punktu widzenia pierwszy rodzaj działania to wyliczanie, czyli ewaluacja, a drugi to „tłumaczenie na język pisany”, to w sensie koncepcyjnym nie ma tu właściwie żadnej różnicy – zamieniamy symbole jednego rodzaju na symbole innego rodzaju. W taki sam sposób właściwie działa kompilator, translator i interpreter i koloryzator składni.  Antlr jest używany także przy analizie składni zapytań w wyszukiwarkach np. Twitter.

 

Jeśli słomiany zapał mi nie opadnie – wpis będzie miał kontynuację..

 

 

 

    Znane każdemu rodzicowi sa ciągi pytań „A dlaczego?”. Dlaczego Niebo Jest Niebieskie? Bo rozpraszania przebiega w taki sposób że czerwone promieniowanie rozprasza się mało, a niebieskie dużo. A dlaczego czerwone mało a niebieskie dużo? Bo taka jest charakterystyka związana z prawem Rayleigha. A dlaczego taka charakterystyka? Bo rozpraszanie zależy od odwrotności długości fali w 4-tej potędze. A dlaczego od 4-je potęgi? Bo takie jest rozwiązanie stacjonarne równania rozpraszania dla dużych długości fali. A dlaczego … I tak dalej i tak dalej.

    Wiadomo ze można taką zabawę ciągnąć bez końca. W wypadku wiedzy fizycznej, realnej wiedzy o realnym świecie, ciąg takich pytań nie ma końca. Jak jest w wypadku matematyki?

    Kiedyś pisałem, niezbyt jasno, o przypadkowej matematyce . Ostatnio zaś w necie natrafiłem na ciekawe pytanie jakoś tam związane z tym tematem. Oto Gil Kalai, matematyk z Izraela pracujący także w Stanach Zjednoczonych, i prowadzący bardzo fajnego bloga, zadał pytanie „Dlaczego jest możliwe uprawianie matematyki?”, po czym dodatkowo zwrócił uwagę na komentarz Timothy Gowersa, laureata medalu Fieldsa, na to pytanie. Wydaje sie że obaj panowie starają sie nadać temu pytaniu nieco bardziej techniczny, niż czysto filozoficzny, czy metamatematyczny charakter.

     Odpowiedź Gowersa jest o tyle ciekawa, że przywołuje pojęcia teorii złożoności obliczeniowej i probabilistyki. Gowers stwierdza, że jeśli wszystkim twierdzeniom matematycznym przypisać liczbę, zdefiniowaną jako „długość dowodu”, i potraktować ją jako zmienną losową, to „efektywna możliwość uprawiania matematyki” odpowiada ciekawej własności tej zmiennej. Otóż zmienna owa może przyjmować w zasadzie dowolnie wielkie wartości, wiemy że mogą istnieć twierdzenia posiadające proste, krótkie dowody, ale oczywiście istnieją także twierdzenia matematyczne, posiadające dowody bardzo długie, właściwie to dowolnie długie. Co prawda pojęcie nieskończenie długiego dowodu nie ma za bardzo sensu, jednak całkiem uzasadnione jest przyjąć że wartość zmiennej „długość dowodu” należy do przedziału od zera do nieskończoności. Mimo to – i tu dochodzimy do niebanalnej własności owej zmiennej – matematyka się rozwija przy użyciu relatywnie krótkich dowodów – zatem Gowers spekuluje że wartość spodziewana owej zmiennej „długości dowodu” jest niewielka. Długość dowodu może być bardzo mała lub bardzo duża, ale większość dowodów zdaje się być zdumiewająco krótka. Oczywiście sa to spekulacje, czego autor nie zapomina nadmienić.

     Wróćmy do kwestii „przypadkowej matematyki”. Rozumowanie Gowersa przypomniało mi to że o tym temacie kiedyś myślałem. I rzeczywiście także i tu, może warto do tematu podejść nieco bardziej rzeczowo. Będziemy starali sie rozumować przez analogię. Przypuśćmy że rozważamy inne pytanie. Mam liczbę, powiedzmy 3. Dodam do niej liczbę 2 – uzyskam 5. Pomnożę przez 8 – uzyskam 40. Mogę potęgować, dodawać, mnożyć. Wreszcie na koniec mogę wszystkie te operacje zapisać jako program komputerowy, albo sporych rozmiarów, wzór. Uzyskam przepis pozwalający wyliczać wynik wszystkich tych działań, nie tylko dla owej jednej liczby, ale dla innych liczb także, mówiąc krótko – stworzę pewną procedurę obliczeniową definiującą funkcję. Funkcja owa, złożona z elementarnych działań ( takich jak dodawania, mnożenie itp) może być bardzo wymyślna. mimo to w pewnych bardzo ogólnych warunkach będzie obliczalna. Wielkim osiągnięciem matematyki początków XX wieku było określenie owych warunków a zwłaszcza pokazanie, że funkcje obliczalne w ogóle wszystkich funkcji sa relatywnie niewielkim zbiorem. Budując analogię do rzeczy które chcę tu rozważać, możemy stwierdzić, że cokolwiek zrobimy z kilkoma elementarnymi działaniami, w skończonej ilości kroków, uzyskana w ten sposób operacja będzie funkcją obliczalną.

    Niemniej istnieją funkcje nieobliczalne, to znaczy takie których nie da się w ten sposób zapisać, ani nawet obliczyć. Czytelnikowi zainteresowanemu tym tematem polecam doskonałą monografię Murawskiego, w tym miejscu zwrócę zaś uwagę, że mamy tu do czynienia z fenomenem wielkiej wagi oraz posiadającym kilka ciekawych cech:

  1. nieobliczalność jest pewnego rodzaju fenomenem obiektywnym. Do tematu wrócimy poniżej.
  2. nieobliczalność nie polega na tym, że nie potrafimy obliczyć wartości funkcji f(x) nieobliczalnej dla pewnego jej argumentu x. To da sie zrobić dla każdego ustalonego argumentu, oczywiście pomijając kwestie techniczne typu rozmiarów pamięci czy wielkości uzyskanych liczb. Natomiast nie jest możliwe podanie „wzoru” czy tez „procedury” – dokładniej algorytmu – który pozwalałby na obliczenie wartości takiej funkcji dla wszystkich możliwych argumentów. Inaczej – nie istnieje pojedyncza procedura obliczeniowa – jedna dla wszystkich elementów dziedziny funkcji nieobliczalnej – która da jej wartość w tych punktach.
  3. w zasadzie brak odpowiedzi na pytanie czym charakteryzuje sie nieobliczalność w wypadku „realnie występujących zjawisk fizycznych”. Na pytanie „czy istnieją zjawiska fizyczne opisywane funkcjami nieobliczalnymi” nie znamy odpowiedzi. Z jednej strony obliczalność zdefiniowana jest dla liczb naturalnych ( ew. całkowitych) zaś fizyka używa liczb wymiernych. Jest to niezbyt istotna, ale jednak zawsze przeszkoda. Z drugiej strony wydaje się że nieobliczalność mogłaby manifestować się na dwa sposoby – albo jako bardzo szybki, nadeksponencjalny wzrost ( i przykładem takiego zjawiska jest np. Busy Beaver function), albo jako losowość.

 

    W tym miejscu przejdę do innego nieco zagadnienia. Jak wiadomo dla każdego systemu formalnego, mamy dwa możliwe sposoby opisu – syntaktyczny i semantyczny. Oba systemy wuymagają określenia symboli języka, relacji i funkcji wraz z ich arością, aksjomatów pozalogicznych i logicznych wraz z regułami inferencji ( jeśli tego nie określimy pozostaniemy w klasie systemów dedukcji). W systemie syntaktycznym możmy zapisywać twierdzenia i szukać ich dowodów, przy czym dowód jest ciągiem zdań zaczynającym sie od aksjomatów, a kończącym się twierdzeniem którego dowodzimy. W ciągu zdań o którym mowa albo zdania kolejne są aksjomatami, albo sa wynikiem użycia reguł inferencji do zdań poprzednich. Uzyskany w ten sposób zbiór twierdzeń, nazywamy konsekwencją syntaktyczną zbioru aksjomatów. Konsekwencja syntaktyczna to odpowiednik „rachunku”, „kalkulacji”.

     W obrazie semantycznym mamy pewien zbiór A zdań, zwykle aksjomatów, podobnie jak wyżej pozalogiczncyh i logicznych. Zdania te sa odnoszone do pewnego modelu – zbioru obiektów które spełniają zadania z wybranego zbioru A. Zwykle modeli – a więc „zbiorów przedmiotów spełniających zdania ze zbioru A” jest więcej niż jeden. Jeśli pewne inne zdania, zapisane w tym samym języku co zdania ze zbioru A są także prawdziwe w każdym z modeli zbioru A – wówczas mówimy że zdania te są konsekwencją semantyczną zdań ze zbioru A. Konsekwencja syntaktyczna to współprawdziwość, czy może lepiej „współspełnianie” gdyż omijając kwestię prawdziwości i ograniczając sie do spełnienia ( w sensie wartościowania logicznego), unikamy niebanalnych rozważań o tym czym jest prawda itp.

     Czy kwestia istnienia matematyki, możliwości jej uprawiania, nie przypomina tezy o obliczalności pewnych operacji? Tak jak zestawiając ze sobą działania elementarne uzyskiwaliśmy funkcje obliczalne, tak budując twierdzenia lub zbiory zdań współspełnialnych – budujemy teorie oparte o pewne elementarne operacje logiczne. Składamy rzeczy z jednakowych i wcześniej przygotowanych klocków. Możemy użyć ich jak nam sie podoba, możemy dokładać je z lewej, z góry i z prawej, ale klocki pozostają niezmienne, a możliwości łączenia pozostają ustalone z góry.

 

    W tym miejscu należy wspomnieć o kwestii niezależności i niedowiedlności. Oto jednym z ważnych faktów jest zjawisko niezależności logicznej. Okazuje sie że dla dostatecznie złożonych systemów, o ile pracujemy w logice pierwszego rzędu, istnieje wiele modeli. Fenomen ten oznacza, że nawet budując systemy fromalne, bradzo precyzyjnie i ścisle, nie określamy jednoznacznie obiektów które opisują wybrane przez nas aksjomaty.  Jest więcej „rodzajów liczb naturalnych” a dokładniej struktór spełniających aksjomatyke liczb naturalnych – niż tylko jeden znany nam przykład szkolny. W niektórych z modeli pewne zdania sa spełnione w innych nie. Przypomnijmy że konsekwencją semantyczna zbioru zdań są jedynie te zdania które są współprawdziwe z tym zbiorem, dla wszystkich modeli spełniających aksjomaty. Zdania te są zatem niezależne od zbioru aksjomatów – semantycznie nie są zdaniami współprawdziwymi. Ponieważ jednak istnieją modele w których możliwa jest współprawdziwość z aksjomatami ( choć w innych modelach nasze zdania sa nieprawdziwe a więc niespełnione) to stajemy przed kwestią wyboru. Wybór jest takiego rodzaju – albo możemy przyjąć że owe niezależne zdania należą do zbioru aksjomatów ( i tym samym poszerzyć ów zbiór, zaś zawęzić zbiór modeli), albo możemy osąd o zdaniach niezależnych zawiesić i badać teorie z większą ilością modeli, ewentualnie dodając że pewne „fakty” zależą od zawieszonego rozstrzygnięcia co do prawdziwości owych zdań. Zwykle w praktyce posiłkujemy sie kryterium efektywności – wybieramy ewentualności prowadzące do ciekawszej, efektywniejszej, bardziej estetycznej matematyki. Nie jest to jedak cała historia. Zdania prawdziwe we wszystkich modelach, będące sematyczną konsekwencją aksjomatów, mogą być niedowiedlne w ramach przyjętych metod syntaktycznych. Fenomen ten objawia się w fakcie że z punktu widzenia metod logiki 1-szego rzędu, dowody pewnych twierdzeń muszą przebiegać „inaczej” dla każdej liczby n która spełnia warunki takich twierdzeń. Każda liczba może być „przypadkiem szczególnym” zaś ogólne rozumowanie dowodzące twierdzenia we wszystkich takich przypadkach możliwe jest dopiero w logice wyższego rzędu lub w mocniejszej teorii ( np. w teorii mnogości)

     Pytając „dlaczego?” dostatecznie długo, w fizyce, nie uzyskujemy ostatecznej odpowiedzi. W matematyce jest inaczej. W końcu ostateczną odpowiedzią zawsze jest aksjomat. „Dlaczego to twierdzenie jest prawdziwe? Bo tak wynika logicznie z aksjomatów.” Zauważmy że w przypadku opisanym powyżej mamy do czynienia z niezależnością od zadanego zbioru aksjomatów. Tym samym fenomen niezależności logicznej jest fenomenem relatywnym. Obiektywnym faktem jest fakt istnienie zdań niezależnych – dla każdego skończonego zbioru aksjomatów ( a nawet dla zbiorów nieskończonych, przeliczalnych, pewnych określonych własnościach) istnieją zdania niezależne. Zdania których prawdziwość w modelach nie jest jednakowo określona. Sama niezależność konkretnego zdania nie wydaje sie jednak być obiektywnym faktem. Zmieniając układ aksjomatów ( w ramach zbiotu zdań pozostających swoimi konsekwencjami semantycznymi), uzyskamy inne zdania niezależne i inne „moce teorii”. Zdania wcześniej niezależne moga stać sie dowodliwe ( jeśli któryś z „nowych aksjomatów” był wcześnij zdaniem współprawdziwym lecz niedowiednlnym). Wreszcie rozszerzenie zbioru aksjomatów o zdania niezależne ( a więc niewspółprawdziwe) prowadzi do innych – mocniejszych teorii. Jest to zupełnie inna sytuacja niż w wypadku fenomenu nieobliczalności. Jak nadmieniłem w punkcie 1 powyżej – fenomen obliczalności funkcji ma znaczenie obiektywne. Być może jest tak, gdyż elementarne operacje jakie wykonujemy na funkcjach – tak zostały zdefiniowane funkcje obliczalne – są określone w sposób obiektywny i ustalony. Dysponujemy tu operacjami arytetycznymi, ograniczonym kwantyfikatorem i efektywnym minimum, oraz operacją składania funkcji ( rekurencja). Nie mamy tu wolności wyboru. Nie umiemy jako „bazy funkcji elementarnych” wybrać operacji nieobliczalnych co być może pozwoliłoby zapisywać złożone funkcje nieobliczalne jako „złożenie” prostszych klocków.

     W tym miejscu mogę wreszcie zadać pytanie o „przypadkową matematykę” w nieco bardziej techniczny sposób. Pytanie to mogłoby brzmieć mniej więcej tak: czy istnieją fakty matematyczne których prawdziwość nie zależy od przyjętego zbioru aksjomatów, pomimo że są spełnione w każdym z modeli? Na przykład – logika 2-giego rzędu pozwala na usunięcie problemów niezależności zdań dla arytmetyki Peano (PA). Fenomen ten polega na tym, iż w logice 2-giego rzędu istnieje tylko jeden model liczb naturalnych, nie ma modeli niestandardowych. Każde twierdzenie takiej teorii albo jest spełnione albo nie. Płacimy za to pewną cenę, teoria taka ma w zasadzie patologiczne własności ( np. niektóre dowody stają sie nieskończenie długie). Jednak przypuśćmy że w takiej teorii występuje pewna własność liczb, powiedzmy „twierdzenie X”, które stwierdza że liczba X o pewnej własności istnieje. Można sobie wyobrazić sytuację w której owa liczba istnieje także w każdym z modeli PA w logice 1-szego rzędu. I że brak jest dowodu tego faktu, bowiem dowód taki wymaga narzędzi dostępnych jedynie w logice 2-giego rzędu, powiedzmy indukcji pozaskończonej ( takie przykłady istnieją). Możemy wówczas stwierdzić, że choć istnienie liczby X nie ma wyjaśnienia na gruncie PA, to przecież nie jest przypadkiem. Jest to „prawdziwa” własność liczb naturalnych, wszakże niezależna od aksjomatów PA w teorii 1-szego rzędu.

     Pytam więc o istnienie takich cech obiektów teorii które są niezależne od aksjomatów – obiektywnie – a więc w dowolnym rzędzie logiki i w dowolnej aksjomatyzacji. Cech których istnienie jest całkowicie przypadkowe, i nie wynika z niczego co jawnie założyliśmy. Być może odwołując sie do kwestii obiektywności obliczalności funkcji, można by napisać że owa „przypadkowa cecha” nie tyle jest przypadkowa, co raczej wynika z pewnych określonych i niemożliwych do zmiany cech naszych rozumowań, tak jak nieobliczalność, nierelatywnych do wygodnych konwencji, lecz związanych z samą naturą języka i konsekwencji logicznej. Byłyby to zdania, twierdzenia czy własności, których istnienie byłoby konsekwencją np. skończoności zapisu elementów języka, związane z elementarnymi koncepcjami logicznymi jak kwantyfikacja czy negacja. Cechy czy własności takie byłyby obecne we wszystkich modelach jednak nie znajdywałyby syntaktycznego dowodu. Istnienie takich własności jest łatwe do przeoczenia, głównie dlatego że praktyka matematyczna, to przede wszystkim nieformalna praktyka syntaktyczna. Wydaje sie że praktykujący matematyk częściej buduje sobie określony model badanych pojęć a następnie szuka dowodu spostrzeżonych cech, niż szuka zdań wspólprawdziwych w jednym z wielu modeli

 

 

    O sztuce definiowania.

    „Gdy Platon podał definicję „Człowiek jest to istota żywa, dwunożna, nieopierzona” i tą definicją chełpił się i zdobył poklask, Diogenes oskubał koguta i zaniósł do szkoły na wykład Platona, mówiąc „Oto jest człowiek Platona”. Odtąd do tej definicji dodawano słowa: „o szerokich pazurach””. ( W oryginale Πλατων = Platon, πλατωνυχοζ- „o szerokich pazurach” )

„Żywoty i poglądy słynnych filozofów” Diogenes Laertios. O Diogenesie z Synopy, str. 331. PWN Wydanie 3. Warszawa 1982

Przekład: Irena Krońska, Kazimierz leśniak, Witold Olszewski przy współpracy Bogdana Kupisa. Opracowanie przekładu, przypisy ( jak ten powyżej w nawiasie wyjaśniający znaczenie greckiej gry słów) i skorowidz – Irena Krońska.

 

    Wygląda na to że Platonowi jako pierwszemu, za sprawą Diogenesa z Synppy, przydażyło się odkryć modele niestandardowe.

    

    Chciałbym napisać tu coś o ułamkach łańcuchowych. Wpis ten ukazał się wczesnej na Google Buzz. Jak widać z fragmentów dyskusji przytoczonych poniżej nie jestem zbyt kompetentną osobą by pisać na ten temat, jednak mimo to napiszę, bez wielkich zmian. Być może w przyszłości, za słuszną sugestią profesora Włodzimierza Holsztyńskiego, zdobędę się na poprawienie swoich potknięć, rewizję poglądów, i uzupełnienie wpisu. Byłoby to ze wszech miar wskazane, jako, że Włodzimierz ma zdecydowanie rację tam gdzie podkreśla że nie posiadam dostatecznej wiedzy i praktyki co do ferowania ogólnych ocen na temat matematyki i matematyków. Z drugiej strony w pewnych kwestiach, jak by to śmieszne się miało nie wydawać, mam własne zdanie na przedstawianą treść. Tak więc by rzecz dobrze wyjaśnić, a czytelnika nie znudzić, chciałbym wyrazić tu pewną prośbę: czytajcie to co poniżej z dystansem, i darujcie mi niekompetencję. Jestem człowiekiem niecierpliwym, a bardzo chcę pokazać coś więcej niż to co mieści się w typowym traktowaniu poniższej tematyki. by jednak było to możliwe, konieczne jest danie kontekstu. Pokazanie pewnego wprowadzenia by rozmowa nie sprowadzała się do napisania kilku wzorów których nikt nie zrozumie. Namawiam zatem do przeczytania, przemyślenia, skomentowania, ale i do poczekania aż uda mi się dojść do bardziej intrygujących, na amatorski sposób, ciekawych, tematów….

    Ułamki łańcuchowe to ciekawa i niezbyt pamiętana współcześnie konstrukcja. Gdyby spytać o nie ucznia szkoły średniej to pewnie jedynie pasjonaci matematyki znaleźliby jakieś wiadomości o tego typu obiektach, na ogół nie potrafiliby jednak podać pewnie żadnych faktów poza definicją. Przypuszczam, ze nawet studenci matematyki nie posiadają jakiejś szczególnej wiedzy na temat ułamków łańcuchowych gdyż nie są one związane w sposób szczególny z żadnym działem współcześnie wykładanej matematyki uniwersyteckiej. Oczywiście znajomość definicji i podstawowych własności jest elementem ogólnej kultury matematycznej, jednak chyba ułamki łańcuchowe są współczesne raczej kuriozum niż szczególnie ważną konstrukcją w matematyce. Współczesna matematyka zdaje się umieszcza je w obrębie tak zwanej matematyki konkretnej, lezą na pograniczu matematyki stosowanej, informatyki i technik numerycznych.

    Warto wiedzieć, że jeszcze kilkadziesiąt lat temu, i na przełomie stuleci XIX i XX, a zwłaszcza w czasach jeszcze wcześniejszych, ułamki łańcuchowe były ważną konstrukcją matematyczną. Ich analiza zaprzątywała umysły tego formatu co Euler który dowiódł za ich pomocą niewymierności liczby e. Lambert używając ułamków łańcuchowych dowiódł niewymierności liczby pi. Uczeni tej miary co Lagrange, Gauss który wprowadził ułamki łańcuchowe zespolone, oraz wyrażał ich wartości a pomocą funkcji hipergeometrycznych prowadzili aktywne badania na ich polu. ważne konstrukcję wprowadził Pade – twórca tzw. aproksymant Pade, ciekawe i charakterystyczne dla niego są wyniki Ramanujana. Wreszcie Chiniczyn – autor monografii na ich temat. Wówczas było to pole ciekawych badań. Ułamki łańcuchowe mają bliski związek z aproksymacją diofantyczną czyli przybliżaniem liczb rzeczywistych niewymiernych liczbami wymiernymi z dobra, najchętniej optymalną dokładnością. Badania związane z ułamkami łańcuchowymi doprowadziły Chniniczyna do odkrycia tak zwanej Stałej Chiniczyna, która w wikipedii wymieniana jest jako jedna z 10 najważniejszych stałych matematycznych obok liczby pi i liczby e.

    Zajmijmy się na początek podstawowymi definicjami. Przez ułamek łańcuchowy, zapisywany jako [a_{1};a_{1},a_{2},a_{3} \ldots a_{k}] będziemy rozumieli liczbę postaci:

[ a_0;a_1,a_2,a_3...a_k ] = a_0 + \frac{1}{ a_1 + \frac{1}{ a_2 + \ldots \frac{1}{ a_k}}}

gdzie liczba a_0 jest liczbą całkowitą ( a więc może być ujemna, zero lub dodatnia) zaś a_{i} są liczbami naturalnymi. Jest to tak zwany ułamek łańcuchowy w postaci kanonicznej lub regularnej lub prostej . Jest to postać wyróżniona – w takim piętrowym ułamku, wszystkie liczniki zawierają wyłącznie cyfrę 1. Oczywiście w sensie ogólnym tak być nie musi – mamy wówczas do czynienia z ułamkiem niekanonicznym lub złożonym. Teoria ułamków niekanonicznych jest co najmniej tak samo, jeśli nie bardziej ciekawa jak ułamków kanonicznych. Jednak w naszych rozważaniach nie będziemy o nich wspominać.

    Skoro mamy definicję, spróbujmy zapisać w tej postaci jakąś liczbę. wiele przykładów jest bardzo prostych, inne wymagają pewnego nakładu pracy:

\frac{3}{2} = [1;2] = 1 + \frac{1}{2}

3 10/71 = [4;2,1,2,1,2,2] = 4 + \frac{1}{2 + \frac{1}{1+\frac{1}{2+\ldots }}}

    Jak szybko wyliczać ułamki łańcuchowe znając daną liczbę?

    Najszybsze jest użycie programu komputerowego. Wiele dostępnych pakietów bardzo sprawnie wylicza rozkład zadanej liczby na ułamki łańcuchowe, polecam jednak dwa z nich: Sage  które jest wspaniałym narzędziem do zabawy matematyka, jednak jego pobranie to około 400 Mb a instalacja zajmuje około 4 Gb! Monstrum. Dla poszukujących czegoś lżejszego – polecam Pari/GP. Wspaniałe narządzie dla wszystkich zabawiających się teorią liczb, kiedy żona i dzieci śpią. A przy tym nadal jedno z najbardziej wydajnych, wśród darmowych programów – z pewnością rekordzista szybkości.

   Uruchamiamy więc Pari/GP i piszemy: contfrac(52163/16604) i naciskamy enter. Magia! Wynik to: %11 = [3, 7, 15, 1, 146] . Jak oni to zrobili?

    Kiedy mamy zadaną liczbę powiedzmy A, to aby przedstawić ją w postaci ułamka łańcuchowego musimy ją zapisać jako:

A = a_0 + 1/x_0

    Och to proste: a_0 to po prostu część całkowita z liczby A! x_0 też znajdziemy w prosty sposób – x_0   jest odwrotnością części ułamkowej liczby A. A dalej? Dalej to samo! Liczbę x_0 przedstawimy w postaci:

x_0= a_1 +1/x_1

    A z x_1 zrobimy to samo i tak dalej, aż cały proces na którymś kroku się zatrzyma – nie będzie już części ułamkowej. Po wstawieniu wszystkich pośrednich rachunków do jednego wzoru dostaniemy formułę z definicji (1). Pojawia się więc ważne pytanie: Dla jakich liczb ten proces ma szansę się zatrzymać?

    Po pierwsze zauważmy, że jeśli mamy ułamek łańcuchowy [a_0;a_1,a_2,a_3...a_k] to w wyniku wyliczenia jego wartości z definicji (1) otrzymamy liczbę wymierną ( jako stosowny wynik operacji dodawania i dzielenia na liczbach wymiernych, a te są przecież ciałem – a więc te operacje nie wyprowadza nas poza zbiór liczb wymiernych). Możemy wypowiedzieć zatem wniosek:

( T1 ) Skończony ułamek łańcuchowy to pewna liczba wymierna.

    Czy każda liczba wymierna ma zatem postać skończonego ułamka łańcuchowego? Rozważmy liczbę wymierną p/q . Nie ma dla nas znaczenia czy jest to ułamek właściwy czy nie, ważne wszakże, że q \neq 0 . Postępując zgodnie z pomysłem na rozkład na ułamki łańcuchowe opisany wyżej możemy zapisać:

\frac{p}{q} = a_0 + \frac{r_0}{q} = a_1 + \frac{1}{\frac{q}{r_0}} = a_0 + \frac{1}{x_0}

    po pierwsze zauważmy, że

r_0 < q

    gdyż a_0 jest częścią całkowita jaką da się tu wyciągnąć, więc r_0/q jest ułamkiem właściwym. Jeśli mamy r_0 = 0 cały proces się kończy i mamy ułamek łańcuchowy w skończonej postaci. Załóżmy że tak nie jest. Co dalej? Wówczas musi być r_0/q <1 a więc q/r_0 >1 Wykonajmy następny krok rozkładu:

x_0 = \frac{q}{r_0} = a_1 + \frac{r_1}{r_0} = a_1 + \frac{1}{\frac{r_0}{r_1}} = a_1 + \frac{1}{x_1}

    I tu ważne spostrzeżenie:

r_1 < r_0

    z tych samych powodów jak wyżej w równaniu (7). Widzimy zatem, że w procesie iteracji uzyskujemy ciąg czynników r_0 > r_1 > ...> r_k > \ldots które są malejące! W wyniku takiego procesu musimy osiągnąć 0, co zakończy działanie całego algorytmu, bo liczby r_i sa liczbami naturalnymi. Dowiedliśmy zatem następującego stwierdzenia;

( T2 ) Każda liczba wymierna może zostać przedstawiona jako skończony ułamek łańcuchowy prosty.

    Analizując rzecz nieco bardziej szczegółowo można spostrzec, że przedstawiony powyżej algorytm jest bardzo podobny do algorytmu Euklidesa znajdowania największego wspólnego podzielnika dwu liczb. To prawda! Algorytm Euklidesa jako wynik uboczny daje także informacje o rozkładzie liczby na ułamek łańcuchowy. Jednak samo dokonanie rozkładu na ułamki łańcuchowe, przedstawione powyżej, wydaje się być nieco prostsze i łatwiejsze.

    A co z liczbami niewymiernymi? Otóż liczby niewymierne nie mają skończonego rozkładu na ułamki łańcuchowe. W zasadzie nie powinno to dziwić, nie tylko dlatego że przyzwyczailiśmy się do ich „patologii” czy wyjątkowości ( co przecież jest ledwie opinią bardziej estetyczną niż obiektywną). Każda liczba niewymierna może być przybliżana przez liczby wymierne. Lepsze przybliżenia- to na ogół bardziej skomplikowane ułamki – o większych liczbach w liczniku i mianowniku – a zatem dłuższe rozwinięcia w ułamki łańcuchowe… Najbardziej znanym przykładem może być tu liczba pi. Popatrzmy na je kolejne przybliżenia i ich rozkłady na ułamki łańcuchowe (przybliżenia za wikipedią, rozkłady za pomocą PARI/GP):

\pi \approx 3, \frac{22}{7}, \frac{333}{106}, \frac{355}{113}, \frac{52163}{16604}, \ldots

3 = [3]
22/7 = [3,7]
333/106 = [3,7,15]
355/113 = [3,7,16]
52163/16604 = [3,7,15,1,146]

    I tak dalej. Początek dokładnego liczby pi na ułamki łańcuchowe wygląda zaś tak (http://oeis.org/A001203 ):

\pi = [3, 7, 15, 1, 292, 1, 1, 1, 2, 1, 3, 1, 14, 2, 1, 1, 2, 2, 2, 2, 1, 84, ... ]

    Warto zwrócić uwagę, ze znana liczba 22/7 to wynik znany już Archimedesowi, oraz, że szczególnie dobre aproksymacje wymierne to te, które urywają się tam gdzie w ułamku łańcuchowym występuje duży czynnik. W takim wypadku następna poprawka a_j jest bowiem szczególnie mała…

    W ten oto sposób doszliśmy do ważnego zastosowania ułamków łańcuchowych: aproksymacji liczb niewymiernych. Jeśli ułamek łańcuchowy dla pewnej liczby niewymiernej, podobnie jak dla liczby pi, ma jakiś duży czynnik na j-tym miejscu, wówczas jego obcięcie na j-tym miejscu, nazywane j-tym konwergentem lub po polsku j-tym reduktem liczby, daje szczególnie dobre przybliżenie owej liczby. Na przykład 333/106 = [3,7,15] = 3.141509434 to drugi redukt liczby pi, i jak widać daje dobrą dokładność do 4-tego miejsca po przecinku.

    Czy każdy ułamek łańcuchowy, skończony lub nieskończony [a_0;a_1,a_2,a_3...a_k, \ldots ] dla całkowitego a_0 i dowolnych naturalnych a_i różnych od zera reprezentuje jakąś liczbę? Okazuje się, i jest to bardzo ważny fakt – że tak! Co więcej można by nawet nieco zliberalizować założenia i dopuścić by liczby ia_i były całkowite ( różne od zera) byle szereg będący ich sumą był rozbieżny. Przy takich założeniach ułamek łańcuchowy jest zbieżny do jakiejś liczby. Co istotne, jeśli jest nieskończony – liczba ta jest niewymierna, a jeśli skończony – wymierna – co dowiedliśmy powyżej ( liczby rzeczywiste są albo wymierne albo nie, jest to podział dychotomiczny i nie ma innych rodzajów liczb).

    Zauważmy, ze jeśli mamy niezerową liczbę A, to jej odwrotność 1/A w zasadzie przypomina fragment zależności (4) jeśli założymy, że a_0 = 0 . I rzeczywiście, prawdziwa jest zależność:

[a_0,a_1,...] = \frac{1}{[0,a_0,a_1,...]}

    Na koniec tego popularnego wprowadzenia uwaga o równaniach kwadratowych. Przypatrzmy się równaniu postaci:

x^2 -x -1 =0

jak wiadomo rozwiązaniem tego równania jest liczba \varphi stosunek złotego podziału. Jako ludzie leniwi, zamiast rozwiązywać równanie przepiszemy je w postaci:

x= 1 + \frac{1}{x}

a następnie za x podstawimy … wyliczony x:

x= 1 + \frac{1}{ 1 + \frac{1}{x} }

    Ponieważ proces ten możemy kontynuować w nieskończoność, aż x „zniknie” po lewej stronie równości ( a przynajmniej będzie już tak małe że go nie będzie widać – proszę samemu spróbować! ), skoro rozwiązanie oznaczyliśmy symbolem \varphi możemy napisać:

\varphi = [1,1,1,1,1, \ldots]

    Ciekawe prawda? Okazuje się, że całkiem podobnie zachowują się wszystkie pierwiastki równań kwadratowych! Jeśli liczba A jest pierwiastkiem równania kwadratowego i jest zarazem liczba niewymierną, to jej rozwinięcie na ułamek łańcuchowy jest okresowe. I odwrotnie – okresowe ułamki łańcuchowe reprezentują liczby niewymierne będące pierwiastkami równań kwadratowych!

    Czy istnieją inne podobne zależności? Oczywiście. Kilka przykładów można znaleźć tutaj. Co ciekawe, nadal nie wiadomo na przykład czy istnieją jakieś szczególne wzory związane z pierwiastkami innych równań wielomianowych – stopnia trzeciego czy dziesiątego. Intrygujące własności i problemy nie mające odpowiedzi kryją się także za pytaniami o długość rozwinięcia w ułamki łańcuchowe liczb wymiernych, pytaniem o długość okresu ułamków łańcuchowych okresowych i tak dalej.

Literatura: „Continued Fractions” A.Ya.Chiniczyn

   W następnym wpisie napiszę o drzewie Sterna-Brockota.
—————————————————
Poniżej dyskusja jaka odbyła się po mojej prośbie o „recenzję” powyższego wpisu.

Włodzimierz Holsztyński Miło, Kazimierzu, gdy piszesz konkretnie. Gorzej, gdy nakreślasz panoramy i ferujesz wyroki. Poza tym, gdy piszesz o otwartych problemach, to należy zaznaczyć, że matematycy stawiali je w przeszłości, pisali o nich wiele prac. Niedobrze jest robić wrażenie, że się te pytania samemu wymyślilo, jakby przez dziesiątki lat innym nie wpadały do głowy. Szczególnie razi to w przypadku narzucających się, naturalnych pytań, które często należą do domeny publicznej, bo na ogół matematycy nie chcą się podpisywać pod czymś, co każdy może naturalnie pomyśleć. Owszem, czasem wielkim matematykom przypisuje się wręcz banalne, choć ważne, rzeczy, by ich w ten sposob uczcić i nagrodzić za ich dzieło. A te drobiazgi slużą za pretekst do wykazania szacunku. Aug 24, 2011
Włodzimierz Holsztyński Pierwszy paragraf (w obecnej postaci) jest mylący. Matematyka nie jest popularna, więc niematematycy nie mogą mieć jasnego obrazu stanu rzeczy (nawet nie ma takiej potrzeby, matematyka jest skromna). Mógłbyś ten swój pierwszy paragraf równie dobrze napisać o zwykłych ułamkach k/m, i byłby równie (nie)prawdziwy.
Chociaż wszędzie w matematyce można stawiać nowe, dzikie, więc często trudne pytania, to jednak pewne działy/narzędzia dojrzały, wiadomo ile z ich pomocą można uzyskać w ich naturalnych ramach (bez przedefiniowywania i zmieniania zakresu dziedziny). One dalej są standardowe dla specjalistów. Tak jest właśnie z ułamkami łańcuchowymi. Wiele szanujących się podręczników teorii liczb zawiera między innymi elegancki i systematyczny wykład z ułamków łańcuchowych. Oprócz najslawniejszych matematyków również wielu mniej znanych, ale budzących swoimi wynikami szacunek, stosowało ułamki łancuchowe z wielkim mistrzostwem.
Twój artykuł jest na tyle niepełny (to nie jest krytyka, jeszcze nie :-), że naturalnego zakresu stosowalności ułamków łańcuchowych z niego nie widać. Zaznaczę ten zakres trochę w następnym komentarzu. Ograniczenie metody klasycznych ułamków łańcuchowych stymulowało pewne ich uogólnienia, by jednak pójść dalej. Aug 24, 2011

Kazimierz Kurz @Wlodzimierz Holsztyński – hm, a mógłbyś bardziej konkretnie o tych poruszanych/zadawanych już pytaniach? Bo właściwie to takich uwag oczekiwałem. Jak wiesz nie jestem zawodowym matematykiem i w większości wypadków zapewne nawet nie jestem świadom, że temat był już poruszany. Prawdę mówiąc zanim zabrałem się do pisania wykonałem pewną internetową kwerendę, ale też nie miałem ambicji pisać monografii a piszę „amatorsko” dla „amatorów” – w żadnym razie nie są to prace naukowe…
Jako, że jest to esej, uważam że mam prawo do własnej opinii, i z wielkim zainteresowaniem zapoznam sie z Twoją, a im bardziej będzie niezgodna z moją, tym więcej ciekawych rzeczy się nauczę ;-) Zgoda – Artur Popławski na G+ wspomniał, że ułamki łańcuchowe są w większości monografii, w tym w Narkiewiczu i Sierpińskim. Oczywiście to prawda – zarazem zwykle jest to samo sedno, poświęcone podstawowej konstrukcji i własnościom, nie wspomina się zwykle o drzewie SB, reprezentacji binarnej i związkach z SL(2,N). Rozumiem że to niszowe sprawy, akurat dla mnie ważne bo przygotowuję sobie grunt by opisać na końcu coś co sam (?) wymyśliłem. Aug 24, 2011

Włodzimierz Holsztyński Napisałeś Kazimierzu „Skoro mamy definicję [skończonego ułamka łancuchowego]”, ale definicji nigdzie nie podaleś. Być może w tego typu artykule nie ma potrzeby. Jednak frazy „mamy definicję” nie należy wtedy używać, bo szkodzi się mało doświadczonym. (Z drugiej strony dodam na zapas, że żadnych usprawiedliwień, zwłaszcza długich, też nie należy dawać). Aug 24, 2011

Kazimierz Kurz Alez definicja jest: „Zajmijmy się na początek podstawowymi definicjami. Przez ułamek łańcuchowy, zapisywany jako [a_0;a_1,a_2,a_3 ... a_k] będziemy rozumieli liczbę postaci:

(1) [ a_0;a_1,a_2,a_3...a_k ] = a_0 + \frac{1}{ a_1 + \frac{1}{ a_2 + \ldots \frac{1}{ a_k}}}

gdzie liczba a_0 jest liczbą całkowitą ( a więc może być ujemna, zero lub dodatnia) zaś a_i sa liczbami naturalnymi. Jest to tak zwany ułamek łańcuchowy w postaci kanonicznej lub regularnej lub prostej .
[…]
Skoro mamy definicję, spróbujmy zapisać w tej postaci jakąś liczbę. wiele przykładów jest bardzo prostych, inne wymagają pewnego nakładu pracy: ” Może nie działa Ci renderowanie wzorów? Aug 24, 2011

Włodzimierz Holsztyński Dowód twierdzenia (T2) jest ładny, a jego metoda cenna dla czytelników. Sformułowanie (T2) jest niepełne. Pelne twierdzenie mówi, że dla każdej liczby wymiernej istnieją dokładnie dwa różne skończone ułamki łancuchowe, reprezentujące daną liczbę. Informacja o dwóch rozkładach jest ważna w kontekście reprezentowania wszystkich liczb rzeczywistych. Jest to ważna część obrazu. Przypomina ułamki dziesiętne: każda liczba wymierna postaci k/10^n dopuszcza dokładnie dwa różne nieskończone rozwinięcia dziesiętne; na przykład (w układzie dziesiętnym):

1/10^0 = 1.0000… = 0.99999…

Wszystkie pozostałe liczby rzeczywiste są reprezentowane przez dokładnie jedno nieskończone rozwinięcie dziesiętne.

Chodzi w obu sytuacjach o reprezentowanie (rozrywanie i sklejanie) ciągłego zbioru liczb rzeczywistych poprzez dyskretne obiekty jak liczby calkowite lub cyfry dziesiętne. Aug 24, 2011

Włodzimierz Holsztyński Powszechnie mówi się o tym, że Archimedes udowodnił podwójną nierówność:
3 + 10/71 < pi < 3 + 1/7
W tej chwili nie jestem pewny, co wiadomo o jego znajomności dalszych przybliżeń. Być może już wtedy znał(?) późniejsze chińskie przybliżenie 355/113 (znane też poza Chinami), ale z pewnością nie więcej. Warto to porządnie sprawdzić. Aug 24, 2011

Włodzimierz Holsztyński Warto zauważyć, że kolejne redukty przybliżają wartość ułamka łancuchowego na przemian: od dołu, od góry, od dołu, od … Jest to prosta obserwacja.
Dobrze wiadomo, że kolejne redukty są (w mojej terminologii) sąsiadami, t.zn.
|k/m – s/t| = 1/(m*t)
Jest to jedna z ich podstawowych własności. Aug 24, 2011

Kazimierz Kurz O reduktach będę wspominał w późniejszym toku, chociaż z innych powodów.
Z Archimedesem – chyba masz rację – i chyba nieco przekoloryzowałem – znał tylko przybliżenie o którym piszesz na podstawie aproksymacji wielokątami. Aug 24, 2011

Włodzimierz Holsztyński Przy okazji niewymierności kwadratowych można podać informację o problemie ułamków łańcuchowych czysto okresowych, rozwiązanym i opublikowanym(!) przez E.Galois. Więc jeszcze jeden wielki matematyk zajmował się ułamkami łańcuchowymi.
Z grubsza mówiąc, teorioliczbowe problemy algebraiczne stopnia 2 oraz niewymierności stopnia 2 stanowią naturalny zakres stosowalności ułamków łancuchowych. Dla problemów stopnia 3 kilku matematyków badało pewne uogólnienia ułamków łancuchowych. Uzyskali pewne ciekawe wyniki, ale nie udało się rozwinąć równie pełnej i harmonijnej teorii, co w przypadku standardowych ulamków okresowych lub ich wariacji. Wygląda na to, że pełna ogólniejsza teoria, pożyteczna dla stopnia 3, nie istnieje. Aug 24, 2011

Włodzimierz Holsztyński Nie mogę się zdecydować, Kazimierzu, czy Twój artykuł jest krótki, czy długi. Mimo to w każdym wypadku zdumiewającym jest, że nie podałeś zasadniczego powodu dla wprowadzenia ułamków łańcuchowych. To, że czasem fuksem przybliżają niewymierności ekstra dokładnie, jest ledwo marginesową uwagą, a nie powodem. Czyli (gdy brak motywacji) mamy do czynienia ze sztuczną, ciężką konstrukcją, która w końcu nic nie daje. Poza odwrotnością liczb dodatnich, to nawet nie widać na oko żadnych na nich pożytecznych operacji arytmetycznych. Prawdziwy powód jest następujący: redukty i tylko ułamki równe reduktom, są tak zwanymi „najlepszymi przybliżeniami wymiernymi” liczby reprezentowanej przez ułamek łańcuchowy.
Przy tym „najlepszymi” w pewnym nie byle jakim silnym sensie – trzeba tu uważać, bo czasem nawet doświadczony matematyk może się w momencie słabości zmylić (czego byłem świadkiem na seminarium z teorii liczb na jednym z czołowych wydziałów matematycznych :-). Aug 24, 2011

Kazimierz Kurz @Włodzimierz – rozpatrujesz ten esej jako samodzielną całość – a tak nie jest – o bardzo praktycznej aproksymacji wspominam już w 2-giej części – przy czym wprowadziłem ją nieco historycznie – za pomocą drzewa SB które zostało użyte do wynajdywania takich przybliżeń. Moim celem jest jednak na koniec przedstawienie własnych wyników – dlatego cykl esejów ma do nich przybliżać. Ponieważ wyniki te (choć dla mnie ciekawe) nie są szczególnie przełomowe czy ważkie, uznałem że podążając w pewnym kierunku, będę jednak pisał nieco popularnie, by osoby niezwiązane uczuciowo z tematem coś z tego wyniosły. Gdybym napisał od razu co wymyśliłem – nikt by się tym nie zainteresował, a tym bardziej żądnej korzyści by z tego nie odniósł ;-) Aug 24, 2011

Włodzimierz Holsztyński @Kazimierz – jest trzykropkowa sugestia, ale definicji nie ma.
Rozpisanie się o ułamkach łańcuchowych bez podania ich zasadniczej własności, po prostu jest bez sensu, niepotrzebnie czytelnikowi zaśmieca się głowę. To, że w następnym artykule masz jakieś obserwacje dotyczące aproksymacji, niczego tu nie zmienia. Nawet nie odważyłeś się napisać, że równoważne. Prawdopodobnie nie wiedziałeś przy pisaniu. Prawdopodobnie słabsze.
Masz prawo do swoich opinii. Masz prawo głosić je publicznie. Co nie zmienia faktu, że aż za często jest to w złym guście. (Mniejsza o wartość merytoryczną, zaciemnioną niejasnym pisaniem).
Co do odnośników, to nie jestem specjalistą, ani nie mam zdolności kolekcjonowania ich. Na dodatek wciąż mi przetrzebiało moją osobistą bibliotekę, taki los. Wskażę na kilka problemów, do których stosowano ułamki łancuchowe. Jednak takich prac były tuziny, jeżeli nie setki. Prawdziwe poznanie ułamków łańcuchowych oznacza przeskoczenie pewnej bariery, Ci, którzy to uczynili, stosowali ułamki łańcuchowe jako swoje regularne narzędzie naukowe. Zaabsorbowanie wiedzy czyli nabycie techniki ułamków łancuchowych wcale nie jest czymś prostym – jest solidnym osiągnieciem (możliwym dla niewielu), które procentowało w twórczości szeregu laikom nieznanych, ale bardzo dobrych, utalentowanych ekspertów.
W każdym razie, skoro nie poszedłeś do biblioteki, nie przeszukałeś starannie literatury, to moralnie nie miałeś prawa podawać swojej opinii o stanie tej teorii. Jako minimum, choć to byłoby bez sensu, mógłbyś napisać, że podajesz opinię ignorancką, nie opartą na znajomości literatury. Internet wciąż, w przypadku matematyki, nie jest głównym źródłem matematycznej wiedzy historycznej lub bieżącej. Z czasem będzie lepiej, mam nadzieję, ale to jeszcze potrwa.
Ułamki łańcuchowe stosowano do dowodu twierdzenia Fermata o reprezentowaniu liczb pierwszych, dających 1 z dzielenia przez 4, jako sumy dwóch kwadratów (np. 5=2^2+1^2, 13 = 3^2 + 2^2, itd); stosowano do rozwiązania równania Pella; w tematyce Stormera; przy wyznaczeniu kolejnych, najgorzej wymiernie przybliżalnych liczb … J.Browkin i J.Brzeziński w publikacji z 1994 zastosowali ułamki łancuchowe heurystycznie do uzyskiwania przykładów, związanych z hipotezą abc.
Twoja uwaga, @Kazimierzu, na samym końcu artykułu o ułamkach łancuchowych, jest niestosowna. (Sam się nad tym zastanów, bo nie będę wywalał kawy na ławę). Aug 25, 2011

Kazimierz Kurz @Wlodzimierz – ja jednak jestem prostak i wolałbym abyś dał kawę na ławę. Nie wiem o czym mówisz, a obawiam się, że liczenie na moją domyślność jest kompletnie bez sensu. Artykuł jest pomyślany jako dosyć swobodna wymiana myśli, broń boże ani podręcznik ani wprowadzenie nie bardzo więc widzę powód dla którego miałbym formalnie pisać: Definicja: …
Krytykę przyjmuję, częściowo się z nią zgadzam, choć nie znalazłem w niej nic ( w mojej opinii) co miałoby spowodować konieczność zmian w tekście (np. napisanie: „J.Browkin i J.Brzeziński w publikacji z 1994 zastosowali ułamki łancuchowe heurystycznie do uzyskiwania przykładów, związanych z hipotezą abc.” – jest szalenie ciekawe i ważne, ale co to wnosi do wiedzy adresata tego wpisu który ułamków łańcuchowych w założeniu wcale nie zna a jeśli już to tylko od strony elementarnej definicji? Zaś przedstawienie hipotezy abc to jednak co najmniej osobny artykuł w którym wytknąłbyś mi – całkiem słusznie – kolejne tysiące błędów ;-) Bardzo chętnie natomiast przeglądnąłbym jakieś wprowadzenie w prace Galois o których wspomniałeś – masz może jakieś namiary?) . Uzupełnienie wiadomości historycznych jest jak najbardziej sensowną sugestia ale do treści niewiele wnosi – większość z tych tematów jest całkiem nieźle opracowana lub zasygnalizowana np. w wikipedii na temat ułamków łańcuchowych – a nie widzę powodu dla którego miałbym dublować tamtejsze wpisy. Dodanie rzetelnego wpisu historycznego wymagałoby po pierwsze bardzo wiele pracy ( sprawdzenie źródeł) a po drugie rozwlekłoby artykuł – musiałbym zrobić część „0” tylko o tym. W mieście ( a raczej miasteczku ) w którym mieszkam nie ma biblioteki naukowej – sam nie jestem afiliowany przy żadnej instytucji edukacyjnej – nie mam dostępu do JSTOR itp. – o szukaniu prac Galois nie mam więc co marzyć ;-) chyba że są na arxiv. Na Buzz czy G+ ( a nawet na blogu) nie ma miejsca na takie wpisy – w sumie szkoda. Ten i tak został nazwany „dłuuugaśnym”.
Ale może kiedyś wykonam jakąś część pracy która mi zalecasz – wówczas pewnie zbiorę to w formę nieco bardziej obszerną – ebook?. W zasadzie pchasz mnie w tym kierunku swoimi uwagami – i to jest intrygująca myśl… Aug 25, 2011

Włodzimierz Holsztyński @Kazimierz – wcale nie sugerowałem, że należy zamieścić odnośniki na które wskazywałem (choć może ze 2-3 przydałoby się, chyba tak, to nic o tym nie pisałem). Aug 26, 2011

Włodzimierz Holsztyński @Kazimierz – nie chodzi o słowo „DEFINICJA”. Chodzi o to, że nie podaleś definicji (nie ważne, czy wodrębnionej formatem, czy nie), a piszesz, że podałes. Nie musiśz podawać, ale wtedy należy jasno napisać, że się podało tylko sugestię ułamka łańcuchowego, a nie definicję. Podanie „wzoru” z trzema kropkami nie jest definicją. W najprostszych wypadkach można sobie na taki luksus pozwolić. W danym wypadku tak nie jest. Dałeś jakąś ideę o co chodzi, ale nie definicję.
Dla przykładu:
()\quad\quad\quad\sum_{k=1}^n\ a_k\ \ :=\ \ a_1 + ... + a_n
nie jest definicją sigmy (sumy od 1 po n). Podobnie dla funkcji rzeczywistej f nie jest definicją jej sumy wyrażenie typu:
(*)\quad\quad\quad\sum, f\ := ... + f(x) + ...
po wszystkich elementach x\in X , gdzie X jest domeną funkcji f,.
=================
Mam nadzieję, że TeX ( [;\TeX;] ) skompiluje się. (U siebie widzę go skompilowanego). Aug 26, 2011

Kazimierz Kurz @Wlodzimierz – co do definicji to zasadniczo nie bardzo rozumiem, a na swoje usprawiedliwienie mam następujące przykład:
http://books.google.com/books?id=R7Fp8vytgeAC&lpg=PP1&dq=continued%20fractions&pg=PA1#v=onepage&q&f=false – tu natomiast jest książka Chiniczyna – w zasadzie da mnie podstawowy materiał źródłowy ( obok wikipedii i strony Bogomolnego)
Czy mógłbyś zatem napisać jak Twoim zdaniem miałaby wyglądać ta definicja?
W moim mniemaniu definicja to „nazwa” na znany obiekt. Po lewej stronie – coś definiowanego – po prawej wyrażenie które znamy ( np. umiemy wyliczyć jego wartość). Oczywiście stosując sztuczne języki jak Coq, matematykę w języku aksjomatyzacji Peano arytmetyki itp. należy definicję także zapisywać formalnie. Nie widzę jednak powodu by w popularnej pogadance o ułamkach łańcuchowych pisanej swobodnym językiem i adresowanej do amatorów wyrażenie które napisałem nie miało być przyjęte za definicje. Coś czego nie zdefiniowałem – to ułamek łańcuchowy nieskończony – ale o tym będę jeszcze pisał a na tym etapie w zasadzie nie było potrzebne – operowałem w zasadzie wyłącznie na skończonych obiektach poza przykładem (!) dla równania kwadratowego co było wtrętem i nie miało związku z treścią. Aug 26, 2011

Włodzimierz Holsztyński @Kazimierz – pisz tak jak piszesz, tylko unikaj mówienia, że podałeś definicję. Możesz napisać, że Twoje dwa czy trzy paragrafy pozwalają dostatecznie jasno czuć czym są ułamki łańcuchowe. Ewentualnie możesz nawet napisać, że nie podałeś formalnej definicji, ale nie ma już wątpliwości czym są ułamki łańcuchowe. Przy tym w żadnym wypadku ani nie usprawiedliwiaj się z niepodania definicji formalnej, ani przede wszystkim nie pisz, że nie podałeś, bo piszesz dla niematematyków, itp. (trudno byłoby o coś gorszego w popularyzatorskim lub podręcznikowym tekście–w słabych jest to nagminne). Co najwyżej, i jak najbardziej, można czytelników po dalszą wiedzę odesłać do dalszych pozycji w literaturze, jak na przykład niewielki klasyczny podręcznik teorii liczb autorstwa Winogradowa (ostro napisany, ale świetny). Aug 26, 2011

Marek Wojcik Kazik, pisz nie przejmuj się. Z matematycznymi purystami zawsze są problemy, co nie zmienia faktu, że są szalenie pożyteczni, wręcz niezbędni na późniejszych etapach pogłębiania wiedzy. Aug 26, 2011

Kazimierz Kurz Heh, dziękuję Marku. Osobiście prosiłem Wlodzimierza o przejrzenie i krytyczną opinię – i jestem mu za nią wdzięczny. Biorę sobie do serca uwagi Wlodzimierza bo wie co mówi, choć zapewne patrzy na to co napisałem z innego kompletnie punktu widzenia niż ja – stąd spore różnice w zdaniach. Mam swoją wizję propagowania matematyki, jakkolwiek zabawnie by to nie brzmiało, drażni mnie maniera wypisywania twierdzenia popieranego następnie dowodem ( co przecież jest chwalebną tradycją ;-). Wolę formułowanie twierdzeń po przedstawieniu rozumowania po którym stają się oczywistymi wnioskami. Ale moim celem nie jest popularyzacja ułamków łańcuchowych tylko napisanie coś o własnym pomyśle którego z powodu braku wiedzy i czasu nie umiem rozwijać dalej. Ponieważ jestem jednak świadom że to co wymyśliłem to taki drobiazg, a żeby o tym napisać i tak trzeba kupę rzeczy objaśnić, pomyślałem, ze zrobię to właśnie w taki, amatorski i popularny sposób. Pomyślałem, ze jeśli będę umiał rzecz wytłumaczyć komuś kto nie wie o ułamkach nic zgoła – sam to lepiej zrozumiem ;-)
Na koniec się pewnie okaże że góra mysz urodziła, wiec niech chociaż ta popularyzacja ma jakąś wartość… Aug 26, 2011

     
    Wszystkie języki ludzkie używają słów. Słowa sa obecne nawet w tak sztucznych zdawałoby się tworach jak języki programowania i to nie tylko na poziomie skonstruowanym dla człowieka ( wszystko od asemblera w gorę, człowiek ma co najmniej pisać a czasem i czytać te twory) ale nawet na poziomie poniżej, w języku maszynowym gdzie również zaznacza sie podział na „słowa” przetwarzane przez maszynę. Wygląda na to, ze konstrukty ludzkiej myśli nie są w stanie oderwać się od koncepcji „sekwencji słów”.
    Ciekawe sa tu dwie konstrukcje:
    Funkcyjny język programowania z całkowitą lazy evaluation jak w Haskelu. Program zostaje wyliczony w całości a przynajmniej taki jest sens jego wykonania. Mamy tu do czynienia z sytuacja kiedy w wysokim poziomie programowania, nadal posiłkując się „słowami” czyli konstruktami niosącymi dyskretne operacje, składając je, uzyskujemy coś co ma zapewnić „jednostopniową procedurę obliczenia”. Aby zapewnić taką atomowość włożono sporo wysiłku. Uzyskuje się w zamian wysoki poziom determinizmu obliczeń: te same dane co do zasady dają te same wyniki. Oczywiście w praktyce brak pełnej izolacji i 100% pewności.      


    Nonfirstorderizability – zjawisko polegające na tym, że pewne wyrażenia logiczne nie dają się zapisać jako zdania w logice pierwszego rzędu. Nic w tym dziwnego, takich stwierdzeń jest bardzo dużo, niektóre całkiem „proste” jak np. „przestrzeń wektorowa skończonego wymiaru”, lub „zbiór o skończone liczbie elementów”. Okazuje się, że istnieje jednak podejście nazywane Branching, które ogólnie polega na porzuceniu liniowego następstwa kwantyfikatorów ogólnych ( „dla każdego” …) i wprowadzeniu dodatkowej konwencji że mogą być one używane „jednocześnie”, lub „atomowo w grupie”. Po wprowadzeniu takiej modyfikacji uzyskujemy logikę która nadal jest słabsza niz logika drugiego rzędu ( a więc nie ma kwantyfikacji po zdaniach) jednak jest mocniejsza niż logika pierwszego rzędu. W szczególności pozwala na wyrażanie stwierdzeń o prawdziwej niezależności dwu i więcej zmiennych ( proszę porównać: http:/terrytao.wordpress.com/2007/08/27/printer-friendly-css-and-nonfirstorderizability )

    Ciekawe, że obydwa podejścia czyli lazy evaluation, i branching sa mocnymi pod pewnymi względami narzędziami w których efekt uzyskuje sie porzucając pewnego rodzaju naturalną dla człowieka i języka sekwencyjność, i dopuszczając pewnego rodzaju, nawet ograniczoną jak w branchingu, atomowość, w obu wypadkach na wysokim ( i niejako emulowanym przez bardziej elementarne „rachunki”) poziomie.

 

 

 

 

 

 

    „Każdy kto uczył sie tzw. matematyki wyższej wie, że na różnych przedmiotach matematycznych tak samo nazywające sie pojęcie ma całkiem różne definicje. [..] Nikt natomiast nie zadaje sobie trudu by udowodnić równoważność tych wszystkich definicji. Często powstałby zresztą w takiej sytuacji problem: na jakim gruncie dowodzić tej równoważności. […] dlaczego nie prowadzi to do bałaganu?

    Najbardziej znana i utożsamiana z Kleinem jest ta część jego wykładu w której rozważa on pytanie, co to właściwie jest teoria matematyczna. Tu mieści się też właśnie owa niewykorzystana droga innego potraktowania matematyki jako całości, nie jest to dziś robione. Teoria matematyczna, według Kleina, jest to coś zupełnie innego, niż można znaleźć w podręcznikach podstaw matematyki, logiki matematycznej itp. Teoria matematyczna powstaje, zdaniem Kleina, w momencie obrania pewnego zbioru Z i pewnej grupy G przekształceń tego zbioru. Zauważmy że podczas wykonywania przekształceń z obranej grupy pewne struktury utworzone z elementów tego zbioru zmieniają się, a inne pozostają bez zmian. […] Teoria zdaniem Kleina to zbiór zdan prawdziwych o niezmiennikach. Takie rozumienie pojęcia teoria ma szereg zalet.

     Dla przeciwstawienia należy teraz opisać konkurencyjna (i zwycięską) koncepcję [..]. Ma ona charakter syntaktyczny[..] Moritz Pasch [..] podjął trud napisania od nowa Elementów Euklidesa, ale tak, by spełniały one ( a raczej ich odpowiednik) wszelkie wymagania jakie sformułowaniom pojęciom i rozumowaniom stawiał koniec XIX wieku. […] Od strony geometrycznej przyniosło ono spostrzeżenie że pojęcie odcinka (równoważnie – porządku na prostej) jest w oryginalnych Elementach czysto intuicyjne. Wskazano tez jakiego rodzaju „szósty postulat” należy dodać […] Zauważmy tyko, że teoria w sensie Kleina nie jest teorią w sensie Pascha. Powód jest bardzo prosty – już dla bardzo nieskomplikowanych zbiorów ich kleinowskie teorie mają nieprzeliczalną liczbę niezmienników, a teoria typu syntaktycznego może mieć jedynie tyle pojęć ile jest możliwych napisów – tych jest ( nawet przy założeniu że dopuszczamy nieskończenie długie ) tylko przeliczalna liczba: napisy to przecież ciągi.”

    „Kończąc ten króciutki tekst poświęcony udziałowi logiki w matematyce, chciałbym stwierdzić, że logika właściwie nigdy matematyce nie pomogła – wspierała tylko, niejako ex post, jej działanie. Zakres stosowanych metod wybierany byl na innej drodze – chodziło o to, by uzyskiwać jakieś prawdy, a to się w logice zmieścić nie chciało. Unikanie błędów nie jest bowiem aktem twórczym. Duże znaczenie jakie logika matematyczna uzyskała w pierwszej połowie XX wieku, bierze się stąd, że postanowiła odpowiadać również na ontologiczne problemy matematyki ( o czym będzie za chwilę mowa) oraz – później – ze względu na domniemanie, że może się niesłychanie przydać informatyce ( o czym pisał nie będę)
[…]
    Zgadzam się z opinią (najostrzej wyrażaną przez bourbakistów), że najczęściej to, co mówi matematyk na ten temat, jest wątpliwej jakości, bo jakoś mało matematyków uprawia filozofię.
[..]
     W Starożytności kłopotu ze statusem pojęć matematyki nie było, jak też nie było kłopotu z prawdziwością jej twierdzeń. Starożytni traktowali bowiem matematykę jako naukę przyrodniczą […] niezależnie od tego czy sąd taki miał nachylenie materialistyczne (Demokryt) czy też idealistyczne (Platon).
[…]
     W konsekwencji matematyka w XVII wieku miała się weryfikować pośrednio – jedynie przez zastosowania. I choć każda rzecz była w niej wątpliwa i o każda trwały spory, sprawy jej prawdziwości w gruncie rzeczy nie dyskutowano.
[…]
    Wszystko było dobrze, dopóki w matematyce nie powstała konieczność dokonywania wyboru jednego z kilku możliwych opisów jednej i tej samej rzeczywistości . Riemann w swoim wykładzie habilitacyjnym pisze: „Pozostaje problem, w jakiej mierze i w jakim sensie hipotezy te potwierdza doświadczenie „, ale przecież sam nie wierzy , że jakieś doświadczenie wykaże iz wymiar fizycznej przestrzeni okaże się np. 1993 ( bo przecież uprawia geometrię n-wymiarową dla dowolnego n).
[…]
     Wyjścia sa trzy: albo machnąć ręką na rzeczywistość i uprawiać sobie taka matematykę, jaką się ona okazała (sama?), albo też przyjąć ostre rozwiązania restrykcyjne i wszelkie niestandardowości wykasować ( a czy coś wtedy zostanie?), albo wreszcie mieć nadzieję, że całą (jedyną już wtedy) matematykę z czegoś się wyprowadzi. Jeśli dodać do tego jeszcze pojawiające się […] paradoksy, to otrzyma sie pełną motywację powołania do życia podstaw matematyki – dyscypliny, której powierzono rozstrzygnięcie tych sporów.

    W tej sytuacji propozycja Moritza Pascha stworzenia dla każdej z dyscyplin matematyki odpowiedniej syntaktycznej teorii […] została powszechnie przyjęta jako droga do wyjścia z sytuacji – począwszy od ostatniego dziesięciolecia XIX wieku, przez ponad pół wieku – wszystko się aksjomatyzuje. Problem prawdy matematycznej staje się w tym ujęciu problemem konkretnym – mamy określoną strukturę – teorię formalną – i chcemy dla niej określić pewną własność ( niech jej będzie prawdziwość – ale to brzydkie słowo), która byłaby dla tej teorii świadectwem moralności. To brzmi sensownie, na tyle sensownie że nawet Poincare – wykpiwający przedtem pojęcie prawdy matematycznej tak jakby to była np. druga świeżość – uznał takie rozwiązanie za właściwe. A co więcej – to się daje zrobić. Konkretnie prace tę wykonał w 1933 roku Alfred Tarski ( „Pojęcie prawdy w językach nauk dedukcyjnych”). Stosowna operacja użyta przez Tarskiego jako indykator prawdziwości to precyzyjnie matematycznie określone spełnianie. Można by więc sądzić, że wszystko trafiło na swoje miejsce – tymczasem wcale tak nie było.

    Zadanie zbudowania aksjomatycznej teorii w sensie Pascha dla wszelkich teorii matematycznych okazało się zadaniem trudnym i niewdzięcznym. Niewdzięcznym dlatego, że powstające teorie miały na ogół mnóstwo zupełnie paskudnych własności. W celu zapobieżenia takim wypadkom program Pascha aksjomatyzowania matematyki znacznie zaostrzono. Od aksjomatycznej teorii formalnej zażądano by spełniała pięć warunków. Oto one:

  • niesprzeczność (oznacza to, że z dwóch przeciwnych zdań w jej języku co najwyżej jedno należy do teorii)
  • zupełność (że co najmniej jedno należy)
  • kategoryczność ( że dowolne dwa obiekty opisywane przez tę teorię sa izomorficzne)
  • rozstrzygalność ( istnieje algorytm pozwalający w skończonej liczbie kroków stwierdzić, czy dane zdanie należy do teorii)
  • skończona – lub choćby przeliczalna – aksjomatyzowalność (wszystkie zdania teorii można uzyskać jako konsekwencje ich skończonego – lub ewentualnie przeliczalnego – zbioru; pożądane jest przy tym, aby były to zdania niezależne czyli takie żeby teoria uzyskana z każdej mniejszej liczby aksjomatów miała mniej twierdzeń)

    Przytoczyłem je dlatego, że program ukonstytuowania każdej gałęzi matematyki w formie takiej pięcioprzymiotnikowej aksjomatycznej teorii formalnej jest znany powszechnie jako program Hilberta i stanowi założenia szkoły metodologicznej zwanej formalizmem.

    Szkoły metodologicznej – to nie żart. Okazuje się bowiem, że stare ostrzeżenie, jakie matki dawały córkom, by się zbyt długo nie wpatrywały w lustro, gdyż zobaczą diabła, spełniło sie w matematyce.: tak długo matematycy przyglądali sie swojej dyscyplinie, aż diabeł się pojawił i matematyka rozpadła się na różne szkoły metodologiczne, tak jak nie przymierzając – historia.
[…]
     Formalizm rozwijał się bardzo bujnie i byl już w latach dwudziestych dominującą doktryną uprawiania matematyki – sam Hilbert w 1917 roku pracował prawie wyłącznie w tym kierunku. Bo mimo nakładu ludzkiej energii zrealizowanie postulatu eleganckiego zaksjomatyzowania matematyki, niestety, nie przynosił spodziewanych sukcesów. Co gorsza z biegiem lat pojawiły się klęski. Była już mowa o niemożności dowodu niesprzeczności arytmetyki zgodnie z zasadami formalizmu (II problem Hilberta). Tenże Goedel który byl autorem tego rezultatu wykazał w 1931 roku również niezupełność arytmetyki ( i każdej teorii w której arytmetykę można zinterpretować). Większość potrzebnych teorii nie spełniała więc dwóch spośród wymaganych warunków. W 1933 roku Theoralf Skolem ( o którym już była mowa) i Leopold Loewenheim (1878;1940) wykazali, że każda teoria (typu Pascha), która ma model nieskończony, ma model każdej nieskończonej mocy – kategoryczność może więc tylko mieć miejsce dla teorii dotyczących skończonych zbiorów (chyba że przez teorię będziemy rozumieli co innego niż Pasch). Z rozstrzygalnością okazało się, że jest to własność egzotyczna, tj. przysługująca bardzo nielicznym teoriom i na dodatek bardzo dziwnie względem siebie usytuowanym – np. arytmetyka liczb naturalnych rozstrzygalna nie jest, a liczb zespolonych – jest. Słowem totalna klęska.

    W tym świetle może się wydawać dziwne, że gdy przyszedłem na studia (lata pięćdziesiąte) na Uniwersytecie Warszawskim większość matematyków ( a nie byli to byle jacy matematycy – dziś wystarczyło by ich dla całej Polski i to z dużą górką) była z przekonań i ze sposoby wykładania formalistami. [..] Dlaczego więc formalizm był w przewadze? […] formaliści kupili większość matematyków na wizję matematyki która dla matematyków jest bardzo dobrze określoną grą i tylko narzędziem dla całej reszty. Na wizję matematyki, której stosowalność w realnym świecie jest niezgłębioną niezgłębialną tajemnicą. Przewaga formalistów ( ogromna w środkowych dziesięcioleciach XX wieku sięgająca 90%) zniknęła w latach siedemdziesiątych.
[…]
Najbardziej rozpowszechniony od lat siedemdziesiątych pogląd na tę sprawę zakłada miałkość problematyki podstaw matematyki i proponuje zachowanie buszmena – jedyną naprawdę pewną rzeczą jest busz, a jaki jest busz, każdy widzi i może się o tym dowolnie mocno na własnej skórze przekonać. Kierunek ten pochodzi od Ersta Zermelo i zakłada że interior w którym żyją matematycy to teoria mnogości […]
Słowem u progu XXI wieku matematykę uprawia się radośnie i beztrosko zupełnie nie przejmując się tym, że żaden z problemów […] nie został rozwiązany. Nikt zresztą nie chce na takie tematy rozmawiać […]”

 

    Cytat z książki „Wykłady z historii matematyki” Kordosa, wydawnictwo SCRIPT z 2005 roku, w moim egzemplarzu strona 246 na temat podejścia Kleina i strona 276 i następne na temat podejścia Pascha ( tu np. jest ta książka, o ile wiem ma wznowienia: http://www.matematyka.wroc.pl/node/1083 )

      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.

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

Dołącz do 256 obserwujących.

%d blogerów lubi to: