Add smem --redundancy-check (tree inclusion)

[kimjune01]

Problem

Semantic memory grows without bound. Soar has no mechanism to detect when one smem entry's knowledge is fully contained in another's. After episodic-to-semantic consolidation (#578), merged entries may structurally subsume older entries, but those older entries persist indefinitely — actively retrieved, never evicted, slowing every subsequent spreading activation pass.

Derbinsky & Laird (2013) showed that without forgetting, a robot exceeded the 50ms decision-cycle threshold within an hour. They built forgetting for working memory and procedural memory. Smem and epmem still have none. This PR addresses the detection half of smem maintenance.

Full analysis: Diagnosis: Soar, SOAP Notes: Soar, Prescription: Soar.

What this PR does

Adds smem --redundancy-check: a CLI command that scans semantic memory for structurally dominated entries via tree inclusion. Detection only — no eviction.

LTI A dominates LTI B if B's augmentation graph embeds injectively into A's — every slot in B has a matching slot in A with a superset of values, child LTIs matched recursively.

Expected consequence

After consolidation (#578) merges N episodes into a semantic entry, this check identifies pre-existing smem entries that the merged result now subsumes. Without it, consolidation adds entries but never removes redundant ones — net store growth is monotonically positive. With it, the eviction path (future PR) can remove dominated entries, making net growth per consolidation cycle potentially negative. Over a 30-day deployment at 72,000 episodes/hour, this is the difference between smem growing without bound and smem staying bounded.

Dependencies

PR	Role	Status
#578	Episodic-to-semantic consolidation (creates the entries that produce redundancy)	Merged to this branch
#579 (this)	Structural redundancy detection (identifies dominated entries)	This PR
Future	Eviction of dominated entries via back-invalidation protocol	Not yet started

The three form a pipeline: consolidation creates entries → tree inclusion detects redundancy → eviction removes dominated entries. Each is independently useful but the full payoff requires all three.

Theory

Tree inclusion (Kilpeläinen & Mannila, 1995) defines structural containment on rooted labeled trees. This PR adapts it to smem's graph structures with three extensions:

1. Coinductive cycle handling. Smem graphs may contain cycles. We use coinductive semantics: revisiting an active pair optimistically assumes inclusion; if the assumption is wrong, non-cyclic proof obligations fail and reject it.

2. Global injective matching. A b_to_a map threaded through all recursion enforces that two distinct B nodes cannot map to the same A node, even via different attributes. Root pinning ensures rooted inclusion.

3. Backtracking child matching. Full backtracking over candidate assignments per attribute, with transactional b_to_a snapshot/restore on failed branches.

BLA (base-level activation) handles staleness — entries that haven't been accessed decay. Tree inclusion handles redundancy — entries whose knowledge is fully contained in a richer entry. They are orthogonal. See Prescription: Soar § Structural redundancy via tree inclusion.

This fills the "Tree × Dominance" cell in the parts bin taxonomy — structural dominance filtering on tree-shaped data. Background on the taxonomy and the blank cell: The Missing Parts.

Implementation

• New file: smem_inclusion.cpp (~400 lines)
  • load_lti_augs() — loads augmentations via web_expand into lightweight structs keyed by hash IDs (no Symbol allocation)
  • smem_lti_includes_impl() — recursive inclusion with coinductive cycles, global injectivity, backtracking
  • CLI_redundancy_check() — iterates all LTI pairs, reports dominated entries and equivalence classes
• CLI: smem --redundancy-check (option 'R', no arguments)
• No schema changes. Reuses existing web_expand and lti_all infrastructure

Methodology

Implementation by Claude Code (Opus 4.6) in an isolated git worktree. Reviewed through five rounds of adversarial volley with codex (GPT-5.4). Volley methodology: june.kim/volley.

Round	Issues found	Fixes applied
1	Greedy matching incorrect, cycle handling unsound, CLI returns wrong, help text missing	Backtracking matcher, split active_pairs from memo, bool return + SetError, help text
2	Global injectivity not enforced (per-attribute only), cycles still wrong (pessimistic)	b_to_a map threaded globally, coinductive cycle semantics
3	Failed branches leak descendant bindings, memoization context-dependent	Transactional b_to_a snapshots, dropped memo
4	Root not pinned (non-root-preserving embeddings accepted), runtime help missing	b_to_a seeded with root binding, smem_settings help updated
5	No correctness blockers. Ready to merge.	—

References

• Kilpeläinen, P. & Mannila, H. (1995). "Ordered and Unordered Tree Inclusion." SIAM J. Computing 24(2):340–356. DOI
• Bille, P. & Gørtz, I.L. (2011). "The Tree Inclusion Problem: In Linear Space and Faster." ACM TALG 7(3). arXiv
• Pinter, R.Y. et al. (2007). "Approximate Labelled Subtree Homeomorphism." J. Discrete Algorithms 5(4). DOI
• Derbinsky, N. & Laird, J.E. (2013). "Effective and Efficient Forgetting of Learned Knowledge in Soar's Working and Procedural Memories." Cognitive Systems Research. DOI
• Laird, J.E. (2022). "Introduction to the Soar Cognitive Architecture." arXiv

Test plan

• Build succeeds (CMake + make, macOS)
• Smoke test: @1 (^name alice ^age 30) dominated by @2 (^name alice ^age 30 ^city boston)
• Five rounds of adversarial code review (codex GPT-5.4)
• Test with cyclic structures (@1 ^next @1 vs @2 ^next @2)
• Test with shared substructure across attributes
• Run against a real agent's smem store after consolidation (Episodic-to-semantic memory consolidation (experimental) #578)
• Verify no regression on existing smem unit tests