Drop-in fast replacement for Peano lengtho when the count fits in a
host integer. Two conde clauses: empty list -> 0; recurse, n = 1 +
length(tail). Uses pluso-i so the length walks to a native int.
5 new tests, 486/486 cumulative.
Sum and product over a list of ground integers via fold + intarith.
Empty list yields the identity (0 for sum, 1 for product). Recurse
combines the head with the recursively-computed tail value via
pluso-i / *o-i.
9 new tests, 481/481 cumulative.
Two conde clauses each: singleton -> the element; multi -> compare head
against the recursive min/max of the tail and pick. Uses lteo-i / lto-i
for the comparisons, so the input must be ground integers.
mino + maxo can run together: (fresh (mn mx) (mino l mn) (maxo l mx)
(== q (list mn mx))) recovers both.
9 new tests, 472/472 cumulative.
Three conde clauses: empty list / singleton list / two-or-more (where
the first two satisfy lteo-i and the rest is recursively sorted). Uses
ground-only integer comparison (intarith), so the input list must
walk to ground integers.
7 new tests, 463/463 cumulative.
Recursive: empty l1 trivially holds; otherwise the head is in l2 (via
membero) and the tail is a subset. Duplicates in l1 are allowed since
each is independently checked.
7 new tests, 456/456 cumulative.
Mitigation for the cyclic-graph divergence (see tests/cyclic-graph.sx).
Threads a `visited` accumulator through the recursion; each candidate
next-step is gated by `nafc (membero z visited)`. Terminates on graphs
with cycles, no Phase-7 tabling required for the simple acyclic-path
query.
Demonstrates a viable alternative to tabling for the common case where
the user wants finite path enumeration over a graph with cycles.
3 new tests, 449/449 cumulative.
Three conde clauses: empty list -> empty result; head matches x ->
skip and recurse; head differs (nafc-gated) -> keep and recurse.
Distinct from rembero, which removes only the first occurrence.
5 new tests, 446/446 cumulative.
Demo of matche dispatch + conde + recursion for tree traversal:
(matche tree
((:leaf x) (== v x))
((:node l r) (conde ((btree-walko l v)) ((btree-walko r v)))))
Test tree ((1 2) (3 (4 5))) yields all 5 leaves under run*. Also tests
membership (run 1) and absence.
4 new tests, 441/441 cumulative.
Four conso calls express the (a b . rest) -> (b a . rest) rewrite as a
purely relational constraint. Self-inverse on length-2+ lists; runs
forward (swap given input) and backward (recover original from the
swapped form). Fails on lists shorter than 2.
6 new tests, 437/437 cumulative.
(pairlisto l1 l2 pairs): pairs is the zipped list of pairs (l1[i] l2[i]).
Recurses on both l1 and l2 in lockstep, building pairs in parallel.
Runs forward, can recover l1 given l2 and pairs, can recover l2 given
l1 and pairs. Different-length lists fail.
5 new tests, 431/431 cumulative.
(iterate-no rel n x result) holds when applying the 2-arg relation rel
n times (Peano n) starting from x produces result. Base case: zero
iterations means result equals x. Recursive case: rel x mid, then
iterate-no n-1 from mid.
Generalises common chains:
succ iteration: (iterate-no succ-rel n :z q) -> n in Peano
list growth: (iterate-no cons-rel n () q) -> n-element list
4 new tests, 426/426 cumulative.
rev-acco is the standard tail-recursive reverse with an accumulator;
rev-2o starts the accumulator at the empty list. Faster than the
appendo-driven reverseo for forward queries because there is no nested
appendo per element.
Trade-off: rev-acco is asymmetric. The accumulator's initial-empty
cannot be enumerated backwards the way reverseo does, so reverseo is
still the right choice when both directions matter.
A test verifies rev-2o and reverseo agree on forward queries.
6 new tests, 422/422 cumulative.
Classic miniKanren relation. (selecto x rest l) holds when l contains
x at any position with `rest` being everything else. Direct base case
(l = (x . rest)) plus the skip-head recursion that threads the head
through to the result rest.
Run modes: enumerate every (x, rest) split; recover rest given an
element; recover an element given the rest; (and ground/all combinations).
6 new tests, 411/411 cumulative.
Composes two appendos: l = front ++ s ++ back, equivalently
(appendo front-and-s back l) and (appendo front s front-and-s).
Goal order matters: doing the (appendo ground:l) split first makes the
search finitary; the second appendo is then deterministic given
front-and-s and ground s. Reversing the order causes divergence on
failing inputs (the front search becomes unbounded).
7 new tests, 405/405 cumulative.
Two-line definitions over appendo:
(prefixo p l) ≡ ∃rest. (appendo p rest l)
(suffixo s l) ≡ ∃front. (appendo front s l)
Both enumerate all prefixes/suffixes when called with a fresh first
arg, and serve as decision relations when called with both grounded.
9 new tests, 398/398 cumulative.
Two-line definition: a list is a palindrome iff it equals its reverse.
Direct composition of reverseo + ==.
7 new tests: empty / singleton / equal pair / unequal pair /
5-element-yes / 5-element-no / strings.
389/389 cumulative.
Mirrors the structure all-distincto already uses internally: walk the
list, ensure each element is not equal to x via nafc, recurse on tail.
Useful as a constraint-style filter:
(membero x (list 1 2 3 4 5))
(not-membero x (list 2 4))
-> x in {1, 3, 5}
4 new tests, 382/382 cumulative.
repeato: produces (or recognizes) a list of n copies of a value, with n
Peano-encoded. Runs forward, backward (recover the count from a uniform
list), and bidirectionally.
concato: fold-appendo over a list-of-lists. (concato (list (list 1 2)
(list) (list 3 4 5)) q) -> ((1 2 3 4 5)).
10 new tests, 378/378 cumulative.
(tako n l prefix) — prefix is the first n elements of l.
(dropo n l suffix) — suffix is l after dropping the first n.
Both use a Peano natural for the count. Round-trip holds:
(tako n l) ⊕ (dropo n l) = l (verified by an end-to-end test)
9 new tests, 368/368 cumulative.
eveno: zero, or (s (s m)) when m is even.
oddo: one, or (s (s m)) when m is odd.
Both run forward (predicate test on a Peano number) and backward
(enumerate even / odd numbers). The two are mutually exclusive — no
number satisfies both.
12 new tests, 359/359 cumulative.
(defrel (NAME ARGS...) (CLAUSE1 ...) (CLAUSE2 ...) ...) expands to
(define NAME (fn (ARGS...) (conde (CLAUSE1 ...) (CLAUSE2 ...) ...))).
Mirrors Prolog's `name(Args) :- goals.` shape. Inherits the Zzz-on-each-
clause laziness from conde, so user relations defined via defrel
terminate on partial answers without needing manual delay. Tests
redefine membero / listo / pluso through defrel and verify equivalence.
3 new tests, 347/347 cumulative.
lasto: x is the final element of l. Direct base case (l = (x)) plus
recurse-on-cdr.
init-o: init is l without its last element. Base case for singleton:
(== init ()). Otherwise recurse, threading the head through to the
init result via conso.
Together with appendo, the round-trip init append (list last) = l
holds, which is exercised by an end-to-end test.
8 new tests, 344/344 cumulative.
tests/rdb.sx shows the library as a small Datalog engine over fact
tables. Each table is an SX list of tuples, wrapped by a relation that
does (membero (list ...) table). Queries compose selection, projection,
and joins entirely in run* / fresh / conde / membero / intarith / nafc.
Five queries: dept filter, salary > threshold, employee-project join,
intersection (engineers on a specific project), anyone on multiple
distinct projects.
5 new tests, 336/336 cumulative.
Demonstrates the naive-patho behaviour on a 2-cycle (a <-> b, plus
b -> c). Without Phase-7 tabling, the search produces ever-longer
paths: (a b), (a b a b), (a b a b a b), ... `run 5` truncates to a
finite prefix; `run*` diverges. Documenting this as a regression-style
test gives Phase 7 a concrete starting point.
3 new tests, 331/331 cumulative.
Ground-only type tests via project. Each succeeds iff its argument
walks to the corresponding host value type. Composes with membero for
type-filtered enumeration:
(fresh (x) (membero x (list 1 "a" 2 "b" 3)) (numbero x) (== q x))
-> (1 2 3)
12 new tests, 328/328 cumulative. Caveat: SX keywords are strings, so
(stringo :k) succeeds.
Defines a small graph as a fact list, edgeo for fact lookup, and patho
that recursively constructs paths. Direct-edge clause yields (x y);
otherwise traverse one edge to z, recurse for z->y, prepend x.
Enumerates all paths between two nodes, including alternates through
shortcut edges:
(run* q (patho :a :d q))
-> ((:a :b :c :d) (:a :c :d)) ; both routes
6 new tests, 316/316 cumulative.
(everyo rel l): every element of l satisfies the unary relation rel.
(someo rel l): some element does. Both compose with intarith and other
predicate-shaped goals:
(everyo (fn (x) (lto-i x 10)) (list 1 5 9)) -> succeeds
(someo (fn (x) (lto-i 100 x)) (list 5 50 200)) -> succeeds
10 new tests, 310/310 cumulative.
(mapo rel l1 l2) takes a 2-argument relation rel and asserts l2 is l1
with each element rel-related to its counterpart. Recursive on both
lists in lockstep. Works forward (fixed l1, find l2), backward (fixed
l2, find l1), or constraining mid-pipeline.
Composes with intarith for arithmetic transforms:
(mapo (fn (a b) (*o-i a a b)) (list 1 2 3 4) q) -> ((1 4 9 16))
7 new tests, 300/300 cumulative.
Recurses positionally, dropping a head from each list each step. Both
arguments can be unbound, giving the natural enumeration:
(run 3 q (fresh (l1 l2) (samelengtho l1 l2) (== q (list l1 l2))))
-> (((), ()) empty/empty
((_.0), (_.1)) pair of 1-element lists
((_.0 _.1), (_.2 _.3))) pair of 2-element lists
5 new tests, 293/293 cumulative.
Finds all (a, b, c) with a, b, c in [1..10], a <= b, a^2 + b^2 = c^2.
Result: ((3 4 5) (6 8 10)) — the two smallest Pythagorean triples
within the domain.
Demonstrates the enumerate-then-filter pattern:
(ino a dom) (ino b dom) (ino c dom) — generate
(lteo-i a b) — symmetry break
(*o-i a a a-sq) (*o-i b b b-sq) (*o-i c c c-sq) — squares
(pluso-i a-sq b-sq sum) (== sum c-sq) — Pythagorean equation
288/288 cumulative.
pluso-i / minuso-i / *o-i / lto-i / lteo-i / neqo-i wrap host arithmetic
in project. They run at native speed but require their inputs to walk
to ground numbers — they are NOT relational the way Peano pluso is.
Use them when puzzle size makes Peano impractical (which is most cases
beyond toy examples).
Composes with relational goals — for instance,
(fresh (x) (membero x (1 2 3 4 5)) (lto-i x 3) (== q x))
filters the domain by < 3 and returns (1 2).
18 new tests, 287/287 cumulative.
Defines latin-2x2 over 4 cells and 4 all-distincto constraints. Enumerates
exactly 2 squares ((1 2)(2 1)) and ((2 1)(1 2)); a corner clue narrows to
one. 3 new tests, 269/269 cumulative.
3x3 (12 squares, the natural showcase) is too slow under naive enumerate-
then-filter — that is the motivating test for Phase 6 arc-consistency.
rembero (remove-first) uses nafc to gate the skip-element clause so
the result is well-defined on ground lists. assoco is alist lookup —
runs forward (key -> value) and backward (find keys with a given
value). nth-o uses Peano-encoded indices into a list, mirroring lengtho.
13 new tests, 266/266 cumulative.
Three conde clauses: nullo tree -> nullo flat; pairo tree -> recurse on
car & cdr, appendo their flattenings; otherwise tree must be a ground
non-list atom (nafc nullo + nafc pairo) and flat = (list tree).
Works on ground inputs of arbitrary nesting:
(run* q (flatteno (list 1 (list 2 3) (list (list 4) 5)) q))
-> ((1 2 3 4 5))
7 tests, 253/253 cumulative. Phase 4 list relations now complete.
Verifies that the Zzz-wraps-each-conde-clause + mk-mplus-suspend-on-
paused-left machinery produces fair interleaving and gives finite
prefixes from infinitely-recursive relations:
- listo-aux has no base case under run* but run 4 q ... produces
exactly the four shortest list shapes, in order.
- mk-disj of two infinite generators (ones-gen, twos-gen) with
run 4 q ... must include both 1-prefixed and 2-prefixed answers
(no starvation).
- run* terminates on a goal that has a finite answer set.
3 tests, 246/246 cumulative.
queens.sx encodes a queen in row i at column ci. ino-each constrains
each ci to {1..n}; all-distincto handles the row/column distinct
property; safe-diag uses project to escape into host arithmetic for the
|c_i - c_j| != |i - j| diagonal guard. all-cells-safe iterates pairs at
goal-construction time so the constraint set is materialised once,
then driven by the search.
(run* q (fresh (a b c d) (== q (list a b c d))
(queens-cols (list a b c d) 4)))
-> ((2 4 1 3) (3 1 4 2))
Both valid 4-queens placements found. 6 new tests including the
two-solution invariant; 243/243 cumulative.
ino is membero with the constraint-store-friendly argument order
(`(ino x dom)` reads as "x in dom"). all-distincto checks pairwise
distinctness via nafc + membero on the recursive tail. These two are
enough to express the enumerate-then-filter style of finite-domain
solving:
(fresh (a b c)
(ino a (list 1 2 3)) (ino b (list 1 2 3)) (ino c (list 1 2 3))
(all-distincto (list a b c)))
enumerates all 6 distinct triples from {1, 2, 3}. Full CLP(FD) with
arc-consistency, fd-plus, etc. remains pending under Phase 6 proper.
9 new tests, 237/237 cumulative.
matche-pattern->expr now treats keyword patterns as literals that emit
themselves bare, rather than wrapping in (quote ...). SX keywords
self-evaluate to their string name; quoting them flips them to a
keyword type that does not unify with the bare-keyword usage at the
target site. This was visible only as a test failure on the diffo
clauses below — tightened the pattern rules.
tests/classics.sx exercises three end-to-end miniKanren programs:
- 3-friend / 3-pet permutation puzzle
- grandparent inference over a fact list (membero + fresh)
- symbolic differentiation dispatched by matche on
:x / (:+ a b) / (:* a b)
228/228 cumulative.
Pattern grammar: _, symbol, atom (number/string/keyword/bool), (), and
(p1 ... pn) list patterns (recursive). Symbols become fresh vars in a
fresh form, atoms become literals to unify against, lists recurse
position-wise. Repeated names produce the same fresh var (so they
unify by ==).
Macro is built with explicit cons/list rather than a quasiquote because
the quasiquote expander does not recurse into nested lambda bodies —
the natural `\`(matche-clause (quote ,target) cl)` spelling left
literal `(unquote target)` forms in the output.
14 tests, 222/222 cumulative. Phase 5 done (project, conda, condu,
onceo, nafc, matche all green).
inserto a l p: p is l with a inserted at some position. Recursive: head
of l first, then push past head and recurse.
permuteo l p: classical recursive permutation. Empty -> empty; otherwise
take a head off l, recursively permute the tail, insert head at any
position in the recursive result.
7 new tests including all-6-perms-of-3 as a set check (independent of
generation order). 208/208 cumulative.
(nafc g) is a three-line primitive: peek the goal's stream for one
answer; if empty, yield (unit s); else mzero. Carries the standard
miniKanren caveats — open-world unsound, diverges on infinite streams.
7 tests: failed-goal-succeeds, successful-goal-fails, double-negation,
conde-all-fail-makes-nafc-succeed, conde-any-success-makes-nafc-fail,
nafc as a guard accepting and blocking.
201/201 cumulative.
(project (vars ...) goal ...) defmacro walks each named var via mk-walk*,
rebinds them in the body's lexical scope, then mk-conjs the body goals on
the same substitution. Hygienic — gensym'd s-param so user vars survive.
Lets you reach into host SX for arithmetic, string ops, anything that
needs a ground value: (project (n) (== q (* n n))), (project (s)
(== q (str s \"!\"))), and so on.
6 new tests, 194/194 cumulative.
Classic miniKanren Peano arithmetic on (:z / (:s n)) naturals. pluso runs
relationally in all directions: 2+3=5 forward, x+2=5 → 3 backward,
enumerates the four pairs summing to 3. *o is iterated pluso. lteo/lto
via existential successor decomposition.
19 new tests, 188/188 cumulative. Phase-tagged in the plan separately
from Phase 6 CLP(FD), which will eventually replace this with native
integers + arc-consistency propagation.
conda-try mirrors condu-try but on the chosen clause it (mk-bind
(head-goal s) (rest-conj)) — all head answers flow through. condu by
contrast applies rest-conj to (first peek), keeping only one head
answer.
7 new tests covering: first-non-failing-wins, skip-failing-head, all-fail,
no-clauses, the conda-vs-condu divergence (`(1 2)` vs `(1)`), rest-goals
running on every head answer, and the soft-cut no-fallthrough property.
169/169 cumulative.
reverseo: standard recursive definition via appendo. Forward works in
run*; backward (input fresh, output ground) works in run 1 but run*
diverges trying to enumerate the unique answer (canonical TRS issue
with naive reverseo).
lengtho: Peano encoding (:z / (:s :z) / (:s (:s :z)) ...) so it works
relationally in both directions without arithmetic-as-relation. Forward
returns the Peano length; backward enumerates lists of a given length.
162/162 cumulative.
Three coupled fixes plus a new relations module land together because
each is required for the next: appendo can't terminate without all
three.
1. unify.sx — added (:cons h t) tagged cons-cell shape because SX has no
improper pairs. The unifier treats (:cons h t) and the native list
(h . t) as equivalent. mk-walk* re-flattens cons cells back to flat
lists for clean reification.
2. stream.sx — switched mature stream cells from plain SX lists to a
(:s head tail) tagged shape so a mature head can have a thunk tail.
With the old representation, mk-mplus had to (cons head thunk) which
SX rejects (cons requires a list cdr).
3. conde.sx — wraps each clause in Zzz (inverse-eta delay) for laziness.
Zzz uses (gensym "zzz-s-") for the substitution parameter so it does
not capture user goals that follow the (l s ls) convention. Without
gensym, every relation that uses `s` as a list parameter silently
binds it to the substitution dict.
relations.sx is the new module: nullo, pairo, caro, cdro, conso,
firsto, resto, listo, appendo, membero. 25 new tests.
Canary green:
(run* q (appendo (list 1 2) (list 3 4) q))
→ ((1 2 3 4))
(run* q (fresh (l s) (appendo l s (list 1 2 3)) (== q (list l s))))
→ ((() (1 2 3)) ((1) (2 3)) ((1 2) (3)) ((1 2 3) ()))
(run 3 q (listo q))
→ (() (_.0) (_.0 _.1))
152/152 cumulative.
run.sx: reify-name builds canonical "_.N" symbols; reify-s walks a term
left-to-right and assigns each unbound var its index in the discovery
order; reify combines the two with two walk* passes. run-n is the
runtime defmacro: binds the query var, takes ≤ n stream answers, reifies
each. run* and run are sugar around it.
First classic miniKanren tests green:
(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))
128/128 cumulative.
condu.sx: defmacro `condu` folds clauses through a runtime `condu-try`
walker. First clause whose head yields a non-empty stream commits its
single first answer; later clauses are not tried. `onceo` is the simpler
sibling — stream-take 1 over a goal's output.
10 tests cover: onceo trimming success/failure/conde, condu first-clause
wins, condu skips failing heads, condu commits-and-cannot-backtrack to
later clauses if the rest of the chosen clause fails.
110/110 cumulative. Phase 2 complete.
