Wiki: Algorithm and Correctness

Bei Postings zu Vorlesungsthema X lassen Sie Ihr Betreff bitte mit "X: " beginnen, gefolgt von einer möglichst präzisen Überschrift, danke!

Moderator: Algorithmen und Datenstrukturen

Forumsregeln
Bei Postings zu Vorlesungsthema X lassen Sie Ihr Betreff bitte mit "X: " beginnen, gefolgt von einer möglichst präzisen Überschrift, danke!
Benutzeravatar
sqrt(2)
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 201
Registriert: 12. Apr 2015 11:35

Wiki: Algorithm and Correctness

Beitrag von sqrt(2) » 8. Mai 2016 10:29

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

Benutzeravatar
sqrt(2)
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 201
Registriert: 12. Apr 2015 11:35

Re: Wiki: Algorithm and Correctness

Beitrag von sqrt(2) » 8. Mai 2016 13:06

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.

Prof. Karsten Weihe
Moderator
Moderator
Beiträge: 1824
Registriert: 21. Feb 2005 16:33

Re: Wiki: Algorithm and Correctness

Beitrag von Prof. Karsten Weihe » 8. Mai 2016 15:19

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

Prof. Karsten Weihe
Moderator
Moderator
Beiträge: 1824
Registriert: 21. Feb 2005 16:33

Re: Wiki: Algorithm and Correctness

Beitrag von Prof. Karsten Weihe » 8. Mai 2016 15:38

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

Benutzeravatar
sqrt(2)
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 201
Registriert: 12. Apr 2015 11:35

Re: Wiki: Algorithm and Correctness

Beitrag von sqrt(2) » 9. Mai 2016 19:14

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.

Prof. Karsten Weihe
Moderator
Moderator
Beiträge: 1824
Registriert: 21. Feb 2005 16:33

Re: Wiki: Algorithm and Correctness

Beitrag von Prof. Karsten Weihe » 20. Mai 2016 13:55

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

Antworten

Zurück zu „AuD: Vorlesung“