Seite 1 von 1

Ein perfekter Induktionsbeweis?

Verfasst: 15. Sep 2016 11:42
von sqrt(2)
Hallo,

ich habe mir nochmal Mühe bei einem rekursiven Induktionsbeweis gegeben und probiert die Dinge gemäß Vorlagen und Beispiele auf den Punkt zu bringen. Der Code prüft die Verzeigerungsstruktur eines Multi-Way-Trees.

Code: Alles auswählen

public boolean isTreeCorrect(TreeNode<T> r) {
	if (r == null)
		return true;
	HashSet<TreeNode<T>> set = new HashSet<TreeNode<T>>();
	return isTreeCorrectRec(r, set);
}

public boolean isTreeCorrectRec(TreeNode<T> m, HashSet<TreeNode<T>> set) {
	if (!set.add(m))
		return false;
		
	if (m.theSuccessors != null)
		for (int i = 0; i <= theSuccessors.length; i++)
			if (!isTreeCorrectRec(theSuccessors[i], set))
				return false;
	
	return true:	
}
Ich habe mich nun an die Reihenfolge vom Muster-Word-Dokument gehalten...



Induktionsbeweis:

Input:
- m != null
- Eine korrekte HashSet

Output:
- True, falls die Verzeigerungsstruktur des Vielwegbaums korrekt gebildet ist
- False, falls dem nicht so ist.

Invariante:
Unmittelbar nach einem rekursiven Schritt liefert der Algorithmus true, wenn m ein korrekt verzeigerter Knoten in einem Vielwegbaum ist. Andernfalls liefert der Algorithmus false und bricht die komplette Rekursion ab.

Induktionsparameter:
- Höhe eines Teilbaums

Induktionsanfang:
Besteht der Vielwegbaum lediglich aus der Wurzel, dann ist m.theSuccessors == NULL, so bricht die Rekursion ab und der Algorithmus liefert true.

Induktionsvoraussetzung:
Sei n > 0 die höhe eines Teilbaums. Für die Höhe m (wobei 0 <= m < n gilt) eines Teilbaums ist dieser Teilbaum ein korrekt verzeigerter Vielwegbaum.

Induktionsschritt:
Nach der Induktionsvoraussetzung gilt für einen Teilbaum \(T'\) von \(T\), dass \(T'\) korrekt gebildet ist. In diesem rekursiven Schritt wird nun, ein Knoten \(v \in U, U := T \backslash T'\) betrachtet. Ist \(v\) bereits in der HashSet enthalten (also der Menge der bereits gesichteten Knoten), bricht die komplette Rekursion ab und der Algorithmus liefert false, da \(U \bigcap T' = \emptyset\) gilt für eine korrekte Verzeigerungsstruktur. Andernfalls wird \(v\) der HashSet hinzugefügt und der Algorithmus überprüft für die Nachfolger von \(v\) ob diese richtig gebildet wurden.

Wohldefiniertheit:
- Keine ArithmeticException, da keine Arithmetischen Operationen durchgeführt werden
- Keine NullpointerException, da m != NULL
- Kein Überlauf oder NaN

Terminierung:
Der Algorithmus terminiert, da der Baum endliche Tiefe besitzt und nach jedem rekursiven Aufruf eine ebene Tiefer in den Baum gegangen wird. Besitzt der Baum eine falsche Verzeigerungsstruktur, so terminiert der Algorithmus vorzeitig.

Korrektheit:
Aus Invariante und Abbruchbedingung folgt die Korrektheit des Algorithmus. (Hier weiß ich nicht was ich noch schreiben könnte. Im Muster steht, dass man bei Rekursionen die in eigene Methoden ausgelagert werden Zusatzargumente benötigt werden :roll:



Komplexität:

Best Case:
Im Best Case ist m.theSuccessors == NULL und wir erhalten somit \(O(1)\).

Worst Case
Es handelt sich um einen korrekt gebildeten Vielwegbaum. Somit muss jeder Knoten betrachtet werden und wir erhalten \(O(n)\).

Re: Ein perfekter Induktionsbeweis?

Verfasst: 15. Sep 2016 20:14
von Prof. Karsten Weihe
sqrt(2) hat geschrieben: Input:
- m != null
- Eine korrekte HashSet
Ok.
sqrt(2) hat geschrieben: Output:
- True, falls die Verzeigerungsstruktur des Vielwegbaums korrekt gebildet ist
- False, falls dem nicht so ist.
Welches Vielwegbaumes?

Es hat sich eingebürgert so etwas zu formulieren wie: "der (Teil)baum mit Wurzel m". Ich denke, das ist eine sinnvolle Sprechweise (Ihre ist natürlich nicht falsch).
sqrt(2) hat geschrieben: Invariante:
Unmittelbar nach einem rekursiven Schritt liefert der Algorithmus true, wenn m ein korrekt verzeigerter Knoten in einem Vielwegbaum ist. Andernfalls liefert der Algorithmus false und bricht die komplette Rekursion ab.
Hier zeigt sich meines Erachtens die Sinnhaftigkeit der obigen Sprechweise, denn hier könnten Sie so etwas schreiben wie: "wenn die (Teil)struktur mit Wurzel m ein korrekter Vielwegbaum ist".

Es fehlt in der Invariante aber noch eine Aussage zum Hashset, nämlich was der Inhalt in dem betrachteten Moment ist. Eine solche Aussage setzen Sie weiter unten im Induktionsschritt stillschweigend voraus, arbeiten sie aber nicht heraus.
sqrt(2) hat geschrieben: Induktionsparameter:
- Höhe eines Teilbaums
Erscheint mir sehr sinnvoll.
sqrt(2) hat geschrieben: Induktionsanfang:
Besteht der Vielwegbaum lediglich aus der Wurzel, dann ist m.theSuccessors == NULL, so bricht die Rekursion ab und der Algorithmus liefert true.
Ok.

Man könnte (muss nicht) Ihre Formulierung zur Klarstellung noch leicht erweitern: "und der Algorithmus liefert korrekterweise true" o.ä.
sqrt(2) hat geschrieben: Induktionsvoraussetzung:
Sei n > 0 die höhe eines Teilbaums. Für die Höhe m (wobei 0 <= m < n gilt) eines Teilbaums ist dieser Teilbaum ein korrekt verzeigerter Vielwegbaum.
Nein, die Induktionsvoraussetzung, auf der Sie Ihren Induktionsschritt aufbauen können, ist etwas anderes: Für die von Ihnen spezifizierte Höhe m liefert die Methode das korrekte Ergebnis true/false (und zwar auch dann, wenn der Teilbaum im Gegensatz zu Ihrer Formulierung kein korrekt verzeigerter Vielwegbaum ist).
sqrt(2) hat geschrieben: Induktionsschritt:
Nach der Induktionsvoraussetzung gilt für einen Teilbaum \(T'\) von \(T\), dass \(T'\) korrekt gebildet ist.
Nein, siehe obige Anmerkung zu Ihrer Induktionsvoraussetzung: Nach Induktionsvoraussetzung liefert die Methode das korrekte Ergebnis true/false zurück.
sqrt(2) hat geschrieben: In diesem rekursiven Schritt wird nun, ein Knoten \(v \in U, U := T \backslash T'\) betrachtet. Ist \(v\) bereits in der HashSet enthalten
Siehe meine Anmerkung oben zu Ihrer Invariante und der fehlenden Aussage zum momentanen Inhalt der HashSet.
sqrt(2) hat geschrieben: Wohldefiniertheit:
- Keine ArithmeticException, da keine Arithmetischen Operationen durchgeführt werden
- Keine NullpointerException, da m != NULL
- Kein Überlauf oder NaN
NaN wäre ja kein Fehler, sondern ist nach IEEE 754 ein wohldefinierter Wert. Und dass es keinen Überlauf gibt, ist ja im Prinzip schon in Ihrem ersten Punkt enthalten.
sqrt(2) hat geschrieben: Terminierung:
Der Algorithmus terminiert, da der Baum endliche Tiefe besitzt und nach jedem rekursiven Aufruf eine ebene Tiefer in den Baum gegangen wird. Besitzt der Baum eine falsche Verzeigerungsstruktur, so terminiert der Algorithmus vorzeitig.
Kann man sicher so schreiben, oder kürzer: Aus der Variante folgt Rekursionsabbruch nach endlich vielen Schritten, fertig (ohne Fallunterscheidung).
sqrt(2) hat geschrieben: Korrektheit:
Aus Invariante und Abbruchbedingung folgt die Korrektheit des Algorithmus.
Unmissverständlicher: Wohldefiniertheit und Terminierung waren oben schon geklärt, korrektes Ergebnis der ausgelagerten rekursiven Methode folgt ohne weitere Argumente aus der Invariante.
sqrt(2) hat geschrieben: (Hier weiß ich nicht was ich noch schreiben könnte. Im Muster steht, dass man bei Rekursionen die in eigene Methoden ausgelagert werden Zusatzargumente benötigt werden :roll:
Eigentlich ist das ein gutes Beispiel für diese Zusatzargumente, nämlich:
1. Durch die if-Anweisung wird das für den allerersten Aufruf der rekursiven Methode gewährleistet, was Sie oben irgendwo voraussetzen: m != null.
2. Das HashSet, das beim allerersten Aufruf übergeben wird, ist ist leer \(\rightarrow\) Die zusätzliche Aussage zur HashSet in der Invariante ist initial korrekt.
sqrt(2) hat geschrieben: Komplexität:
Best Case:
Im Best Case ist m.theSuccessors == NULL und wir erhalten somit \(O(1)\).
NEIEN!!!

Sowohl Worst als auch Best Case sind Funktionen in der Knotenzahl des Baumes. Der Best Case tritt also nicht ein, wenn die Knotenzahl kleinstmöglich ist, sondern für jede Knotenzahl gibt es einen Best Case.

Der ist in diesem Fallbeispiel aber tatsächlich \({\cal O}(1)\), aber aus einem anderen Grund: Für eine Struktur mit n Knoten ist die Laufzeit kleinstmöglich, wenn schon ganz oben ein Fehler entdeckt wird, weil die Methode dann nicht mehr weiter hinabsteigt.

KW

Re: Ein perfekter Induktionsbeweis?

Verfasst: 15. Sep 2016 21:19
von sqrt(2)
Naja, da ist noch viel Verbesserungspotenzial. Schonmal vielen Dank für Ihr Feedback.
Prof. Karsten Weihe hat geschrieben:
sqrt(2) hat geschrieben: Komplexität:
Best Case:
Im Best Case ist m.theSuccessors == NULL und wir erhalten somit \(O(1)\).
NEIEN!!!

Sowohl Worst als auch Best Case sind Funktionen in der Knotenzahl des Baumes. Der Best Case tritt also nicht ein, wenn die Knotenzahl kleinstmöglich ist, sondern für jede Knotenzahl gibt es einen Best Case.

Der ist in diesem Fallbeispiel aber tatsächlich \({\cal O}(1)\), aber aus einem anderen Grund: Für eine Struktur mit n Knoten ist die Laufzeit kleinstmöglich, wenn schon ganz oben ein Fehler entdeckt wird, weil die Methode dann nicht mehr weiter hinabsteigt.
Peinlicher Fehler... :oops: Danke für den Hinweis

____

Den Rest werde ich soweit berücksichtigen. Hier noch zum Induktionsschritt paar Fragen.
____
Prof. Karsten Weihe hat geschrieben: Nein, die Induktionsvoraussetzung, auf der Sie Ihren Induktionsschritt aufbauen können, ist etwas anderes: Für die von Ihnen spezifizierte Höhe m liefert die Methode das korrekte Ergebnis true/false (und zwar auch dann, wenn der Teilbaum im Gegensatz zu Ihrer Formulierung kein korrekt verzeigerter Vielwegbaum ist).
Verstanden.
Prof. Karsten Weihe hat geschrieben: Nein, siehe obige Anmerkung zu Ihrer Induktionsvoraussetzung: Nach Induktionsvoraussetzung liefert die Methode das korrekte Ergebnis true/false zurück.
Berichtigung Induktionsschritt 1/2:
Nach der Induktionsvoraussetzung gilt für einen Teilbaum \(T'\) von \(T\), dass der Algorithmus für \(T'\) ein korrektes Ergebnis liefert.
Prof. Karsten Weihe hat geschrieben:
sqrt(2) hat geschrieben: In diesem rekursiven Schritt wird nun, ein Knoten \(v \in U, U := T \backslash T'\) betrachtet. Ist \(v\) bereits in der HashSet enthalten
Siehe meine Anmerkung oben zu Ihrer Invariante und der fehlenden Aussage zum momentanen Inhalt der HashSet.
Berichtigung Induktionsschritt 2/2:
Sei \(v\) ein Knoten aus dem noch nicht Betrachteten Teilbaum \(v \in U, U := T \backslash T'\). Befindet sich \(v\) bereits in der Menge der gesichteten Knoten, so bricht der Algorithmus die Rekursion ab und liefert false. Andernfalls prüft der Algorithmus die Nachfolger von \(v\), ob diese eine korrekte Verzeigerungsstruktur besitzen. Wurden alle Knoten betrachtet und jeder besitzt eine korrekte Verzeigerungsstruktur, d.h. es wurde nie probiert ein Duplikat in den HashSet einzufügen, terminiert der Algorithmus mit dem Ergebnis true.


Wäre das so besser?

Re: Ein perfekter Induktionsbeweis?

Verfasst: 16. Sep 2016 10:58
von Prof. Karsten Weihe
sqrt(2) hat geschrieben:Naja, da ist noch viel Verbesserungspotenzial.
Natürlich bekommt man nicht 0 Punkte, wenn man dieses Verbesserungspotential nicht ausschöpft. Und eine eventuelle Klausuraufgabe enthält natürlich noch ein paar hilfreiche Instruktionen.
sqrt(2) hat geschrieben: Berichtigung Induktionsschritt 1/2:
Nach der Induktionsvoraussetzung gilt für einen Teilbaum \(T'\) von \(T\), dass der Algorithmus für \(T'\) ein korrektes Ergebnis liefert.
Ok.

Zur Klarstellung würde ich schreiben: "einen echten Teilbaum \(T'\) von \(T\)" so wie bei "echt kleiner" oder "echte Teilmenge".
sqrt(2) hat geschrieben: Berichtigung Induktionsschritt 2/2:
Sei \(v\) ein Knoten aus dem noch nicht Betrachteten Teilbaum \(v \in U, U := T \backslash T'\). Befindet sich \(v\) bereits in der Menge der gesichteten Knoten, so bricht der Algorithmus die Rekursion ab und liefert false. Andernfalls prüft der Algorithmus die Nachfolger von \(v\), ob diese eine korrekte Verzeigerungsstruktur besitzen. Wurden alle Knoten betrachtet und jeder besitzt eine korrekte Verzeigerungsstruktur, d.h. es wurde nie probiert ein Duplikat in den HashSet einzufügen, terminiert der Algorithmus mit dem Ergebnis true.
Sie erzählen den Algorithmus mehr oder weniger nach. Vergleichen Sie das doch einmal mit folgender Formulierung:

Nach Induktionsvoraussetzung enthält das HashSet genau die Knoten, die bisher gesehen wurden, also genau die Knoten, die ... Der Test, ob der aktuelle Knoten im Hashset ist, führt also genau dann zum Abbruch der Methodenausführung mit Rückgabe false, wenn ..., und dann ist Rückgabe false auch korrekt. Andernfalls wird false zurückgeliefert, wenn mindestens einer der rekursiven Methodenaufrufe false zurückliefert. Nach Induktionsvoraussetzung liefern die rekursiven Aufrufe das korrekte Ergebnis zurück, wenn das HashSet ... enthält.

Das Fallbeispiel, das Sie sich hergenommen haben, ist besonders schwierig, weil die Korrektheit eines rekursiven Aufrufs nicht nur von der lokalen Situation im Teilbaum abhängt, sondern auch vom Inhalt des HashSets. Dieser Inhalt ist in vorhergehenden rekursiven Schritten sukzessive eingefügt worden, aus Teilbäumen, die mit dem betrachteten Teilbaum gar nicht direkt zu tun haben, sondern weiter links im Gesamtbaum sind.

Die Invariante müsste auf Basis dieser Einsicht auch differenzierter formuliert werden (hatte ich bei meiner gestrigen Antwort auch noch übersehen), ungefähr so: Ein rekursiver Aufruf liefert true zurück, wenn es keine Duplikate gibt in der Vereinigung aus den Schlüsselwerten in dem Teilbaum mit Wurzel m und dem Inhalt des HashSets. Die Invariante über den Inhalt des HashSets müsste dann ungefähr lauten: enthält nach einem rekursiven Aufruf mit m alles, was "links" und was "unter" m ist (einschließlich m). Aus beidem folgt dann für den allerersten rekursiven Aufruf, dass die Rückgabe true/false korrekt ist.

Ich denke, ich werde dieses Fallbeispiel 2017 dann in der Vorlesung für eine Live-Performance verwenden, bei der ich schrittweise die Invariante von einem ersten Versuch bis zur korrekten Formulierung verbessere. 8)

KW

Re: Ein perfekter Induktionsbeweis?

Verfasst: 16. Sep 2016 11:37
von sqrt(2)
Okay, vielen Dank für die Unterstützung. Ja ich werde das so nochmal überarbeiten. Den HashSet in der Invariante zu übernehmen ist ein guter Hinweis, daran habe ich gar nicht gedacht.
Prof. Karsten Weihe hat geschrieben: Sie erzählen den Algorithmus mehr oder weniger nach. Vergleichen Sie das doch einmal mit folgender Formulierung:

Nach (...).
Ja das ist meine größte Schwierigkeit, das so hinzubekommen. Werde das noch weiterhin üben. Ich finde das der Induktionsschritt irgendwie eine Nacherzählung auf besondere Art und Weise ist. Aber Übung macht den Meister (:

Prof. Karsten Weihe hat geschrieben: Ich denke, ich werde dieses Fallbeispiel 2017 dann in der Vorlesung für eine Live-Performance verwenden, (...).
Das klingt gut! Hoffentlich ohne mich ^^ (ich gebe mein bestes :P)


EDIT: Vielleicht könnte man ein eigenen Thread für Induktionsbeweise aufmachen.