Dowód Turinga: Różnice pomiędzy wersjami
| [wersja przejrzana] | [wersja przejrzana] |
jęz. |
lin. |
||
| Linia 13: | Linia 13: | ||
==Dowód== |
==Dowód== |
||
Dowód, że Entscheidungsproblem nie ma rozwiązania (lemat 3), stanowi wniosek w pracy Turinga wynikający z dwóch wcześniejszych lematów. Pierwszy lemat ma bliski związek z [[problem stopu|problemem stopu]], drugi z [[twierdzenie Rice’a|twierdzeniem Rice’a]]. |
Dowód, że [[Entscheidungsproblem]] nie ma rozwiązania (lemat 3), stanowi wniosek w pracy Turinga wynikający z dwóch wcześniejszych lematów. Pierwszy lemat ma bliski związek z [[problem stopu|problemem stopu]], drugi z [[twierdzenie Rice’a|twierdzeniem Rice’a]]. |
||
'''Lemat 1''' mówi, że nie istnieje maszyna Turinga, zdolna rozstrzygnąć w skończonej liczbie kroków czy dowolna maszyna Turinga jest "circle-free" {{odn|Turing|1937|s=246}}. Dana maszyna jest "circle-free" jeżeli nie istnieje górne, skończone ograniczenie na liczbę symboli zerowych lub niezerowych, które generuje maszyna (np. maszyna, która kończy pracę nie jest "circle-free"){{odn|Turing|1937|s=233}}. |
'''Lemat 1''' mówi, że nie istnieje maszyna Turinga, zdolna rozstrzygnąć w skończonej liczbie kroków czy dowolna maszyna Turinga jest "circle-free" {{odn|Turing|1937|s=246}}. Dana maszyna jest "circle-free" jeżeli nie istnieje górne, skończone ograniczenie na liczbę symboli zerowych lub niezerowych, które generuje maszyna (np. maszyna, która kończy pracę nie jest "circle-free"){{odn|Turing|1937|s=233}}. |
||
Wersja z 04:41, 1 paź 2021
Dowód Turinga – dowód przedstawiony przez Alana Turinga w 1937 w pracy "On Computable Numbers, With an Application to the Entscheidungsproblem" pokazujący, że pewne ogólne klasy problemów są nierozstrzygalne, to znaczy nie istnieje uniwersalny algorytm rozwiązujący każdą instancje problemów z tych klas. W szczególności dowód daje negatywną odpowiedź na Entscheidungsproblem [1].
Entscheidungsproblem - tło historyczne
W 1928 David Hilbert przedstawił problem decyzyjny (Entscheidungsproblem) dotyczący teorii aksjomatycznych logiki pierwszego rzędu, który można wyrazić następująco: podać algorytm rozstrzygający w skończonej liczbie kroków czy dla danego zbioru aksjomatów NT logiki pierwszego rzędu, zdanie T jest prawdziwe (czy T jest prawdziwe w każdym modelu spełniającym aksjomaty NT). Na mocy udowodnionego rok później twierdzenia Gödla o zupełności tak postawiony problem jest równoważny pytaniu czy zdanie T może zostać dedukcyjnie wyprowadzone z aksjomatów NT (patrz: dedukcja naturalna, system Hilberta).
W 1931 Kurt Gödel pokazał, że system dowodzenia twierdzeń arytmetycznych sformalizowany w ramach Principia Mathematica nie jest zupełny i niesprzeczny. Dowód Gödla jest czysto logiczny i nie odnosi się do żadnej notacji obliczalności, w związku z tym nie implikuje bezpośrednio nierozstrzygalności w obrębie zdań systemów aksjomatycznych logiki pierwszego rzędu.
Formalnie, negatywna odpowiedź na Entscheidungsproblem pojawiła się wraz z pracą Alonzo Churcha'a w 1936 i niezależną od niej, opublikowaną rok później, wyżej wspomnianą pracą Alana Turinga. Church przedstawił dowód w ramach rozwijanego przez siebie formalizmu rachunku lambda. Turing posłużył się wprowadzoną przez siebie koncepcją maszyny Turinga. Formalizmy te, jak się okazało, są równoważne [1][2], jednak wersja dowodu przedstawiona przez Turinga zyskała większą popularność.
W 1970 roku Yuri Matiyasevich udowodnił silniejsze twierdzenie dotyczące równań diofantycznych, które m.in. implikuje wyniki Churcha i Turinga (patrz: dziesiąty problem Hilberta).
Dowód
Dowód, że Entscheidungsproblem nie ma rozwiązania (lemat 3), stanowi wniosek w pracy Turinga wynikający z dwóch wcześniejszych lematów. Pierwszy lemat ma bliski związek z problemem stopu, drugi z twierdzeniem Rice’a.
Lemat 1 mówi, że nie istnieje maszyna Turinga, zdolna rozstrzygnąć w skończonej liczbie kroków czy dowolna maszyna Turinga jest "circle-free" [3]. Dana maszyna jest "circle-free" jeżeli nie istnieje górne, skończone ograniczenie na liczbę symboli zerowych lub niezerowych, które generuje maszyna (np. maszyna, która kończy pracę nie jest "circle-free")[4].
Lemat 2 mówi, że nie istnieje maszyna Turinga, która jest w stanie rozstrzygnąć w skończonej liczbie kroków czy dana maszyna Turinga generuje kiedykolwiek określony symbol (np. symbol zerowy). Jeżeliby tak było, prowadziłoby to do sprzeczności z lematem 1[5].
Lemat 3 mówi, że odpowiednio dla każdej maszyny Turinga M można skonstruować formułę Un(M) i nie istnieje ogólny, mechaniczny proces (maszyna Turinga) rozstrzygający czy Un(M) jest dowodliwe. Jeżeliby tak było, prowadziłoby to do sprzeczności z lematem 2[6].
Turing napisał: "Warto zaznaczyć, że to ... różni się od dobrze znanych wyników Gödla. Gödel pokazał, że (w formalizmie Principia Mathematica) istnieją twierdzenia T takie, że ani T ani ~T nie jest dowodliwe. Ja ... pokazuję, że nie istnieje ogólna [mechaniczna] metoda, która pozwala sprawdzić czy dana formuła T jest dowodliwa..."[6].
Zobacz też
Przypisy
- ↑ a b Turing 1937 ↓, s. 231.
- ↑ Turing 1937 ↓, s. 263.
- ↑ Turing 1937 ↓, s. 246.
- ↑ Turing 1937 ↓, s. 233.
- ↑ Turing 1937 ↓, s. 248.
- ↑ a b Turing 1937 ↓, s. 259.
Bibliografia
- Alan Turing. On Computable Numbers, With an Application to the Entscheidungsproblem. „Proceedings of the London Mathematical Society”. 42 (1), s. 230–265, 1937. DOI: 10.1112/plms/s2-42.1.230.