Algorytm rozwiązywania „problemu zatrzymania” Turinga

23

„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?

— Kaveh
źródło

Podobne pytanie: stackoverflow.com/questions/8412741/...

3

CACM miał bardzo interesujący artykuł w maju: Zakończenie programu Proving

— Christoph Walesch

3

„ogólny algorytm [...] dla niektórych możliwych par danych wejściowych programu” - to prawie sprzeczne. Chyba chcesz się ograniczyć do nieskończonej podklasy wszystkich programów?

— Raphael

25

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ć)).

— sepp2k
źródło

1

Klasa funkcji prymitywno-rekurencyjnych jest dobrze znanym „językiem programowania”, dla którego problem zatrzymania jest trywialnie rozstrzygalny.

— Raphael

Istnieje kilka języków „ programowania funkcjonalnego ”, w których wszystkie programy mogą zostać zakończone.

— Anderson Green

3

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.

— Yttrill
źródło

4

Myślę, że to ty całkowicie i całkowicie przegapiłeś ten punkt. Pierwszy akapit odpowiedzi nie dotyczy pytania, ponieważ dotyczy algorytmów - a nie tego, czego człowiek może, a czego nie może udowodnić. Reszta odpowiedzi odpowiada na pierwszy akapit pytania, tj. Czy algorytm może udowodnić zakończenie dla niektórych programów. Wszystkie poprzednie odpowiedzi już brzmiały „tak”.

— sepp2k

3

Twoje twierdzenie, że można napisać algorytm, który może udowodnić zakończenie każdego dobrze napisanego programu w wystarczająco prostym języku Turinga, jest całkowicie fałszywe. Dla każdego możliwego algorytmu, który próbuje udowodnić zakończenie, istnieją problemy, w których każdy program, który rozwiązuje ten problem, nie może zostać zatrzymany przez ten algorytm. Więc jeśli nie mówisz, że każdy program rozwiązujący ten problem jest źle napisany z definicji (co byłoby absurdalne), to obala twój punkt widzenia.

— sepp2k

1

@Sam Jeśli ktoś zapyta mnie, czy jakiś kod się zatrzymuje, spojrzę na kod i spróbuję go rozgryźć. Ale nie jestem algorytmem. I tak, można napisać algorytm, który może sprawdzić, czy program zatrzymuje się dla wielu programów. Ale nie to powiedział Yttrill. Yttrill powiedział, że jest to możliwe dla wszystkich dobrze napisanych programów. I jak powiedziałem w poprzednim komentarzu, jest to po prostu fałsz, chyba że twierdzisz, że niektóre problemy mogą być rozwiązane tylko przez źle napisane programy (co znowu byłoby śmieszne).

— sepp2k

1

@Sam „wydaje mi się proste, że programy celowo napisane w celu zatrzymania można łatwo analizować pod kątem warunków zatrzymania” - jeśli tak, to dlaczego nie mamy takich narzędzi? To nie tak, że ludzie nie próbowali. (Jednym z winowajców jest przesłanianie metod: w czasie kompilacji nie znasz całego kodu, który zostanie wykonany.)

— Raphael

1

@Sam „jest tam nieskończona pętla” jest trudna do osiągnięcia, nawet w pętli w świecie rzeczywistym. Oczywiście nauczono mnie, jak znaleźć niezmienniki pętli, ale to nie znaczy, że mogę znaleźć (łatwo) w wielu przypadkach. O ile mi wiadomo, zgadnij i udowodnij, że obecnie jest złotym standardem. Ponownie, jeśli nie były algorytmy dość ogólne, chciałbym oczekiwać od nich być zawarte w głównych kompilacji lub IDE (co zrobić wykonać jakieś trywialne, składniowe kontrole). Czy możesz podać odniesienie do dość silnego algorytmu?

— Raphael

3

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)

— vzn
źródło

ps jako imponujący przykład tego, jak potężne mogą być quasialgorytmy, ACM stwierdza, że funkcja ackermanns może zostać zatrzymana przez quasialgorytm, ale jest większy niż (nieobliczalny) przez wszystkie pierwotne funkcje rekurencyjne.

— vzn

1

„słowo„ algorytm ”jest zwykle zarezerwowane dla programów, które zawsze się zatrzymują.” - Nie jestem pewien, czy to prawda. Wokół jest wiele algorytmów częściowo kończących (szczególnie w weryfikacji) i nigdy nie słyszałem, żeby ktoś nie powiedział „algorytm”.

— Raphael

istnieją nieformalne zastosowania „algorytmu”. „częściowe zakończenie” jest w porządku, ale prawdopodobnie jest to nonstd. jak powiedziano, termin ten nie wydaje się jeszcze terminem standardowym. wikipedia definiuje algorytm jako skuteczną metodę, tj. rozstrzygalną z następującymi cechami (1) zawsze daje pewną odpowiedź zamiast nigdy nie dawać odpowiedzi; (2) zawsze udziel prawidłową odpowiedź i nigdy nie udzielaj złej odpowiedzi; (3) zawsze należy wykonać w skończonej liczbie kroków, a nie w nieskończonej liczbie; (4) praca dla wszystkich przypadków problemów klasy.

— vzn

a następnie w tym samym artykule jest napisane: „Dalsze wyjaśnienie terminu„ skuteczna metoda ”może obejmować wymóg, że w przypadku problemów spoza klasy, dla których metoda jest skuteczna, metoda może zatrzymać się lub zapętlić na zawsze bez zatrzymywania , ale nie może zwracać wyniku, jakby był odpowiedzią na problem ”. tzn. prawie się przeczy!!! tak wyraźnie, co zaskakujące, istnieje prawdziwe zamieszanie w kluczowej kwestii, a istniejąca terminologia nie jest ścisła. zwróć uwagę, że słowo „algorytm” jest bliskie ponad tysiącowi lat i znacznie się zmieniło…

— dniu

To prawda: tradycyjne znaczenie jest prawdopodobnie „skuteczną metodą” w sposób, w jaki mówi Wikipedia (w cytowanym zdaniu nie ma sprzeczności; jest to jednak niejasne) - ludzie nie wymyślili funkcji / algorytmów, które się nie kończyły (dla niektóre dane wejściowe). Myślę, że zmieniło się to od lat 50. XX wieku; jak powiedziałem, dziś ludzie wyraźnie nazywają metodę „kończącą się” metodą „algorytmu”.

— Raphael

2

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.

3

„Ponieważ wszystkie języki oprócz najbardziej prymitywnych są kompletne w Turingu (wymaga tylko czegoś takiego jak zmienne i warunkowe)” To nieprawda. Przede wszystkim potrzebowałbyś przynajmniej rekurencji lub jakiejś formy zapętlonej konstrukcji (która powinna być tak potężna jak pętla while - prosta pętla zliczania nie wystarczy). Po drugie, nie sądzę, że jest wiele osób, które nazywają języki takie jak Coq lub Agda (które są całkowite, a tym samym nie są kompletne), języki prymitywne lub zabawkowe.

— sepp2k

@ sepp2k: Cóż, tak. Arytmetyka Peano jest również bardzo przydatna i nie jest kompletna w Turingu. Uproszczone stwierdzenie, jak sądzę. Jeśli PO będzie wystarczająco dobrze zaznajomiony z problemem, miejmy nadzieję, że będzie w stanie podać szczegóły techniczne.

3

Istnieje ogromna przepaść między byciem „wystarczająco złożonym” a byciem kompletnym w Turingu. Coq jest naprawdę złożony i nadaje się do bardzo szerokiego zakresu praktycznych zadań.

1

@Kerrek SB Cóż, możliwe jest, że język Turing-complete jest używany w sposób, który może zostać rozwiązany. Jeśli możesz udowodnić, że formuła rekurencyjna zawsze zbliża się do warunku zakończenia (np. Funkcja czynnikowa), możesz udowodnić, że kończy się ona, nawet jeśli nie będziesz w stanie obsłużyć każdego rodzaju rekurencji.

@ArtB: Jasne, zawsze istnieje kilka programów, które mogą zostać zakończone. Pierwsze pytanie OP może na to wskazywać, choć nie jestem pewien, czy w pełni się z tym zgadzam. Na przykład, nie można mieć „ogólny algorytm”, który określa, czy dana rodzina programów odebrane, natomiast odwrotnie ty mógłby prawdopodobnie skonstruować ograniczoną rodzinę funkcji takich, że przyjmując funkcję należy do tej rodziny, można powiedzieć, czy to algorytmicznie kończy się. (Nie jestem jednak pewien, czy ta rodzina może być nietrywialna.

2

$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$

— Kaveh
źródło

1

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.

4

Jak myślisz, dlaczego Coq i Agda nie są przydatne? Przeceniasz wartość kompletności Turinga.

Korzystałem z Coq, ale moje roszczenie pozostaje, ponieważ większość komercyjnego oprogramowania jest napisana w Javie / C ++ / Ruby / C #, co do których moje twierdzenia są prawdziwe. Takie programy, które 90% ludzi jest zainteresowanych pisaniem, nie skorzystałoby. Zasadniczo, jeśli nie znasz Coq / Agda itp., Nie jesteś dla niego rynkiem docelowym.

5

Powiedziałbym, że 99% programów ze świata rzeczywistego skorzystałoby z wdrożenia w niekompletnym podzbiorze języka. Nie wdrożysz, powiedzmy, funkcji Ackermanna każdego dnia. 100% CRUD nie potrzebuje „prawdziwego” języka. Przetwarzanie danych jest prawie zawsze trywialne. Zobacz projekt Terminator - obsługują nawet przyzwoity podzbiór możliwych programów C ++, co w zupełności wystarcza do rzeczy w świecie rzeczywistym (w tym sterowników i innego kodu niskiego poziomu).

Większość projektów w świecie rzeczywistym chce ponownie wykorzystywać biblioteki napisane w językach kompletnych Turinga i używać swoich IDE oraz debuggerów i samouczków. Tak, możesz osiągnąć coś w językach innych niż Turing, ale nie wyobrażam sobie, żeby ktoś powiedział „Chcę zrobić X”, a moją odpowiedzią jest „Użyj Coq”. ps- dziękuję za zapoznanie mnie z The Terminator Project .

4

niewyobrażalnie duża część logiki biznesowej jest już zaimplementowana w niekompletnym języku Turing SQL. A DSL i eDSL rosną teraz. Wkrótce większość programistów aplikacji biznesowych zapomni o wszystkich językach „ogólnego zastosowania”.