Inspirujące idee

Duże znaczenie dla rozwoju informatyki miały idee i odkrycia Alfreda Tarskiego. Chociaż nie znalazły bezpośredniego zastosowania, to miały decydujące znaczenie dla rozwoju wielu powstałych w obrębie informatyki rozwiązań.

Duże znaczenie dla rozwoju informatyki miały idee i odkrycia Alfreda Tarskiego. Chociaż nie znalazły bezpośredniego zastosowania, to miały decydujące znaczenie dla rozwoju wielu powstałych w obrębie informatyki rozwiązań.

W 1997 r. Anita Feferman wygłosiła na Uniwersytecie Warszawskim wykład "Saga o Alfredzie Tarskim: Z Warszawy do Berkely", oparty na materiałach zbieranych przez Anitę i Solomona Fefermanów do biografii tego jednego z największych logików wszech czasów. Wówczas jeszcze jej autorzy nie mieli wyobrażenia, ile trzeba będzie czasu do zakończenia dzieła. Praca nad książka "Alfred Tarski: Life and Logic" została ukończona dopiero jesienią 2004 r.

Alfred Tarski urodził się 14 stycznia 1901 r. w średnio zamożnej rodzinie żydowskiej w Warszawie, gdzie też dorastał, ukończył studia, zrobił doktorat (jego promotorem był Stanisław Leśniewski). Opuścił Polskę w 1939 r., udając się na spotkanie na Uniwersytecie Harvarda planowane na początek września. W związku z wybuchem wojny do Polski już nie wrócił. Przez kilka lat uczestniczył w różnych projektach badawczych oraz wykładał na uczelniach wschodniego wybrzeża. Kiedy otrzymał ofertę jednorocznego zatrudnienia na odległym wówczas Uniwersytecie Kalifornii w Berkeley, zdecydował się z niej skorzystać. Już pod koniec wojny osiągnął tam najwyższe stanowisko profesorskie.

W Berkeley Tarski stworzył od początku światowe centrum logiki matematycznej. Tu pozostawał, pracował ze studentami i kolegami, aż do swojej śmierci w 1983 r. Miejsce w światowej logice zapewnił sobie pracami z teorii mnogości, teorii modeli, semantyki języków formalnych, teorii rozstrzygalnych i procedur rozstrzygania, teorii nierozstrzygalnych, algebry uniwersalnej, aksjomatyki geometrii oraz algebry logiki. Można postawić pytanie, czy to, co robił, miało w ogóle jakieś związki z informatyką, a jeśli tak, to jakie?

Solomon Feferman pisze, że kiedy Anita rozpoczęła prace nad biografią Tarskiego - dopiero później stało się to ich wspólnym projektem - zadała sobie właśnie takie pytanie. Odpowiedź brzmiała: nie. Inaczej odpowiedział jej John Etchmenedy (kolega Solomona Fefermana z Uniwersytetu Stanforda) - "Czy widzisz te wielkie lśniące wieże Oracle'a na autostradzie 101? Nigdy by nie powstały, gdyby nie było rekurencyjnej definicji spełniania oraz prawdy autorstwa Tarskiego". Zafascynowało to Solomona Fefermana, który podjął się wskazania, jaki wpływ na rozwój informatyki miał Alfred Tarski. Interesująca jest w tym kontekście postawa samego Alfreda Tarskiego wobec informatyki.

W 1950 r. Feferman był studentem Tarskiego. Wówczas to Tarski rozpoczął systematyczne prace nad teorią modeli i algebrą logiki. W 1957 r. Feferman uzyskał doktorat i zaraz po tym uczestniczył w legendarnej, jak się potem okazało, konferencji na Cornel University. Według słów Anil Nerode - "Do tej pory w logice nie miało miejsca coś porównywalnego. Spotkali się po raz pierwszy czołowi naukowcy, początkujący badacze i studenci ze wszystkich ważnych dziedzin logiki. Oprócz Tarskiego i jego towarzystwa byli Alonzo Church, Stephen Kleene, Willard Quine, Barkley Rosser, a z nowej generacji Abraham Robinson i George Kreisel". Spotkanie inspirował matematyk Paul Halmos, który w swojej "Automathography" napisał o tym spotkaniu - "W tym czasie było wiele konferencji, zjazdów, kolokwiów, a nieliczne z nich były cenione. Uznałem, że miło byłoby mieć coś takiego w logice, w szczególności gdyby częściowo było to algebraiczne".

Podczas spotkania po raz pierwszy wygłoszono wiele referatów z zakresu formującej się wówczas dziedziny teoretycznych podstaw informatyki. Same teoretyczne podstawy informatyki stworzyli w latach 30. Gödel, Church, Turing, Post i Kleene. Zaś powiązanie teorii i zastosowań zaczęło się pod koniec II wojny światowej. John von Neumann był tym, który pokazał, jak obchodzić się ze sterowaniem maszyn, wprowadzając pierwsze formy programów.

Do 1957 r. firmy takie jak IBM i Remington Rand wytwarzały pierwszą generację elektronicznych komputerów. FORTRAN stał się standardowym językiem wysokiego poziomu. Niektórzy logicy - jednak nie wszyscy - szybko pojęli, jakie niesie to konsekwencje. Na konferencji na Cornel University, Barkley Rosser mówił o związkach między maszyną Turinga a realnym komputerem; Church o logicznej syntezie obwodów elektrycznych dla sprzętu komputerowego; Abraham Robinson o dowodzeniu twierdzeń przez człowieka i przez maszynę. Spośród młodszych uczestników, Michael Rabin i Dana Scot mówili o automatach skończonych, a Martin Davis o zastosowaniu komputera "Johnniac" do procedury rozstrzygania dla arytmetyki liczb całkowitych z dodawaniem - procedury odkrytej przez Mojżesza Presburgera.

IBM i inne firmy zatrudniały wówczas wielu badaczy z wykształceniem matematycznym i logicznym. Wielka ich liczba zjawiła się na konferencji na Cornel. Było 15 wystąpień badaczy z IBM, wielu z nich pokazywało użyteczność programów typu FORTRAN dla rozwiązywania problemów, które mogły zainteresować logików. Było wśród nich wystąpienie George'a Collinsa o zastosowaniu na IBM 704 Tarskiego procedury rozstrzygania dla algebry liczb rzeczywistych. To powinno było zwrócić uwagę Tarskiego, ponieważ wskazywało na możliwe praktyczne zastosowanie jego procedury. Kilka lat temu profesor Feferman zapytał Collinsa o reakcję Tarskiego. Usłyszał - "Nie okazał żadnego uznania dla mojej pracy, ani wtedy, ani później. Byłem tym zdziwiony i zdezorientowany". Mimo że Tarski uznawał ważność problemu rozstrzygalności wielu teorii algebraicznych i sam systematycznie się nim zajmował, to nie przejawiał najmniejszego zainteresowania praktycznymi, obliczeniowymi zastosowaniami tych problemów, dla których znalazł procedury rozstrzygania.

Rozstrzygalność i prawda

Tarski podjął zagadnienie rozstrzygalności dla liczb rzeczywistych w połowie 1920 r. w związku z aksjomatyzacją geometrii w języku pierwszego rzędu. Problem zupełności tej aksjomatyzacji doprowadził go do jej interpretacji w teorii pierwszego rzędu liczb rzeczywistych. W późnych latach 20., kiedy prowadził ćwiczenia na seminarium profesora Łukasiewicza, na którym badano metodę eliminacji kwantyfikatorów, zasugerował Presburgerowi jako ćwiczenie znalezienie procedury eliminacji kwantyfikatorów w teorii liczb całkowitych z dodawaniem. W 1928 r. rozwiązanie było podstawą nadania Presburgerowi tytułu magistra. W tym czasie nie rozumiano jeszcze doniosłości tego wyniku.

Pracę nad eliminacją kwantyfikatorów w elementarnej teorii liczb rzeczywistych zakończył Tarski z sukcesem przed 1930 r. Wynik przygotowany do publikacji przed 1939 r. obok teorii prawdy uznawał za jedno ze swoich dwóch najważniejszych osiągnięć. W 1948 r. J. C. C. McKinsey, przyjaciel Tarskiego, pracował dla RAND Corporation. Profesor Feferman przypuszcza, że McKinsey zasugerował swoim przełożonym potencjalną wartość zastosowania procedury Tarskiego do komputerowych obliczeń optymalnych strategii w pewnych grach (implementacja wymagała uprzedniego pisemnego sformułowania szczegółów).

W celu komercyjnej reprodukcji treści Computerworld należy zakupić licencję. Skontaktuj się z naszym partnerem, YGS Group, pod adresem [email protected]

TOP 200