Czy problem zatrzymania jest rozstrzygalny dla czystych programów na idealnym komputerze?

Dość proste jest zrozumienie, dlaczego problem zatrzymania jest nierozstrzygalny w przypadku nieczystych programów (tj. Tych, które mają operacje we / wy i / lub stany zależne od stanu globalnego maszyny); ale intuicyjnie wydaje się, że zatrzymanie czystego programu na idealnym komputerze byłoby rozstrzygalne np. poprzez analizę statyczną.

Czy tak jest w rzeczywistości? Jeśli nie, jakie kontrprzykłady lub dokumenty potwierdzają to twierdzenie?

Oto dowód nierozstrzygalności poprzez ograniczenie problemu Haltinga.

Redukcja: Biorąc pod uwagę maszynę i wejście x , zbuduj nową maszynę Turinga H, która nie odczytuje żadnego wejścia, ale zapisuje M i x na taśmie i symuluje M na x, dopóki M się nie zatrzyma.$M$$x$$H$$M$$x$$M$$x$$M$

Zachowanie tej nowej maszyny jest niezależne od taśmy wejściowej, więc jest to czysta maszyna Turinga, na której można stosować tylko analizę statyczną. Gdyby analiza statyczna była wystarczająca, mógłby wykazać, czy H zatrzymuje się, co pokazałoby, czy M zatrzymuje się na x , co rozwiązałoby problem zatrzymania dla nieczystych maszyn, o których wiemy, że jest nierozstrzygalny, a zatem twój problem również jest nierozstrzygalny.$H$$H$$M$$x$

Nie, nie jest, a ponadto nie zależy od I / O.

Prosty kontrprzykład: napisz program, aby znaleźć idealną liczbę nieparzystą (jest to otwarty problem: nie wiemy jeszcze, czy istnieje) - nie pobiera żadnych danych wejściowych i nie wykonuje żadnych nieczystych zadań; może się zatrzymać, gdy go znajdzie, lub może działać nieskończenie (w przypadku, gdy taka liczba nie istnieje). Teraz, jeśli analiza statyczna była wystarczająco silna, aby określić przypadek zatrzymania, byłaby użyta do odpowiedzi na to (i wiele innych pytań), gdzie zatrzymanie oznaczałoby pozytywne istnienie takiej liczby, a brak zatrzymania oznaczałby, że nie ma takiej liczby, ale niestety analiza statyczna nie jest tak potężny.

Klasyczny dowód diagonalizacji jest czystą maszyną , nie tylko jest czystą maszyną Turinga, ale nie opiera się na „otwartych problemach”.

Na przykład maszyna Turinga, która wykonuje hipotezę Collatz, ma nieznany status zatrzymania, ale to zależy od naszej niewiedzy o hipotezie Collatz, pewnego dnia możemy udowodnić, że Collatz miał rację, a następnie moglibyśmy zdecydować o stanie wstrzymania hipotezy (Albo dla niektórych danych wejściowych się nie zatrzymuje, albo zawsze zatrzymuje się).

Więc hipoteza Collatza może już odpowiedzieć na twoje pytanie (przynajmniej tymczasowo), ale opiera się na czymś, czego nie wiemy . Zamiast tego klasyczny dowód jest rozwiązanym problemem: wiemy już, że jest to nierozstrzygalne .

Dla przypomnienia, standardowy dowód nierozstrzygalności problemu zatrzymania opiera się na tym samym pomyśle co quines: że można napisać program, którego podokres ocenia na kod źródłowy dla całego programu. Następnie, gdyby istniała funkcja, haltsktóra podając kod źródłowy dla programu, zwracała wartość Prawda, jeśli program zatrzymałby się na wszystkich danych wejściowych, a w przeciwnym razie False, byłby to legalny program:

prog() = if halts "prog" then prog() else ()

gdzie "prog"byłoby jakieś wyrażenie, które oceniało kod źródłowy dla prog; jednak szybko widać, że progzatrzymuje się (dla wszystkich danych wejściowych), jeśli się nie zatrzymuje, co jest sprzecznością. Nic w tym dowodzie w żaden sposób nie opiera się na We / Wy (czy potrzebujesz We / Wy, aby napisać quine?).

Nawiasem mówiąc, możesz zajrzeć do „I / O opartego na oknie dialogowym”, aby uzyskać dalsze dowody, że I / O jest całkowicie nieistotne dla twojego problemu (w zasadzie programy, które robią I / O, można sprowadzić do programów, które przyjmują dane wejściowe jako (jawne) argumenty funkcjonalne i zwracają dane wyjściowe jako (jawne) dodatkowe wyniki w leniwym języku). Niestety nie mogę teraz znaleźć rozsądnej, pozbawionej stronniczości (lub pro-dialogowej) strony w sieci.