Ein weiterer Induktionsbeweis (insertionSort aus V26)

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

Ein weiterer Induktionsbeweis (insertionSort aus V26)

Beitrag von sqrt(2) » 16. Sep 2016 13:10

Hallo,

ich wollte hier mal probieren einen Induktionsbeweis zum Algorithmus selectionSort aus der letzten Vorlesung (V26) durchzuführen.

Input:
- oldHead verweist auf den Kopf einer korrekt gebildeten linearen, doppelt verketteten Liste, die auch leer sein kann.
- Duplikate erlaubt

Output:
- Ohne Änderung der Key-Attribute wird die Eingabeliste aufsteigend nach den Key-Attributen umsortiert. Zurückgeliefert wird der Kopf dieser umsortierten Liste.

Wohldefiniertheit:
- Falls oldHead == NULL ist wird eine NullpointerException durch die if-Abfrage am Anfang abgefangen
- Keine ArithmethicException, da keine arithmetischen Operatoren verwendet werden
- In diesem Fall eher unwichtig, denn in der Klausur wird das weiter spezifiziert sein worauf man achten muss (sofern ich das richtig verstanden habe)

Terminierung:
- Die while-Schleife terminier sobald man das letzte Element der linearen Liste erreicht, aufgrund des korrekten Inputs existiert so ein Ende
- Die for-Schleife terminiert sobald der Pointer p == NULL ist

Variante:
- While-Schleife: searchMinFromHere iteriert nach jedem Schleifendurchlauf zum Schwanz der Liste oldHead
- For-Schleife: p verweist nach einer Iteration auf das nächste Listenelement

Invariante (= Induktionshypothese):
Nach i >= 0 Iterationen gilt:
1. das \(newHead\) auf eine korrekt gebildete Liste verweist
2. das\(searchMinFromHere\) ein Pointer auf das erste Element der unsortierten Teilliste von oldHead ist.
3. das \(elemWithMinValue\) auf das Element mit dem kleinsten Key der Teilliste von \(searchMinFromHere\) bis \(p\) verweist.
4. das \(p\) auf ein Element der unsortierten Teilliste von \(searchMinFromHere\) bis zum Schwanz von oldHead verweist.

Induktionsanfang:
Ist oldHead == NULL, so terminiert der Algorithmus und liefert null. Dies ist ein korrekter Output gemäß obiger Spezifikation.

Induktionsvoraussetzung:
Für n > 0 Iterationen gilt, dass 0,..., m Listenelemente aufsteigend nach ihren keys sortiert sind. Des Weitern gilt m < n.

Induktionsschritt:
Nach Induktionsvoraussetzung gilt, dass die Liste von Position 0 bis m korrekt sortiert ist. In dieser Iteration passiert nun, dass im Intervall von m + 1 bis zum Listenende (:= tail) das Listenelement mit dem minimalen Key gesucht wird. searchMinFromHere verweist auf das Listenelement mit Position m + 1. Sei k das kleinste Listenelment im oben genannten Intervall:
a. hat k die selbe Position wie searchMinFromHere, so befindet sich k an der richtigen Position und der Algorithmus beginnt mit der nächsten Iteration
b. ansonsten wird k von seiner position entfernt und vor die Position des Listenelements searchMinFromHere positioniert und der Algorithmus beginnt mit der nächsten Iteration

(Ist die Formulierung [1]"der Algorithmus beginnt mit der nächsten Iteration okay? und ist es korrekt [2]das Terminieren hier nicht zu erwähnen? letzteres wird ja in einem separaten Kapitel behandelt)

Korrektheit:
Wohldefiniertheit und Terminierung waren oben schon geklärt, korrektes Ergebnis der ausgelagerten rekursiven Methode folgt ohne weitere Argumente aus der Invariante.

Komplexitätsklasse:
Best Case:
- Dieser tritt ein wenn oldHead == NULL ist. Somit erhalten wir eine Komplexität von \(\Theta(1)\)
- Ist das \(\Theta\) zu begründen mit \({\cal O}(1)\) und \(\Omega(1)\)?
Worst Case:
- Im worst case muss der Algorithmus \(n\)-Mal mit der while-Schleife über alle \(n\) Elemente iterieren. Des weiteren iteriert die for-Schleife in den \(n\) Iterationen der while-Schleife von \(n\) bis \(tail\), wobei \(tail\) das letzte Element der Liste oldHead bezeichnen soll. Da sich das Intervall der for-Schleife nach jeder Iteration um ein Listenelement verkleinert, hat man (mit \(N\) = Länge der Liste) \(\sum_{i=n}^N N-i\) viele Iterationen und dies \(n\)-Mal. Wobei \(\sum_{i=n}^N N-i = (n^2 + n)/2\). Demnach erhält man \(\Theta(n*(n^2 + n)/2)\) als Komplexitätsklasse im worst Case.
EDIT: https://wiki.algo.informatik.tu-darmsta ... ction_sort das Wiki sagt leider was anderes. Demnach muss ich hier einen Denkfehler haben...
Zuletzt geändert von sqrt(2) am 17. Sep 2016 11:15, insgesamt 1-mal geändert.

Prof. Karsten Weihe
Dozentin/Dozent
Beiträge: 1824
Registriert: 21. Feb 2005 16:33

Re: Ein weiterer Induktionsbeweis (selectionSort aus V26)

Beitrag von Prof. Karsten Weihe » 17. Sep 2016 08:46

sqrt(2) hat geschrieben: Input:
- oldHead verweist auf den Kopf einer korrekt gebildeten linearen, doppelt verketteten Liste, die auch leer sein kann.
- Duplikate erlaubt
Ok.
sqrt(2) hat geschrieben: Output:
- Ohne Änderung der Key-Attribute wird die Eingabeliste aufsteigend nach den Key-Attributen umsortiert. Zurückgeliefert wird der Kopf dieser umsortierten Liste.
Gut formuliert: Seiteneffekt und dann Rückgabewert!
sqrt(2) hat geschrieben: Wohldefiniertheit:
- Falls oldHead == NULL ist wird eine NullpointerException durch die if-Abfrage am Anfang abgefangen
Ok.
sqrt(2) hat geschrieben: - Keine ArithmethicException, da keine arithmetischen Operatoren verwendet werden
- In diesem Fall eher unwichtig, denn in der Klausur wird das weiter spezifiziert sein worauf man achten muss (sofern ich das richtig verstanden habe)
Yep.
sqrt(2) hat geschrieben: Terminierung:
- Die while-Schleife terminier sobald man das letzte Element der linearen Liste erreicht, aufgrund des korrekten Inputs existiert so ein Ende
- Die for-Schleife terminiert sobald der Pointer p == NULL ist
Ich nehme an, Sie betrachten hier die innere Schleife (die das Maximum unter den verbleibenden Schlüsselwerten sucht) und die äußere Schleife zusammen? Mein dringender Vorschlag ist, die innere Schleife als einen eigenen Algorithmus zu behandeln und diesen auch zu benennen, z.B. maxVonVerbleibenden. Das macht sowohl den Code als auch den Beweis übersichtlicher (ok, habe ich in der Vorlesung wohl nicht gemacht...).
sqrt(2) hat geschrieben: Variante:
- While-Schleife: searchMinFromHere iteriert nach jedem Schleifendurchlauf zum Schwanz der Liste oldHead
Was heißt das?

Aus bekannten pubertärsprachlichen Gründen würde ich im Deutschen eher vom Ende der Liste sprechen (ist natürlich für die Klausur egal). :wink:
sqrt(2) hat geschrieben: - For-Schleife: p verweist nach einer Iteration auf das nächste Listenelement
Ok.
sqrt(2) hat geschrieben: Invariante (= Induktionshypothese):
Nach i >= 0 Iterationen gilt:
1. das \(newHead\) auf eine korrekt gebildete Liste verweist
2. das\(searchMinFromHere\) ein Pointer auf das erste Element der unsortierten Teilliste von oldHead ist.
Hmh, die grundlegende Information an den Leser, die für das Verständnis sicher notwendig ist, schreiben Sie gar nicht: Die größten i Elemente in der LIste sind schon auf ihren korrekten Positionen am Ende der LIste (insbesondere aufsteigend sortiert).

Die Zustände aller Variablen sind wichtig, aber dazu gehört eben auch die Liste selbst, nicht nur die Pointer auf Listenelemente.

Vielleicht modifizieren Sie die Formulierung Ihres Korrektheitsbeweises erst dahingehend?
sqrt(2) hat geschrieben: Komplexitätsklasse:
Best Case:
- Dieser tritt ein wenn oldHead == NULL ist. Somit erhalten wir eine Komplexität von \(\Theta(1)\)
Ist das bei Ihnen der Fall, dass die Eingabeliste leer ist? Dazu hatte ich schon hier etwas geschrieben: https://www2.fachschaft.informatik.tu-d ... EN#p171982 (suchen Sie nach NEIEN).

KW

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

Re: Ein weiterer Induktionsbeweis (selectionSort aus V26)

Beitrag von sqrt(2) » 17. Sep 2016 11:44

Prof. Karsten Weihe hat geschrieben:
sqrt(2) hat geschrieben: Terminierung:
- Die while-Schleife terminier sobald man das letzte Element der linearen Liste erreicht, aufgrund des korrekten Inputs existiert so ein Ende
- Die for-Schleife terminiert sobald der Pointer p == NULL ist
Ich nehme an, Sie betrachten hier die innere Schleife (die das Maximum unter den verbleibenden Schlüsselwerten sucht) und die äußere Schleife zusammen? Mein dringender Vorschlag ist, die innere Schleife als einen eigenen Algorithmus zu behandeln und diesen auch zu benennen, z.B. maxVonVerbleibenden. Das macht sowohl den Code als auch den Beweis übersichtlicher (ok, habe ich in der Vorlesung wohl nicht gemacht...).
Alles klar.
Prof. Karsten Weihe hat geschrieben:
sqrt(2) hat geschrieben: Invariante (= Induktionshypothese):
Nach i >= 0 Iterationen gilt:
1. das \(newHead\) auf eine korrekt gebildete Liste verweist
2. das\(searchMinFromHere\) ein Pointer auf das erste Element der unsortierten Teilliste von oldHead ist.
Hmh, die grundlegende Information an den Leser, die für das Verständnis sicher notwendig ist, schreiben Sie gar nicht: Die größten i Elemente in der LIste sind schon auf ihren korrekten Positionen am Ende der LIste (insbesondere aufsteigend sortiert).

Die Zustände aller Variablen sind wichtig, aber dazu gehört eben auch die Liste selbst, nicht nur die Pointer auf Listenelemente.

Vielleicht modifizieren Sie die Formulierung Ihres Korrektheitsbeweises erst dahingehend?
Berichtigung:
Invariante:
Nach i >= 0 Iterationen gilt:
1. das \(newHead\) auf eine korrekt gebildete Liste verweist
2. das\(searchMinFromHere\) ein Pointer auf das erste Element der unsortierten Teilliste von oldHead ist.
3. das \(elemWithMinValue\) auf das Element mit dem kleinsten Key der Teilliste von \(searchMinFromHere\) bis \(p\) verweist.
4. das \(p\) auf ein Element der unsortierten Teilliste von \(searchMinFromHere\) bis zum Schwanz von oldHead verweist.
5. das die kleinsten i Elemente in der Liste aufsteigend und an ihren korrekten Positionen am Ende der Liste sortiert stehen. (Danke!)

Induktionsschritt:
Nach Induktionsvoraussetzung gilt, dass die Listenelemente von 0 bis i korrekt und aufsteigend nach ihren Schlüsselwerten sortiert sind. In dieser Iteration liefert die for-Schleife das kleinste Listenelement k aus der unsortierten Teilliste von i + 1 bis tail (sollte ja als eigener Algorithmus betrachtet werden. Setze hier jetzt voraus, dass dies so korrekt schon bewiesen wurde). Das kleinste Listenelement k wird nun unmittelbar an das Ende der sortierten Teilliste angefügt, sofern es sich noch nicht an dieser Position (i+1) befindet. Nach i = n Iterationen terminiert der Algorithmus und liefert den Kopf der korrekt sortierten Teilliste zurück.
Prof. Karsten Weihe hat geschrieben:
sqrt(2) hat geschrieben: Komplexitätsklasse:
Best Case:
- Dieser tritt ein wenn oldHead == NULL ist. Somit erhalten wir eine Komplexität von \(\Theta(1)\)
Ist das bei Ihnen der Fall, dass die Eingabeliste leer ist? Dazu hatte ich schon hier etwas geschrieben: https://www2.fachschaft.informatik.tu-d ... EN#p171982 (suchen Sie nach NEIEN).
Wenn die lineare Liste bereits sortiert ist wäre der best case. Komplexität wäre dann bei \(\Omega(1)\) oder liege ich jetzt wieder falsch? Denn man kann ja eine sortierte Liste mit \(10^{100}\) Elementen haben und da müsste man ja jedes Element betrachten, deshalb \(\Omega(1)\)...

Prof. Karsten Weihe
Dozentin/Dozent
Beiträge: 1824
Registriert: 21. Feb 2005 16:33

Re: Ein weiterer Induktionsbeweis (selectionSort aus V26)

Beitrag von Prof. Karsten Weihe » 17. Sep 2016 19:24

sqrt(2) hat geschrieben: Invariante:
Nach i >= 0 Iterationen gilt:
1. das \(newHead\) auf eine korrekt gebildete Liste verweist
2. das\(searchMinFromHere\) ein Pointer auf das erste Element der unsortierten Teilliste von oldHead ist.
3. das \(elemWithMinValue\) auf das Element mit dem kleinsten Key der Teilliste von \(searchMinFromHere\) bis \(p\) verweist.
4. das \(p\) auf ein Element der unsortierten Teilliste von \(searchMinFromHere\) bis zum Schwanz von oldHead verweist.
5. das die kleinsten i Elemente in der Liste aufsteigend und an ihren korrekten Positionen am Ende der Liste sortiert stehen.
Meinen Sie nicht, dass dem Leser das Verständnis leichter fällt, wenn Sie Punkt 5 zu Punkt 1 machen und dann noch dazuschreiben, dass die "unsortierte Teilliste" aus allen Elementen vor den letzten i besteht?

Zudem wird mir als Leser nicht der Zusammenhang klar: Zeigen die Pointer nun auf Elemente aus unterschiedlichen Listen oder aus derselben Liste?
sqrt(2) hat geschrieben: Komplexitätsklasse:
Best Case:
Wenn die lineare Liste bereits sortiert ist wäre der best case. Komplexität wäre dann bei \(\Omega(1)\)
Also, in jedem Fall - also auch im Best und Worst Case gleichermaßen - wird die äußere Schleife (n-1)-mal durchlaufen, und in der i-ten Iteration der äußeren Schleife durchläuft die innere Schleife n-i+1 Positionen, oder?

Damit komme ich doch immer auf \(\Theta(n^2)\).

KW

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

Re: Ein weiterer Induktionsbeweis (selectionSort aus V26)

Beitrag von sqrt(2) » 17. Sep 2016 20:02

Prof. Karsten Weihe hat geschrieben:
sqrt(2) hat geschrieben: Invariante:
Nach i >= 0 Iterationen gilt:
1. das \(newHead\) auf eine korrekt gebildete Liste verweist
2. das\(searchMinFromHere\) ein Pointer auf das erste Element der unsortierten Teilliste von oldHead ist.
3. das \(elemWithMinValue\) auf das Element mit dem kleinsten Key der Teilliste von \(searchMinFromHere\) bis \(p\) verweist.
4. das \(p\) auf ein Element der unsortierten Teilliste von \(searchMinFromHere\) bis zum Schwanz von oldHead verweist.
5. das die kleinsten i Elemente in der Liste aufsteigend und an ihren korrekten Positionen am Ende der Liste sortiert stehen.
Meinen Sie nicht, dass dem Leser das Verständnis leichter fällt, wenn Sie Punkt 5 zu Punkt 1 machen und dann noch dazuschreiben, dass die "unsortierte Teilliste" aus allen Elementen vor den letzten i besteht?

Zudem wird mir als Leser nicht der Zusammenhang klar: Zeigen die Pointer nun auf Elemente aus unterschiedlichen Listen oder aus derselben Liste?
sqrt(2) hat geschrieben: Komplexitätsklasse:
Best Case:
Wenn die lineare Liste bereits sortiert ist wäre der best case. Komplexität wäre dann bei \(\Omega(1)\)
Also, in jedem Fall - also auch im Best und Worst Case gleichermaßen - wird die äußere Schleife (n-1)-mal durchlaufen, und in der i-ten Iteration der äußeren Schleife durchläuft die innere Schleife n-i+1 Positionen, oder?

Damit komme ich doch immer auf \(\Theta(n^2)\).
Ja, stimme beidem zu. Danke (:

Antworten

Zurück zu „Archiv“