Pisanie dowodu na algorytm

Question

Witam faceci próbuję porównać 2 algorytmy i pomyślałem, że mogę spróbować napisać dla nich dowód !!! (Moje matematyki bani więc stąd to pytanie)

Normalnie w naszej lekcji matematyki w ubiegłym roku chcielibyśmy mieć takie pytanie

udowodnić: (2r + 3) = n (n + 4)

następnie Zrobiłbym potrzebne 4 sceny i dostaję odpowiedź na końcu

Gdzie utknąłem udowadniając prims i Kruskals - jak mogę dostać te algorytmy w formie takiej jak matematyczne powyżej, więc mogę udowodnić

uwaga: nie pytam ludzi o ans wer to dla mnie - po prostu mi pomóc go do formularza, gdzie mogę mieć go sobie

dzięki

Answer 1

Nie dać wiele szczegółów, ale jest społeczność matematyków (Mathematical Knowledge Management MKM) którzy opracowali narzędzia do obsługi komputerowych dowodów matematyki. Patrz, na przykład:

http://imps.mcmaster.ca/

i ostatnią konferencję

http://www.orcca.on.ca/conferences/cicm09/mkm09/

Answer 2

z mojego klas matematycznych w Uni I (niejasno) pamiętać udowadniając Prims i algorytmy Kruskals - i nie atakują pisząc to w formie matematycznej. Zamiast tego, wypróbuj sprawdzone teorie dla wykresów i połącz je np. http://en.wikipedia.org/wiki/Prim%27s_algorithm#Proof_of_correctness, aby zbudować dowód.

Jeśli chcesz udowodnić złożoność, to po prostu działanie algorytmu to O (n^2). Istnieją pewne optymalizacje dla specjalnego przypadku, w którym wykres jest rzadki, co może zmniejszyć to do O (nlogn).

Answer 3

gdzie jestem zatrzymany okazuje Prims i Kruskals - jak mogę dostać te algorytmy w celu formie jak w matematycznym jeden powyżej, aby można było przystąpić do udowodnienia

Nie sądzę, można bezpośrednio. Zamiast tego udowodnij, że oba generują MST, a następnie udowodnij, że dowolne dwa MST są równe (lub równoważne, ponieważ możesz mieć więcej niż jeden MST dla niektórych wykresów). Jeśli oba algorytmy generują MST, które są równoważne, algorytmy są równoważne.

Answer 4

Aby udowodnić poprawności algorytmu, zazwyczaj trzeba pokazać (a), że kończy i (b) że produkt spełnia zdawczego specyfikacja co próbujesz zrobić. Te dwa dowody będą dość różne od algebraicznych dowodów, o których wspomniałeś w swoim pytaniu. Kluczową koncepcją, której potrzebujesz, jest mathematical induction. (Jest to recursion dla proofów.)

Jako przykład podajemy quicksort.

Aby udowodnić, że zawsze kończy quicksort, byś najpierw pokazać, że kończy się na wejściu długości 1. (To jest trywialnie prawdziwe). Następnie pokazują, że jeśli kończy się na wejściu długości do n, to będzie zacisku dla wejścia długości n + 1. Dzięki indukcja, to wystarczy, aby udowodnić, że algorytm kończy się dla wszystkich danych wejściowych.

Aby udowodnić, że quicksort jest poprawny, należy przekonwertować specyfikację sortowania porównania na precyzyjny język matematyczny. Chcemy wyjście być permutation wejścia tak, że jeśli i ≤ j następnie w _í ≤ _j. Udowodnienie, że wyjście quicksort jest permutacją wejścia jest łatwe, ponieważ zaczyna się od elementów wejściowych i po prostu zamienia. Udowodnienie drugiej właściwości jest trochę trudniejsze, ale znowu możesz użyć indukcji.

Answer 5

W większości przypadków dowód zależy od problemu, który masz w dłoni. Prosty argument może być wystarczający w niektórych momentach, w innych przypadkach może być potrzebny rygorystyczny dowód. Kiedyś użyłem następstwa i dowód na udowodnione już twierdzenie, które uzasadnia mój algorytm, jest właściwy. Ale to jest na projekt uczelni.

Answer 6

Może chcesz wypróbować półautomatyczną metodę sprawdzania. Po prostu przejdźmy do czegoś innego;) Na przykład, jeśli posiadasz specyfikację Java algorytmów Prim i Kruskala, optymalnie opierając się na tym samym modelu wykresu, możesz użyć KeY Prover, aby udowodnić równoważność algorytmu.

Najważniejszą częścią jest sformalizowanie zobowiązania dowodowego w Dynamic Logic (jest to rozszerzenie logiki pierwszego rzędu z typami i sposobami symbolicznego wykonywania programów Java). Formuła udowodnić mógł dopasować następujący wzór (szkicowy):

\forall Graph g. \exists Tree t. 
    (<{KRUSKAL_CODE_HERE}>resultVar1=t) <-> (<{PRIM_CODE_HERE}>resultVar2=t) 

Wyraża że dla wszystkich wykresach, oba algorytmy zakończyć, a wynik jest taki sam drzewo.

Jeśli masz szczęście, a twoja formuła (i implementacje algorytmów) mają rację, to KeY może to dla Ciebie automatycznie sprawdzić. Jeśli nie, może być konieczne utworzenie pewnych zmiennych ilościowych, co powoduje konieczność sprawdzenia poprzedniego drzewa próbnego.

Po sprawdzeniu tego w KeY, możesz być szczęśliwy, że nauczyłeś się czegoś lub spróbować zrekonstruować ręczny dowód z proofa KeY - może to być żmudne zadanie, ponieważ KeY zna wiele zasad specyficznych dla Javy, które nie są łatwe do zrozumienia. Być może jednak możesz zrobić coś takiego, jak wyodrębnienie kombinacji Herbranda z pojęć, które KeY użył do utworzenia kwantyfikatorów egzystencjalnych po prawej stronie sekwencji w dowodzie.

Myślę, że kluczem jest interesującym narzędziem więcej ludzi powinno przyzwyczaić do udowodnienia krytycznej kodu Java przy użyciu narzędzi takich jak to;)