giles
ef0a24f0db
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 28s
Captures the work left on the shelf after the loops/minikanren squash
merge:
Piece A — Phase 7 SLG (cyclic patho, mutual recursion). The hardest
piece; the brief's "research-grade complexity" caveat
still stands. Plan documents the in-progress sentinel +
answer-accumulator + fixed-point-driver design.
Piece B — Phase 6 polish: bounds-consistency for fd-plus / fd-times
in the (var var var) case. Math is straightforward
interval reasoning; low risk, self-contained.
Piece C — =/= disequality with a constraint store. Generalises
nafc / fd-neq to logic terms via a pending-disequality
list re-checked after each ==.
Piece D — Bigger CLP(FD) demos: send-more-money and Sudoku 4x4.
Both validate Piece B once it lands.
Suggested ordering: B (low risk, unlocks D) → D (concrete validation)
→ C (independent track) → A (highest risk, do last).
Operating ground rules carried over from the original loop brief:
loops/minikanren branch, sx-tree MCP only, one feature per commit,
test count must monotonically grow.
217 lines
9.1 KiB
Markdown
217 lines
9.1 KiB
Markdown
# 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.
|