Seite 1 von 1

Wiki: Algorithm and Correctness

Verfasst: 8. Mai 2016 10:29
von sqrt(2)
Hallo,

ist der Link https://wiki.algo.informatik.tu-darmsta ... orrectness nur über moodle erreichbar? Finde leider keinen Hyperlink auf der Startseite vom Algowiki.


Grüße

Re: Wiki: Algorithm and Correctness

Verfasst: 8. Mai 2016 13:06
von sqrt(2)
Hallo,

mir ist eine Frage aufgekommen. Im letzten Kapitel Induction in case of a recursion werden zwei mögliche Ansätze vorgestellt um die Korrektheit einer Rekursion zu beweisen.

Fall 2: So wir wir das bereits gemacht haben. Ist auch verständlich von der Logik her. Ich würde es unpräzise einfach so formulieren, dass man von oben nach unten geht.

Fall 1: Ich verstehe noch nicht ganz die Logik hinter dieser Art einen Beweis zu führen. Mein Verständnisproblem würde ich gerne anhand des, im Wiki angeführten Beispiels binary search erklären.

Problem:

Die Tiefe eines rekursiven Aufrufs ist die Induktionsvariable. Ich kann mir hier leider nichts darunter vorstellen wie man der Induktionsvariable eine "Tiefe" zuordnen kann. Ist es einfach ein leere Liste oder eine Liste mit nur einem Element?

Der Originalaufruf der Subroutine muss der Induktionsbasis gleichen. Also das zu suchende Element ist in dem gegebenen Array? (Aber es kann ja sein, dass das Element nicht im Array ist, dann würde man eine entsprechende Meldung erhalten?)

Induktionsschritt -> man verringert im reden Schritt das zu suchende Intervall.

Re: Wiki: Algorithm and Correctness

Verfasst: 8. Mai 2016 15:19
von Prof. Karsten Weihe
sqrt(2) hat geschrieben: ist der Link https://wiki.algo.informatik.tu-darmsta ... orrectness nur über moodle erreichbar? Finde leider keinen Hyperlink auf der Startseite vom Algowiki.
Sie können auf jeden Fall immer auch in die Suchleiste gehen.

KW

Re: Wiki: Algorithm and Correctness

Verfasst: 8. Mai 2016 15:38
von Prof. Karsten Weihe
sqrt(2) hat geschrieben: Die Tiefe eines rekursiven Aufrufs ist die Induktionsvariable. Ich kann mir hier leider nichts darunter vorstellen wie man der Induktionsvariable eine "Tiefe" zuordnen kann. Ist es einfach ein leere Liste oder eine Liste mit nur einem Element?
Die Induktionsvariable ist die ganzzahlige Variable, über die die vollständige Induktion durchgeführt wird. Bei Schleifen ist die Anzahl der Iterationen zweckmäßig. Bei manchen rekursiven Algorithmen wie etwa Mergesort und Quicksort ist es hingegen zweckmäßig, die Länge der Sequenz als Induktionsvariable zu nehmen. Ich denke, das ist meist der Ziel führende Ansatz, wenn die Invariante "das Ergebnis eines rekursiven Aufrufs ist korrekt" tragfähig für einen lückenlosen Beweis ist, wie das bei Mergesort und Quicksort der Fall ist.

Bei binärer Suche hingegen ist die folgende Invariante zweckmäßig (vgl. Wiki): "Falls das gesuchte Element im Array ist, dann ist es in dem Intervall zwischen linkem und rechtem Begrenzer." Das wird man wohl nicht analog zu Mergesort und Quicksort über die Länge des Intervalls als Induktionsvariable beweisen können. Statt dessen kann man sich aber klarmachen, dass die Aussage beim allerobersten rekursiven Aufruf trivial ist, denn das Intervall zwischen linkem und rechtem Begrenzer ist hier der gesamte Indexbereich des Arrays (=> Induktionsbasis). Genauso kann man sich klarmachen, dass diese Invariante durch die Fallunterscheidung erhalten bleibt, wenn der Prozess im Rekursionsbaum einen Schritt weiter hinabsteigt (=> Induktionsschritt).

Es ist also alles da für einen lückenlosen Beweis auf Basis einer vollständigen Induktion, es fehlt nur die Induktionsvariable. Die Induktionsvariable müsste so gewählt sein, dass sie ihren kleinsten Wert bei der Induktionsbasis annimmt und im Induktionsschritt wächst. Was käme in dieser spezifischen Situation dafür in Frage? Antwort: die Tiefe des rekursiven Aufrufs im Rekursionsbaum. 8)

Klarer geworden?

KW

Re: Wiki: Algorithm and Correctness

Verfasst: 9. Mai 2016 19:14
von sqrt(2)
Fast :D

Vielen Dank für die ausführliche Antwort. Ich werde nochmal schreiben wenn mir etwas unklar ist. Möchte aber vorher nochmal selbst drüber nachdenken mit Ihrer Erklärung.

Re: Wiki: Algorithm and Correctness

Verfasst: 20. Mai 2016 13:55
von Prof. Karsten Weihe
Ich habe selbst noch einmal darüber nachgedacht, unter welchen Umständen man die vollständige Induktion eigentlich über die Rekursionstiefe als Induktionsvariable führen kann, und habe meine Erleuchtung ins Wiki geschrieben: http://wiki.algo.informatik.tu-darmstad ... _recursion.

Zitat: "In case of a tail recursion, the induction proof for the equivalent loop may be transformed into a proof for the recursion. The depth of a recursive call is then the induction variable; the original call to this subroutine has to ensure the induction basis; the induction step has to be ensured by every descent in the recursion tree. Example: binary search."

KW