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 (deferred — needs atom predicate)
• permuteo l p — permutation of list (deferred to Phase 5 with matche)
• 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 — access reified values of logic vars inside a goal; escapes to ground values for arithmetic or string ops
• matche — pattern matching over logic terms (extension from core.logic) (matche l ((head . tail) goal) (() goal))
• 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 with constraint
• 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]
• in x domain — constrain x to domain
• 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-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.