Dwóch

Jeden znaleziony w rzece Zbrucz pochodzi z IX wieku, drugi sfotografowany został zeszłorocznej jesieni na rynku w Lanckoronie. Oba na swój sposób ładne.

Pół biedy jeśli obserwator rozszerza źrenicę gdy dzieje się coś złego znudzonym wzrokiem ledwie tylko łypiąc przy ukradkowych pocałunkach wstydliwych parek czy szybkim łyku wódki nie tam gdzie wolno. Gorzej jeśli patrzy z wypiekami ocierając spocone z podniecenia czoło. Jeszcze gorzej gdy patrzy i nie ma skrupułów.
Czy na pewno wiemy kto będzie na nas patrzył kiedy pozwalamy by się nam przyglądać?

Informacje o prawach autorskich: Zdjęcie Światowida ze Zbrucza zostało zrobione i udostępnione w zasobach Wikipedii w ramach licencji GFDL i Creative Commons Attribution ShareAlike 2.5 przez pana Jana Mehlicha.

Sprowokowany zabawnym artykułem...

Ponieważ zapronumerowałem wieści o świeżo pojawiających się w niektórych działach serwisu arXiv artykułach, trzymam rękę na pulsie. Przedwczoraj właśnie serwis zaanonsował mi, jak się okazało zabawny i ciekawy, artykulik niejakiego Dorona Zeilbergera. Tytuł jest nieco krzykliwy: "Teaching the Computer how to Discover(!) and then Prove(!!) (all by Itself(!!!)) Analogs of Collatz's Notorious 3x+1 Conjecture".
Zanim po krótce objaśnię o czym ten artykuł, podywaguję (co lubię najbardziej). Zeilberger jest m.in. współautorem (z Petkovsekem i Wilfem) głośnej swego czasu książki "A=B" . W książce tej o ile dobrze pamiętam ćwiczy się intensywnie (choć nie jedynie) automatyczne odkrywanie i dowodzenie identyczności różnych sum z symbolem Newtona w roli głównej. Jest to pewna forma uprawiania wspomaganej komputerowo matematyki w której nie walczy się o ogólność podejścia komputerowego (np. żeby maszyna potrafiła twórczo podejść do udowodnienia bądź nawet odkrycia dowolnego twierdzenia jakiejś teorii), ale raczej eksploatuje się pewne szczególne podejście które daje dużo dobrych twierdzeń jakiejś szczególnej postaci - np. tożsamości - powielając bądź lekko wariując jedną metodę.
W ogóle, to jest historia, która mnie trochę bawi z tymi algorytmami z książki "A=B". Rosyjski matematyk Jurij Matiasiewicz, sławny dzięki zadaniu coup de grace słynnemu X problemowi Hilberta, w pracach z końca lat 90-tych (choćby tu ) pokazał metody tłumaczenia twierdzeń z teorii liczb na tożsamości z użyciem symbolu Newtona, w typie zbliżonym do tych, o których mowa u Zelbergera, Wilfa i Petkoveska. W niektórych pracach wprost nawiązuje on do książki "A=B" wyrażając nadzieję, że uda się kiedyś dzięki jego translacjom, przez (automatyczne) udowodnienie takich tożsamości dowodzić twierdzeń o innej bardziej interesującej matematycznie treści. W szczególności, w pracy Matjasiewicza, którą tu linkuję zajmuje się on translacją do tożsamości dwumiennych starej hipotezy zwanej "problemem Collatza", czasem "problemem Ulama", względnie "problem 3x+1". Zagadnienie jest dobrze znane i szeroko opisywane nie będę go więc tu przedstawiał w szczegółach.
Zeilberger, że zatoczę w moich dygresjach koło, we wspomnianym na początku artykule zajmuje się rodziną problemów formalnie podobnych do problemu Collatza, analizując strukturę dowodów (podanych przez ludzi) dla pewnych przypadków szczególnych. Następnie, pokazuje w jaki sposób można przymusić komputer do postępowania według podobnego schematu: generowania konkretnych przypadków zagadnienia za pomocą metod "rachunkowych" , znajdowania wzorca spełanianego przez przypadki satysfakcjonujące, tworzenia na tej bazie hipotezy (pewnej z góry znanej twórcy programu postaci, ale zależnej od wielu parametrów ustalonych przez komputer w krokach poprzednich), generowania (jeśli się uda) dowodu, który też jest konstruowany według pewnego szczególnego, znanego apriori schematu. Konkretna realizacja tego schematu jest jednak wyszukiwana przez komputer. W efekcie, maszyna wypluwa szereg twierdzeń i dowodów o całkiem interesującej matematycznie treści, wysycając potencjał tkwiący w zaszytych w algorytmie schematach.
Poruszam się tu na dużym poziomie ogólności więc po szczegóły odsyłam bezpośrednio do wzmiankowanej pracy. Nie jest to ani typowa praca matematyczna, ani lektura trudna pojęciowo a i napisana jest leciutko. Sądzę, że jest, bez wielkiego trudu, do przejścia dla tzw. zdolnego licealisty. Niezbyt zawiłe ćwiczenie z nierówności trójkąta, indukcji matematycznej i zrozumienia sposobu działania algorytmów.
Kilka myśli, a może i jakiś morał.
Po pierwsze, w typowym myśleniu o automatycznym dowodzeniu twierdzeń rozważa, się mniej więcej coś takiego:
Przestrzenią w której się poruszamy jest skierowany graf (drzewo właściwie) możliwych wywodów, węzłami którego są wywody, tj. zbiory (być może puste) stwierdzeń.
Wywody w węzłach mają tę własność, że wywód w węźle na końcu strzałki jest powtórzeniem wywodu z początku strzałki z dopisanym aksjomatem lub stwierdzeniem będącym logiczną konsekwencją stwierdzeń wchodzących w skład wywodu z początku strzałki.
Abstrakcyjnie pojęty algorytm automatycznego dowodzenia przeszukuje według pewnej strategii owe drzewo starając się znaleźć nasze twierdzenie jako jeden z elementów wywodu w którymś węźle¹. Pułapka leży w tym, że przestrzeń poszukiwań (ów graf) jest ogromny i startegie prostackie, nie mają szans. Strategie wyrafinowane mają wbudowaną w siebie jakąś podpowiedź (heurystykę). To co proponuje Zeilberger to, w tych terminach, bardzo silna heurystyka, która ryzykując chybienie celu przeszukuje bardzo mały ale obiecujący obszar przestrzeni. Ta strategia może nieźle działać: jesteśmy w stanie zidentyfikować pewne "metody" czy "schematy" dowodzenia które aplikują się w wielu sytuacjach. Jesteśmy w stanie podać sposoby generowania skomplikowanych ale schematycznych prób dowodzenia czegoś. Np. (ograniczając sie jedynie do hasła "indukcja matematyczna"), przez piętrowe dowody indukcyjne albo przez stopniowe wzmacnianie hipotez indukcyjnych jak w pracy Zeilbergera. W takich sytuacjach mechanizacja jest możliwa i może być bardzo efektywna. Oczywiście czytelność takich dowodów jest problematyczna: człowiek może nie być w stanie ogarnąć, dajmy na to, kilkunastopiętrowej indukcji. Może być tak oczywiście, że jakieś teorie wyższego poziomu pozwolą zrezygnować z niezrozumiałych dowodów na rzecz prostszych, z wyższego punktu widzenia niejako przeprowadzonych (ale wtedy same te teorie ukryją w sobie prawdopodobnie całą złożoność). Ale raczej sądzę, że zagadnienia typu np. hipotezy Robbinsa staną się jednak domeną komputerów. Pozostaje wierzyć w maszyny i cieszyć się wynikami. Nie można apriori wykluczyć, ze są twierdzenia, które po prostu dadzą się tylko tak udowodnić - jeśli chcemy więc znać prawdę być może będziemy skazani, również w matematyce, na zaufanie do maszyn.
Ciekawym aspektem pracy Zeilbergera jest też mechanizacja procesu stawiania hipotez. Tu do indukcji matematycznej dochodzi indukcja empiryczna, ale to zupełnie inny temat, zresztą lekko tylko tam poruszony. To zagadnienie - moim zdaniem centralne dla rozwoju tzw. Sztucznej Inteligencji - zasługuje na osobne potraktowanie, na co, w tym sprowokowanym lekturą pracy Zeilerbergera poście, nie znajduję miejsca (ale w przyszłości, kto wie...).
Dołączam się w końcu do apelu autora artykułu: może któryś z nadpobudliwych intelektualnie młodych kolegów, zamiast myśleć o hackowaniu kolejnej strony czy ściąganiu zabezpieczeń z kolejnego programu, zająłby się uczciwszym, a stawiającym wyższe poprzeczki jego umiejętnościom, zajęciem i podjął się dalszych eksperymentów w duchu tych o których mowa w dyskutowanej pracy? Autor tego bloga pewnie chciałby, ale jeśli zdoła to uczynić to chyba dopiero na emeryturze (jeśli dożyje i nie będzie musiał żebrać).


¹Często konstruuje się ten graf inaczej: wychodzi się od zaprzeczenia twierdzenia wyjściowego, aksjomatów i zachowując regułę wynikania z poprzedzajacych wywodów szuka się sprzecznosci.

Wszelkie pogłoski

o śmierci tego bloga (rozpuszczane anonimowo!!!) wydają się być nieco przesadzone. Przyznaję, przyznaję, tegoroczny marzec obfitując w wydarzenia, nawarstwiające się komplikacje, nawał prac rozmaitych, wydaje się być dla blogowania stracony, ale po wynikach jednej bitwy nie rozstrzygajmy o losach wojny.
Wracam więc na łamy z garścią nie do końca powiązanych myśli. Po pierwsze, przeoczyłem niemal poprzedni (marcowy, bo marcowy pojawia się już w lutym, a w marcu konsekwentnie pojawia się kwietniowy) numer "Notices of AMS", gdzie znaleźć można ciekawy artykuł Time-frequency Analysis of Musical Rhythm. Polecam miłośnikom muzyki, przetwarzania sygnałów i nowej nauki (a może odmiany filozofii), którą właśnie obmyślam ;) i którą roboczo i uroczo nazywam ordobabilistyką (zresztą nieważne, o tym kiedy indziej).
Apropos muzyki, o czym pewnie tu jeszcze nie wspominałem, jestem miłośnikiem, choć nie takim jak drzewiej bywało, muzyki - głównie klasycznej ale i dobrych dźwięków nieco lżejszej natury (w tym staroci i zapomnianych ramotek). Idąc za najbardziej ogólną klasyfikacją: preferuję muzykę smutną... Renesans moich zainteresowań muzycznych, dla których znajdowałem w ostatnich latach mało bardzo czasu, wiąże się ściśle z gwiazdkowym prezentem od Mojej Małżonki jakim był odtwarzacz ZEN firmy Creative, a który stał się jednym z moich Najlepszych Przyjaciół. Słucham więc na całego co przy okazji i w miejscach w których nigdy przedtem muzyki nie słuchałem, co jest przy okazji łagodną formą eskapizmu. Najnowszymi czasy, wyrwawszy się z kartezjańskiej pułapki czasu i częstotliwości, w której, na zasadzie obsesji, zamknęły mnie "Wariacje goldbergowskie" Bacha w wykonaniu fortepianowym Bronisławy Kawalli, wpadłem w drugą pułapkę zastawioną przez niezwykłą portugalską śpiewczkę: Marizę. O istnieniu pani Marizy dowiedziałem się, będzie ze dwa lata temu, z telewizji Mezzo, gdzie, przystając w szaleńczej galopadzie po kanałach telewizyjnych, natknąłem się na jej koncert z Londynu. Zrobił na mnie wielkie wrażenie ale jakoś w pierwszym odruchu nie zakupiłem żadnej płyty a potem wspomnienie stopniowo mi się zacierało. Ostatnio wszak nabyłem ich aż trzy i rozrywam sobie serce niezwykłą muzyką fado w wykonaniu niezwykłej Portugalki. Nie jest to przesadnie wyrafinowana muzyka. Fado - to raczej dźwięki i melodie, które z łatwością wzruszają i zapadają w pamięć. Jej prostota jednakże jest szlachetna i nie ma nic wspólnego z prostactwem. Zresztą nie sama forma i melodia są tu zdaje się najważniejsze. Najważniejszy jest głos i emocja. I choć fado jako takie jest wytworem XIX wiecznej miejskiej kultury Lizbony, w tym kraju marynarzy nie mogło nie nasiąknąć elementami kultur obcych. Słuchanie fado jest więc prawdziwą podróżą do podstaw, do "miejsca" w którym z prostych wzruszeń rodzi się sztuka zwana muzyką. Słowem: polecam Marizę. Próbka z YouTube (kiedyś cała ta żerująca radośnie jutubowa szarańcza co się nie boi Boga i praw autorskich pójdzie siedzieć a wiatr będzie hulał po wyludnionych miastach) :

Cóż, wspomnę jeszcze w tym reanimacyjnym wpisie o tym, że niestety częśc moich lektur późnozimowych stała się lekturami wczesnowiosennymi, bo jakoś nie mogę uzyskać tego poziomu koncentracji by je po prostu skończyć. O jednej szczególnej będę musiał napisać osobno, bo zanosi się na moją osobistą porażkę. Odsyłam do wpisów przyszłości gwoli poznania szczegółów, powiem teraz tylko tyle, ża (jak już kiedyś pisałem) matematyka nie jest łatwa niestety...