propagation-terminates-deterministically
IN derived (depth 1)
Truth propagation is guaranteed to terminate: BFS prevents stack overflow, stop-on-unchanged prevents oscillation, and fixpoint iteration bounds the outer loop
Summary
The system's truth propagation algorithm is guaranteed to finish and produce a stable result. Three mechanisms work together to ensure this: breadth-first traversal avoids blowing the call stack, unchanged nodes short-circuit further processing, and the outer loop has a hard upper bound on iterations. This means there are no scenarios where updating one belief causes the system to hang, crash, or flip-flop indefinitely.
Justifications
SL — Three complementary mechanisms each address a different termination failure mode
Antecedents (all must be IN):
- propagation-is-bfs — Truth value propagation in `_propagate` uses `deque`-based BFS through the `dependents` graph, not DFS, ensuring breadth-first wavefront expansion.
- propagate-cascade-stops-on-unchanged — If a dependent's recomputed truth value equals its current value, it is not enqueued — the cascade terminates along that path, making propagation selective rather than exhaustive
- recompute-all-uses-fixpoint — `recompute_all` iterates until no truth values change, bounded by `len(nodes) + 1` iterations, handling cascading dependencies from arbitrary node ordering.
Dependents
These beliefs depend on this one:
- add-justification-achieves-consistent-propagation — Adding a justification to an existing node produces a fully consistent network state through guaranteed-terminating multi-dimensional propagation: truth values cascade via BFS through dependents, the reverse index is updated, and access tags recompute transitively — all within a single operation whose termination is guaranteed by BFS traversal and stop-on-unchanged semantics.
- all-reconciliation-converges-deterministically — All reconciliation operations converge deterministically to stable states: individual propagation terminates via BFS with stop-on-unchanged, while system-wide operations (sync, dependents rebuild, recompute) all reach idempotent fixed points — the system has no divergent operational paths.
- belief-revision-is-fully-reliable — The complete belief revision pipeline — outlist-based defeat for proactive retraction plus dependency-directed backtracking for reactive contradiction resolution — produces correct, consistent, auditable results with deterministic propagation settling all consequences.
- challenge-defense-is-crash-safe — The dialectical challenge/defend system reaches correct truth states through recursive outlist injection evaluated by deterministic terminating propagation.
- contradiction-triggers-deterministic-resolution — When contradictions are detected, resolution and propagation form a deterministic pipeline: backtracking identifies the least-entrenched culprit premise, retraction triggers BFS propagation that terminates via stop-on-unchanged, producing a new consistent state with minimal network disruption and guaranteed convergence.
- propagation-is-crash-free — Truth propagation completes without runtime errors across all reachable nodes
- propagation-is-safe-and-terminating — Truth propagation is both lifecycle-safe and guaranteed to terminate: retracted nodes are skipped, trigger nodes are never recomputed, BFS prevents stack overflow, and stop-on-unchanged prevents oscillation — propagation respects every node state it encounters.
- tms-core-is-crash-safe — The TMS core provides crash-free truth maintenance: deterministic termination, pure evaluation, and conservative failure semantics ensure correct results across all reachable nodes.
- tms-core-is-deterministic-and-conservative — The TMS engine produces deterministic, terminating truth maintenance through uniform pure evaluation, guaranteed convergence, and conservative asymmetric failure semantics for missing nodes.