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

25

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?

Jules
źródło
35
Zauważ, że standardowe dowody, że problem zatrzymania jest nierozstrzygalny (taki jak ten opisany na wikipedia: en.wikipedia.org/wiki/Halting_problem#Sketch_of_proof ) wszystkie działają na modelach obliczeniowych, które nawet nie próbują reprezentować We / Wy. I chociaż np. Maszyny Turinga są stanowe, ich zachowanie jest formalnie zdefiniowane w kategoriach czystych funkcji. Tak więc w pewnym sensie „czyste programy na idealnym komputerze” to tak naprawdę ustawienie, w którym problem zatrzymania okazuje się zwykle nierozstrzygalny.
Ben
1
Jakie badania przeprowadziłeś? Google „Problem z zatrzymaniem” powinien już był odpowiedzieć na to pytanie.
Jonathan Cast

Odpowiedzi:

38

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.MxHMxMxM

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.HHMx

Lieuwe Vinkhuijzen
źródło
@HendrikJan Precisely!
Lieuwe Vinkhuijzen
16

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.

Zło
źródło
18
Naprawdę nie widzę sensu w tej odpowiedzi. To, że obecnie nie wiemy, czy taka liczba istnieje, nie oznacza, że ​​tak nie jest, ani że nie możemy w przyszłości napisać analizatora statycznego, który byłby w stanie o tym zadecydować. Lepszą alternatywą jest użycie jakiegoś znanego nierozstrzygalnego problemu. Na przykład wiadomo, że nie ma programu, który rozwiązałby wszystkie równania diofantyczne, a rozwiązanie takiego równania jest zadaniem podobnym do tego pokazanego w odpowiedzi.
Bakuriu
2
Cóż, jeśli problem zatrzymania byłby rozstrzygalny, wówczas każdy problem byłby rozstrzygalny, gdybyśmy mogli wprowadzić go do postaci, w której pytamy, czy program się zatrzymuje, czy nie. Lub dowolne pytanie o formę: istnieje zestaw policzalny i mogę zdecydować, czy którykolwiek potencjalny element jest w zestawie, czy nie. Czy zestaw jest pusty? Równania diofantyczne mają policzalny zestaw potencjalnych rozwiązań i mogę sprawdzić, czy każde pojedyncze potencjalne rozwiązanie jest rozwiązaniem, czy nie. Gdyby problem Halting był rozstrzygalny, rozstrzygałyby się równania diofantyczne.
gnasher729,
10
@ gnasher729 Tak, a ponieważ nie są, problem zatrzymania jest nierozstrzygalny. To mój punkt. Chociaż stwierdzenie w tej odpowiedzi nie ma rzeczywistych implikacji: „Rozważ tę matematyczną definicję. Obecnie nie mamy pojęcia, czy program decydujący się na to zatrzyma się, czy nie, ale jutro facet może dowiedzieć się, że tak się dzieje, a nie, a ta odpowiedź wynosi 100 % bez znaczenia ”.
Bakuriu
6
Czy nie jest to przypadek podobny do Jak można rozstrzygać, czy π ma jakąś sekwencję cyfr? problem zatrzymania jest nierozstrzygalny w przypadku klas problemów, a nie pojedynczych problemów.
npostavs
2

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 .

Twórca gier
źródło
0

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.

Jonathan Cast
źródło