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 = (list) (empty assoc list)
• Tests in lib/minikanren/tests/unify.sx: ground terms, vars, lists, failure, occurs

Phase 2 — streams + goals

• Stream type: mzero (empty stream = nil), unit s (singleton = (list s)), mplus (interleave two streams), bind (apply goal to stream)
• Lazy streams via delay/force — mature pairs for depth-first, immature for lazy
• == goal: (fn (s) (let ((s2 (unify u v s))) (if s2 (unit s2) mzero)))
• succeed / fail — trivial goals
• fresh — (fn (f) (fn (s) ((f (make-var)) s))) — introduces one var; fresh* for many
• conde — interleaving disjunction of goal lists
• condu — committed choice (soft-cut): only explores first successful clause
• onceo — succeeds at most once
• Tests: basic goal composition, backtracking, interleaving

Phase 3 — run + reification

• run* goal → list of all answers (reified)
• run n goal → list of first n answers
• reify term subst → replace unbound vars with _0, _1, ... names
• reify-s → builds reification substitution for naming unbound vars consistently
• fresh with multiple variables: (fresh (x y z) goal) sugar
• Query variable conventions: q as canonical query variable
• Tests: classic miniKanren programs — (run* q (== q 1)) → (1), (run* q (conde ((== q 1)) ((== q 2)))) → (1 2), Peano arithmetic, appendo preview

Phase 4 — standard relations

• appendo l s ls — list append, runs forwards and backwards
• membero x l — x is a member of l
• listo l — l is a proper list
• nullo l — l is empty
• pairo p — p is a pair (cons cell)
• caro p a — car of pair
• cdro p d — cdr of pair
• conso a d p — cons
• firsto / resto — aliases for caro/cdro
• reverseo l r — reverse of list
• flatteno l f — flatten nested lists
• permuteo l p — permutation of list
• lengtho l n — length as a relation (Peano or integer)
• Tests: run each relation forwards and backwards; generate from partial inputs

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 disjunction (like Prolog ->)
• condu — committed choice (already in phase 2; refine semantics here)
• 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.

(awaiting phase 1)