Dowody z komputera

Podstawowe zasady konstrukcji i działania każdego komputera cyfrowego wynikają z matematycznej koncepcji maszyny Turinga. Są wynikiem dyskusji, jakie matematycy i logicy prowadzili nad problemem efektywnej metody obliczania, czyli stosowania algorytmu do rozwiązywania problemów obliczeniowych. Z tego zrodziła się informatyka i przemysł komputerowy. Sukcesy maszyn liczących mają coraz częściej zwrotne zastosowanie w czystej matematyce; informatyka zdaje się spłacać dług wobec swej szacownej i starszej siostry. Wzajemne powiązania dają okazję do ciekawych spostrzeżeń.

Podstawowe zasady konstrukcji i działania każdego komputera cyfrowego wynikają z matematycznej koncepcji maszyny Turinga. Są wynikiem dyskusji, jakie matematycy i logicy prowadzili nad problemem efektywnej metody obliczania, czyli stosowania algorytmu do rozwiązywania problemów obliczeniowych. Z tego zrodziła się informatyka i przemysł komputerowy. Sukcesy maszyn liczących mają coraz częściej zwrotne zastosowanie w czystej matematyce; informatyka zdaje się spłacać dług wobec swej szacownej i starszej siostry. Wzajemne powiązania dają okazję do ciekawych spostrzeżeń.

Szachy, podobnie jak warcaby czy inne gry i łamigłówki umysłowe doskonale nadają się do zmechanizowania, gdyż zbudowano je na bazie skończonego zbioru jednoznacznych reguł i prostych stanów początkowych. Choć liczba kombinacji dla dowolnej sytuacji wyjściowej jest zasadniczo duża, niemniej obliczalna.

W przypadku szachów dla każdej pozycji istnieje blisko 30 dopuszczalnych pozycji, co przy rozpatrywaniu tylko dwóch ruchów do przodu daje konieczność prześledzenia około 800 tys. kombinacji.

Zasługi dla programowania maszyn do gry w szachy ma ojciec sztucznej inteligencji - Alan Turing, który pod koniec życia poświęcił się badaniom nad "zastosowaniem komputerów cyfrowych do gier", jak głosił tytuł napisanego przez niego i współpracowników cyklu artykułów. Trudno ocenić wartość tych prac, gdyż sam Turing nie napisał żadnego podręcznika o zasadach programowania w tej dziedzinie. Jego program szachowy, napisany w 1951 roku do spółki z przyjacielem Champernownem (nazwany Turochampem) był mało skuteczny, gdyż stosował strategię największego zysku w planowaniu posunięć, co nie sprawdzało się w grze ze słabymi szachistami. Turing jest raczej znany z niekonwencjonalnego rozgrywania partii szachów ze swoim przyjacielem. Polegało to na zyskiwaniu dodatkowego ruchu, jeśli... zdążyło się obiec dom (Turing był wytrawnym maratończykiem), zanim przeciwnik wykonał swój ruch.

Dzieła programowania i budowy maszyn cyfrowych do gry w szachy (także warcaby czy w Go) podjęli się na szeroką skalę dopiero amerykańscy programiści ze środowisk uniwersyteckich i ośrodków komputerowych. Najgłośniejszym i jednym z pierwszych był program napisany przez A. Newella, J. C. Shawa i H. Simona, pionierów badań nad sztuczną inteligencją - nazwany NSS, który na poczciwym JOHNNIAC-u w 1958 roku nawiązał w miarę równorzędną rywalizację z przeciętnymi jednak szachistami. Wspólne wysiłki programistów i takich mistrzów szachowych, jak Botwinnik doprowadziły do wieloletnich zmagań komputera z szachistami o prym w tej najbardziej inteligentnej grze. Ostatnie potyczki Deep Blue z Kasparowem to właściwie nie koniec tych zmagań, lecz nowy ich etap (ale to już oddzielna opowieść).

Rozwiązywacz ogólnych problemów

Równolegle do prac nad programami szachowymi trwały prace nad programami przeznaczonymi do dowodzenia twierdzeń matematycznych i logicznych. Wysiłki w projektowaniu maszyny cyfrowej, która podałaby poprawny dowód najbardziej złożonego twierdzenia matematycznego nie mają tylko prestiżowego czy spektakularnego znaczenia, jak zmagania maszyn z mistrzami szachowymi. Idzie tu o rzeczywisty postęp w matematyce, rozwiązanie starych zagadnień, a także eksperymentalne ich sprawdzenie. W istocie rzeczy komputery wprzęgnięte do procedury dowodzenia uczyniły dzisiaj z matematyki - ku zaskoczeniu wielu matematyków - dyscyplinę w jakiejś części eksperymentalną.

Wszystko zaczęło się od prób konstrukcji uniwersalnej maszyny cyfrowej do rozwiązywania wszelkich ogólnych problemów, w tym dowodzenia twierdzeń matematycznych jako najbardziej inteligentnej czynności. Pierwsze prace konstrukcyjne i programistyczne podjęte w połowie lat pięćdziesiątych w USA (jako sztandarowy program sztucznej inteligencji) wyrastały z ogólnej idei sformułowanej jeszcze z początkiem stulecia. Zakładano w niej, że rozwiązywanie wszelkich problemów, tak przez człowieka, jak i przez maszyny, jest przekształcaniem wyrażeń o dowolnym znaczeniu zgodnie z regułami logiki symbolicznej. Czynność tę rozpatruje się z dwóch punktów widzenia - informatycznego, gdy dowolne wyrażenie (słowo języka naturalnego, symbol czy znak) zakodowane w systemie binarnym zostaje przetworzone w sposób zgodny z danym językiem programowania, oraz - logicznego, gdy jedno z wyrażeń traktuje się jako przesłanki, a inne jako wnioski wyciągane z nich według logicznych reguł wnioskowania indukcyjnego i dedukcyjnego. W każdym przypadku przekształcanie wyrażeń oznacza przeprowadzanie dowodu - uszeregowanie ciągu wyrażeń tak, aby na początku były przesłanki, w trakcie dołączane były aksjomaty i reguły, a na końcu pojawiło się twierdzenie w postaci wniosku. Z formalnego punktu widzenia zadanie (dowód) jest do wykonania, gdy istnieje dla niego algorytm - procedura przejścia (obliczenia) w skończonej liczbie kroków między tymi wyrażeniami. Jak jednak wiadomo z rewolucyjnych ustaleń A. Churcha, Turinga, a wcześniej K. G?dla, nie ma uniwersalnego algorytmu, który pozwoliłby dowieść, że dane zadanie ma swoje rozwiązanie (dowód).

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

TOP 200