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 które jest kodowaniem maszyny Turinga i , niezależnie od tego, czy zatrzymuje się. Następnie rozważ maszynę Turinga która bierze i i używa aby zdecydować, czy zatrzymać, czy nie, a następnie robi coś przeciwnego, tj. zatrzymuje się, jeśli się nie zatrzyma i nie zatrzyma się, jeśli $Q$ $M$ $X$ $M(X)$ $K$ $M$ $X$ $Q$ $M(X)$ $K$ $M(X)$ $M(X)$ zatrzymuje się Następnie wykazuje sprzeczność, ponieważ 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 , wówczas nie odnosi się do jeśli wyklucza wszystkie maszyny, które wywołują na (bezpośrednio lub pośrednio). (Oczywiście oznacza to, że nie może być członkiem ) $Q$ $S$ $S$ $Q$ $Q$ $S$ $Q$ $S$

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

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

computability lo.logic

— M. Alaggan
źródło

„pozostały zestaw nie odwołujący się do siebie” Zanim będę mógł rozsądnie omówić ten zestaw, chciałbym zdefiniować „odniesienie do siebie”. Myślę jednak, że będzie to trudne do zdefiniowania?

— Sam Nead,

Istnieją badania nad programami, które można udowodnić (ta klasa nie obejmuje wszystkich programów zatrzymywania). Zasadniczo są one parą programu i dowodem na to, że się zatrzymuje. Na przykład, jeśli się nie mylę, Agda zezwala tylko na programy, które się zatrzymały. Myślę, że ludzie zajmujący się logiką i językami programowania mają więcej do powiedzenia na ten temat.

— Tsuyoshi Ito,

@M. Alaggan. Teraz chciałbym zdefiniować definicję „wywołuje

pośrednio”, która, jak podejrzewam, jest tak trudna do zdefiniowania, jak oryginalna „referencja” :)

Q

$Q$

S

$S$

— Rob Simmons,

Rodzi to interesujące pytanie: czy wszystkie dowody nieobliczalności (nierozstrzygalności) można prześledzić metodą diagonalizacji Cantora? Czy istnieje dowód na nierozstrzygalność, który nie opiera się bezpośrednio lub pośrednio na metodzie diagonalizacji?

— Mohammad Al-Turkistany

Ewentualnie powiązane pytania: czy istnieje teoria złożoności analogiczna do twierdzenia o rice w teorii obliczalności? , MO: kompletność najłatwiejsze najtrudniejsze problemy .

— Kaveh

Odpowiedzi:

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.

— Mark Reitblatt
źródło

Q

$Q$

H

$H$

To nie jest takie proste. Twoja definicja jest teraz paradoksalna, ponieważ szukasz obliczalnego HALT. Ale jeśli jest to możliwe do obliczenia, każda funkcja obliczeniowa jest jej obliczeniowo równoważna. Ale jeśli Twój zestaw danych wejściowych zawierał problemy pół-obliczalne (TM), miałbyś sprzeczność, ponieważ decyzja o problemie zatrzymania dla takiej TM dałaby ci procedurę decyzyjną dla tego problemu.

— Mark Reitblatt,

1) Czy obliczenie HALT nie oznaczałoby nierozstrzygalności? Zakładałem, że istnieje taki obliczalny HALT, licząc na sprzeczność. 2) Nie znam pojęcia, że wszystkie obliczalne funkcje są sobie równoważne, zacytowałem cię, co oznacza, że jest to funkcja rozwiązująca problem HALT. Najwyraźniej λx.1 jest obliczalny, ale nie decyduje o HALT. Popraw mnie, jeśli się mylę, proszę. Jeśli chodzi o problemy częściowo obliczalne, HALT może podjąć nieskończoną liczbę kroków, które nadal nie prowadziłyby do sprzeczności w oryginalnym dowodzie, że HALT nie jest rozstrzygalny.

— M. Alaggan,

1) Racja. Problem polega jednak na zdefiniowaniu pojęcia „braku odniesienia do siebie”. Albo jest to słabe ograniczenie, które pozwala na przekątną, jak argumentowałem, albo silne ograniczenie, które eliminuje wszystko. 2) To proste. „Obliczalnie równoważny” z grubsza oznacza, że istnieje obliczalne odwzorowanie od jednego do drugiego, które zachowuje odpowiedzi. Ale jeśli potrafię obliczyć odpowiedź, mogę oszukać i uczynić mapowanie banalnym. 3) Jeśli TM decydująca HALT sama się nie zakończy, nie decyduje HALT.

— Mark Reitblatt,

Coś innego, co jest nieco mylące, to połączenie TM z obliczonym przez nich problemem decyzyjnym. Nie jest normalne mówienie o tym, że TM jest obliczeniowo równoważna sobie nawzajem. Obliczone przez nie funkcje mogą być równoważne (lub równe). Problem polega na tym, że próba powiedzenia, że TM nie symuluje innej TM, jest ogólnie trudna do zdefiniowania, nie dając niczego konkretnego do oddzielenia obliczanych przez nią funkcji. Na przykład log-space TM nie może symulować TM rozwiązującego problem przestrzeni EXP.

— Mark Reitblatt,

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

— Rob Simmons
źródło

Dzięki za świetną odpowiedź. Byłoby to z pewnością przydatne dla mojego kolegi. Jednak ja (niezależnie od mojego kolegi) bardziej interesują mnie teoretyczne implikacje dowodu problemu zatrzymania, że jeśli pozbyliśmy się przypadku wykazującego sprzeczność, to co jeszcze wiemy o rozstrzygalności problemu zatrzymania?

— M. Alaggan,