Problem nierozstrzygalny
Z Wikipedii
Problem nierozstrzygalny - w teorii obliczeń - problem decyzyjny, dla którego nie istnieje algorytm, który po skończonej liczbie kroków jednoznacznie odpowie tak lub nie dla dowolnych danych wejściowych.
Turing w 1937 roku wykazał, że udzielenie odpowiedzi na pytanie, czy Maszyna Turinga o numerze n wykonując działania nad liczbą m zakończy kiedyś swoją pracę, czy też przewidziany dla niej algorytm będzie realizowany w nieskończoność, jest problemem nierozstrzygalnym.
Innym przykładem problemu nierozstrzygalnego jest tzw. zadanie Gödla o postaci 17 Gen r (generalizacja {kwantyfikator ogólny} formuły r względem zmiennej z numerem 17) Jest to zdanie posiadające tę własność, że ani ono ani jego negacja nie dają się formalnie dowieść. Zdanie nierozstrzygalne 17 gen r powstało w wyniku odwzorowania antynomii logicznej (zwanej antynomią Richarda) poprzez tak zwaną arytmetyzacją języka klasycznego rachunku zdań. Arytmetyzacja języka pozwala na odwzorowanie relacji logicznych jakie zachodzą między zdaniami w relacje arytmetyczne między liczbami stanowiącymi numery tych zdań. Dzięki temu zamiast o relacjach logicznych można mówić o relacjach arytmetycznych.
Istnienie zdania 17 gen r jest powodem nierozstrzygalności arytmetyki, uważanej do czasów Gödla za system rozstrzygalny, to znaczy taki, w którym albo da się dowieść dowolna formuła arytmetyczna albo negacja tej formuły. Inaczej mówiąc zbiór twierdzeń arytmetycznych jest nieobliczalny, co znaczy że nie można w skończonej ilości kroków rozstrzygnąć czy dany element tego zbioru, będący oczywiście twierdzeniem arytmetycznym, jest czy nie jest elementem zbioru twierdzeń.
Na przykład wspomniane zdanie 17 Gen r należy do zbioru twierdzeń arytmetycznych wtedy i tylko wtedy gdy do niego nie należy. Tymczasem zbiór dowodów twierdzeń arytmetycznych jest obliczalny, ponieważ w skończonej ilości kroków można rozstrzygnąć, czy dany ciąg napisów jest czy nie jest dowodem danego twierdzenia. Tak więc zbiór zdań prawdziwych nie pokrywa się ze zbiorem twierdzeń. Istnieją bowiem zdania prawdziwe, których nie da się dowieść. Jednym z nich jest właśnie zdanie 17Gen r. Z faktu nierozstrzygalności arytmetyki wynika z kolei niemożliwość udowodnienia jej niesprzeczności.
[edytuj] Nierozstrzygalność problemu stopu
Wyobraźmy sobie, że istnieje algorytm pobierający funkcję i argument, i rozstrzygający czy dany algorytm się zatrzyma dla danego argumentu. Zapytamy go więc czy zatrzyma się f dla argumentu g:
def f(g) { if (zatrzyma_się(f,g)) nieskończona_pętla() else return }
Jeśli stwierdzimy, że się zatrzyma to się nie zatrzyma, jeśli natomiast stwierdzimy, że się nie zatrzyma, to się zatrzyma.