[BFS] Inhalt der Variante

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!
wintermute
Erstie
Erstie
Beiträge: 15
Registriert: 6. Jul 2016 13:07

[BFS] Inhalt der Variante

Beitrag von wintermute » 6. Jul 2016 13:44

Hallo,

mir ist beim Lesen des Wiki-Eintrags zur Breitensuchen (Breadth-first search) aufgefallen, dass dort als Variante
One node is removed from \(Q\).
gewählt wurde.

Nun wird im Abschnitt "Induction step" beschrieben, was innerhalb einer Iteration passiert:
  1. Extract the first element \(v\) from \(Q\).
  2. Append \(v\) to the output sequence.
  3. For each outgoing arc \((v,w)\) of \(v\) such that \(w\) is not yet seen:
    1. Insert \(w\) and \((v,w)\) in \(A\).
    2. Label \(w\) as seen.
    3. Append \(w\) to \(Q\).
(Hervorhebungen hinzugefügt)

Der 1. Schritt passt zur Invariante, dort wird wie gefordert ein Knoten aus \(Q\) entfernt. Allerdings werden in Schritt 3.3 möglicherweise ein oder mehrere Knoten wieder zu \(Q\) hinzugefügt. Laut dem Artikel Algorithms and correctness ist die Variante eines Algorithmus wie folgt definiert:
The variant of a loop consists of all differences between the state immediately before an iteration and the state immediately after that iteration (typically, but not exclusively, the values of integral loop variables).
(Hervorhebung hinzugefügt).

Demnach müsste meines Verständnis nach die Invariante doch erweitert werden, um ebendiese Veränderungen des Zustands auch zu beschreiben. Sie sollte dann im Ansatz wie folgt lauten:
The first node \(v\) of \(Q\) is removed and all nodes adjacent to \(v\) which have not been seen yet are appended to \(Q\).
Problematisch ist dann aber, dass die Terminierung des Algorithmus nicht mehr unmittelbar aus der Variante folgt. Ohne weitere Einschränkungen ist nicht garantiert, dass die FIFO queue \(Q\) nach endlicher Zeit leer sein wird.

Ist die Variante wie im Artikel angegeben korrekt und ich habe etwas missverstanden oder muss diese tatsächlich erweitert werden?

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

Re: [BFS] Inhalt der Variante

Beitrag von Prof. Karsten Weihe » 6. Jul 2016 14:32

wintermute hat geschrieben: Der 1. Schritt passt zur Invariante, dort wird wie gefordert ein Knoten aus \(Q\) entfernt. Allerdings werden in Schritt 3.3 möglicherweise ein oder mehrere Knoten wieder zu \(Q\) hinzugefügt. Laut dem Artikel Algorithms and correctness ist die Variante eines Algorithmus wie folgt definiert:
The variant of a loop consists of all differences between the state immediately before an iteration and the state immediately after that iteration (typically, but not exclusively, the values of integral loop variables).
(Hervorhebung hinzugefügt).
Sie finden im Abschnitt zur Variante auf besagter Wikiseite noch folgendes: "The variant of an algorithm has a specific function in the correctness proof for the algorithm. Typically, in a documentation, only those variant assertions are stated that are relevant for this purpose."

Hat sich Ihre Nachfrage damit geklärt?

KW

wintermute
Erstie
Erstie
Beiträge: 15
Registriert: 6. Jul 2016 13:07

Re: [BFS] Inhalt der Variante

Beitrag von wintermute » 6. Jul 2016 21:08

Das beantwortet meine Frage teilweise. Ich kann nachvollziehen, dass Änderungen an Variablen, die keinen Einfluss auf die Abbruchbedingung haben, für den Korrektheitsbeweis unerheblich sind.

Im gegebenen Fall ist die Abbruchbedingung "\(Q = \emptyset\)." Das heißt sie hängt von der Variable \(Q\) ab. In diesem Fall, muss die Variante also die Zustandsänderung von \(Q\) zwischen zwei Iterationen beschreiben. Nun beschreibt die Variante aber die Änderungen an \(Q\) nicht vollständig. Es können schließlich auch Knoten zu \(Q\) hinzugefügt worden sein.

Woraus folgt jetzt in diesem Fall die Terminierung?

Ist folgendes soweit korrekt?

Es muss gezeigt werden, dass nach endlicher Anzahl von Iterationen keine neuen Knoten mehr in \(Q\) eingefügt werden. Dann folgt unmittelbar, dass die Abbruchbedingung schließlich erfüllt wird. Diese Voraussetzung liefert die Variante in der Form nicht. Nun soll aber, wie ich es verstanden habe, aus der Variante die Terminierung folgen. ("The variant implies that the break condition will be fulfilled, ...")

Natürlich terminiert der Algorithmus trotzdem, da nur besuchte Knoten in \(Q\) enthalten sind. Irgendwann sind alle Knoten besucht, weshalb \(Q\) ab diesem Zeitpunkt tatsächlich mit jeder Iteration weniger Elemente enthält.

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

Re: [BFS] Inhalt der Variante

Beitrag von Prof. Karsten Weihe » 7. Jul 2016 10:20

wintermute hat geschrieben:Das beantwortet meine Frage teilweise. Ich kann nachvollziehen, dass Änderungen an Variablen, die keinen Einfluss auf die Abbruchbedingung haben, für den Korrektheitsbeweis unerheblich sind.
Der wichtige Punkt für das Erreichen der Abbruchbedingung nach linear (in den Knoten) vielen Iterationen ist, dass kein Knoten mehr als einmal eingefügt wird. Daher kann auch kein Knoten mehr als einmal aus der Queue entfernt werden, und da in jeder Iteration ein Knoten entfernt wird, haben wir entsprechend viele (bzw. wenige) Iterationen. Für diese Argumentationslinie brauche ich mich nicht im Detail mit dem Einfügen von Knoten herumzuschlagen, was ja etwas unübersichtlich wäre, weil in jeder Iteration potentiell unterschiedlich viele Knoten eingefügt werden können.

KW

wintermute
Erstie
Erstie
Beiträge: 15
Registriert: 6. Jul 2016 13:07

Re: [BFS] Inhalt der Variante

Beitrag von wintermute » 10. Jul 2016 12:02

Danke für die Antworten.

Mir ist klar geworden, wie die Terminierung des Algorithmus gezeigt werden kann.

Mein Problem war die Annahme, dass die Variante als alleinige Voraussetzung genügen soll (neben den impliziten allgemein üblichen Annahmen und Definitionen), um die Terminierung zu beweisen:
Variante \(\implies\) Abruchbedingung wird nach endlich Anzahl von Iterationen erreicht \(\implies\) Terminierung
Wenn man zulässt, dass die Variante Änderungen an Variablen nur unvollständig beschreiben darf wie hier im Fall bei der FIFO queue \(Q\), benötigt man weitere Voraussetzungen um die Terminierung zu beweisen. Also ergibt sich folgendes Beweisschema:
Variante, weitere Voraussetzungen \(\implies\) Abruchbedingung wird nach endlich Anzahl von Iterationen erreicht \(\implies\) Terminierung
Im konkreten Fall ist eine der weiteren Voraussetzungen eben genau die Annahme, dass ein Knoten nicht mehr als einmal in \(Q\) eingefügt wird.

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

Re: [BFS] Inhalt der Variante

Beitrag von Prof. Karsten Weihe » 10. Jul 2016 13:02

wintermute hat geschrieben: Wenn man zulässt, dass die Variante Änderungen an Variablen nur unvollständig beschreiben darf wie hier im Fall bei der FIFO queue \(Q\), benötigt man weitere Voraussetzungen um die Terminierung zu beweisen.
Hmh, so habe ich meine Antwort eigentlich nicht gemeint, und so verhält sich dieses Fallbeispiel meines Erachtens auch nicht.

Die textuelle Beschreibung der Variante soll alle Veränderungen von Iteration zu Iteration enthalten, die für die Terminierung (und für die Anzahl Iterationen wegen der asymptotische Komplexität) relevant sind. Das ist in diesem Beispiel der Fall: Es reicht festzuhalten, dass in jeder Iteration ein Knoten aus der Queue entfernt wird. Alle weiteren Zustandsänderungen der Variablen von einer Iteration zur nächsten sind für den Beweise der Terminierung bzw. Anzahl der Iterationen überflüssig und brauchen daher nicht erwähnt zu werden.

Mir scheint, die Verwirrung kommt daher: Natürlich kann es sein, dass noch zusätzliche Argumente notwendig sind, um aus den Zustandsänderungen, die in die textuelle Beschreibung der Variante aufgenommen worden sind, Abbruch nach so-und-soviel Iterationen zu folgern. Das Zusatzargument im Fallbeispiel ist, dass kein Knoten zweimal in die Queue eingefügt wird und jeder Knoten daher auch nur einmal entfernt werden kann. Das gehört aber nicht zur Variante, mit der eben nur die Zustandsänderungen aller Variablen von einer Iteration zur nächsten bezeichnet werden und sonst nichts.

Es hat schon seine Gründe, warum ich BFS nicht in der AuD, sondern erst in einer weiterführenden Vorlesung (Effiziente Graphenalgorithmen) behandle ... :wink:

KW

wintermute
Erstie
Erstie
Beiträge: 15
Registriert: 6. Jul 2016 13:07

Re: [BFS] Inhalt der Variante

Beitrag von wintermute » 10. Jul 2016 15:08

Danke für die schnelle Antwort.

Ich glaube jetzt habe ich es verstanden.

Ich wollte mit folgenden Satz:
wintermute hat geschrieben: Wenn man zulässt, dass die Variante Änderungen an Variablen nur unvollständig beschreiben darf wie hier im Fall bei der FIFO queue \(Q\), benötigt man weitere Voraussetzungen um die Terminierung zu beweisen.
auch nicht aussagen, dass die Variante verändert werden soll. Was ich meinte, ist dass dann die Variante alleine nicht ausreicht um das Erreichen der Abbruchbedingung nach endlicher Anzahl von Iterationen zu zeigen. Dazu ist das von Ihnen genannte Zusatzargument (Jeder Knoten wird nur einmal eingefügt) erforderlich. Damit lässt sich dann die Terminierung natürlich problemlos beweisen.

Ich habe jetzt auch verstanden, dass das Zusatzargument nicht Teil der Variante ist.

Antworten

Zurück zu „AuD: Theoretische Aufgaben“