giles
0ba60d6a25
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 57s
lib/minikanren/stream.sx: mzero/unit/mk-mplus/mk-bind/stream-take. Three stream shapes (empty, mature list, immature thunk). mk-mplus suspends and swaps on a paused-left for fair interleaving (Reasoned Schemer style). lib/minikanren/goals.sx: succeed/fail/==/==-check + conj2/disj2 + variadic mk-conj/mk-disj. ==-check is the opt-in occurs-checked variant. Forced-rename note: SX has a host primitive `bind` that silently shadows user-level defines, so all stream/goal operators are mk-prefixed. Recorded in feedback memory. 82/82 tests cumulative (48 unify + 34 goals).
159 lines
8.9 KiB
Markdown
159 lines
8.9 KiB
Markdown
# 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
|
||
- [x] `make-var` → fresh logic variable (unique mutable box)
|
||
- [x] `var?` `v` → bool — is this a logic variable?
|
||
- [x] `walk` `term` `subst` → follow substitution chain to ground term or unbound var
|
||
- [x] `walk*` `term` `subst` → deep walk (recurse into lists/dicts)
|
||
- [x] `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.
|
||
- [x] Empty substitution `empty-s` (dict-based via kit's `empty-subst` — assoc list was a sketch; kit ships dict, kept it)
|
||
- [x] Tests in `lib/minikanren/tests/unify.sx`: ground terms, vars, lists, failure, occurs
|
||
|
||
### Phase 2 — streams + goals
|
||
- [x] 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.
|
||
- [x] 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.
|
||
- [x] `==` goal: `(fn (s) (let ((s2 (mk-unify u v s))) (if s2 (unit s2) mzero)))`
|
||
- [x] `==-check` — opt-in occurs-checked equality goal
|
||
- [x] `succeed` / `fail` — trivial goals
|
||
- [x] `conj2` / `mk-conj` (variadic) — sequential conjunction
|
||
- [x] `disj2` / `mk-disj` (variadic) — interleaved disjunction (raw — `conde`
|
||
adds the implicit-conj-per-clause sugar later)
|
||
- [ ] `fresh` — introduces logic variables inside a goal body
|
||
- [ ] `conde` — sugar over disj+conj, one row per clause
|
||
- [ ] `condu` — committed choice (soft-cut)
|
||
- [ ] `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._
|
||
|
||
- **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.
|