Niektóre problemy są nierozstrzygalne, ale mimo to można poczynić pewne postępy w ich rozwiązywaniu. Na przykład problem zatrzymania jest nierozstrzygalny, ale można poczynić praktyczne postępy w tworzeniu narzędzi do wykrywania potencjalnych nieskończonych pętli w kodzie. Problemy z układaniem płytek są często nierozstrzygalne (np. Czy ta płytka poliomino ma jakiś prostokąt?), Ale ponownie możliwe jest osiągnięcie postępu w tej dziedzinie.
Zastanawiam się, czy istnieje jakaś przyzwoita teoretyczna metoda pomiaru postępu w rozwiązywaniu nierozwiązywalnych problemów, która przypomina aparat teoretyczny opracowany do pomiaru postępu w problemach trudnych dla NP. Czy też wydaje się, że utknęliśmy w ocenach ad hoc, wiem, czy postęp, kiedy widzę, o ile konkretnych przełomów usprawnia nasze rozumienie nierozstrzygniętych problemów?
Edycja : Kiedy myślę o tym pytaniu, przychodzi mi do głowy, że być może sparametryzowana złożoność może być tutaj istotna. Problem nierozstrzygalny może stać się rozstrzygalny, jeśli wprowadzimy parametr i naprawimy wartość parametru. Nie jestem jednak pewien, czy ta obserwacja jest przydatna.
Odpowiedzi:
W przypadku problemu zatrzymania odpowiedź brzmi „jeszcze nie”. Powodem jest to, że standardowa logiczna metoda charakteryzowania tego, jak trudny jest dowód zakończenia programu (np. Analiza porządkowa), ma tendencję do utraty zbyt dużej struktury kombinatorycznej i / lub teorii liczb.
Oznacza to, że nie ma zgrabnego związku między siłą dowodową teorii metalogicznej, w której wykazuje się terminację (jest to bardzo ważne na przykład w teorii przepisywania) a funkcjami, które techniki takie jak synteza funkcji rangi mogą pokazać terminacją .
W przypadku rachunku lambda mamy dokładną charakterystykę terminacji pod względem typowości: termin lambda silnie normalizuje się wtedy i tylko wtedy, gdy można go wpisać w ramach dyscypliny typu przecięcie. Oczywiście oznacza to, że pełne wnioskowanie typów dla typów skrzyżowań jest niemożliwe, ale może również dać możliwość porównania algorytmów wnioskowania częściowego.
źródło
Z pamiętnej rozmowy osoby, która wdrożyła algorytm, który rozwiązuje nierozstrzygalny problem: „Zajmuje 2-3 sekundy dla wszystkich danych wejściowych, które próbowałem”.
źródło
Odpowiada to bardziej na tytuł pytania niż na jego treść, ale można również rozważyć „przybliżenie” problemu zatrzymania jako algorytmy, które dadzą prawidłową odpowiedź na „prawie wszystkie” programy.
Pojęcie „prawie wszystkich” programów ma sens tylko wtedy, gdy twój model obliczeń jest optymalny (w tym samym sensie, co w przypadku złożoności Kołmogorowa ), aby uniknąć sytuacji, w których większość twoich programów jest trywialna.
źródło