smem: add --redundancy-check for rooted structural containment (read-only)

[kimjune01]

What this PR does

Adds smem --redundancy-check: a read-only CLI command that scans semantic memory for LTIs structurally contained in other LTIs under a rooted inclusion predicate. Reports pairs where one LTI is contained in another, and groups of LTIs that are mutually contained under the same predicate. Makes no changes to the store.

Under the predicate, LTI A contains LTI B if B's augmentation graph embeds into A's: every slot in B has a matching slot in A with a superset of values, child LTIs matched recursively, subject to a global injective node mapping rooted at B and A. The predicate ignores activation state, base-level activation history, support and status metadata, aliases, ordering, and multiplicity. It is a structural test only.

The implementation is inspired by tree inclusion (Kilpeläinen & Mannila, 1995) but adapted for smem's rooted graphs, which may contain cycles and shared substructure. The adaptation has not been proved correct; see limitations below.

Read-only command. Intended as a diagnostic tool for inspecting smem contents.

Algorithm

• Coinductive cycle handling. When recursion revisits an active pair, the pair is assumed included for the purpose of the local check; the global result is only accepted if every non-cyclic obligation also succeeds. This is an implementation choice, not a proved soundness argument for cyclic inputs.

• Global injective mapping over LTI nodes. A b_to_a map threaded through all recursion prevents two distinct B-side LTI nodes from mapping to the same A-side LTI node. Injectivity is enforced at the LTI-node level; constants and slot-value occurrences are compared but not themselves tracked in the map.

• Backtracking child matching. Full backtracking over candidate assignments per attribute, with transactional b_to_a snapshot and restore on failed branches. Root nodes are pinned before recursion begins.

Limitations

• Cyclic and shared-substructure cases are not covered by tests in this PR. The cycle handling described above is designed to be sound on the non-cyclic portion of any proof, but correctness on inputs with cycles or shared substructure has not been established by regression tests.
• Predicate ignores non-structural state. Activation, BLA history, status/support metadata, aliases, multiplicity, and ordering are not considered. Two LTIs that differ only in these dimensions can be reported as one containing the other.
• "Structural containment" is not retrieval equivalence. Even when A contains B structurally, B may be preferred over A under activation or spreading rules. This command does not reason about retrieval behavior at all.
• No regression run against the existing smem test suite is included here; only the targeted smoke test is reported.

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 pairs under the predicate
• CLI: smem --redundancy-check (option 'R', no arguments)
• No schema changes. Reuses existing web_expand and lti_all infrastructure.

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

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

Test plan

• Build succeeds (CMake + make, macOS)
• Smoke test: @1 (^name alice ^age 30) contained in @2 (^name alice ^age 30 ^city boston)
• Test with cyclic structures (@1 ^next @1 vs @2 ^next @2)
• Test with shared substructure across attributes
• Verify no regression on existing smem unit tests

[kimjune01]

Retiring this PR. The assumptions it was built on were wrong:

1. D&L 2013 extrapolation. The prior diagnosis extrapolated from D&L 2013's WM/procedural forgetting to claim smem eviction was needed. D&L 2013 treats smem as the stable backup enabling WM forgetting (R4), not as a target for eviction.

2. Scaling motivation retired. Laird rates real-time capability "yes, yes" with "millions of items" (§10 item 3). The scaling-wall framing does not hold.

3. Wrong level of analysis. Smem redundancy checking and structural compaction assumed smem accumulates unboundedly in a way that degrades performance. The evidence does not support this at current hardware scales (Laird §10 items 3, 12).

See the re-intake at june.kim for the corrected SOAP analysis.