rose-ash/plans/minikanren-deferred.md

miniKanren-on-SX: deferred work

The main plan (plans/minikanren-on-sx.md) carries Phases 1–7 through the naive-tabling milestone. This file collects the four pieces left on the shelf, with enough scope and design notes to drive a follow-up loop.

Branch convention: keep the same loops/minikanren worktree; commit and push to origin/loops/minikanren. Squash-merge to architecture only when each numbered piece is shipped + tests green.

Cumulative test count snapshot at squash-merge: 644 across 71 test files. Every change below should grow the number, not break existing tests.

The four pieces

Piece A — Phase 7 SLG (cyclic patho, mutual recursion, fixed-point iteration)

Problem. Naive tabling drains the answer stream eagerly, then caches. Recursive tabled calls with the SAME ground key see an empty cache (the in-progress entry never exists), so they recurse and the host overflows. Fibonacci works only because each recursive call has a different key; cyclic patho and any genuinely self-recursive tabled predicate diverge.

Approach — a small subset of SLG / OLDT resolution, enough to handle the demos in the brief.

1. In-progress sentinel. When a tabled call T(args) starts, store (:in-progress nil) under its key. Recursive calls into T(args) from inside its own computation see the sentinel and return only the answers accumulated so far (initially empty).
2. Answer accumulator. As each new answer is found, push it into the cache entry: (:in-progress accumulated-answers). After a cycling caller returns, the outer continuation can re-consult the updated cache.
3. Fixed-point iteration. The driver repeatedly re-runs the goal until no new answers appear in a full pass, then transitions the cache from :in-progress to :done.
4. Subgoal table. Track (subgoal, last-seen-cache-version) per subscriber so each consumer only re-reads what it hasn't seen.

Suggested artefacts.

• lib/minikanren/tabling-slg.sx — new module with table-slg-2 (parallel to table-2 from naive tabling). Keep table-2 working unchanged so Fibonacci/Ackermann don't regress.
• lib/minikanren/tests/cyclic-graph-tabled.sx — the canonical demo: two-cycle patho from a→b→a→b plus a→b→c. With SLG, (run* q (tab-patho :a :c q)) returns the single shortest path, not divergence.
• lib/minikanren/tests/mutual-recursion.sx — even/odd via mutual recursion (even-o n ↔ odd-o (n-1)), tabled at both names.

Reference reading.

• TRS chapter on tabling.
• "Tabled Logic Programming" — Sagonas & Swift (the XSB / SLG paper).
• core.logic's tabled macro for an SX-dialect-friendly precedent.

Risk. This is the brief's "research-grade complexity, not a one-iteration item". Plan for 4–6 commits: in-progress sentinel, answer accumulator, fixed-point driver, then one demo per commit.

Piece B — Phase 6 polish: bounds-consistency for fd-plus / fd-times

Problem. Current fd-plus-prop and fd-times-prop propagate only when two of three operands walk to ground numbers. When all three are domain-bounded vars, the propagator returns s unchanged — search has to label down to ground before any narrowing happens.

Approach — narrow domains via interval reasoning even when no operand is ground.

For (fd-plus x y z) with bounded x, y, z:

• x ∈ [z.min − y.max .. z.max − y.min]
• y ∈ [z.min − x.max .. z.max − x.min]
• z ∈ [x.min + y.min .. x.max + y.max]

For (fd-times x y z): same shape, but with multiplication; need to handle sign cases (negative domain ranges) and the divisor-when-not-zero constraint already in place.

Suggested artefacts.

• Patch fd-plus-prop and fd-times-prop in lib/minikanren/clpfd.sx with new :else branches that compute new domain bounds and call fd-set-domain for each var.
• New tests in lib/minikanren/tests/clpfd-plus.sx / clpfd-times.sx exercising the all-domain case: two domain-bounded vars in the body of a goal, with no labelling, after which their domains have narrowed.
• A demo: cryptarithmetic puzzle (see Piece D) using bounds consistency to avoid labelling explosion.

Risk. Low. The math is well-known; just careful min/max arithmetic and watch for edge cases (empty domain after narrowing).

Piece C — =/= disequality with constraint store

Problem. nafc is sound only on ground args; fd-neq only on FD domains. There is no general-purpose Prolog-style structural disequality =/= that works on logic terms.

Approach. Generalise the FD constraint store to a uniform "constraint store" that carries:

• domain map (existing)
• pending disequalities — a list of (u v) pairs that must remain non-unifiable under any future extension.

After every == / mk-unify, re-check each pending disequality:

• If (u v) are now unifiable, fail.
• If they're now structurally distinct (no shared substitution can unify), drop from the store (the constraint is satisfied).
• Otherwise leave in store.

Where it bites. The kernel currently uses mk-unify everywhere. Either:

1. Replace mk-unify with a constraint-aware wrapper everywhere (intrusive, but principled).
2. Keep mk-unify for goals that don't use =/=, and provide a parallel ==-cs / =/=-cs pair plus an alternative run*-cs driver that fires the constraint check after each binding.

Option 2 mirrors the fd-fire-store pattern and stays out of the common path.

Suggested artefacts.

• lib/minikanren/diseq.sx — disequality store on top of the existing _fd reserved key (re-using the constraint list, just with disequality-shaped closures instead of FD propagators).
• =/= goal that posts a disequality and immediately checks it.
• =/=-test integration: rewrite a few Phase 5 puzzles using =/= instead of nafc + ==.
• Tests covering: ground-pair fail, partial-pair satisfied later by binding, partial-pair contradicted later by binding.

Risk. Medium. The hard cases are eventual unifiability — a disequality (=/= (cons a 1) (cons 2 b)) should hold until both a gets bound to 2 and b gets bound to 1. Implementations like core.logic's encode this as a list of "violating bindings" the disequality remembers.

Piece D — Bigger CLP(FD) demos: send-more-money + Sudoku 4×4

Problem. The current N-queens demo only verifies the constraint chain end-to-end. The brief's full Phase 6 list includes "send-more-money, N-queens with CLP(FD), map coloring, cryptarithmetic" — most of which exercise more than just fd-neq + fd-distinct.

Approach. Two concrete puzzles that both stress bounds-consistency (Piece B) once it lands:

send-more-money

  S E N D
+ M O R E
---------
M O N E Y

8 distinct digits ∈ {0..9}, S ≠ 0, M ≠ 0. Encoded as a sum-of-digits equation using fd-plus + carry chains.

Without Piece B (bounds-consistency), the search labels every digit combination upfront — slow but tractable on a fast machine. With Piece B, the impossible high-digit cases prune early.

Test: a single solution (9 5 6 7 1 0 8 2).

Sudoku 4×4

Easier than 9×9 but exercises the full pattern:

• 16 cells, each ∈ {1..4}
• 4 rows, 4 cols, 4 2×2 boxes — 12 fd-distinct constraints
• Some cells fixed as clues

A small solver should handle 4×4 in well under a second once bounds-consistency narrows columns / boxes after each label step.

Suggested artefacts.

• lib/minikanren/tests/send-more-money.sx — single-solution test.
• lib/minikanren/tests/sudoku-4x4.sx — at least three cluesets: unique solution, multiple solutions, no solution.
• Optional: lib/minikanren/sudoku.sx with a parameterised sudoku-n for both 4×4 and a 9×9 stress test.

Risk. Low–medium for 4×4 + send-more-money once Piece B lands. 9×9 Sudoku is a stretch; treat it as a stretch goal once the smaller demos are green.

Suggested ordering

1. Piece B first (bounds-consistency for fd-plus / fd-times). Self-contained, low-risk, and unlocks Piece D's harder puzzles.
2. Piece D (the two demos). Validates Piece B with concrete puzzles. Doubles as the brief's missing canary tests.
3. Piece C (=/=). Independent track; once shipped, refactor the pet/diff puzzles in Phase 5 to use it instead of nafc.
4. Piece A (SLG tabling). Last because it's the highest-risk piece; do it when the rest of the library is stable so regressions are easy to spot.

Operating ground rules (carry over from the original brief)

• Scope: lib/minikanren/** and the two plan files (this one and the original).
• Commit cadence: one feature per commit. Short factual messages (mk: piece B — bounds-consistency for fd-plus).
• Plan updates: tick boxes here as pieces land; mirror status in plans/minikanren-on-sx.md Roadmap.
• Test discipline: every commit ends with the cumulative count green. No-regression rule from the original brief still applies.
• sx-tree MCP only for .sx edits. sx_validate after every structural edit.
• Pushing: origin/loops/minikanren only. Never main. Squash to architecture only with explicit user permission, as we did for the v1 merge.