Czy można rozwiązać problem zatrzymania, jeśli masz ograniczony lub przewidywalny wkład?

Problemu zatrzymania nie można rozwiązać w ogólnym przypadku. Można wymyślić zdefiniowane reguły, które ograniczają dozwolone dane wejściowe i czy problem zatrzymania można rozwiązać w tym szczególnym przypadku?

Na przykład wydaje się prawdopodobne, że język, który nie dopuszcza na przykład pętli, bardzo łatwo będzie stwierdzić, czy program się zatrzyma, czy nie.

Problem, który próbuję rozwiązać w tej chwili, polega na tym, że próbuję utworzyć moduł sprawdzania skryptów, który sprawdza poprawność programu. Czy problem zatrzymania można rozwiązać, jeśli dokładnie wiem, czego oczekiwać od autorów skryptów, co oznacza bardzo przewidywalne dane wejściowe. Jeśli nie da się tego dokładnie rozwiązać, jakie są dobre techniki przybliżania, aby rozwiązać ten problem?

Intuicyjna odpowiedź jest taka, że ​​jeśli nie masz nieograniczonych pętli i nie masz rekurencji i nie masz goto, twoje programy zostaną zakończone. Nie jest to do końca prawdą, istnieją inne sposoby na ukrycie braku wypowiedzenia, ale wystarcza w większości praktycznych przypadków. Oczywiście odwrotność jest błędna, istnieją języki z tymi konstrukcjami, które nie pozwalają na nie kończące się programy, ale używają innych rodzajów ograniczeń, takich jak wyrafinowane systemy typów.

Rekurencja

Częstym ograniczeniem w językach skryptowych jest dynamiczne zapobieganie rekurencji: jeśli A wywołuje B wywołuje C wywołuje… wywołuje A, wówczas interpreter (lub w twoim przypadku moduł sprawdzający) rezygnuje lub sygnalizuje błąd, nawet jeśli rekursja faktycznie się zakończy. Dwa konkretne przykłady:

• Preprocesor C pozostawia makro nienaruszone podczas jego rozwijania. Najczęstszym zastosowaniem jest zdefiniowanie opakowania wokół funkcji:

  #define f(x) (printf("calling f(%d)\n", (x)), f(x))
  f(3);
  

  To rozwija się do

  (printf("calling f(%d)\n", (3)), f(3))
  

  Obsługiwana jest również wzajemna rekurencja. Konsekwencją jest to, że preprocesor C zawsze kończy działanie, chociaż możliwe jest budowanie makr o dużej złożoności w czasie wykonywania.

  #define f0(x) x(x)x(x)
  #define f1(x) f0(f0(x))
  #define f2(x) f1(f1(x))
  #define f3(x) f2(f2(x))
  f3(x)
  

• Powłoki uniksowe rozwijają aliasy rekurencyjnie, ale tylko do momentu napotkania aliasu, który jest już rozwijany. Ponownie głównym celem jest zdefiniowanie aliasu dla polecenia o podobnej nazwie.

  alias ls='ls --color'
  alias ll='ls -l'
  

Oczywistym uogólnieniem jest umożliwienie głębokości rekurencji do , przy czym może być konfigurowalne.$n$$n$

Istnieją bardziej ogólne techniki, aby udowodnić zakończenie połączeń rekurencyjnych, takie jak znalezienie pewnej dodatniej liczby całkowitej, która zawsze zmniejsza się z jednego połączenia rekurencyjnego do drugiego, ale są one znacznie trudniejsze do wykrycia. Często są trudne do zweryfikowania, nie mówiąc już o wnioskach.

Pętle

Pętle się kończą, jeśli można ograniczyć liczbę iteracji. Najczęstszym kryterium jest to, że jeśli masz forpętlę (bez lew, tj. Taką , która naprawdę liczy się od do ), wykonuje skończoną liczbę iteracji. Więc jeśli ciało pętli się kończy, sama pętla się kończy.$m$$n$

W szczególności w przypadku pętli (oraz rozsądnych konstrukcji języka, takich jak warunkowe), możesz pisać wszystkie prymitywne funkcje rekurencyjne i odwrotnie. Prymitywne funkcje rekurencyjne można rozpoznać składniowo (jeśli są napisane w sposób nieudokumentowany), ponieważ nie używają pętli while ani goto, rekurencji lub innej sztuczki. Pierwotne funkcje rekurencyjne mają zagwarantowane zakończenie, a większość praktycznych zadań nie wykracza poza prymitywną rekurencję.

Zobacz Terminator i AProVe . Zwykle polegają na heurystyce i nie jestem pewien, czy jasno opisują klasę programów, dla których pracują. Mimo to są one uważane za najnowocześniejsze, więc powinny być dla Ciebie dobrym punktem wyjścia.

Tak, może być możliwe. Jednym z powszechnych sposobów rozwiązywania takich problemów jest rozważenie dodatkowego (monotonicznego) nieobliczalnego parametru w zależności od kodu jako części danych wejściowych. Złożoność problemu mającego ten parametr można znacznie zmniejszyć.

Nie możemy obliczyć parametru, ale jeśli wiesz, że instancje wejściowe, z którymi masz do czynienia, mają małe wartości parametrów, możesz naprawić go do małej liczby i użyć algorytmu.

Te i podobne sztuczki są stosowane w metodach formalnych, aby poradzić sobie z nierozstrzygalnością zatrzymania i podobnych problemów. Ale jeśli to, co chcesz zdecydować, jest skomplikowane, złożoność algorytmów raczej nie będzie lepsza niż uruchomienie algorytmu w tych instancjach.

Jeśli chodzi o drugie pytanie, jeśli wystarczająco ograniczysz nakłady, problem zatrzymania może być łatwy. Na przykład, jeśli wiesz, że dane wejściowe są wielomianowymi algorytmami czasowymi, podjęcie decyzji o ich zatrzymaniu jest banalne (ponieważ każdy algorytm wielomianowy zatrzymuje się).

Problemy pojawiające się w metodach formalnych są zwykle nierozstrzygalne, możesz zajrzeć do literatury dotyczącej tego, jak radzą sobie z tymi problemami w praktyce.

Nie jest to formalnie sztywna odpowiedź, ale oto:

Problem z określeniem, czy zatrzyma się na zawsze, czy zapętli. Pętle w kolekcjach skończonych jeden element na raz lub między przedziałami liczb jest w porządku. EDYCJA: Oczywiście, zadziała to tylko wtedy, gdy iterowana kolekcja lub interwał nie mogą się zmienić (np. Przez niezmienność) podczas iteracji (lub przynajmniej zabrania się ich wzrostu).

Rekurencja prawdopodobnie nie jest w porządku, chyba że ustawisz sztuczną regułę, aby była skończona, na przykład zezwalając na maksymalną głębokość stosu lub zmuszając do zmniejszenia wartości nieujemnej w każdej iteracji.

Arbitralne gotos są ogólnie złe. Wsteczne goto najprawdopodobniej prowadzą do pętli, które mogą być nieskończone.

Instrukcje Whiles i do-whiles stanowią problem, ponieważ zależą od warunku, który nie ma gwarancji zmiany lub nie podczas wykonywania. Możliwym (ale prawdopodobnie bardzo niezadowalającym) sposobem ograniczenia jest zapewnienie maksymalnej możliwej liczby iteracji.

Musisz podać definicję języka skryptowego i co rozumiesz przez „oczekiwać” od autorów skryptów.

${\cal O}(n^\omega)$

Podobny wynik ma klasa programów wielomianowych Aarona R. Bradleya, Zohara Manny i Henny B. Sipmy. Ale AFAIK (mogę się tutaj mylić), środowisko wykonawcze jest podwójnie wykładnicze (zasadniczo czas potrzebny do obliczenia podstawy Groebnera).