rose-ash/plans/minikanren-on-sx.md

miniKanren-on-SX: relational programming on the CEK/VM

miniKanren is not a language to parse — it is an embedded DSL implemented as a library of SX functions. No tokenizer, no transpiler. The entire system is a set of define forms in lib/minikanren/. Programs are SX expressions using the miniKanren API.

The unique angle: SX's delimited continuation machinery (perform/cek-resume, call/cc) maps almost perfectly to the search monad miniKanren needs. Backtracking is cooperative suspension, not a separate trail machine. This is the cleanest possible host for miniKanren.

End-state goal: full core miniKanren (run, fresh, ==, conde, condu, onceo, project, matche) + core.logic-style relations (appendo, membero, listo, numbero, etc.) + arithmetic constraints (fd domain, CLP(FD) subset).

Ground rules

• Scope: only touch lib/minikanren/** and plans/minikanren-on-sx.md. Do not edit spec/, hosts/, shared/, or other lib/<lang>/.
• Shared-file issues go under "Blockers" below with a minimal repro; do not fix here.
• SX files: use sx-tree MCP tools only.
• Architecture: pure library — no source parser. Programs are written in SX using the API.
• Reference: The Reasoned Schemer (Friedman/Byrd/Kiselyov) + Byrd's dissertation.
• Commits: one feature per commit. Keep ## Progress log updated and tick boxes.

Architecture sketch

SX program using miniKanren API
    │
    ├── lib/minikanren/unify.sx      — terms, variables, walk, unification, occurs check
    ├── lib/minikanren/substitution.sx — substitution as association list / hash table
    ├── lib/minikanren/stream.sx     — lazy streams of substitutions (via delay/force)
    ├── lib/minikanren/goals.sx      — == / fresh / conde / condu / onceo / project / matche
    ├── lib/minikanren/run.sx        — run* / run n — drive the search, extract answers
    ├── lib/minikanren/relations.sx  — standard relations: appendo, membero, listo, etc.
    └── lib/minikanren/clpfd.sx      — arithmetic constraints (CLP(FD) subset)

Key semantic mappings:

• Logic variable → SX vector of length 1 (mutable box); make-var creates fresh one; walk follows the substitution chain
• Substitution → SX association list (or hash table for performance) mapping var → term
• Stream of substitutions → lazy list using delay/force (Phase 9 of primitives)
• Goal → SX function substitution → stream-of-substitutions
• == → unifies two terms, extending substitution or failing (empty stream)
• fresh → introduces new logic variables; (fresh (x y) goal) → goal with x, y bound
• conde → interleave streams from multiple goal clauses (depth-first with interleaving)
• run n → drive the stream, collect first n substitutions, reify answers

Roadmap

Phase 1 — variables + unification

• make-var → fresh logic variable (unique mutable box)
• var? v → bool — is this a logic variable?
• walk term subst → follow substitution chain to ground term or unbound var
• walk* term subst → deep walk (recurse into lists/dicts)
• unify u v subst → extended substitution or #f (failure) Handles: var/var, var/term, term/var, list unification, number/string/symbol equality. No occurs check by default; unify-check with occurs check as opt-in.
• Empty substitution empty-s (dict-based via kit's empty-subst — assoc list was a sketch; kit ships dict, kept it)
• Tests in lib/minikanren/tests/unify.sx: ground terms, vars, lists, failure, occurs

Phase 2 — streams + goals

• Stream type: mzero (empty), unit s (singleton), mk-mplus (interleave), mk-bind (apply goal to stream). Names mk-prefixed because SX has a host bind primitive that silently shadows user defines.
• Lazy streams via thunks: a paused stream is a zero-arg fn; mk-mplus suspends and swaps when its left operand is paused, giving fair interleaving.
• == goal: (fn (s) (let ((s2 (mk-unify u v s))) (if s2 (unit s2) mzero)))
• ==-check — opt-in occurs-checked equality goal
• succeed / fail — trivial goals
• conj2 / mk-conj (variadic) — sequential conjunction
• disj2 / mk-disj (variadic) — interleaved disjunction (raw — conde adds the implicit-conj-per-clause sugar later)
• fresh — introduces logic variables inside a goal body. Implemented as a defmacro: (fresh (x y) g1 g2 ...) ⇒ (let ((x (make-var)) (y (make-var))) (mk-conj g1 g2 ...)). Also call-fresh for programmatic goal building.
• conde — sugar over disj+conj, one row per clause; defmacro that wraps each clause body in mk-conj and folds via mk-disj. Notes: with eager streams ordering is left-clause-first DFS; true interleaving requires paused thunks (Phase 4 recursive relations).
• condu — committed choice. defmacro folding clauses into a runtime condu-try walker; first clause whose head goal yields a non-empty stream commits its first answer, rest-goals run on that single subst.
• onceo — (stream-take 1 (g s)); trims a goal's stream to ≤1 answer.
• Tests: basic goal composition, backtracking, interleaving (110 cumulative)

Phase 3 — run + reification

• run* goal → list of all answers (reified). defmacro: bind q-name as fresh var, conj goals, take all from stream, reify each.
• run n goal → list of first n answers (defmacro; n = -1 means all)
• reify term subst → walk* + build reification subst + walk* again
• reify-s → maps each unbound var (in left-to-right walk order) to a _.N symbol via (make-symbol (str "_." n))
• fresh with multiple variables — already shipped Phase 2B.
• Query variable conventions: q as canonical query variable (matches TRS)
• Tests: classic miniKanren programs — (run* q (== q 1)) → (1), (run* q (conde ((== q 1)) ((== q 2)))) → (1 2), (run* q (fresh (x y) (== q (list x y)))) → ((_.0 _.1)). Peano + appendo deferred to Phase 4.

Phase 4 — standard relations

• appendo l s ls — list append, runs forwards AND backwards. Canary green: (run* q (appendo (1 2) (3 4) q)) → ((1 2 3 4)); (run* q (fresh (l s) (appendo l s (1 2 3)) (== q (list l s)))) → all four splits.
• membero x l — enumerates: (run* q (membero q (a b c))) → (a b c)
• listo l — l is a proper list; enumerates list shapes with laziness
• nullo l — l is empty
• pairo p — p is a (non-empty) cons-cell / list
• caro / cdro / conso / firsto / resto
• reverseo l r — reverse of list. Forward is fast; backward is run 1-clean, run* diverges due to interleaved unbounded list search (canonical TRS issue).
• flatteno l f — flatten nested lists. Three conde clauses: empty → empty; pair → recurse on car & cdr + appendo; otherwise atom → (== flat (list tree)). Atom-ness is asserted via nafc (nullo tree) + nafc (pairo tree) — both succeed only when tree is a ground non-list. Works on ground inputs.
• permuteo l p — permutation of list. Built on inserto (insert at any position) and recursive permutation of tail. All 6 perms of (1 2 3) generated forward; backward run 1 q (permuteo q (a b c)) finds the input.
• lengtho l n — length as a relation, Peano-encoded: :z / (:s :z) / (:s (:s :z)) ... matches TRS. Forward is direct; backward enumerates lists of a given length.
• Tests: run each relation forwards and backwards (so far 25 in tests/relations.sx; reverseo/flatteno/permuteo/lengtho deferred)

Phase 5 — project + matche + negation

• project (x ...) body — defmacro: rebinds named vars to (mk-walk* var s) in the body's lexical scope, then runs (mk-conj body...) on the same substitution. Hygienic via gensym'd s-param. (Phase 5 piece B)
• matche — pattern matching over logic terms. Pattern grammar: _ / symbol / atom / () / (p1 p2 ... pn). Each clause becomes (fresh (vars-in-pat) (== target pat-expr) body...). Repeated symbol names in a pattern produce the same fresh var, so they unify (== check). Built without quasiquote (the expander does not recurse into lambda bodies). Fixed-length list patterns only — head/tail destructuring uses (fresh (a d) (conso a d target) body) directly.
• conda — soft-cut: first non-failing head wins; ALL of head's answers flow through rest-goals; later clauses not tried (Phase 5 piece A)
• condu — committed choice (Phase 2)
• nafc — negation as finite failure: (nafc g) yields the input subst iff g has zero answers. Standard caveats apply (open-world unsoundness; diverges if g is infinite). Phase 5 piece C.
• Tests: Zebra puzzle, N-queens, Sudoku via project, family relations via matche

Phase 6 — arithmetic constraints CLP(FD)

• Finite domain variables: fd-var with domain [lo..hi]
• ino x domain — alias for (membero x domain) with the constraint-store-friendly argument order. Sufficient for the enumerate-then-filter style of finite-domain solving.
• all-distincto l — pairwise-distinct elements via nafc + membero.
• fd-eq x y — x = y (constraint propagation)
• fd-neq x y — x ≠ y
• fd-lt fd-lte fd-gt fd-gte — ordering constraints
• fd-plus x y z — x + y = z (constraint)
• fd-times x y z — x * y = z
• Arc consistency propagation — when domain narrows, propagate to constrained vars
• Labelling: fd-run drives search by splitting domains when propagation stalls
• Tests: send-more-money, N-queens with CLP(FD), map coloring, cryptarithmetic

Phase 7 — tabling (memoization of relations)

• tabled annotation: memoize calls to a relation using a hash table
• Prevents infinite loops in recursive relations like patho on cyclic graphs
• Producer/consumer scheduling for tabled relations (variant of SLG resolution)
• Tests: cyclic graph reachability, mutual recursion, Fibonacci via tabling

Blockers

(none yet)

Progress log

Newest first.

• 2026-05-08 — samelengtho: classic miniKanren relation that succeeds when two lists have equal length. Symmetric — works to enumerate both lists fresh: (run 3 q (fresh (l1 l2) (samelengtho l1 l2) (== q (list l1 l2)))) produces empty/empty, then 1-elem pairs, then 2-elem. 5 new tests, 293/293 cumulative.
• 2026-05-08 — Pythagorean triples (intarith showcase): search for (a, b, c) ∈ [1..10]³, a ≤ b, a² + b² = c² via ino + lteo-i + *o-i + pluso-i + ==. Finds exactly (3 4 5) and (6 8 10). Demonstrates the enumerate-then-filter pattern with intarith escape into host arithmetic. 1 new test, 288/288 cumulative.
• 2026-05-08 — intarith.sx — fast ground-only integer arithmetic: pluso-i / minuso-i / *o-i / lto-i / lteo-i / neqo-i wrap host arithmetic via project. They are not relational like Peano pluso (require args to walk to numbers), but run at native host speed — a viable escape hatch when puzzle size makes Peano impractical. Composes with relational goals: (membero x dom) (lto-i x 3) filters dom by < 3. 18 new tests, 287/287 cumulative.
• 2026-05-08 — 2x2 Latin square: small classic constraint demo using ino + 4 all-distincto constraints. Enumerates exactly 2 squares (((1 2)(2 1)) and ((2 1)(1 2))); a clue (top-left = 1) narrows to one. 3 new tests, 269/269 cumulative. Note: 3x3 (12 squares) is the natural showcase but too slow under naive enumerate-then-filter — needs Phase 6 arc-consistency.
• 2026-05-08 — rembero / assoco / nth-o: more standard list relations. rembero removes the first occurrence (uses nafc (== a x) to gate the skip clause, so it's well-defined on ground lists). assoco is alist lookup — works forward (key → value) and backward (value → key). nth-o uses Peano indices into a list. 13 new tests, 266/266 cumulative.
• 2026-05-08 — flatteno: nested-list flattener via conde + appendo. Atom-ness is detected via nafc (nullo ...) + nafc (pairo ...) so the third clause only fires when the input is a ground non-list. Works for () / atoms / flat lists / arbitrarily-nested lists. 7 new tests, 253/253 cumulative. Phase 4 list relations all complete.
• 2026-05-08 — Laziness tests: explicitly verifies the Zzz-on-conde-clauses + mk-mplus-swap-on-paused machinery: an infinitely-recursive relation truncated via run 4 q (listo-aux q) produces exactly (() (_.0) (_.0 _.1) (_.0 _.1 _.2)); mixing two infinite generators via mk-disj keeps both alive (no starvation); run* terminates on a bounded query. 3 new tests, 246/246 cumulative.
• 2026-05-08 — N-queens (classic miniKanren benchmark green): lib/minikanren/queens.sx. Encoding cols(i) = column of queen in row i; ino-each + all-distincto cover row/column constraints; safe-diag uses project to escape into host arithmetic for the |c_i - c_j| ≠ |i - j| diagonal check; all-cells-safe walks pairs at construction time. (run* q (fresh (a b c d) (== q (list a b c d)) (queens-cols (list a b c d) 4))) returns the two valid 4-queens placements (2 4 1 3) and (3 1 4 2). 6 new tests, 243/243 cumulative.
• 2026-05-08 — Phase 6 piece A — minimal FD (ino + all-distincto): lib/minikanren/fd.sx. ino is membero with the FD-style argument order; all-distincto is nafc + membero walking the list. Together they cover the enumerate-then-filter style of finite-domain solving — (fresh (a b c) (ino a D) (ino b D) (ino c D) (all-distincto (list a b c))) enumerates all distinct triples from D. Full FD with arc-consistency, fd-plus etc. is still pending. 9 new tests, 237/237 cumulative.
• 2026-05-08 — Classic puzzles + matche keyword fix: matche now emits keywords bare in the pattern->expr conversion so they self-evaluate to their string name and unify with the same-keyword target value (instead of becoming a quoted-keyword type). New tests/classics.sx: pet permutation puzzle, parent/grandparent inference over a fact list, symbolic differentiation driven by matche dispatch on :x / (:+ a b) / (:* a b) patterns. 6 new tests, 228/228 cumulative.
• 2026-05-08 — Phase 5 piece D — matche, Phase 5 done: pattern matching macro (lib/minikanren/matche.sx) — symbols become fresh vars, atoms become literals, lists recurse positionally, repeated names unify. 14 new tests (literals, vars, wildcards, list patterns, multi-clause dispatch, nested patterns, repeated-var-implies-eq). Built via cons/list rather than quasiquote because SX's quasiquote does not recurse into lambda bodies — a worth-knowing gotcha. 222/222 cumulative.
• 2026-05-08 — Phase 4 piece C — permuteo + inserto: standard recursive insert-at-any-position + permute-tail. 7 new tests, including all-6-perms-of-3 as a set check. 208/208 cumulative.
• 2026-05-07 — Phase 5 piece C — nafc: lib/minikanren/nafc.sx. Three-line primitive: stream-take 1; if empty, (unit s), else mzero. 7 tests including double-negation and use as a guard. 201/201 cumulative.
• 2026-05-07 — Phase 5 piece B — project: lib/minikanren/project.sx — defmacro that walks each named var, rebinds them, and runs the body's mk-conj. Demonstrated escape into host arithmetic / string ops ((* n n), (str s "!")). Hygienic gensym'd s-param. 6 new tests, 194/194 cumulative.
• 2026-05-07 — Peano arithmetic (lib/minikanren/peano.sx): zeroo, pluso, minuso, lteo, lto, *o on Peano-encoded naturals (:z / (:s n)). pluso runs forward, backward, and enumerates: (run* q (fresh (a b) (pluso a b 3) (== q (list a b)))) → all 4 pairs summing to 3. *o uses repeated pluso — works for small inputs, slower for larger. 19 new tests, 188/188 cumulative.
• 2026-05-07 — Phase 5 piece A — conda: soft-cut. Mirrors condu minus the onceo on the head: all head answers are conjuncted through the rest of the chosen clause. 7 new tests including the conda-vs-condu divergence test. 169/169 cumulative.
• 2026-05-07 — Phase 4 piece B — reverseo + lengtho: reverseo runs forward cleanly and run 1-cleanly backward; lengtho uses Peano-encoded lengths so it works as a true relation in both directions (tests use the encoding directly). 10 new tests, 162/162 cumulative.
• 2026-05-07 — Phase 4 piece A — appendo canary green: cons-cell support in unify.sx + (:s head tail) lazy stream refactor in stream.sx + hygienic Zzz (gensym'd subst-name) wrapping each conde clause + lib/minikanren/ relations.sx with nullo / pairo / caro / cdro / conso / firsto / resto / listo / appendo / membero. 25 new tests in tests/relations.sx, 152/152 cumulative.
  • Three deep fixes shipped together, all required to make appendo terminate in both directions:
    1. SX has no improper pairs, so a stream cell of mature subst + thunk tail can't use cons — moved to a (:s head tail) tagged shape.
    2. (Zzz g) wrapped its inner fn in a parameter named s, capturing the user goal's own s binding (the (appendo l s ls) convention). Replaced with (gensym "zzz-s-") for hygiene.
    3. SX cons cells (:cons h t) for relational decomposition (so (conso a d l) can split a list by head/tail without proper improper pairs); mk-walk* re-flattens cons cells back to native lists for clean reification output.
• 2026-05-07 — Phase 3 done (run + reification): lib/minikanren/run.sx (~28 lines). reify/reify-s/reify-name for canonical _.N rendering of unbound vars in left-to-right occurrence order; run* / run / run-n defmacros. 18 new tests in tests/run.sx, including the first classic miniKanren tests green: (run* q (== q 1)) → (1); (run* q (fresh (x y) (== q (list x y)))) → ((_.0 _.1)). 128/128 cumulative.
• 2026-05-07 — Phase 2 piece D + done (condu / onceo): lib/minikanren/condu.sx. Both are commitment forms: onceo is (stream-take 1 ...); condu walks clauses and commits the first one whose head produces an answer. 10 tests in tests/condu.sx, 110/110 cumulative. Phase 2 complete — ready for Phase 3 (run + reification).
• 2026-05-07 — Phase 2 piece C (conde): lib/minikanren/conde.sx — single defmacro folding clauses through mk-disj with internal mk-conj. 9 tests in tests/conde.sx, 100/100 cumulative. Confirmed eager DFS ordering for ==-only streams; true interleaving is a Phase 4 concern (paused thunks under recursion).
• 2026-05-07 — Phase 2 piece B (fresh): lib/minikanren/fresh.sx (~10 lines). defmacro form for nice user-facing syntax + call-fresh for programmatic use. 9 new tests in tests/fresh.sx, 91/91 cumulative.
• 2026-05-07 — Phase 2 piece A (streams + ==/conj/disj): lib/minikanren/stream.sx (mzero/unit/mk-mplus/mk-bind/stream-take, ~25 lines of code) + lib/minikanren/goals.sx (succeed/fail/==/==-check/conj2/disj2/mk-conj/mk-disj, ~30 lines). Found and noted a host-primitive name clash: bind is built in and silently shadows user defines — must use mk-bind/mk-mplus etc. throughout. 34 tests in tests/goals.sx, 82/82 cumulative all green. fresh/conde/condu/onceo still pending.
• 2026-05-07 — Phase 1 done: lib/minikanren/unify.sx (53 lines, ~22 lines of actual code) + lib/minikanren/tests/unify.sx (48 tests, all green). Kit consumption: walk-with, unify-with, occurs-with, extend, empty-subst, mk-var, is-var?, var-name all supplied by lib/guest/match.sx. Local additions: a miniKanren-flavoured cfg (treats native SX lists as cons-pairs via :ctor-head = :pair, occurs-check off), make-var fresh-counter, deep mk-walk* (kit's walk* only recurses into :ctor form, not native lists), and mk-unify / mk-unify-check thin wrappers. The kit earns its keep ~3× over by line count — confirms lib-guest match kit is reusable for logic-language hosts as designed.