Przykład algorytmu bez dowodu poprawności

Mamy logikę Hoare'a. Dlaczego wciąż jest możliwe, że algorytm ma rację, ale nie ma dowodów na jego poprawność? Załóżmy, że algorytm jest wyrażony w C. Następnie możemy argumentować krok po kroku, że robi to, co powinien.

Więc moje pytanie brzmi:

Podaj przykład algorytmu, który jest odpowiedni, ale nie ma dowodu poprawności.

EDYCJA: Myślę, że trochę tła może pomóc wyjaśnić, dokąd zmierzam. Pozwól, że zacytuję Scott Aaronson:

Od lat siedemdziesiątych pojawiły się spekulacje, że P NP może być niezależny (to znaczy nie do udowodnienia ani obalenia) od standardowych systemów aksjomatów dla matematyki, takich jak teoria mnogości Zermelo-Fraenkla. Dla jasności oznaczałoby to również jedno$\ne$

1. algorytm wielomianowy dla problemów z kompletnym NP nie istnieje, ale nigdy nie możemy tego udowodnić (przynajmniej nie w naszych zwykłych systemach formalnych), albo

2. algorytm wielomianowy czasu dla problemów NP-zupełny nie istnieją, ale też nie możemy udowodnić, że to działa, czy nie możemy udowodnić, że zatrzymuje się w czasie wielomianowym.

Mam na myśli drugą możliwość. Ponieważ Aaronson może tak pewnie wymienić tę możliwość, myślę, że musi istnieć przykład typu 2. Dlatego zadaję to pytanie. Ale wydaje się, że szybka i jasna odpowiedź nie jest widoczna.

Oto algorytm funkcji tożsamości:

• Dane wejściowe: $n$
• Sprawdź, czy ty ciąg binarny koduje dowód 0 > 1 w ZFC, a jeśli tak, wyślij n + $n$$0 > 1$$n+1$
• W przeciwnym razie wyjdź $n$

Większość ludzi podejrzewa, że ​​ten algorytm oblicza funkcję tożsamości, ale nie wiemy i nie możemy tego udowodnić w powszechnie przyjętym środowisku matematycznym, ZFC .

Większość algorytmów nie została udowodniona w logice Hoare'a. Głównym powodem jest to, że takie dowody poprawności są wyjątkowo drogie od stycznia 2017 r., Prawdopodobnie o kilka rzędów wielkości w porównaniu z „zwykłym” programowaniem. Trwa wiele prac nad obniżeniem tego kosztu dzięki automatyzacji, ale jest to trudna walka.

Innym powodem, dla którego algorytm może nie mieć dowodu poprawności, a który jest bardziej odpowiedni w praktyce niż zjawiska niekompletności, o których wspominali Yuval i chi, jest to, że możemy nie wiedzieć, czym jest ta specyfikacja. Ten problem ma dwa wymiary.

• Klienci nie wiedzą, czego chcą. Jest to dobrze znany problem w inżynierii oprogramowania, a inżynierowie oprogramowania opracowali wiele sposobów rozwiązania tego problemu.

• $n$przekraczające liczby naturalne, a przeciwnicy to wielomianowe probabilistyczne maszyny Turinga. Według mojej najlepszej wiedzy (proszę mnie poprawić, jeśli się mylę) istnieje rozbieżność między teorią a praktyką, a konkretne algorytmy, takie jak AES i SHA256, nie mieszczą się w zakresie tych teoretycznych specyfikacji. Nie sądzę, aby istniała pełna specyfikacja takich algorytmów, dlatego w zasadzie nie możemy ich zweryfikować w sensie np. Logiki Hoare'a.

Jest to związane z niekompletnością podstawowej logiki. Rzeczywiście, logika Hoare'a zawiera zwykle zasadę osłabienia lub „post-post”

$P(n)$$P(0)$$P(1)$$P(2)$$\forall n\in \mathbb{N}.\ P(n)$

$M$$n$$P(n)$$M$$\forall n.\ P(n)$$M$$\forall n.\ P(n)$

Problem: Wydrukuj „Tak”, jeśli każda liczba parzysta ≥ 4 jest sumą dwóch liczb pierwszych, i „Nie”, jeśli liczba parzysta ≥ 4 nie jest sumą dwóch liczb pierwszych.

Algorytm: Drukuj „Tak”

Większość ludzi uważa, że ​​algorytm jest poprawny. Nie jest znane dowód, i to jest całkiem możliwe, że nie ma żadnego dowodu.

Każdy algorytm, który jest poprawny, ale nie wiemy, ile czasu zajmuje jego uruchomienie, można przekształcić w algorytm, który zatrzymuje się w gwarantowanym czasie, ale nie jesteśmy pewni, czy jest poprawny.

$n$$n+1$$0$$\log(n)^2$$0$$\sqrt{n}$

$P=NP$