mir ist beim Lesen des Wiki-Eintrags zur Breitensuchen (Breadth-first search) aufgefallen, dass dort als Variante
gewählt wurde.One node is removed from \(Q\).
Nun wird im Abschnitt "Induction step" beschrieben, was innerhalb einer Iteration passiert:
(Hervorhebungen hinzugefügt)
- Extract the first element \(v\) from \(Q\).
- Append \(v\) to the output sequence.
- For each outgoing arc \((v,w)\) of \(v\) such that \(w\) is not yet seen:
- Insert \(w\) and \((v,w)\) in \(A\).
- Label \(w\) as seen.
- Append \(w\) to \(Q\).
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:
(Hervorhebung hinzugefügt).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).
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:
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.The first node \(v\) of \(Q\) is removed and all nodes adjacent to \(v\) which have not been seen yet are appended to \(Q\).
Ist die Variante wie im Artikel angegeben korrekt und ich habe etwas missverstanden oder muss diese tatsächlich erweitert werden?