T 2.3 2015 - Invariante und Induktion bei Rekursion

Bei Postings zu Aufgabe Nr. x auf Blatt Nr. y lassen Sie Ihr Betreff bitte mit "y.x: " beginnen, gefolgt von einer möglichst präzisen Überschrift, danke!

Moderator: Algorithmen und Datenstrukturen

Forumsregeln
Bei Postings zu Aufgabe Nr. x auf Blatt Nr. y lassen Sie Ihr Betreff bitte mit "y.x: " beginnen, gefolgt von einer möglichst präzisen Überschrift, danke!
yokop
Windoof-User
Windoof-User
Beiträge: 28
Registriert: 13. Apr 2016 12:49

T 2.3 2015 - Invariante und Induktion bei Rekursion

Beitrag von yokop » 9. Sep 2016 16:40

Hallo,
ich tue mir aktuell bei manchen rekursiven Algorithmen noch etwas schwer die Invariante aufzustellen und den Induktionsbeweis durchzuführen. Deswegen habe ich mich mal an einer Theorieaufgabe (2.3) von 2015 versucht und hätte dazu bitte etwas Feedback, danke :D

Funktion
Sortiert ein ganzzahliges Array in aufsteigender Reihenfolge anhand von paarweisen Vergleichen.

Input
Ein ganzzahliges, voll besetztes Array a, wobei gilt, dass l und r ein Intervall auf a begrenzen, sprich l >= 0, r < a.length und l >= r. Zudem muss r-l+1 <= Integer.MAX_VALUE und a.length <= Integer.MAX_VALUE.

Output
Ein in aufsteigender Reihenfolge sortiertes ganzzahliges Array.

Wohldefiniertheit
Durch die Spezifikationen an den Input sind ArrayIndexOutOfBounds und Overflow ausgeschlossen, NullPointer können auch nicht auftreten. Zudem wird nicht durch 0 dividiert und es gibt auch keinerlei andere Möglichkeiten, dass ein Fehler auftritt.

Variante
In jedem Rekursionsschritt bewegen sich l und r echt aufeinander zu, das heißt, der Abstand l-r wird kleiner.

Terminierung
Aus der Variante und der Spezifikation im Input folgt eine Auswertung der Abbruchbedingung l < r-1 zu wahr nach endlich vielen Rekursionsschritten.

Invariante == Induktionshypothese
Nach jedem Rekursionsaufruf sind die Element im Intervall [l,r] in aufsteigender Reihenfolge sortiert.

Induktion über die Größe des Intervalls [l,r].

Induktionsanfang
Sei l = r-1, dann werden die zwei Elemente im Intervall durch die swap-Methode aufsteigend sortiert.

Induktionsschritt
Sei nun l < r-1, dann ist durch swap a[l] < a[r]. Darauf wird nun der Algorithmus 3 mal rekursiv aufgerufen und zwar jeweils auf 2/3 der Länge der Intervalls (anhand von k = (int) ((r-l+1)/3)). Nach Induktionsvoraussetzung ist das Intervall [l,r-k] nun aufsteigend sortiert, die größeren Elemente befinden sich also im oberen Teil dieses Intervalls. Diese werden nun mit dem Rest des Intervalls auf [l+k,r] sortiert, nun befinden sich also die größten Elemente des Intervalls an der richtigen Stelle. Es verbleibt den unteren Teil des gesamten Intervalls zu sortieren, was durch Aufruf der Methode auf [l,r-k] geschieht. Damit ist die Invariante erhalten, also die Elemente im Intervall [l,r] aufsteigend sortiert.

Korrektheit
Aufgrund der Variante und der Abbruchbedingung terminiert der Algorithmus für jede Eingabe. Zudem bleibt die Invariante mit jedem Rekursionsaufruf erhalten, das Ergebnis ist also korrekt, sprich das Array a ist in aufsteigender Reihenfolge sortiert.

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

Re: T 2.3 2015 - Invariante und Induktion bei Rekursion

Beitrag von Prof. Karsten Weihe » 11. Sep 2016 06:30

yokop hat geschrieben: ich tue mir aktuell bei manchen rekursiven Algorithmen noch etwas schwer
Sind Sie Berliner? :wink:
yokop hat geschrieben: Funktion
Sortiert ein ganzzahliges Array in aufsteigender Reihenfolge anhand von paarweisen Vergleichen.

Input
Ein ganzzahliges, voll besetztes Array a, wobei gilt, dass l und r ein Intervall auf a begrenzen, sprich l >= 0, r < a.length und l >= r. Zudem muss r-l+1 <= Integer.MAX_VALUE und a.length <= Integer.MAX_VALUE.
Ich verstehe nicht ganz: Sind l und r Parameter der Methode? Wenn ja, wozu, wenn nein, warum betrachten Sie sie hier?
yokop hat geschrieben: Output
Ein in aufsteigender Reihenfolge sortiertes ganzzahliges Array.

Wohldefiniertheit
Durch die Spezifikationen an den Input sind ArrayIndexOutOfBounds und Overflow ausgeschlossen
Nein: Wohldefiniertheit ist eine Eigenschaft der Implementation, nicht des Inputs. Natürlich kann der Code fälschlich auf Arrayindex -1 zugreifen oder Zahlen solange addieren, bis Overflow passiert.
yokop hat geschrieben: Variante
In jedem Rekursionsschritt bewegen sich l und r echt aufeinander zu, das heißt, der Abstand l-r wird kleiner.
Ich verstehe jetzt gar nichts mehr. Nach Spezifikation des Outputs soll es um einen Sortieralgorithmus gehen, hier scheint es aber eher um binäre Suche zu gehen!?

KW

yokop
Windoof-User
Windoof-User
Beiträge: 28
Registriert: 13. Apr 2016 12:49

Re: T 2.3 2015 - Invariante und Induktion bei Rekursion

Beitrag von yokop » 11. Sep 2016 09:36

Sind Sie Berliner?
Nein :roll:
Ich verstehe nicht ganz: Sind l und r Parameter der Methode? Wenn ja, wozu, wenn nein, warum betrachten Sie sie hier?
Ja, l und r sind Parameter des Inputs, die die linke und rechte Grenze (des Arrays) bilden. In der Methode werden die beiden Elemente an den beiden Indizes verglichen und falls a[l] > a[r] entsprechend vertauscht. Danach wird die Funktion drei Mal mit neuen Parametern aufgerufen, falls der Rekursionsanker noch nicht erreicht ist.

yokop
Windoof-User
Windoof-User
Beiträge: 28
Registriert: 13. Apr 2016 12:49

Re: T 2.3 2015 - Invariante und Induktion bei Rekursion

Beitrag von yokop » 13. Sep 2016 11:40

Hilft der Code weiter ? :oops:

Code: Alles auswählen

	/**
	* sorts the given list
	*
	* @param input
	*		given list
	* @param l
	*		left bound
	* @param r
	* 		right bound	
	*/	
	public void awesomealgo(Array[int] input, int l, int r) {
		if (input[l] > input[r])
			// swaps index l and index r
			swap(input,l,r);
			
		if (l < r-1) {
			int k = (int) Math.floor((r-l+1)/3);
			awesomealgo(input,l,r-k);
			awesomealgo(input,l+k,r);
			awesomealgo(input,l,r-k);
		}
	}

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

Re: T 2.3 2015 - Invariante und Induktion bei Rekursion

Beitrag von Prof. Karsten Weihe » 14. Sep 2016 21:10

Ok, mit dem Code verstehe ich jetzt, worum es eigentlich geht.
yokop hat geschrieben: Funktion
Sortiert ein ganzzahliges Array in aufsteigender Reihenfolge anhand von paarweisen Vergleichen.
Ok.
yokop hat geschrieben: Input
Ein ganzzahliges, voll besetztes Array a, wobei gilt, dass l und r ein Intervall auf a begrenzen, sprich l >= 0, r < a.length und l >= r. Zudem muss r-l+1 <= Integer.MAX_VALUE und a.length <= Integer.MAX_VALUE.
Ok.

Die Sache mit MAX_VALUE ist aber redundant. In einem anderen Thread hatten wir schon geklärt, dass man in Java wohl kein Array der Länge > Integer.MAX_VALUE einrichten kann. Und durch die Bedingungen l>=0 und r<a.length gilt automatisch auch r-l+1 <= Integer.MAX_VALUE.
yokop hat geschrieben: Output
Ein in aufsteigender Reihenfolge sortiertes ganzzahliges Array.
Wenn ich die Methode gemäß dieser Spezifikation implementieren soll, würde ich alle Komponenten auf 0 setzen, dann ist die Spezifikation erfüllt. :shock: 8) :wink:
yokop hat geschrieben: Wohldefiniertheit
Durch die Spezifikationen an den Input sind ArrayIndexOutOfBounds und Overflow ausgeschlossen, NullPointer können auch nicht auftreten. Zudem wird nicht durch 0 dividiert und es gibt auch keinerlei andere Möglichkeiten, dass ein Fehler auftritt.
Ich denke, das kann man so stehen lassen.
yokop hat geschrieben: Variante
In jedem Rekursionsschritt bewegen sich l und r echt aufeinander zu, das heißt, der Abstand l-r wird kleiner.
Ok, wobei der zweite Teil allein auch ausreichen würde.
yokop hat geschrieben: Terminierung
Aus der Variante und der Spezifikation im Input folgt eine Auswertung der Abbruchbedingung l < r-1 zu wahr nach endlich vielen Rekursionsschritten.
Aus der Variante allein schon, denn egal wie groß l und r am Anfang sind, nach endlich vielen Schritten sind sie beieinander, oder?
yokop hat geschrieben: Invariante == Induktionshypothese
Nach jedem Rekursionsaufruf sind die Element im Intervall [l,r] in aufsteigender Reihenfolge sortiert.
Ok.
yokop hat geschrieben: Induktion über die Größe des Intervalls [l,r].
Macht für mich Sinn.
yokop hat geschrieben: Induktionsanfang
Sei l = r-1, dann werden die zwei Elemente im Intervall durch die swap-Methode aufsteigend sortiert.
Die Fortsetzungsbedingung ist l < r - 1, also Abbruchbedingung l >= r - 1: Kann l > r - 1 auftreten?
yokop hat geschrieben: Induktionsschritt
Sei nun l < r-1, dann ist durch swap a[l] < a[r]. Darauf wird nun der Algorithmus 3 mal rekursiv aufgerufen und zwar jeweils auf 2/3 der Länge der Intervalls (anhand von k = (int) ((r-l+1)/3)). Nach Induktionsvoraussetzung ist das Intervall [l,r-k] nun aufsteigend sortiert, die größeren Elemente befinden sich also im oberen Teil dieses Intervalls. Diese werden nun mit dem Rest des Intervalls auf [l+k,r] sortiert, nun befinden sich also die größten Elemente des Intervalls an der richtigen Stelle. Es verbleibt den unteren Teil des gesamten Intervalls zu sortieren, was durch Aufruf der Methode auf [l,r-k] geschieht. Damit ist die Invariante erhalten, also die Elemente im Intervall [l,r] aufsteigend sortiert.
Ok.
yokop hat geschrieben: Korrektheit
Aufgrund der Variante und der Abbruchbedingung terminiert der Algorithmus für jede Eingabe. Zudem bleibt die Invariante mit jedem Rekursionsaufruf erhalten, das Ergebnis ist also korrekt, sprich das Array a ist in aufsteigender Reihenfolge sortiert.
Ok.

Na ja doch! :)

KW

yokop
Windoof-User
Windoof-User
Beiträge: 28
Registriert: 13. Apr 2016 12:49

Re: T 2.3 2015 - Invariante und Induktion bei Rekursion

Beitrag von yokop » 15. Sep 2016 09:35

Dankeschön :)
Prof. Karsten Weihe hat geschrieben:
yokop hat geschrieben: Output
Ein in aufsteigender Reihenfolge sortiertes ganzzahliges Array.
Wenn ich die Methode gemäß dieser Spezifikation implementieren soll, würde ich alle Komponenten auf 0 setzen, dann ist die Spezifikation erfüllt. :shock: 8) :wink:
Also sowas wie "Das Eingangsarray a, wobei die einzelnen Komponenten nun in aufsteigender Reihenfolge sortiert sind" ?

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

Re: T 2.3 2015 - Invariante und Induktion bei Rekursion

Beitrag von Prof. Karsten Weihe » 15. Sep 2016 10:19

yokop hat geschrieben:Dankeschön :)
Also sowas wie "Das Eingangsarray a, wobei die einzelnen Komponenten nun in aufsteigender Reihenfolge sortiert sind" ?
Es wäre sicher unmissverständlich für den Leser, wenn Sie von einer "Umordnung" oder "Umsortierung" des Eingangsarrays sprechen würden.

KW

Antworten

Zurück zu „AuD: Theoretische Aufgaben“