[BFS] Inhalt der Variante

[wintermute]

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]

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]

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]

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]

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]

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 ...

KW

[wintermute]

Danke für die schnelle Antwort.

Ich glaube jetzt habe ich es verstanden.

Ich wollte mit folgenden Satz:

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.