|
circuits[T: TYPE]: THEORY
%
% A circuit is a pre_circuit with no small loops (i.e. reduced)
%
% pre_circuit?(G: graph[T], w: prewalk): bool = walk?(G,w) AND
% w(0) = w(length(w)-1)
%
% NOTE: The extra term "w(1) /= w(length(w)-2)" in the definition of
% cyclically_reduced? handles the special case where
% w(0) is a small loop
%
% removed "walk?(G,w)" from circuit? defn because it is in pre_circuit
%
BEGIN
IMPORTING walks[T]
G: VAR graph[T]
reducible?(G: graph[T], w: Seq(G)): bool =
(EXISTS (k: posnat): k < length(w) - 1 AND w(k-1) = w(k+1))
reduced?(G: graph[T], w: Seq(G)): bool = NOT reducible?(G,w)
%
% cyclically_reduced?(G: graph[T], w: Long_walk(G)): bool =
% reduced?(G,w) AND
% (FORALL (j: below(length(w)-1)): reduced?(G,w^(j+1, length(w)-1) o w^(1,j)))
cyclically_reduced?(G: graph[T], w: Seq(G)): bool = length(w) > 2 AND
reduced?(G,w) AND w(1) /= w(length(w)-2)
circuit?(G: graph[T], w: Seq(G)): bool = %% walk?(G,w) AND
cyclically_reduced?(G,w) AND
pre_circuit?(G,w)
END circuits
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
