Operational correctness via bounded closure

This page is a theory note. It expands the topic in short chapters and defines terminology without duplicating the formal specification documents.

The diagram has a transparent background and is intended to be read together with the caption and the sections below.

Related wiki pages: VM, event stream, VSA, bounded closure, consistency contract.

Related specs: DS004.

Overview

Correctness in VSAVM is not a vague aspiration; it is a contract. The system is allowed to emit a conclusion only if bounded closure does not reveal contradictions within the configured budget and scope. This makes the cost of correctness explicit and configurable.

Correctness contract definition

The correctness contract establishes the fundamental guarantee: conclusions will not be emitted if they would create contradictions within the explored reasoning space. Key principles:

• Operational correctness: Differs from traditional logical correctness by acknowledging computational limitations. Requires consistency within the subset of inferences explorable given available resources.
• Definitive vs. hypothetical: The guarantee applies to conclusions explicitly asserted as facts. Hypothetical, conditional, or uncertain content uses different standards.
• Budget-bounded guarantees: Parameters include maximum search depth, inference steps, parallel branches, and computation time. These are configurable based on query importance and resources.
• Budget monotonicity: Verification claims are monotonic with respect to their stated horizon. If consistent up to budget B, that claim remains true when the budget increases (assuming unchanged knowledge base). Higher budgets may surface new issues beyond the previous frontier.

Strict mode and conditional response

Two modes handle situations where contradictions cannot be ruled out within budget:

• Strict mode: Refuses to emit any conclusion that cannot be verified as consistent. Prioritizes reliability over completeness. Declares queries unanswerable rather than risk incorrect information.
• Conditional mode: Emits conclusions marked with explicit conditions or uncertainty qualifiers indicating verification limitations. Provides partial answers with appropriate uncertainty markers.

Degradation strategies for budget exhaustion operate through a hierarchy of verification levels, falling back to lower levels while clearly reporting limitations.

Bounded closure algorithm

The bounded closure algorithm explores logical consequences within computational limits:

• Transitive closure computation: Repeatedly apply rules until no new conclusions or until budget exhausted. Operate in phases alternating between rule application and consistency checking.
• Rule application prioritization: Learned heuristics identify rules most likely to produce useful conclusions or reveal contradictions. Consider both historical effectiveness and current context.
• Dynamic budget allocation: Distribute resources across closure aspects to maximize contradiction detection. Adjust based on results (more checking if potential contradictions detected, more rule application if many new facts).
• Conflict detection: Multiple complementary mechanisms identify direct contradictions (same fact with opposite values), indirect contradictions (incompatible logical consequences), and temporal contradictions (incompatible states at same time).
• Branch exploration and pruning: Manage combinatorial explosion by maintaining parallel branches, pruning those leading to contradictions or becoming less promising. Maintain diversity to avoid premature convergence.

Canonical facts and negation

Contradictions cannot be reliably detected at the text level. VSAVM maps assertions into canonical fact identifiers with typed slots and explicit polarity. Different surface forms can map to the same canonical identifier, making paraphrase-invariant conflict checks possible.

• Canonical comparison: Foundation for direct contradiction detection. Specialized indexing enables rapid identification of potentially conflicting facts.
• Negation handling: Distinguishes explicit negation, implicit negation (incompatible properties), and absence of information. Explicit negative facts are recorded rather than simply omitting positive facts.
• Polarity conflict detection: Identifies same fact with both positive and negative polarity within same reasoning context.

Context scoping and isolation

Context scoping prevents contradictions in one structural region from invalidating reasoning elsewhere:

• Separate reasoning contexts: Maintain different fact sets and rules for different time periods, hypothetical scenarios, or distinct structural regions in the source data.
• Context isolation: Contradictions within one context do not propagate unless explicit connections exist. Enables multiple internally-consistent but mutually-contradictory theories.
• Context management: Mechanisms for creating, merging, and transferring information between contexts while maintaining consistency.

Conflict resolution strategies

When contradictions are detected, systematic resolution approaches apply:

• Source-based resolution: Use reliability and authority of information sources. Prefer more reliable sources while maintaining records of rejected alternatives.
• Temporal resolution: Determine temporal ordering of contradictory facts. Maintain separate facts for different time periods if situation changed.
• Probabilistic resolution: Assign confidence levels and maintain probabilistic beliefs rather than definitive conclusions.

Resolution maintains detailed records for later review and revision if new information changes the basis for decisions.

Execution tracing and auditability

A correctness claim is only meaningful if it is auditable. VSAVM logs the closure budget, explored branches, applied rules, and detected conflicts. This allows the system to produce operational explanations that are traces of what was executed rather than post-hoc narratives.

• Log format: Structured entries capturing operation type, inputs, results, time, and side effects. Multiple detail levels (high-level summaries to complete traces).
• Budget usage reporting: Transparent resource consumption tracking across categories (rule applications, consistency checks, search, memory). Patterns reveal problem complexity.
• Branch exploration documentation: Record all considered paths including pruned/abandoned branches and pruning rationale.
• Reproducibility guarantees: Identical inputs and parameters produce identical results. Control all nondeterminism sources (random seeds, parallel scheduling, memory allocation). Maintain version information for all components.

References

Consistency (Wikipedia) Transitive closure (Wikipedia) Non-monotonic logic (SEP) Execution trace (Wikipedia)