8299308021

Twierdzenie 1.18 oraz wniosek 1.19 wykluczają możliwość, że kiedyś, w wyniku rozwoju informatyki, programiści będą mogli wykrywać niebezpieczeństwo ślepych pętli w programach za pomocą innych programów; przynajmniej jeśli teza 1.15 jest prawdziwa. Jest to możliwe tylko dla bardzo „słabych” języków, w których nie da się wiele zaprogramować.

Ale to twierdzenie nie oznacza, że nigdy nie możemy wiedzieć, czy dany program się zatrzyma. Nie istnieje metoda ogólna, stosująca się do wszystkich programów, ale w konkretnym przypadku możemy umieć zbadać własności konkretnego programu¹. Twierdzenie 1.18 nie wyklucza też istnienia programu, który zawsze prawidłowo orzeka o zatrzymywaniu się innych programów, ale z rzadka poddaje się i mówi „nie wiem”.

Każda nauka powinna znać swoje możliwości i ograniczenia. Twierdzenie 1.18 ma poważne konsekwencje w ustalaniu granic informatyki. Z nierozstrzygalności własności stopu dla maszyn Turinga wyprowadza się bardzo wiele innych twierdzeń o nierozstrzygalności. Nierozstrzygalne są między innymi

•    uniwersalny problem stopu — czy dany program zatrzymuje się dla wszystkich danych;

•    problem równoważności programów — czy dwa dane programy dają te same wyniki na każdych danych;

•    problem Rice’a — czy funkcja obliczana przez dany program ma daną własność (dla każdej „sensownej” nietrywialnej własności).

Twierdzenie 1.18 ma bardzo bliski związek ze słynnym twierdzeniem Godła o niezupełno-ści aksjomatyzacji arytmetyki. Oba twierdzenia są negatywne, czyli stwierdzają niemożność zrobienia czegoś. I dla dowodu obu stosuje się t.zw. rozumowanie przekątniowe, które trochę przypomina wyciąganie siebie samego za włosy z bagna. Nietrudno jest wykazać równoważność obu twierdzeń.

1.2.3 A-rachunek

W rozdz. 1.2.2.5 rozważaliśmy przede wszystkim rozstrzyganie problemów, chociaż zostało również wspomniane, że podobne rozważania stosują się do obliczania wartości. Modelem, specjalnie dostosowanym do funkcji obliczalnych (rekurencyjnych), jest t.zw. A-rachunek. Został on zaproponowany w latach 1930. przez Alonzo Churcha w ramach badań nad podstawami matematyki.

1.2.3.1 Określenia i konwersje

A-rachunek operuje na wyrażeniach postaci Xx.e. Takie wyrażenie oznacza, nieformalnie mówiąc, funkcję, która dla argumentu x daje wynik e — oczywiście w e może (ale nie musi) występować zmienna x. Np. \x.x • x oznacza funkcję podnoszącą swój argument do kwadratu.

Występujący na początku wyrażenia symbol A jest operatorem wiążącym zmienne, takim jak np. kwantyfikatory. To oznacza, że zmienna, występująca bezpośrednio za symbolem A, nie jest widoczna z zewnątrz wyrażenia i może bez zmiany jego znaczenia zostać zastąpiona inną zmienną²; np. wyrażenia \x.x-x i Ay.y-y oznaczają tą samą funkcję. Taka zmienna

14

1

Więcej o dowodzeniu stopu konkretnych programów będzie w rozdz. I.6.2.2.

2

Taką zmianę nazwy zmiennej, t.zw. a-konwersję, należy wykonywać ostrożnie.