Co wiemy o ograniczonych wersjach problemu zatrzymania

( AKTUALIZACJA : postawiono tutaj lepiej sformułowane pytanie , ponieważ komentarze do przyjętej odpowiedzi poniżej pokazują, że to pytanie nie jest dobrze zdefiniowane)

Klasyczny dowód na niemożność problemu zatrzymania zależy od wykazania sprzeczności przy próbie zastosowania algorytmu wykrywania zatrzymania jako danych wejściowych. Aby uzyskać więcej informacji, zobacz tło poniżej.

Wykazana sprzeczność ma zastosowanie z powodu paradoksu autoreferencji (jak zdanie „To zdanie nie jest prawdziwe”). Ale jeśli surowo zabroniliśmy takich odnośników (tj. Zaakceptowaliśmy fakt, że takich odnośników nie można rozstrzygnąć), to z jakim rezultatem jesteśmy? Czy problem zatrzymania pozostałego zestawu maszyn, które nie zawierają odnośników, można rozwiązać, czy nie?

Pytania są następujące:

Jeśli weźmiemy pod uwagę podzbiór wszystkich możliwych maszyn Turinga, które nie odwołują się do siebie (tj. Nie traktują ich jako danych wejściowych), co wiemy o problemie zatrzymania dla tego podzbioru?

AKTUALIZACJA

Może lepszym przeformułowaniem tego, czego szukam, jest lepsze zrozumienie tego, co definiuje decydujący zbiór. Próbowałem wyodrębnić klasyczny dowód nierozstrzygalności, ponieważ nie dodaje on żadnych informacji o nierozstrzygalności, z wyjątkiem przypadków, w których uruchamiasz HALT na sobie.

Tło: Zakładając sprzeczność, że istnieje maszyna Turinga która może decydować o wejściu M, które jest kodowaniem maszyny Turinga i X , niezależnie od tego, czy M ( X ) zatrzymuje się. Następnie rozważ maszynę Turinga K, która bierze M i X i używa Q, aby zdecydować, czy M ( X ) ma się zatrzymać, czy nie, a następnie robi coś przeciwnego, tj. K zatrzymuje się, jeśli M ( X ) się nie zatrzyma i nie zatrzyma się, jeśli M ( $Q$$M$$X$$M(X)$$K$$M$$X$$Q$$M(X)$$K$$M(X)$$M(X)$zatrzymuje się Następnie wykazuje sprzeczność, ponieważ K powinien się zatrzymać, jeśli się nie zatrzyma, i nie zatrzyma się, gdy się zatrzyma.$K(K)$$K$

Motywacja: kolega pracuje nad formalną weryfikacją systemów oprogramowania (zwłaszcza, gdy system jest już sprawdzony na poziomie kodu źródłowego i chcemy go naprawić dla wersji skompilowanej, aby zneutralizować problemy z kompilatorem), aw jego przypadku zależy mu na specjalny zestaw wbudowanych programów sterujących, dla których wiemy na pewno, że nie byłyby samodzielnymi odnośnikami. Jednym z aspektów weryfikacji, którą chce przeprowadzić, jest to, czy zagwarantowane jest, że skompilowany program zatrzyma się, jeśli okaże się, że wejściowy kod źródłowy został zakończony.

AKTUALIZACJA

W oparciu o poniższe komentarze wyjaśniam znaczenie maszyn Turinga, które nie zawierają odnośników.

Celem jest zdefiniowanie go jako zbioru, który nie prowadzi do sprzeczności przedstawionej w dowodzie (por. „Tło” powyżej). Można go zdefiniować w następujący sposób:

Zakładając, że istnieje maszyna Turinga która decyduje o problemie zatrzymania zestawu maszyny Turinga S , wówczas S nie odnosi się do Q, jeśli wyklucza wszystkie maszyny, które wywołują Q na S (bezpośrednio lub pośrednio). (Oczywiście oznacza to, że Q nie może być członkiem S. )$Q$$S$$S$$Q$$Q$$S$$Q$$S$

Aby wyjaśnić, co oznacza pośrednie wywoływanie na S :$Q$$S$

Wywołanie na S jest oznaczone przez maszynę Turinga Q z zestawem stanów i pewnymi możliwymi początkowymi wejściami na taśmie (odpowiadającymi dowolnemu członkowi S ), z głową początkowo na początku tego wejścia. Maszyna W wywołuje Q na S „pośrednio”, jeśli istnieje (skończona) sekwencja kroków, które W podjąłby, aby dokonać konfiguracji „homomorficznej” do początkowej konfiguracji Q ( S ) .$Q$$S$$Q$$S$$W$$Q$$S$$W$$Q(S)$

AKTUALIZACJA 2

Z odpowiedzi poniżej, która dowodzi, że istnieje nieskończenie wiele maszyn Turinga wykonujących to samo zadanie, a zatem nie jest unikalna, zmieniamy powyższą definicję, mówiąc, że Q nie jest pojedynczą maszyną Turinga, ale (nieskończonym) zestawem wszystkich maszyn obliczeniowych ta sama funkcja (HALT), gdzie HALT jest funkcją, która decyduje, kiedy maszyna Turinga zatrzymuje się na określonym wejściu.$Q$$Q$

AKTUALIZACJA 3

Definicja homomorfizmu maszyny Turinga:

TM A jest homomorficzna do TM B, jeśli wykres przejścia A jest homomorficzny do B, w standardowym znaczeniu homomorfizmów grafów z oznaczonymi węzłami ORAZ krawędziami. Wykres przejścia (V, E) bazy TM jest taki, że V = stany, E = łuki przejścia między stanami. Każdy łuk jest oznaczony (S, W, D), S = symbol odczytany z taśmy, a W = symbol, który zostanie na nim zapisany, a D = kierunek, w którym porusza się pokaz głowy.

Myślę, że zajmie trochę więcej pracy, aby dostać się do „dobrze zdefiniowanego” pytania. W szczególności jest to problematyczne:

Wywołanie Q na S jest oznaczone przez maszynę Turinga Q z zestawem stanów i pewnymi możliwymi początkowymi wejściami na taśmie (odpowiadającymi dowolnemu członkowi S), z głową początkowo na początku tego wejścia. Maszyna W wywołuje Q na S „pośrednio”, jeśli istnieje (skończona) sekwencja kroków, które W podjąłby, aby dokonać konfiguracji „homomorficznej” do początkowej konfiguracji Q (S).

Jednym z problemów jest to, że istnieje nieskończenie wiele maszyn Turinga, które wykonują tę samą funkcję. W standardowym argumencie diagonalizacji mogę po prostu zastąpić podprogram Q innym decydującym czynnikiem HALT, ponieważ jest ich nieskończenie wiele. Lub funkcja, która jest obliczalnie równoważna HALT. Nie jest więc dla mnie całkowicie jasne, jak zdefiniować swoje pojęcie „wywołania pośredniego”.

Inne pytanie może brzmieć: dla jakich zestawów maszyn Turinga można rozwiązać problem zatrzymania? Tutaj jest mnóstwo odpowiedzi: bazy TM z ograniczonymi zasobami (np. Używają tylko miejsca f (n), gdzie f jest jakąś określoną funkcją obliczalną), bazy TM, które są operacyjnie ograniczone w określony sposób (np. Głowica odczytu przesuwa się tylko w jedną stronę), itp. Ale kolejnym interesującym pytaniem jest to, czy można decydować o członkostwie w tym ograniczonym zestawie, czy też trzeba ograniczyć się do „problemów z obietnicą”, w których gwarantuje się prawidłową odpowiedź na niektóre „obiecane” podziały danych wejściowych, ale nie weryfikuje się członkostwo.

Jeśli dobrze rozumiem twoją motywację, wydaje się, że jest to kwestia „poprawności kompilatora” bardziej niż problem „ograniczonego zatrzymania”. Masz właściwość (zakończenie), którą udowodniłeś dla jakiegoś programu Prog na poziomie źródłowym , który chcesz rozszerzyć na skompilowany kod, aby uzyskać tę samą właściwość co skompilowany (Prog) . Ale kompilator może (ogólnie) robić dowolne, głupie rzeczy, takie jak implementacja środowiska wykonawczego z pełną obsługą Turinga (powiedzmy JVM), kompilować program kończący w kod bajtowy JVM, a następnie zrzucić plik wykonywalny, który uruchamia JVM i podaje mu skompilowany kod bajtowy.

W praktyce prawdopodobnie całkiem możliwe jest wykorzystanie ukrytej wiedzy na temat działania kompilatora w celu zaimplementowania pewnej procedury weryfikacji, która właściwie dowodzi, że skompilowane programy są poprawne, biorąc pod uwagę poprawne programy źródłowe (w rzeczywistości wiele narzędzi automatycznej weryfikacji dla programów wykorzystuje ukrytą wiedzę „kompilatora” algorytm-kod w mózgach programistów). Jednak ogólnie prawdopodobnie patrzysz na problem z poprawnością kompilatora. Rozumiem, że istnieją dwa klasyczne sposoby.

Jedną z opcji jest posiadanie kompilatora, który pobiera jako dane wejściowe program Prog, a dowód kończy się (Prog), a dane wyjściowe są kompilowane (Prog) i kończy się (skompilowany (Prog)) - ten drugi jest dowodem, który można następnie dwukrotnie sprawdzić niezależnie od kompilator. Klasyczny artykuł na ten temat to Necula i Lee . Projekt i wdrożenie kompilatora certyfikującego , jak sądzę.

Alternatywnie możesz udowodnić fakt dotyczący funkcji compiles () - że ilekroć kompilacja () podaje dane końcowe, generuje dane wyjściowe. Dostępnym wprowadzeniem do tego sposobu myślenia o poprawności kompilatora jest artykuł CACM Xaviera Leroya, Formalna weryfikacja realistycznego kompilatora .

(PS Mam nadzieję, że ta odpowiedź jest pomocna - zdaję sobie sprawę, że jest nieco rozbieżna w stosunku do zadanego pytania, więc daj mi znać, jeśli jestem nieuczciwy i / lub powtarzam coś, co już wiesz.)