fix/predicate-grounding-correctness #3

davidfactor commented 2026年02月06日 06:27:36 +01:00

Summary

This PR addresses several correctness issues discovered while integrating spindle-rust into a workflow engine. The core problem is that predicate arguments were being ignored during reasoning — p(a) and p(b) were treated as identical, causing rules to fire incorrectly.
Key fixes:

• Literal identity now includes predicate arguments and mode — predicates with different arguments are now correctly treated as distinct
• Grounding pipeline integration — variable theories are now grounded before reasoning via a unified prepare() entry point
• JSON output contracts — spindle reason --json now works as documented
• Comprehensive test coverage — regression tests that would have caught these issues
  A detailed RFC spec is included at spindle-rust-fixes-spec.md documenting the problems, design decisions, and implementation approach.

---

Motivation

While planning integration with a workflow engine, I discovered that rules requiring needs_classify("doc_1","h1") would fire even when only needs_classify("doc_2","h2") was present. Investigation revealed:

1. Literal identity collapsed arguments — IndexedTheory and proven-sets were keyed by name+negation only (via literal_id()), ignoring predicate args and mode
2. Grounding was never wired in — ground_theory() existed but was never called in reason, query, why_not, etc.
3. CLI --json didn't work for reason — docs claimed it did, but the flag was ignored
4. Parser/doc mismatches — temporal defaults produced noisy [-inf,-inf] suffixes
   This wasn't a regression from recent perf work — the original port used canonical_name() which also ignored args. The perf commits entrenched the same assumption.

---

Changes

Commit 1: fix(core): make literal identity include predicate arguments and mode

• Refactors index.rs to use full literal identity (functor + args + mode + negation)
• Updates scalable.rs reasoning to respect argument discrimination
• Adds reference_time support to Literal for temporal filtering
• Adds regression tests demonstrating the fix
  Commit 2: fix: resolve build errors in benchmarks, examples, and WASM
• Updates call sites to match new API signatures
  Commit 3: feat(core): add grounding pipeline and query improvements
• Adds pipeline.rs module with unified prepare() entry point
• Implements query argument discrimination for targeted queries
• Adds wildcard _ support with validation (rejected in rule heads)
• Improves explanation output with structured literal info
• Updates temporal documentation
  Commit 4: test: add comprehensive test coverage and JSON output contracts
• reason_json_contract_tests.rs — stable CLI JSON output
• query_arg_discrimination_tests.rs — targeted query correctness
• grounding_metadata_tests.rs — superiority preservation across grounded instances
• scalable_parity_tests.rs — ScalableReasoner matches Reasoner semantics
• temporal_asof_tests.rs — reference_time filtering
• wasm_contract.rs — WebAssembly bindings

---

Breaking Changes

This PR prioritizes correctness over backward compatibility:

• Reasoning results will change for any theory using predicates with arguments (this is the bug fix)
• literal_id() semantics changed — now includes full literal identity
• JSON output schema for reason is now stable and documented (see spec)
• Temporal defaults no longer produce [-inf,-inf] noise

---

Testing

All new tests are designed to:

1. Fail on the previous behavior (would have caught the bugs)
2. Pass with the fixes (verify correctness)
   Run with:
   cargo test --workspace

---

Decision	Choice	Rationale
Canonical literal format	SPL s-expressions	Matches downstream parsing expectations
Grounding	Always via prepare()	Single entry point, consistent behavior
Wildcard _	Anonymous, rejected in heads	Standard logic programming semantics
Temporal (Phase T1)	Timepoint "as-of" filtering	Practical for workflow engines without interval-set complexity
API breaking	Allowed	Correctness > compatibility

Design Decisions
Key decisions documented in the RFC spec (spindle-rust-fixes-spec.md):

Future Work (Deferred)

The spec outlines a roadmap for features intentionally deferred:

• Phase T2: Interval-aware temporal inference (union/splitting)
• Allen relations with interval variables
• Expanded (moment ...) parsing (timezones, calendar forms)

---

Notes for Reviewers

I tried to keep each commit focused and reviewable:

1. Core fix (the meat of the change)
2. Build fixes (mechanical)
3. Pipeline + query improvements (new functionality)
4. Test coverage (validation)
   The RFC spec (spindle-rust-fixes-spec.md) has detailed context including:

• Root cause analysis with file/line references
• Design rationale for each decision
• Acceptance criteria per milestone
  Happy to discuss any design choices or split this differently if preferred!

## Summary This PR addresses several correctness issues discovered while integrating spindle-rust into a workflow engine. The core problem is that **predicate arguments were being ignored during reasoning** — `p(a)` and `p(b)` were treated as identical, causing rules to fire incorrectly. Key fixes: - **Literal identity now includes predicate arguments and mode** — predicates with different arguments are now correctly treated as distinct - **Grounding pipeline integration** — variable theories are now grounded before reasoning via a unified `prepare()` entry point - **JSON output contracts** — `spindle reason --json` now works as documented - **Comprehensive test coverage** — regression tests that would have caught these issues A detailed RFC spec is included at `spindle-rust-fixes-spec.md` documenting the problems, design decisions, and implementation approach. --- ### Motivation While planning integration with a workflow engine, I discovered that rules requiring `needs_classify("doc_1","h1")` would fire even when only `needs_classify("doc_2","h2")` was present. Investigation revealed: 1. **Literal identity collapsed arguments** — `IndexedTheory` and proven-sets were keyed by name+negation only (via `literal_id()`), ignoring predicate args and mode 2. **Grounding was never wired in** — `ground_theory()` existed but was never called in `reason`, `query`, `why_not`, etc. 3. **CLI `--json` didn't work for `reason`** — docs claimed it did, but the flag was ignored 4. **Parser/doc mismatches** — temporal defaults produced noisy `[-inf,-inf]` suffixes This wasn't a regression from recent perf work — the original port used `canonical_name()` which also ignored args. The perf commits entrenched the same assumption. --- ### Changes Commit 1: `fix(core): make literal identity include predicate arguments and mode` - Refactors `index.rs` to use full literal identity (functor + args + mode + negation) - Updates `scalable.rs` reasoning to respect argument discrimination - Adds `reference_time` support to `Literal` for temporal filtering - Adds regression tests demonstrating the fix Commit 2: `fix: resolve build errors in benchmarks, examples, and WASM` - Updates call sites to match new API signatures Commit 3: `feat(core): add grounding pipeline and query improvements` - Adds `pipeline.rs` module with unified `prepare()` entry point - Implements query argument discrimination for targeted queries - Adds wildcard `_` support with validation (rejected in rule heads) - Improves explanation output with structured literal info - Updates temporal documentation Commit 4: `test: add comprehensive test coverage and JSON output contracts` - `reason_json_contract_tests.rs` — stable CLI JSON output - `query_arg_discrimination_tests.rs` — targeted query correctness - `grounding_metadata_tests.rs` — superiority preservation across grounded instances - `scalable_parity_tests.rs` — `ScalableReasoner` matches `Reasoner` semantics - `temporal_asof_tests.rs` — reference_time filtering - `wasm_contract.rs` — WebAssembly bindings --- ### Breaking Changes This PR prioritizes correctness over backward compatibility: - **Reasoning results will change** for any theory using predicates with arguments (this is the bug fix) - `literal_id()` semantics changed — now includes full literal identity - JSON output schema for `reason` is now stable and documented (see spec) - Temporal defaults no longer produce `[-inf,-inf]` noise --- ### Testing All new tests are designed to: 1. **Fail on the previous behavior** (would have caught the bugs) 2. **Pass with the fixes** (verify correctness) Run with: cargo test --workspace --- Design Decisions Key decisions documented in the RFC spec (spindle-rust-fixes-spec.md): | Decision | Choice | Rationale | |----------|--------|-----------| | Canonical literal format | SPL s-expressions | Matches downstream parsing expectations | | Grounding | Always via prepare() | Single entry point, consistent behavior | | Wildcard _ | Anonymous, rejected in heads | Standard logic programming semantics | | Temporal (Phase T1) | Timepoint "as-of" filtering | Practical for workflow engines without interval-set complexity | | API breaking | Allowed | Correctness > compatibility | --- ### Future Work (Deferred) The spec outlines a roadmap for features intentionally deferred: - Phase T2: Interval-aware temporal inference (union/splitting) - Allen relations with interval variables - Expanded (moment ...) parsing (timezones, calendar forms) --- ### Notes for Reviewers I tried to keep each commit focused and reviewable: 1. Core fix (the meat of the change) 2. Build fixes (mechanical) 3. Pipeline + query improvements (new functionality) 4. Test coverage (validation) The RFC spec (spindle-rust-fixes-spec.md) has detailed context including: - Root cause analysis with file/line references - Design rationale for each decision - Acceptance criteria per milestone Happy to discuss any design choices or split this differently if preferred!