Czy zatrzymanie problemu jest obliczalne dla poszczególnych danych wejściowych / założeń

19

Z mojego rozumienia dowodu, że problemu zatrzymania nie można obliczyć, problemu tego nie da się obliczyć, ponieważ jeśli mamy program P (x), który oblicza, czy program x zatrzymuje się, czy nie, mamy paradoks, gdy P podaje się jako dane wejściowe do to samo P, mając: P (P), próbując zdecydować, czy P zatrzymuje się, czy nie używać samego P.

Więc moje pytanie brzmi: czy zatrzymanie problemu jest obliczalne przez program P dla wszystkich innych programów używanych jako dane wejściowe, ale sam P? Innymi słowy: czy zatrzymanie problemu nie jest możliwe do obliczenia tylko w tym szczególnym przypadku, czy dowód jest bardziej ogólny i czegoś mi brakuje?

halting-problem

— Alessio Martorana
źródło

Myślę, że nie rozumiesz dowodu, że problemu zatrzymania nie da się obliczyć. P (P) po prostu zwraca true, ponieważ P zawsze określa, czy program zatrzymuje się w skończonym czasie. Musisz wykonać nieco trudniejszą konstrukcję, aby osiągnąć sprzeczność.

— Dan Staley

Myślę, że uzyskałbyś lepsze i być może bardziej odpowiednie odpowiedzi, gdybyś zapytał, czy istnieje wiele programów, dla których problem zatrzymania można rozwiązać. W końcu wiele programów można nawet formalnie zweryfikować , co z pewnością obejmuje ustalenie, czy zatrzymają się przy danych wejściach. Zdecydowanie przypuszczam, że nie można ustalić tej grupy (ponieważ to oznaczałoby rozwiązanie ... wiesz), ale że w zdecydowanej większości programów w świecie rzeczywistym nie ma przeszkód, aby stwierdzić, czy się zatrzymują, czy nie, w przypadku odpowiednich danych wejściowych.

— Peter - przywróć Monikę

10

Jeśli jest dowolną funkcją obliczalną, to , zdefiniowane jako $f$ $g$

g (n) = {\begin{cases} f (n) & if n \neq k \\ v & otherwise \end{cases}

$g(n) = \begin{cases} f(n) & \mbox{if } n \neq k \\ v & \mbox{otherwise} \end{cases}$

jest również obliczalny dla dowolnego wyboru . $k,v$

Zasadniczo, jeśli masz program który oblicza dla wszystkich , z wyjątkiem , możesz "naprawić" ten przypadek (np. Używając an ) i uzyskać inny program który oblicza dla wszystko . $P'$ $g(n)$ $n$ $n=k$ if then else $P$ $g(n)$ $n$

Dlatego jeśli można obliczyć funkcję zatrzymania „z wyjątkiem jednego przypadku”, można również obliczyć funkcję zatrzymania (bez wyjątków). Dzięki temu można uzyskać jak zwykle sprzeczność.

Wniosek: nie, nie możesz zdecydować o problemie zatrzymania „z wyjątkiem jednego przypadku” (ani „z wyjątkiem skończonej liczby przypadków”).

— chi
źródło

1

Ok, chyba mam to matematyczne ... Ale zastanawiałem się: czy spróbuję napisać program, który oblicza HP, z jakimi konkretnymi problemami bym się spotkał? Dlaczego i jak w pewnym momencie rozumiem, że nie mogę napisać takiego programu?

— Alessio Martorana

@AlessioMartorana To zależy: jak podejdziesz do takiego problemu? Głównym problemem jest to, że musi się zawsze zatrzymywać, nawet jeśli jego wejście jest programem bez zatrzymywania - więc nie można po prostu spróbować symulować programu wprowadzania.

P

$P$

— chi

Przypuśćmy, że możemy zobaczyć kod programu wejściowego? Czy nie możemy z kodu sprawdzić, czy program się zatrzymuje?

— Alessio Martorana,

2

@AlessioMartorana Rzeczywiście możemy zobaczyć kod, ale jeśli istnieje np. Pętla while, nie możemy wiele powiedzieć w ogóle. Pętla while może sprawdzić wszystkie możliwe dowody arbitralnego przypuszczenia matematycznego i zatrzymać się tylko w przypadku znalezienia dowodu. Decyzja, czy ta pętla się zatrzymuje, oznacza decyzję, czy domniemanie jest możliwe do udowodnienia. Rozwiązanie HP dałoby nam maszynę, która odpowiedziałaby Tak (dający się udowodnić) / Nie (nie dający się udowodnić) na jakiekolwiek formalne pytanie matematyczne. To byłoby nierealistycznie potężne.

— chi

1

@AlessioMartorana Jeśli myślałeś, że napisałeś program, który rozwiązuje problem HP, awaria twojego programu może być na jeden z dwóch sposobów: w przypadku niektórych programów może zwrócić zły wynik (mówiąc, że coś się zatrzymuje, gdy się nie powiedzie lub mówiąc, że coś nie działa) zatrzyma się, gdy to zrobi) i / lub sam program decyzyjny nie zatrzyma się na wielu wejściach, a Ty nie będziesz w stanie wiedzieć, czy naprawdę się nie zatrzyma, czy też po prostu potrzebuje więcej czasu na obliczenie odpowiedzi.

— Shufflepants

21

czy problem zatrzymania jest obliczany przez program P dla wszystkich innych programów używanych jako dane wejściowe, ale sam P?

Nie Rozważmy nieskończoną sekwencję programów , gdzie jest „przesunięcie głowicy placów w prawo, a następnie placów w lewo, a następnie zrobić dokładnie to, co zrobi.” Każdy z tych programów generuje dokładnie to samo wyjście co dla każdego wejścia (włączając w to zapętlanie na zawsze, jeśli zapętla się na zawsze), ale wszystkie są różnymi programami. $P_1, P_2, \dots$ $P_i$ $i$ $i$ $P$ $P$ $P$

Nie można tego obejść, wymagając od tylko pracy na programach, które nie są funkcjonalnie równoważne z sobą, ponieważ ta właściwość jest również nierozstrzygalna. Być może problem będzie rozstrzygalny, gdy ograniczy się do tych przypadków (choć podejrzewam, że nie), ale zestaw instancji jest nierozstrzygalny, więc nie można w rzeczywistości wykonać ograniczenia. $P$

— David Richerby
źródło

15

Podejrzewam, że twoje ostatnie zdanie jest prawdopodobnie prawdziwe, ale nie sądzę, że wynika z tego, że ponieważ właściwość jest nierozstrzygalna, to ograniczenie zestawu danych wejściowych na podstawie tej właściwości pozostawi problem nierozstrzygalny. Jako głupi przykład, jeśli ograniczysz zestaw danych wejściowych do kończących programów (właściwość nierozstrzygalna), problem będzie rozstrzygalny (przez program, który zawsze zwraca wartość true).

— Owen

3

@Owen Gdy samo ograniczenie jest nierozstrzygalne, nie możesz narzucić ograniczenia, więc nie może ci niczego kupić w rzeczywistości.

— David Richerby

5

Istnieją algorytmy pokazujące, że niektóre klasy programów zatrzymują się lub nie zatrzymują. Na przykład,

Możliwe jest algorytmiczne ustalenie, czy program modelujący maszynę o stanie skończonym zatrzymuje się.
Możliwe jest arytmetyczne ustalenie, czy zatrzymująca się maszyna liniowa ograniczona liniowo
Jeśli wiesz, w jakiej klasie złożoności znajduje się program, wiesz, że program zatrzymuje się na skończone dane wejściowe.

Chociaż nie ma algorytmu określającego, czy dowolny program się zatrzymuje, większość kodu została zaprojektowana albo do zatrzymania (jak większość podprogramów), albo do zatrzymania (jak nieskończona pętla do obsługi zdarzeń), i możliwe jest algorytmiczne określenie, który jest który. Innymi słowy, można mieć algorytm, który odpowiada albo „zatrzymanie”, „nie zatrzymuje się” lub „nie wiem”, a taki algorytm może być przeznaczony na pokrycie wystarczającej ilości programów, że byłoby użyteczne.

— Antonio Perez
źródło

Co to ma wspólnego z goto? Czy nie możemy mieć programu, który używa goto i nadal decyduje, czy się zatrzyma, o ile modeluje maszynę skończoną?

— Bergi

Zamierzałem pisać o zatrzymywaniu w kategoriach pętli for, a potem zmieniłem to, żeby mówić o skończonych automatach stanowych i tak dalej

— Antonio Perez

4

Dowody sprzeczności nie muszą być wyczerpujące , wystarczy jeden kontrprzykład. Dowód, że problem zatrzymania jest nierozstrzygalny, przedstawia jeden przykład P, dla którego nie można ustalić właściwości zatrzymania. Dowód ten nie stwierdza, że P jest jedynym takim programem, w rzeczywistości mogą istnieć niezależne dowody konstruujące zupełnie różne klasy P.

— Dmitrij Grigoriew
źródło

3

Dowód jest rzeczywiście bardziej ogólny: problem zatrzymania jest szczególnym przypadkiem twierdzenia Rice'a , które stwierdza

$\Phi$

$A$ $B$ $\Phi(A)$ $\Phi(B)$

$x$ $x$

Państwo może uzyskać pewne rezultaty ograniczając przestrzeń programów, które chcesz pracować, jeśli ograniczenia te muszą być dość drastyczne. Na przykład, jeśli masz gwarancję, że program, który otrzymujesz, zatrzymuje się w ciągu 100 kroków lub działa wiecznie, decydując, czy program się zatrzyma, stanie się łatwy.

$N$ $k$ $BB(k)$

— Anton Golov
źródło

1

N

$N$

1

Ostatni akapit przypomina Busy Beaver.

— Zły

Odnośnie do „dość drastycznych” ograniczeń: całkowita liczba języków programowania to coś. Zwykle wymagają stosunkowo wysokiego stopnia wyrafinowania, więc może uważasz to za drastyczne, ale możliwe jest rozwiązanie prawdziwych problemów w przestrzeni programów, które prawdopodobnie przestaną działać.

— Ben Millwood,

Dołączenie linku do en.wikipedia.org/wiki/Rice%27s_theorem miałoby sens IMO.

— Dmitrij Grigoryev,

Dzięki, zaktualizowałem odpowiedź. @BenMillwood Z pewnością, ale biorąc pod uwagę ich rozwiązanie, „zatrzymaj wszystko”, nie jestem pewien, czy naprawdę tego szuka Alessio. Interesujący byłby jednak przypadek, w którym zatrzymanie jest rozstrzygalne, ale nietrywialne: może typy koindukcyjne Agda +?

— Anton Golov,

0

Niech R będzie dowolnym rekurencyjnie wyliczalnym, ale nierekurencyjnym zbiorem. Istnieje nieskończenie wiele takich zestawów. Niech T będzie maszyną Turinga, która zatrzymuje się na wejściu k wtedy i tylko wtedy, gdy k znajduje się w R. Taki T istnieje dla dowolnego zbioru rekurencyjnie wyliczalnego. Niemożliwe jest napisanie programu, który może rozwiązać problem zatrzymania dla tego T. Jest tak, ponieważ każdy algorytm określający, czy T zatrzymuje się, dałby algorytm określający członkostwo w R, co jest niemożliwe, jeśli R nie jest rekurencyjny. Ponieważ istnieje nieskończenie wiele takich R, z których każda daje różne maszyny Turinga, istnieje nieskończenie wiele maszyn Turinga, na których nie powiódłby się żaden program zatrzymania P.

— John Coleman
źródło