Jak sprawdzić, czy dwa algorytmy zwracają ten sam wynik dla dowolnego wejścia?

18

Jak sprawdzisz, czy dwa algorytmy (powiedzmy: Sortuj i Naiwne) zwracają ten sam wynik dla dowolnego wejścia, gdy zestaw wszystkich danych wejściowych jest nieskończony?

Aktualizacja: Dziękuję Ben za opisanie, w jaki sposób niemożliwe jest algorytmiczne wykonanie tego przypadku w ogólnym przypadku. Odpowiedź Dave'a jest doskonałym podsumowaniem metod algorytmicznych i ręcznych (w zależności od ludzkiego rozumu i metafory), które nie zawsze działają, ale są dość skuteczne.

computability formal-methods software-engineering software-verification Andres Riofrio
źródło
5
jak powiedział yuval, nie ma procedury, która mogłaby to ustalić dla dowolnych dwóch programów. ale w specjalnym przypadku, takim jak twój przykład, możesz to udowodnić: na przykład, jeśli udowodnisz, że oba algorytmy zwracają posortowaną sekwencję i są stabilne, zostaniesz skończony.
Sasho Nikolov
1
Czy potrzebujesz automatycznej techniki / algorytmu czy zestawu technik manualnych?
Dave Clarke
@SashoNikolov, jeśli wydajność jest uważana za część wyniku, musisz również pokazać, że oba działają w tej samej złożoności czasowo-przestrzennej.
edA-qa mort-ora-y
1
Masz na myśli „czek” czy udowodnienie? Czy oznacza „wszelkie dane wejściowe” czy wszystkie dane wejściowe? Jaka jest motywacja i kontekst pytania?
Kaveh
2
@AndresRiorio: Techniki sprawdzania różnią się od algorytmów, które rozwiązują ogólny problem. Na przykład problem zatrzymania jest nierozstrzygalny, ale z pewnością można udowodnić zakończenie wielu programów (ręcznie lub za pomocą automatycznej heurystyki).
Raphael

Odpowiedzi:

16

W przeciwieństwie do tego, co mówią nie-mówcy, istnieje wiele skutecznych technik, aby to zrobić.

  • Bisimulacja to jedno podejście. Zobacz na przykład artykuł Gordona na temat koindukcji i programowania funkcjonalnego .

  • Innym podejściem jest wykorzystanie operacyjnych teorii równoważności programów, takich jak praca Pittsa .

  • Trzecim podejściem jest sprawdzenie , czy oba programy spełniają tę samą specyfikację funkcjonalną. Istnieją tysiące artykułów na temat tego podejścia.

  • Czwarte podejście polega na pokazaniu, że jeden program można przepisać na inny za pomocą transformacji programu dźwiękowego .

Oczywiście żadna z tych metod nie jest kompletna z powodu nierozstrzygalności, ale w celu rozwiązania tego problemu opracowano wiele prac.

Dave Clarke
źródło
heurryzm . [Gr. εὑρίσκω „discover”] n. 1. Technika zaprojektowana w celu rozwiązania problemu, która ignoruje to, czy można udowodnić, że rozwiązanie jest poprawne, ale która zwykle daje dobre rozwiązanie lub rozwiązuje prostszy problem, który zawiera rozwiązanie problemu bardziej złożonego lub z nim się krzyżuje. 2. ( Teoria. ) Algorytm, który nie działa.
JeffE
1
Bart Simpson: „Nie mogę wygrać. Nie próbuj”.
Dave Clarke
9
@JeffE: Jeśli chcesz sprawdzić, czy dwa algorytmy zwracają ten sam wynik, robisz dowód. Istnieje wiele dobrych technik, aby to zrobić. Jasne, wszystkie metody są niekompletne, ale kogo to obchodzi? Twierdzenie Goedela o niekompletności nie jest powodem do rezygnacji z matematyki!
Neel Krishnaswami
3
@JeffE To, że nie ma funkcji obliczeniowej umożliwiającej ustalenie, czy dwa arbitralne algorytmy zwracają ten sam wynik, nie oznacza, że ​​nie można odpowiedzieć na pytanie dotyczące dwóch konkretnych algorytmów, zwłaszcza że proces wyszukiwania dowodu nie jest obliczalny funkcja . Podobnie istnieje mnóstwo dokumentów, które potwierdzają gwarantowane zakończenie dla poszczególnych algorytmów, niezależnie od faktu, że nie można mechanicznie ustalić, czy dowolny algorytm zawsze się zakończy.
Ben
2
W praktyce dwa algorytmy, które mają obliczać tę samą funkcję, prawie nigdy nie pozwalają na oparty na bisimulacji dowód równoważności. (W przypadku wyżej wspomnianych algorytmów sortowania pośrednie etapy pętli / rekurencji są różne.) Powiedziałbym, że używanie starej dobrej logiki Hoare'a w celu wykazania, że ​​obie implementują tę samą specyfikację zachowania We / Wy jest sposobem iść.
Kai
10

Aby rozwinąć nieco stwierdzenia „to niemożliwe”, oto prosty szkic dowodu.

Możemy modelować algorytmy z wyjściem przez maszyny Turinga, które zatrzymują się wraz z wyjściem na taśmie. Jeśli chcesz mieć maszyny, które mogą się zatrzymać, akceptując z wyjściem na taśmie lub odrzucając (w takim przypadku nie ma wyjścia), możesz łatwo wymyślić kodowanie, które pozwala modelować te maszyny za pomocą „zatrzymaj lub nie zatrzymuj”, nie ma maszyn odrzuconych.

Załóżmy teraz, że mam algorytm P do określania, czy dwie takie bazy TM mają takie same dane wyjściowe dla każdego wejścia. Następnie, biorąc pod uwagę TM A i wejście X , mogę zbudować nową TM B, która działa w następujący sposób:

  1. Sprawdź, czy dane wejściowe to dokładnie X
  2. Jeśli tak, wprowadź nieskończoną pętlę
  3. Jeśli nie, uruchom A na wejściu

Teraz mogę uruchomić P na A i B . B nie zatrzymuje się na X , ale ma takie samo wyjście jak A dla wszystkich innych danych wejściowych, więc jeśli i tylko jeśli A nie zatrzyma się na X, te dwa algorytmy mają takie same dane wyjściowe dla każdego wejścia. Ale założono, że P jest w stanie stwierdzić, czy dwa algorytmy mają takie same dane wyjściowe dla każdego wejścia, więc jeśli mielibyśmy P , moglibyśmy stwierdzić, czy dowolna maszyna zatrzymuje się na dowolnym wejściu, co stanowi problem zatrzymania. Ponieważ wiadomo, że problem zatrzymania jest nierozstrzygalny, P nie może istnieć.

Oznacza to, że nie ma ogólnego (obliczalnego) podejścia do ustalenia, czy dwa algorytmy mają takie same dane wyjściowe, które zawsze działają, więc musisz zastosować rozumowanie specyficzne dla pary analizowanych algorytmów. Jednak w praktyce mogą istnieć metody obliczeniowe, które działają dla dużych klas algorytmów, a z pewnością istnieją techniki, których można użyć, aby wypracować dowód na konkretny przypadek. Odpowiedź Dave'a Clarke'a daje ci kilka istotnych rzeczy do obejrzenia tutaj. Wynik „niemożliwości” dotyczy tylko opracowania ogólnej metody, która rozwiąże problem raz na zawsze, dla wszystkich par algorytmów.

Ben
źródło
P.
@Raphael Tak, naszkicowany przeze mnie argument nie mówi nic o tak ograniczonym P , tylko że nie może istnieć w pełni ogólny. Moją instynktem jest to, że problem zatrzymania jest wciąż nierozstrzygalny, nawet jeśli ograniczysz go do „algorytmów sortujących” zamiast algorytmów ogólnych, w którym to przypadku dowód niemożliwości nadal obowiązuje, chociaż nigdy nie słyszałem takiego twierdzenia.
Ben
2
Mówiąc bardziej ogólnie, twierdzenie Rice'a stwierdza, że ​​nie ma możliwego do obliczenia sposobu udowodnienia czegoś o algorytmie, gdy tylko istnieje co najmniej jeden algorytm, który ma właściwość, którą próbujesz udowodnić, i co najmniej taki, który tego nie robi. Na przykład, biorąc pod uwagę algorytm A, nie ma funkcji obliczeniowej, która przyjmuje algorytm B jako dane wejściowe i sprawdza, czy B jest równoważne A.
Gilles „SO- przestań być zły”
Należy zauważyć, że twierdzenie Rice'a dotyczy tylko właściwości języków , a nie maszyn Turinga (gdy używasz ich jako modelu „algorytmu”). Jeśli możliwe jest istnienie dwóch Maszyn Turinga, które rozpoznają ten sam język, ale jedna ma właściwość, a druga nie, to twierdzenie Rice'a nie ma zastosowania i może istnieć ogólna obliczalna metoda testowania właściwości. Ale twierdzenie Rice'a wyraźnie odnosi się do tej sprawy, tak.
Ben
2

Zasadniczo jest to niemożliwe, ale wiele ograniczeń może to umożliwić. Na przykład możesz sprawdzić równoważność dwóch programów kodu prostego za pomocą BDD. Wykonanie symboliczne może obsługiwać wiele innych przypadków.

James Koppel
źródło
1

Niemożliwe jest opracowanie algorytmu, który ogólnie potwierdza tę równość. Wskazówka: redukcja problemu zatrzymania.

Yuval Filmus
źródło
Istnieje wiele technik, ale żadna nie jest w pełni automatyczna.
Dave Clarke
Nie wiem, czy to możliwe, czy nie, twoja odpowiedź to tylko komentarz. nie odpowiedź.
@ SaeedAmiri: Przeszedłem nieco do kontekstu odpowiedzi; Myślę, że jest wystarczająco kompletny, jeśli nie może szczególnie dobry.
Raphael
@Raphael, Redukcja, która jest w umyśle Yuval, jest oczywista i nie sądzę, że OP nie jest tego świadomy, ale trudnym problemem IMO jest znalezienie sposobu na specjalne przypadki, więc ta oczywista redukcja może być komentarzem do przypomnienia OP w ogólnym przypadku.
2
@ SaeedAmiri: Decyzja należy do OP i wyborców, a nie my.
Raphael