Algorytm rozwiązywania „problemu zatrzymania” Turinga

„Alan Turing udowodnił w 1936 r., Że nie może istnieć ogólny algorytm rozwiązania problemu zatrzymania dla wszystkich możliwych par danych wejściowych programu”

Czy mogę znaleźć ogólny algorytm rozwiązania problemu zatrzymania dla niektórych możliwych par danych wejściowych programu?

Czy mogę znaleźć język programowania (lub języki), w którym dla każdego rodzaju programu w tym języku może on zdecydować, czy program się zakończy lub uruchomi na zawsze?

Czy mogę znaleźć ogólny algorytm rozwiązania problemu zatrzymania dla niektórych możliwych par danych wejściowych programu?

Tak, oczywiście. Na przykład możesz napisać algorytm, który zwraca „Tak, kończy się” dla każdego programu, który nie zawiera ani pętli, ani rekurencji, i „Nie, nie kończy się” dla każdego programu, który zawiera while(true)pętlę, która na pewno zostanie osiągnięta i nie zawiera instrukcja break i „Dunno” dla wszystkiego innego.

Czy mogę znaleźć język programowania (lub języki), w którym dla każdego rodzaju programu w tym języku może on zdecydować, czy program się zakończy lub uruchomi na zawsze?

Nie, jeśli ten język jest kompletny w Turingu, nie.

Istnieją jednak niekompletne języki Turinga, takie jak na przykład Coq , Agda lub Microsoft Dafny, dla których problem zatrzymania jest rozstrzygalny (i w rzeczywistości decydują o tym odpowiednie systemy typów, co czyni je kompletnymi językami (tzn. Program, który może nie zostać zakończony, nie będzie skompilować)).

Myślę, że wszystkie odpowiedzi tutaj całkowicie i całkowicie pomijają sens. Odpowiedź na pytanie brzmi: zakładając, że program ma się zatrzymać, wtedy tak, lepiej być w stanie pokazać, że się zatrzymał. Jeśli nie możesz pokazać, że łatwo się zatrzymuje, program należy uznać za bardzo źle napisany i jako taki odrzucony przez kontrolę jakości.

To, czy potrafisz napisać odpowiedni algorytm maszynowy, zależy od wejściowego języka programowania i tego, jak ambitny jesteś. Jest rozsądnym celem projektowym dla języka programowania, aby łatwo było udowodnić zakończenie.

Jeśli językiem jest C ++, prawdopodobnie nie możesz napisać tego narzędzia, w rzeczywistości jest mało prawdopodobne, abyś uruchomił parser, nie mówiąc już o udowodnieniu zakończenia. Aby uzyskać lepiej ustrukturyzowany język, powinieneś być w stanie wygenerować dowód lub przynajmniej zrobić to z pewnymi założeniami: w tym drugim przypadku narzędzie powinno wygenerować te założenia. Podobne podejście polegałoby na uwzględnieniu stwierdzeń zakończenia w języku i stosowaniu ich w złożonych sytuacjach, w których narzędzie ufa tym stwierdzeniom.

Najważniejsze jest to, że nikt nie zdaje sobie sprawy z tego, że dowód zatrzymania programu jest rzeczywiście możliwy, ponieważ (dobrzy) programiści zamierzający napisać takie programy zatrzymujące zawsze robią to umyślnie i z mentalnym obrazem, dlaczego kończą i działają poprawnie: taki kod jest celowo napisane tak, aby było jasne, że się zatrzymały i są poprawne, a jeśli rozsądny algorytm nie może tego udowodnić, być może z pewnymi wskazówkami, program powinien zostać odrzucony.

Chodzi o to, że programiści nie piszą dowolnych programów, więc teza twierdzenia o zatrzymaniu nie jest spełniona, a wniosek nie ma zastosowania.

doskonałe i (prawdopodobnie niezamierzenie głębokie) pytanie. istnieją programy wykrywające zatrzymanie, które mogą odnieść sukces przy ograniczonych zestawach danych wejściowych. jest to aktywny obszar badań. ma bardzo silne powiązania z (automatycznymi) obszarami dowodzenia twierdzeń.

jednak informatyka nie wydaje się mieć dokładnego terminu „programy”, które „czasami” odnoszą sukces. słowo „algorytm” jest zwykle zarezerwowane dla programów, które zawsze się zatrzymują.

koncepcja wydaje się wyraźnie różnić od algorytmów probabilistycznych, w których teoretycy CS twierdzą, że istnieje pewne znane lub obliczalne prawdopodobieństwo ich sukcesu.

istnieje termin semialgorytmy, który jest czasami używany, ale najwyraźniej jest synonimem rekurencyjnie wyliczalnego lub niekompatybilnego.

więc dla celów tutaj nazwijmy je quasial algorytmami . koncepcja jest inna niż rozstrzygalna vs nierozstrzygalna.

$A$$X$$B$$Y$$X \subset Y$$X$$Y$$B$$A$

w CS ta „hierarchia quasi-algorytmowa” wydaje się jak dotąd badana głównie nieformalnie.

pojawia się w badaniach zajętego bobra [1] i problemie PCP [2]. w rzeczywistości atak komputerowy oparty na DNA na PCP może być postrzegany jako quasi-algorytm. [3] i widać to w innych już odnotowanych obszarach, takich jak dowodzenie twierdzeń [4].

[1] Nowy tysiącletni atak na problem zajętego bobra

[2] Problem korespondencji w Tackling Posts autorstwa Zhao (v2?)

[3] Wykorzystanie DNA do rozwiązania problemu korespondencji związanej przez Kari i in

[4] potwierdzające zakończenie programu przez Cooka i in., Comm. ACM

(więc to jest naprawdę bardzo głębokie pytanie, które defn zasługuje na to, aby być na TCS.SE imho ... może ktoś może zadać to pytanie w taki sposób, aby pasowało i zostało)

Tak długo, jak długo dany język programowania jest wystarczająco złożony (tzn. Jeśli jest kompletny w Turingu), zawsze istnieją programy w języku, których żaden program nie może zakończyć.

Ponieważ wszystkie języki z wyjątkiem najbardziej prymitywnych są kompletne Turinga (wymaga to tylko zmiennych i warunków), można naprawdę zbudować bardzo małe języki zabawek, dla których można rozwiązać problem zatrzymania.

Edycja: W świetle komentarzy pozwól, że wyrażę się bardziej precyzyjnie: każdy język, który możesz zaprojektować, dla którego możesz rozwiązać problem zatrzymania, musiałby koniecznie być niekompletny. Wyklucza to każdy język, który zawiera odpowiedni zestaw podstawowych składników (np. „Zmienne, warunkowe i skoki” lub, jak mówi @ sepp2k, rodzajowy „while” -loop).

Najwyraźniej istnieje kilka praktycznych „prostych” języków takich jak ten (np. Rozwiązujące twierdzenia, takie jak Coq i Agda). Jeśli spełniają one twoje pojęcie „języka programowania”, możesz sprawdzić, czy spełniają one jakąś kompletność, czy też problem zatrzymania jest dla nich możliwy do rozwiązania.

$T$$T$

To jest dość trywialne. Jeśli weźmiemy połączenie dowolnego podzbioru ce zatrzymujących baz TM i dowolnego podzbioru ce nie zatrzymujących baz TM, wynikiem będzie zestaw baz, dla których problem zatrzymania jest rozstrzygalny (uruchom obie maszyny równolegle, jeśli pierwsza akceptuje TM zatrzymuje się, jeśli drugi akceptuje, maszyna się nie zatrzymuje). Nie doprowadzi to jednak do wielu interesujących języków.

$\mathsf{ALogTime}$$c$$M$

Tak, możesz, ale wątpię, czy to się przyda. Prawdopodobnie musiałbyś to zrobić, analizując przypadki, a wtedy będziesz w stanie szukać tylko najbardziej oczywistych przypadków. Na przykład możesz grep pliku dla kodu while(true){}. Jeśli plik ma ten kod, nigdy się nie skończy ^. Mówiąc bardziej ogólnie, można powiedzieć, że program bez pętli lub rekurencji zawsze kończy się i istnieje kilka przypadków, w których można zagwarantować, że program się zakończy lub nie, ale nawet dla programów średniej wielkości byłoby to bardzo trudne i w wielu przypadkach nie byłby w stanie udzielić odpowiedzi.

tl; dr: Tak, ale nie będziesz w stanie sprawić, by był on przydatny w przypadku najbardziej przydatnych programów.

^ Tak, technicznie rzecz biorąc, jeśli ten kod nie znajduje się na ścieżce kodu lub istnieją inne wątki, które wciąż mogą zostać zakończone, ale tutaj mam ogólny punkt.