Problem z zatrzymaniem - Halting problem

W teorii obliczalności The zatrzymanie problemem jest problem określenia, z opisu dowolnego programu komputerowego i wejście, czy program zakończy bieg, czy nadal działać wiecznie. Alan Turing udowodnił w 1936 roku, że nie może istnieć ogólny algorytm do rozwiązania problemu zatrzymania dla wszystkich możliwych par program-wejście.

W przypadku każdego programu f, który może określić, czy programy się zatrzymają, „patologiczny” program g , wywołany z pewnym wejściem, może przekazać swoje własne źródło i dane wejściowe do f, a następnie wykonać dokładnie odwrotność tego, co f przewiduje, że zrobi g . Nie może istnieć żadne f , które obsługuje ten przypadek. Kluczową częścią dowodu jest matematyczna definicja komputera i programu, znana jako maszyna Turinga ; problem zatrzymania jest nierozstrzygnięty w przypadku maszyn Turinga. Jest to jeden z pierwszych przypadków problemów decyzyjnychokazał się nierozwiązywalny. Dowód ten jest istotny dla praktycznych wysiłków obliczeniowych, definiując klasę aplikacji, których żaden wynalazek programistyczny nie jest w stanie wykonać idealnie.

Jack Copeland (2004) przypisuje wprowadzenie terminu problem zatrzymania pracy Martina Davisa w latach 50. XX wieku.

Tło

Problem zatrzymania jest problemem decyzyjnym dotyczącym właściwości programów komputerowych na ustalonym modelu obliczeń z pełnym Turingiem, tj. wszystkich programów, które można napisać w danym języku programowania, który jest wystarczająco ogólny, aby odpowiadał maszynie Turinga. Problem polega na określeniu, biorąc pod uwagę program i dane wejściowe do programu, czy program ostatecznie zatrzyma się po uruchomieniu z tymi danymi wejściowymi. W tej abstrakcyjnej strukturze nie ma ograniczeń dotyczących zasobów dotyczących ilości pamięci lub czasu wymaganego do wykonania programu; może to potrwać dowolnie długo i wykorzystać dowolną ilość miejsca do przechowywania przed zatrzymaniem. Pytanie brzmi po prostu, czy dany program kiedykolwiek zatrzyma się na określonym wejściu.

Na przykład w pseudokodzie program

while (true) continue

nie zatrzymuje się; raczej trwa w nieskończoność w nieskończonej pętli . Z drugiej strony program

print "Hello, world!"

zatrzymuje się.

Podczas gdy decyzja, czy te programy się zatrzymają, jest prosta, bardziej złożone programy okazują się problematyczne. Jednym ze sposobów rozwiązania problemu może być uruchomienie programu na pewną liczbę kroków i sprawdzenie, czy się zatrzyma. Ale jeśli program się nie zatrzyma, nie wiadomo, czy w końcu zostanie zatrzymany, czy będzie działał w nieskończoność. Turing udowodnił, że nie istnieje algorytm, który zawsze poprawnie decyduje, czy dla danego dowolnego programu i wejścia program zatrzymuje się po uruchomieniu z tym wejściem. Istotą dowodu Turinga jest to, że każdy taki algorytm można sprawić, by zaprzeczał sam sobie i dlatego nie może być poprawny.

Konsekwencje programowania

Niektóre nieskończone pętle mogą być całkiem przydatne. Na przykład pętle zdarzeń są zwykle kodowane jako pętle nieskończone. Jednak większość podprogramów ma na celu zakończenie (zatrzymanie). W szczególności w przypadku twardych obliczeń czasu rzeczywistego programiści próbują pisać podprogramy, które nie tylko mają gwarancję zakończenia (zatrzymania), ale także mają gwarancję, że zakończą się przed określonym terminem.

Czasami programiści ci używają języka programowania ogólnego przeznaczenia (uzupełniającego Turinga), ale próbują pisać w ograniczonym stylu — takim jak MISRA C lub SPARK — co ułatwia udowodnienie, że wynikowe podprogramy kończą się przed wyznaczonym terminem.

Innym razem programiści ci stosują zasadę najmniejszej mocy — celowo używają języka komputerowego, który nie jest w pełni kompletny pod względem Turinga. Często są to języki, które gwarantują zakończenie wszystkich podprogramów, takie jak Coq .

Typowe pułapki

Trudność w problemie zatrzymania polega na tym, że procedura decyzyjna musi działać dla wszystkich programów i danych wejściowych. Poszczególny program albo zatrzymuje się na danym wejściu, albo nie zatrzymuje się. Rozważ jeden algorytm, który zawsze odpowiada „zatrzymuje się” i inny, który zawsze odpowiada „nie zatrzymuje się”. W przypadku dowolnego konkretnego programu i danych wejściowych jeden z tych dwóch algorytmów odpowiada poprawnie, chociaż nikt nie może wiedzieć, który z nich. Jednak żaden algorytm ogólnie nie rozwiązuje problemu zatrzymania.

Istnieją programy ( interpretery ), które symulują wykonanie dowolnego kodu źródłowego, który im podano. Takie programy mogą zademonstrować, że program zatrzymuje się w takim przypadku: sam interpreter ostatecznie zatrzyma swoją symulację, co pokazuje, że oryginalny program się zatrzymał. Jednak interpreter nie zatrzyma się, jeśli jego program wejściowy nie zatrzyma się, więc takie podejście nie może rozwiązać problemu zatrzymania, jak stwierdzono; nie odpowiada "nie zatrzymuje się" w przypadku programów, które się nie zatrzymują.

Problem zatrzymania jest teoretycznie rozstrzygalny dla automatów liniowo ograniczonych (LBA) lub maszyn deterministycznych ze skończoną pamięcią. Maszyna ze skończoną pamięcią ma skończoną liczbę konfiguracji, a zatem każdy deterministyczny program na niej musi w końcu zatrzymać lub powtórzyć poprzednią konfigurację:

... każda maszyna skończona, pozostawiona całkowicie samej sobie, w końcu popadnie w idealnie okresowy, powtarzalny wzór . Czas trwania tego powtarzającego się wzorca nie może przekroczyć liczby stanów wewnętrznych maszyny... (kursywa w oryginale, Minsky 1967, s. 24)

Minsky zauważa jednak, że komputer z milionem małych części, każda z dwoma stanami, miałby co najmniej 2 ^{000 000} możliwych stanów:

Jest to jedynka, po której następuje około trzystu tysięcy zer… Nawet gdyby taka maszyna miała działać na częstotliwościach promieni kosmicznych, eony ewolucji galaktycznej byłyby niczym w porównaniu z czasem podróży przez taki cykl ( Minsky 1967 s. 25):

Minsky stwierdza, że ​​chociaż maszyna może być skończona, a automaty skończone „mają szereg teoretycznych ograniczeń”:

... zaangażowane wielkości powinny prowadzić do podejrzeń, że twierdzenia i argumenty oparte głównie na samej skończoności diagramu stanów mogą nie mieć dużego znaczenia. (Minsky s. 25)

Można również automatycznie zdecydować, czy niedeterministyczna maszyna ze skończoną pamięcią zatrzyma się na żadnej, niektórych lub wszystkich możliwych sekwencjach decyzji niedeterministycznych, wyliczając stany po każdej możliwej decyzji.

Historia

Problem zatrzymania jest historycznie ważny, ponieważ był to jeden z pierwszych problemów, które okazały się nierozstrzygnięte . (Dowód Turinga trafił do druku w maju 1936, podczas gdy dowód Alonzo Churcha o nierozstrzygalności problemu w rachunku lambda został już opublikowany w kwietniu 1936 [Church, 1936].) Następnie opisano wiele innych nierozstrzygalnych problemów.

Oś czasu

• 1900: David Hilbert stawia swoje "23 pytania" (obecnie znane jako problemy Hilberta ) na Drugim Międzynarodowym Kongresie Matematyków w Paryżu. „Spośród nich drugim było udowodnienie spójności„ aksjomatów Peano ”, od których, jak wykazał, zależała rygoryzm matematyki”. (Hodges s. 83, komentarz Davisa w Davis, 1965, s. 108)
• 1920–1921: Emil Post bada problem zatrzymywania się systemów znaczników , traktując go jako kandydata do nierozwiązywalności. ( Całkowicie nierozwiązywalne problemy i stosunkowo nierozstrzygalne propozycje – relacja z antycypacji , w Davis, 1965, s. 340–433). Jej nierozwiązywalność ustalił dopiero znacznie później Marvin Minsky (1967).
• 1928: Hilbert przepracowuje swój „Drugi problem” na Międzynarodowym Kongresie w Bolonii. (Reid s. 188–189) Hodges twierdzi, że zadał trzy pytania: np. #1: Czy matematyka była kompletna ? #2: Czy matematyka była spójna ? #3: Czy matematyka była rozstrzygalna ? (Hodges s. 91). Trzecie pytanie znane jest jako Entscheidungsproblem (Problem Decyzji). (Hodges s. 91, Penrose s. 34)
• 1930: Kurt Gödel ogłasza dowód jako odpowiedź na pierwsze dwa pytania Hilberta z 1928 r. [por. 198]. „Na początku [Hilbert] był tylko zły i sfrustrowany, ale potem zaczął próbować konstruktywnie radzić sobie z problemem… Sam Gödel czuł – i wyraził tę myśl w swoim artykule – że jego praca nie jest sprzeczna z formalistycznym punktem Hilberta widok” (Reid s. 199)
• 1931: Gödel publikuje „O formalnie nierozstrzygalnych propozycjach Principia Mathematica i systemów pokrewnych I” (przedruk w Davis, 1965, s. 5ff)
• 19 kwietnia 1935: Alonzo Church publikuje „An Unsolvable Problem of Elementary Number Theory”, który proponuje, że intuicyjne pojęcie efektywnie obliczalnej funkcji może być sformalizowane przez ogólne funkcje rekurencyjne lub równoważnie przez funkcje definiowalne lambda . Udowadnia, że ​​problem zatrzymania dla rachunku lambda (tj. czy dane wyrażenie lambda ma postać normalną ) nie jest efektywnie obliczalny.
• 1936: Church publikuje pierwszy dowód na to, że problem Entscheidungs jest nierozwiązywalny. ( A Note on the Entscheidungsproblem , przedrukowany w Davis, 1965, s. 110.)
• 7 października 1936: Otrzymuje pracę Emila Posta "Finite Combinatory Processes. Formula I". Post dodaje do swojego „procesu” instrukcję „(C) Stop”. Nazwał taki proces „typ 1… jeśli proces, który określa, kończy się dla każdego konkretnego problemu”. (Davis, 1965, s. 289nn)
• 1937: Artykuł Alana Turinga On Computable Numbers with a Application to the Entscheidungsproblem trafia do druku w styczniu 1937 (przedruk w Davis, 1965, s. 115). Dowód Turinga odchodzi od obliczania przez funkcje rekurencyjne i wprowadza pojęcie obliczania przez maszynę. Stephen Kleene (1952) określa to jako jeden z „pierwszych przykładów problemów decyzyjnych, które okazały się nierozwiązywalne”.
• 1939: J. Barkley Rosser zauważa zasadniczą równoważność „efektywnej metody” zdefiniowanej przez Gödla, Churcha i Turinga (Rosser in Davis, 1965, s. 223, „Nieformalne przedstawienie dowodów twierdzenia Gödla i twierdzenia Churcha”)
• 1943: W artykule Stephen Kleene stwierdza, że ​​„Ustanawiając kompletną teorię algorytmiczną, to co robimy, to opisujemy procedurę… która to procedura koniecznie się kończy i w taki sposób, że z wyniku możemy odczytać definitywną odpowiedź:” Tak 'lub 'Nie' na pytanie 'Czy wartość predykatu jest prawdziwa?'."
• 1952: Kleene (1952) Rozdział XIII („Funkcje obliczalne”) zawiera omówienie nierozwiązywalności problemu zatrzymania maszyn Turinga i przeformułowuje go w kategoriach maszyn, które „w końcu zatrzymują się”, tj. zatrzymują się: „... nie ma algorytm decydujący o tym, czy dana maszyna, uruchomiona z dowolnej sytuacji, w końcu się zatrzyma ." (Kleene (1952) s. 382)
• 1952: " Martin Davis uważa za prawdopodobne, że po raz pierwszy użył terminu 'zatrzymanie problemu' w serii wykładów, które wygłosił w Laboratorium Systemów Sterowania na Uniwersytecie Illinois w 1952 roku (list Davisa do Copelanda, 12 grudnia 2001). " (Przypis 61 w Copeland (2004) s. 40ff)

Formalizowanie

W swoim oryginalnym dowodzie Turing sformalizował pojęcie algorytmu , wprowadzając maszyny Turinga . Jednak wynik nie jest dla nich w żaden sposób specyficzny; odnosi się to w równym stopniu do każdego innego modelu obliczeń, który jest równoważny pod względem mocy obliczeniowej z maszynami Turinga, takimi jak algorytmy Markowa , rachunek Lambda , systemy Post , maszyny rejestrujące lub systemy znaczników .

Co ważne, formalizacja umożliwia proste mapowanie algorytmów na pewien typ danych , na którym algorytm może operować. Na przykład, jeśli formalizm pozwala algorytmom na definiowanie funkcji na ciągach znaków (takich jak maszyny Turinga), to powinno istnieć mapowanie tych algorytmów na łańcuchy, a jeśli formalizm pozwala algorytmom na definiowanie funkcji na liczbach naturalnych (takich jak funkcje obliczalne ) być mapowaniem algorytmów na liczby naturalne. Mapowanie do łańcuchów jest zwykle najprostsze, ale łańcuchy w alfabecie z n znakami można również mapować na liczby, interpretując je jako liczby w n- argumentowym systemie liczbowym .

Reprezentacja jako zbiór

Konwencjonalna reprezentacja problemów decyzyjnych to zbiór obiektów posiadających daną właściwość. Zatrzymanie zestaw

K = {( i , x ) | program i zatrzymuje się po uruchomieniu na wejściu x }

reprezentuje problem zatrzymania.

Ten zestaw jest rekurencyjnie przeliczalny , co oznacza, że ​​istnieje obliczalna funkcja, która wyświetla wszystkie zawarte w niej pary ( i ,  x ). Jednak dopełnienie tego zbioru nie jest rekurencyjnie przeliczalne.

Istnieje wiele równoważnych sformułowań problemu zatrzymania; Takim sformułowaniem jest każdy zbiór, którego stopień Turinga jest równy stopniowi problemu zatrzymania. Przykłady takich zestawów obejmują:

• { ja | program i ostatecznie zatrzymuje się po uruchomieniu z wejściem 0}
• { ja | istnieje wejście x takie, że program i ostatecznie zatrzymuje się po uruchomieniu z wejściem x }.

Koncepcja dowodowa

Christopher Strachey przedstawił sprzeczny dowód na to, że problemu zatrzymania nie da się rozwiązać. Dowód przebiega następująco: Załóżmy, że istnieje całkowicie obliczalna funkcja halts(f), która zwraca prawdę, jeśli podprogram f zatrzymuje się (gdy jest uruchamiany bez danych wejściowych), aw przeciwnym razie zwraca fałsz. Rozważmy teraz następujący podprogram:

def g():
    if halts(g):
        loop_forever()

halts(g) musi zwracać prawdę lub fałsz, ponieważ przyjęto , że halts ma wartość total . Jeśli halts(g) zwróci prawdę, to g wywoła loop_forever i nigdy nie zatrzyma, co jest sprzecznością. Jeśli halts(g) zwróci false, to g zatrzyma się, ponieważ nie wywoła loop_forever ; to też jest sprzeczność. Ogólnie rzecz biorąc, g działa odwrotnie do tego, co hals mówi, że g powinno działać, więc halts(g) nie może zwrócić wartości logicznej, która jest zgodna z tym, czy g zatrzymuje się. Dlatego początkowe założenie, że stop jest funkcją całkowicie obliczalną, musi być fałszywe.

Szkic rygorystycznego dowodu

Powyższe pojęcie pokazuje ogólną metodę dowodu, ale obliczalna funkcja stops nie przyjmuje bezpośrednio podprogramu jako argumentu; zamiast tego pobiera kod źródłowy programu. Co więcej, definicja g jest autoreferencyjna . Rygorystyczny dowód dotyczy tych kwestii. Ogólnym celem jest pokazanie, że nie istnieje żadna całko- wicie obliczalna funkcja decydująca o tym, czy dowolny program i zatrzymuje się na dowolnym wejściu x ; oznacza to, że następująca funkcja h (od „zatrzymuje”) nie jest obliczalna (Penrose 1990, s. 57-63):

${\ Displaystyle h (i, x) = {\ zacząć {przypadki} 1 i {\ tekst {jeśli}} {\ tekst { program}} i {\ tekst { zatrzymuje się na wejściu}} x \ \ 0 i {\ tekst { inaczej.}}\end{przypadki}}}$

Tutaj program i odnosi się do i- tego programu w wyliczeniu wszystkich programów ustalonego kompletnego modelu obliczeń Turinga .

Dowód przebiega przez bezpośrednie ustalenie, że żadna całkowita obliczalna funkcja z dwoma argumentami nie może być wymaganą funkcją h . Podobnie jak w szkicu koncepcji, mając daną całkowitą obliczalną funkcję binarną f , następująca funkcja częściowa g jest również obliczana przez pewien program e :

${\ Displaystyle g (i) = {\ zacząć {przypadki} 0 i {\ tekst {jeśli}} f (i, ja) = 0, \ \ {\ tekst {niezdefiniowany}} i {\ tekst {w przeciwnym razie}} \ koniec{sprawy}}}$

Weryfikacja, czy g jest obliczalne, opiera się na następujących konstrukcjach (lub ich odpowiednikach):

• podprogramy obliczalne (program obliczający f jest podprogramem w programie e ),
• powielanie wartości (program e oblicza wejścia i , i dla f z wejścia i dla g ),
• rozgałęzienie warunkowe (program e wybiera między dwoma wynikami w zależności od wartości obliczanej dla f ( i , i )),
• nie dający określonego rezultatu (np. przez zapętlenie w nieskończoność),
• zwracając wartość 0.

Poniższy pseudokod ilustruje prosty sposób obliczania g :

procedure compute_g(i):
    if f(i, i) == 0 then
        return 0
    else
        loop forever

Ponieważ g jest częściowo obliczalne, musi istnieć program e, który oblicza g , przy założeniu, że model obliczeń jest kompletny według Turinga. Ten program jest jednym ze wszystkich programów, w których zdefiniowana jest funkcja zatrzymania h . Kolejny krok dowodu pokazuje, że h ( e , e ) nie będzie mieć takiej samej wartości jak f ( e , e ).

Z definicji g wynika, że ​​musi mieć miejsce dokładnie jeden z dwóch następujących przypadków:

• f ( e , e ) = 0 i tak g ( e ) = 0. W tym przypadku h ( e , e ) = 1 , ponieważ program e zatrzymuje się na wejściu e .
• f ( e , e ) ≠ 0 , więc g ( e ) jest niezdefiniowane. W tym przypadku h ( e , e ) = 0 , ponieważ program e nie zatrzymuje się na wejściu e .

W obu przypadkach f nie może być tą samą funkcją co h . Ponieważ f było arbitralną całkowitą funkcją obliczalną z dwoma argumentami, wszystkie takie funkcje muszą różnić się od h .

Dowód ten jest analogiczny do argumentu przekątnego Cantora . Można wizualizować dwuwymiarową tablicę z jedną kolumną i jednym wierszem dla każdej liczby naturalnej, jak wskazano w powyższej tabeli. Wartość f ( i , j ) jest umieszczona w kolumnie i , wierszu j . Ponieważ zakłada się, że f jest funkcją całkowicie obliczalną, każdy element tablicy można obliczyć za pomocą f . Konstrukcję funkcji g można zwizualizować za pomocą głównej przekątnej tej tablicy. Jeśli tablica ma 0 na pozycji ( i , i ), to g ( i ) wynosi 0. W przeciwnym razie g ( i ) jest niezdefiniowane. Sprzeczność wynika z faktu, że istnieje jakaś kolumna e tablicy odpowiadająca samemu g . Teraz załóżmy, że f było funkcją zatrzymania h , jeśli g ( e ) jest zdefiniowane ( g ( e ) = 0 w tym przypadku), g ( e ) zatrzymuje się, więc f ( e,e ) = 1. Ale g ( e ) = 0 tylko wtedy, gdy f ( e,e ) = 0, sprzeczne z f ( e,e ) = 1. Podobnie, jeśli g ( e ) nie jest zdefiniowane, wtedy funkcja zatrzymania f ( e,e ) = 0, co prowadzi do g ( e ) = 0 pod konstrukcją g . Przeczy to założeniu, że g ( e ) nie jest zdefiniowane. W obu przypadkach powstaje sprzeczność. Dlatego dowolna obliczalna funkcja f nie może być funkcją zatrzymującą h .

Teoria obliczalności

Typowym sposobem udowodnienia problem się nierozstrzygalny jest zmniejszenie go do powstrzymania problemu. Na przykład nie może istnieć ogólny algorytm decydujący o tym, czy dane zdanie o liczbach naturalnych jest prawdziwe czy fałszywe. Powodem tego jest to, że zdanie mówiące, że pewien program zatrzyma się przy określonym wejściu, może zostać przekształcone w równoważne zdanie o liczbach naturalnych. Gdyby algorytm mógł znaleźć prawdziwość każdego twierdzenia o liczbach naturalnych, to z pewnością mógłby znaleźć prawdziwość tego; ale to określiłoby, czy oryginalny program zostanie zatrzymany.

Twierdzenie Rice'a uogólnia twierdzenie, że problem zatrzymania jest nierozwiązywalny. Stwierdza, że ​​w przypadku jakiejkolwiek nietrywialnej właściwości nie istnieje ogólna procedura decyzyjna, która w przypadku wszystkich programów decyduje o tym, czy funkcja częściowa realizowana przez program wejściowy ma tę właściwość. (Funkcja częściowa to funkcja, która nie zawsze może dawać wynik, dlatego jest używana do modelowania programów, które mogą albo generować wyniki, albo nie zatrzymywać się.) Na przykład właściwość „zatrzymaj dla wejścia 0” jest nierozstrzygalna. Tutaj „nietrywialne” oznacza, że ​​zbiór funkcji częściowych, które spełniają tę właściwość, nie jest ani zbiorem pustym, ani zbiorem wszystkich funkcji częściowych. Na przykład, "zatrzymuje się lub nie zatrzymuje się na wejściu 0" jest wyraźnie prawdziwe dla wszystkich funkcji częściowych, więc jest to trywialna właściwość i może być określona przez algorytm, który po prostu zgłasza "prawdę". Również to twierdzenie dotyczy tylko właściwości funkcji częściowej zaimplementowanej przez program; Twierdzenie Rice'a nie dotyczy właściwości samego programu. Na przykład "zatrzymaj przy wejściu 0 w ciągu 100 kroków" nie jest właściwością funkcji częściowej, która jest zaimplementowana przez program — jest właściwością programu realizującego funkcję częściową i jest bardzo rozstrzygalna.

Gregory Chaitin zdefiniował prawdopodobieństwo zakończenia pracy, reprezentowane przez symbol Ω , rodzaj liczby rzeczywistej, o której nieformalnie mówi się, że reprezentuje prawdopodobieństwo zatrzymania się losowo utworzonego programu. Liczby te mają ten sam stopień Turinga, co problem zatrzymania. Jest to liczba normalna i transcendentalna, którą można zdefiniować, ale nie można jej całkowicie obliczyć . Oznacza to, że można udowodnić, że nie istnieje algorytm produkujący cyfry Ω, chociaż kilka pierwszych cyfr można obliczyć w prostych przypadkach.

Podczas gdy dowód Turinga pokazuje, że nie może istnieć ogólna metoda lub algorytm do określenia, czy algorytmy zatrzymają się, poszczególne przypadki tego problemu mogą być bardzo podatne na atak. Mając konkretny algorytm, można często wykazać, że musi się on zatrzymać dla każdego wejścia, i faktycznie informatycy często robią to właśnie jako część dowodu poprawności . Ale każdy dowód musi być opracowany specjalnie dla danego algorytmu; nie ma mechanicznego, ogólnego sposobu ustalenia, czy algorytmy na maszynie Turinga zatrzymują się. Istnieją jednak pewne metody heurystyczne, które można wykorzystać w sposób zautomatyzowany do próby skonstruowania dowodu, co często kończy się powodzeniem w typowych programach. Ta dziedzina badań nazywana jest automatyczną analizą terminacji .

Ponieważ negatywna odpowiedź na problem zatrzymania wskazuje, że istnieją problemy, których nie może rozwiązać maszyna Turinga, teza Churcha-Turinga ogranicza to, co może osiągnąć każda maszyna, która wdraża skuteczne metody . Jednak nie wszystkie maszyny możliwe do wyobrażenia ludzkiej wyobraźni podlegają tezie Kościoła-Turinga (np. maszyny wyroczni ). Pytaniem otwartym jest, czy mogą istnieć rzeczywiste deterministyczne procesy fizyczne, które na dłuższą metę wymykają się symulacji przez maszynę Turinga, a w szczególności, czy jakikolwiek taki hipotetyczny proces można z pożytkiem wykorzystać w postaci maszyny liczącej ( hiperkomputer ). które mogłyby rozwiązać między innymi problem zatrzymania maszyny Turinga. Pozostaje również otwarte pytanie, czy jakieś takie nieznane procesy fizyczne są zaangażowane w pracę ludzkiego mózgu i czy ludzie mogą rozwiązać problem zatrzymania (Copeland 2004, s. 15).

Twierdzenia o niezupełności Gödla

Koncepcje podniesione przez twierdzenia o niezupełności Gödla są bardzo podobne do tych podniesionych przez problem zatrzymania, a dowody są dość podobne. W rzeczywistości słabsza forma Pierwszego Twierdzenia o Niezupełności jest łatwą konsekwencją nierozstrzygalności problemu zatrzymania. Ta słabsza forma różni się od standardowego twierdzenia o niezupełności twierdzeniem, że aksjomatyzacja liczb naturalnych, która jest zarówno pełna, jak i poprawna, jest niemożliwa. Część „dźwiękowa” to osłabienie: oznacza to, że wymagamy, aby dany system aksjomatyczny dowodził tylko prawdziwych twierdzeń o liczbach naturalnych. Ponieważ solidność implikuje spójność , ta słabsza forma może być postrzegana jako następstwo formy silnej. Należy zauważyć, że twierdzenie standardowej postaci Pierwszego Twierdzenia o Niezupełności Gödla jest zupełnie nie związane z wartością prawdziwości twierdzenia, a dotyczy jedynie kwestii, czy można je znaleźć za pomocą dowodu matematycznego .

Słabszą postać twierdzenia można wykazać z nierozstrzygalności problemu zatrzymania w następujący sposób. Załóżmy, że mamy solidną (a więc spójną) i pełną aksjomatyzację wszystkich prawdziwych zdań logicznych pierwszego rzędu o liczbach naturalnych . Następnie możemy zbudować algorytm, który wylicza wszystkie te stwierdzenia. Oznacza to, że istnieje algorytm N ( n ), który przy danej liczbie naturalnej n oblicza prawdziwe zdanie logiki pierwszego rzędu dotyczące liczb naturalnych, i że dla wszystkich zdań prawdziwych istnieje co najmniej jedno n takie, że N ( n ) daje to stwierdzenie. Załóżmy teraz, że chcemy, aby zdecydować, czy algorytm z reprezentacją ciągu postojów na wejściu í . Wiemy, że to zdanie można wyrazić za pomocą zdania logiki pierwszego rzędu, powiedzmy H ( a , i ). Od aksjomatyzacji zakończeniu wynika, że gdy istnieją n taki sposób, że N ( n ) = H ( , I ), lub nie jest N ' , tak że N ( n ) = Ź H ( , I ). Jeśli więc będziemy iterować przez wszystkie n, aż znajdziemy H ( a , i ) lub jego negację, zawsze zatrzymamy się, a ponadto odpowiedź, którą nam udzieli, będzie prawdziwa (przez rozsądek). Oznacza to, że daje nam to algorytm do rozstrzygania problemu zatrzymania. Ponieważ wiemy, że taki algorytm nie może istnieć, wynika z tego, że założenie, że istnieje spójna i pełna aksjomatyzacja wszystkich prawdziwych zdań logicznych pierwszego rzędu o liczbach naturalnych, musi być fałszywe.

Uogólnienie

Wiele wariantów problemu zatrzymania można znaleźć w podręcznikach obliczalności (np. Sipser 2006, Davis 1958, Minsky 1967, Hopcroft i Ullman 1979, Börger 1989). Zazwyczaj ich nierozstrzygalność wynika z redukcji standardowego problemu zatrzymania. Jednak niektóre z nich mają wyższy stopień nierozwiązywalności . Kolejne dwa przykłady są typowe.

Zatrzymanie na wszystkich wejściach

Uniwersalny zatrzymanie problemem , znany również (w teorii rekursji ) jako całości , jest problem określenia, czy dany program komputerowy będzie zatrzymać dla każdego wejścia (nazwa całość pochodzi od równoważnej pytanie, czy funkcja komputerowej jest całkowity ). Ten problem jest nie tylko nierozstrzygalny, jak problem zatrzymania, ale wysoce nierozstrzygalny. Pod względem hierarchii arytmetycznej jest ona kompletna (Börger 1989, s. 121). ${\ Displaystyle \ Pi _ {2} ^ {0}}$

Oznacza to w szczególności, że nie można tego rozstrzygnąć nawet z wyrocznią dla problemu zatrzymania.

Rozpoznawanie rozwiązań częściowych

Istnieje wiele programów, które dla niektórych danych wejściowych zwracają poprawną odpowiedź na problem zatrzymania, podczas gdy dla innych danych wejściowych w ogóle nie zwracają odpowiedzi. Jednak problem „dany program p , czy jest to rozwiązanie z częściowym zatrzymaniem” (w opisanym sensie) jest co najmniej tak samo trudny jak problem z zatrzymaniem. Aby to zobaczyć, załóżmy, że istnieje algorytm PHSR ("rozpoznawanie rozwiązania z częściowym zatrzymaniem"), aby to zrobić. Następnie można go użyć do rozwiązania problemu zatrzymania w następujący sposób: Aby sprawdzić, czy program wejściowy x zatrzymuje się na y , skonstruuj program p , który na wejściu ( x , y ) zgłasza prawdę i rozbiega się na wszystkich innych danych wejściowych. Następnie przetestuj p z PHSR.

Powyższy argument jest redukcją problemu zatrzymywania do rozpoznawania PHS, i w ten sam sposób trudniejsze problemy, takie jak zatrzymywanie na wszystkich wejściach, mogą być również zredukowane, co oznacza, że ​​rozpoznawanie PHS jest nie tylko nierozstrzygalne, ale wyższe w hierarchii arytmetycznej , w szczególności -kompletny. ${\ Displaystyle \ Pi _ {2} ^ {0}}$

Obliczanie stratne

Urządzenie stratny Turinga jest maszyna Turinga w którym część taśmy mogą nie deterministyczny zniknie. Problem zatrzymania jest rozstrzygalny dla stratnej maszyny Turinga, ale nieprymitywnej rekurencyjnej .

Maszyny Oracle

Maszyna z wyrocznią dla problemu zatrzymania może określić, czy poszczególne maszyny Turinga zatrzymają się na określonych wejściach, ale nie mogą ogólnie określić, czy maszyny równoważne sobie zatrzymają się.

Zobacz też

• Zajęty bóbr
• Twierdzenie o niezupełności Gödla
• Kontrowersje Brouwera-Hilberta
• Złożoność Kołmogorowa
• Problem P kontra NP
• Analiza terminacji
• Najgorszy czas wykonania

Uwagi

Bibliografia

• Turing, AM (1937). „Na liczbach obliczalnych, z aplikacją do Entscheidungsproblem” . Procedury Londyńskiego Towarzystwa Matematycznego . Wileya. s2-42 (1): 230-265. doi : 10.1112/plms/s2-42.1.230 . ISSN  0024-6115 ., Turing, AM (1938). „Na liczbach obliczalnych, z aplikacją do Entscheidungsproblem. Korekta” . Procedury Londyńskiego Towarzystwa Matematycznego . Wileya. s2-43 (1): 544-546. doi : 10.1112/plms/s2-43.6.544 . ISSN  0024-6115 .Jest to epokowa praca, w której Turing definiuje maszyny Turinga , formułuje problem zatrzymania i pokazuje, że jest on (podobnie jak problem Entscheidungs ) nie do rozwiązania.
• Sipser, Michael (2006). „Sekcja 4.2: Problem zatrzymania” . Wprowadzenie do teorii obliczeń (wyd. drugie). Wydawnictwo PWS. s.  173–182 . Numer ISBN 0-534-94728-X.
• c2:Problem z zatrzymaniem
• Kościół, Alonzo (1936). „Nierozwiązywalny problem elementarnej teorii liczb”. American Journal of Mathematics . 58 (2): 345-363. doi : 10.2307/2371045 . JSTOR  2371045 .
• B. Jack Copeland wyd. (2004), The Essential Turing: Seminal Writings in Computing, Logic, Philosophy, Artificial Intelligence, and Artificial Life plus The Secrets of Enigma , Clarendon Press (Oxford University Press), Oxford UK, ISBN  0-19-825079-7 .
• Davis, Marcin (1965). Nierozstrzygalne, podstawowe artykuły o nierozstrzygalnych twierdzeniach, nierozwiązywalnych problemach i funkcjach obliczalnych . Nowy Jork: Raven Press.. Artykuł Turinga zajmuje trzecie miejsce w tym tomie. Dokumenty obejmują prace Godela, Churcha, Rossera, Kleene i Posta.
• Davis, Martin (1958). Obliczalność i nierozwiązywalność . Nowy Jork: McGraw-Hill..
• Alfred North Whitehead i Bertrand Russell , Principia Mathematica do *56, Cambridge w University Press, 1962. Re: problem paradoksów, autorzy omawiają problem zbioru, który nie może być obiektem w żadnej ze swoich „funkcji determinujących”, w w szczególności „Wstęp, Rozdz. 1 s. 24 „...trudności, które pojawiają się w logice formalnej” oraz Rozdz. 2.I „Zasada błędnego koła” s. 37 i n. oraz Rozdział 2.VIII. „Sprzeczności s. 60 n.
• Martin Davis , „Co to jest obliczenie”, w Mathematics Today , Lynn Arthur Steen, Vintage Books (Random House), 1980. Cudowny mały artykuł, być może najlepszy, jaki kiedykolwiek napisano o maszynach Turinga dla niespecjalistów. Davis redukuje maszynę Turinga do znacznie prostszego modelu opartego na modelu obliczeń Posta. Omawia dowód Chaitina . Zawiera krótkie biografie Emila Posta , Julii Robinson .
• Marvin Minsky , Computation: Finite and Infinite Machines , Prentice-Hall, Inc., NJ, 1967. Patrz rozdział 8, Sekcja 8.2 „Nierozwiązywalność problemu zatrzymania”.
• Roger Penrose , The Emperor's New Mind: Concerning computers, Minds and the Laws of Physics , Oxford University Press , Oxford England, 1990 (z poprawkami). Por. Rozdział 2, „Algorytmy i maszyny Turinga”. Zbyt skomplikowana prezentacja (zobacz artykuł Davisa, aby uzyskać lepszy model), ale dokładna prezentacja maszyn Turinga i problemu zatrzymania oraz rachunku Lambda Church'a.
• John Hopcroft i Jeffrey Ullman , Wprowadzenie do teorii automatów, języki i obliczenia , Addison-Wesley, Reading Mass, 1979. Patrz rozdział 7 „Maszyny Turinga”. Książka skoncentrowana wokół maszynowej interpretacji „języków”, NP-kompletności itp.
• Andrew Hodges , Alan Turing: The Enigma , Simon and Schuster , Nowy Jork. Por. Rozdział „Duch Prawdy” poświęcony historii prowadzącej i omówieniu jego dowodu.
• Constance Reid , Hilbert , Copernicus: Springer-Verlag, New York, 1996 (pierwsze wydanie 1970). Fascynująca historia niemieckiej matematyki i fizyki od 1880 do 1930. Na jej łamach pojawiają się setki nazwisk znanych matematykom, fizykom i inżynierom. Być może zakłócony brakiem jawnych odniesień i nielicznymi przypisami: Reid twierdzi, że jej źródłami były liczne wywiady z tymi, którzy osobiście znali Hilberta, oraz listy i dokumenty Hilberta.
• Edward Beltrami , Co to jest losowość? Szansa i porządek w matematyce i życiu , Copernicus: Springer-Verlag, New York, 1999. Ładna, delikatna lektura dla niespecjalistów o skłonnościach matematycznych, twardsze rzeczy umieszcza na końcu. Ma w sobie model maszyny Turinga. Omawia wkład Chaitina .
• Moore, Cristopher ; Mertens, Stephan (2011), The Nature of Computation , Oxford University Press, ISBN 9780191620805
• Ernest Nagel i James R. Newman , Godel's Proof , New York University Press, 1958. Wspaniałe pisanie na bardzo trudny temat. Dla niespecjalistów o skłonnościach matematycznych. Omawia dowód Gentzena na stronach 96–97 i przypisach. Dodatki omawiają krótko Aksjomaty Peano , delikatnie wprowadzają czytelników w logikę formalną.
• Taylor Booth , Maszyny sekwencyjne i teoria automatów , Wiley, Nowy Jork, 1967. Zob. Rozdział 9, Maszyny Turinga. Trudna książka, przeznaczona dla inżynierów elektryków i specjalistów technicznych. Omawia rekurencję, rekurencję częściową w odniesieniu do maszyn Turinga, problem zatrzymania. Ma w sobie model maszyny Turinga . Odniesienia na końcu rozdziału 9 obejmują większość starszych książek (tj. 1952-1967, w tym autorów Martina Davisa, FC Hennie, H. Hermesa, SC Kleene, M. Minsky'ego, T. Rado) i różne artykuły techniczne. Patrz uwaga w sekcji Programy zajętych bobrów.
• Programy Busy Beaver są opisane w Scientific American, sierpień 1984, również marzec 1985 s. 23. Odniesienie w Booth przypisuje je Rado, T. (1962), O funkcjach nieobliczalnych, Bell Systems Tech. J. 41. Booth definiuje również problem pracowitego bobra Rado w problemach 3, 4, 5, 6 rozdziału 9, s. 396.
• David Bolter , Turing's Man: Western Culture in the Computer Age , The University of North Carolina Press, Chapel Hill, 1984. Dla czytelnika ogólnego. Może być datowany. Ma w sobie jeszcze jeden (bardzo prosty) model maszyny Turinga.
• Egona Börgera. „Obliczalność, złożoność, logika”. Holandia Północna, 1989.
• Stephen Kleene , Wprowadzenie do metamatematyki , North-Holland, 1952. Rozdział XIII („Funkcje obliczalne”) zawiera omówienie nierozwiązywalności problemu zatrzymania dla maszyn Turinga. W odejściu od terminologii Turinga dotyczącej maszyn niezatrzymujących się bez okręgu, Kleene odnosi się do maszyn, które „zatrzymują się”, tj. zatrzymują się.
• Sven Köhler, Christian Schindelhauer, Martin Ziegler, O przybliżaniu rzeczywistych problemów z zatrzymywaniem się , str.454-466 (2005) ISBN  3540281932 Springer Lecture Notes in Computer Science tom 3623: Undecidability of the Halting Problem oznacza, że ​​nie na wszystkie przypadki można poprawnie odpowiedzieć ; ale może "niektóre", "wiele" lub "większość" mogą? Z jednej strony ciągła odpowiedź „tak” będzie nieskończenie często poprawna, a nieskończenie często błędna. Aby pytanie było uzasadnione, rozważ gęstość przypadków, które można rozwiązać. Okazuje się, że zależy to w dużej mierze od rozważanego Systemu Programowania .
• Logiczne ograniczenia etyki maszyn, z konsekwencjami dla śmiercionośnej broni autonomicznej – artykuł omówiony w: Czy problem zatrzymania oznacza brak robotów moralnych?
• Nicholas J. Daras i Themistocles M. Rassias , Współczesna matematyka i analiza dyskretna: z aplikacjami w kryptografii, systemami informacyjnymi i modelowaniem Springer, 2018. ISBN  978-3319743240 . Rozdział 3 Sekcja 1 zawiera opis jakościowy problemu zatrzymania, dowód przez sprzeczność i pomocną graficzną reprezentację problemu zatrzymania.

Zewnętrzne linki

• Scooping the loop Snooper - poetycki dowód nierozstrzygalności problemu zatrzymania
• film animowany - animacja wyjaśniająca dowód nierozstrzygalności problemu zatrzymania
• 2-minutowy dowód drugiego najważniejszego twierdzenia drugiego tysiąclecia - dowód w zaledwie 13 wierszach