(aux kanren arith): the arithmetic relations of The Reasoned Schemer
Arithmetic as a relation
Chapters 7 and 8 of The Reasoned Schemer, Second Edition build addition, subtraction, multiplication, division, exponentiation and the logarithm out of two truth tables and a great deal of unification. The definitions in (aux kanren arith) are that development, translated line by line into the (aux kanren micro) idiom and then exercised here, with a dozen relations added that the book has no use for -- four mirrored comparisons, then multiple°, divisor°, even°, odd°, square°, composite°, between°, common-divisor°, numeral° and prime°, each a few lines over what chapters 7 and 8 already give. Nothing in the translation is clever: defrel becomes define-relation, conde becomes cond°, fresh becomes fresh°, == becomes =°, (run n (q) g ...) becomes (μkanren-run (q n #t) g ...), and the book's trailing o -- the mark that a name denotes a relation rather than a function -- becomes the trailing ° this repository uses for the same purpose. So addero is adder°, *o is *°, logo is log°. The two relations null° and cons° are not redefined here; they already live in (aux kanren micro).
The numeral
A number is a list of the bits 0 and 1, least significant first, with zero written as the empty list and with no trailing 0. Two is (0 1), five is (1 0 1), six is (0 1 1) and nine is (1 0 0 1). build-num is the only function in the module -- everything else is a relation -- and its quotient recursion stops at zero?, which is what guarantees the absence of a trailing zero. That canonicality is not cosmetic: it makes the encoding injective, so one number has one term, and a term that unifies with (0 0 1) is four and cannot be anything else.
Little-endian is what makes the whole system run in every direction. Addition consumes its arguments from the low bit up, so adder° can peel one cell off each addend and recur without knowing how long either list is -- and the very same clause, read with the sum ground and an addend fresh, subtracts. There is no mode declaration anywhere in the module and no guard on which argument happens to be known. minus° has no body beyond (plus° m k n); division by *° is the multiplication goal with the product ground; factorisation is the same goal with both factors fresh; and (exp° b 2 9) is an integer square root only because exp° is log° with the remainder pinned to '(). Termination in those backward directions is bought, explicitly, by the length guards -- pos°, >1°, <l°, bound-*° -- and the cases below are written to pin exhaustion, not just correctness: a query that asks for more answers than exist asserts that the stream closes.
Goal construction and δ°
In (aux kanren micro), and°, or° and cond° are macros that expand into calls to the procedures andª and orª -- so every goal sub-expression of every clause is evaluated while the goal tree is being built, long before any substitution exists to search over. That used to be the one respect in which the translation could not be literal: define-relation expanded to a plain define, so a recursive call sitting next to other goals in a conjunction was built while its caller was, building the tree for adder° built the tree for adder°, and the first query reaching it never returned. Now define-relation is inverse-η-delayed, exactly as the book's defrel: calling a relation only returns a λ that builds the body when it is applied to a state, and then suspends. No call site needs a hand-written delay to terminate any more.
The module still carries the explicit delay it once needed, an eta-expansion around a δ:
(define-syntax-rule (δ° g) (μ s (δ (g s))))
((=° 1 b) (=° '() m) (δ° (adder° 0 n '(1) r)))Three self-calls of adder° wear it: the two that discharge a carry against an empty addend and the one that commutes '(1) into the first position; (aux kanren date) wraps its recursive calls the same way. Around a relation made by define-relation the wrapper is redundant for termination. It is kept because removing it drops a suspension, which can shift where answers of a disjunction interleave -- the expectations below were read off runs with the wrappers in place. It is still required around a goal-returning procedure written with a plain define, which nothing delays.
Reading the expected values
Every expectation below was read off a real run. The third argument of μkanren-run is the grounding flag, and it is #t throughout: a variable the search never had to instantiate is reified as a Greek letter in order of appearance, so (α 1) is a single answer standing for both 2 and 3, and (α . β) is pos° and nothing more. Those partially ground answers are the interesting ones -- they are the relation declining to decide a bit it was never asked about, and an expectation that spelled a concrete bit there would be asserting something the code does not claim. Answer ORDER is asserted too: cond° disjoins by INTERLEAVING its clauses, and for a truth table -- where every clause yields exactly one answer -- the interleaving coincides with textual order, so that order is observable ten definitions later in the order plus° hands back its solutions. Where a clause yields more than one answer the two part company, and the expectations below are read off the interleaving.
The definitions under test are a module, (aux kanren arith), rather than a preamble to this suite: the arithmetic is worth importing on its own, and keeping it out here means a case cannot quietly depend on a definition it also supplies. The #;-commented alternatives -- the frame 7:12 half-adder, the frame 7:15 full-adder, and the two flawed /°s of frames 8:54 and 8:64 -- are kept because several cases below exist precisely to say what the surviving definition does that the discarded one does not.
test/car°+cdr°: pass
car° and cdr° are not accessors: each is the one constraint (=° (cons a d) p) projected onto a different variable, which is why the same relation runs backwards and (car° q 'x) answers with the invented pair (x . α) -- a fresh tail, reified as a Greek letter, rather than a failure for lack of input.
Both fail on '(), since no substitution unifies the empty list with a cons cell. That is a contract and not an accident: it is why append° has to test null° in its first clause instead of letting the cdr° chain run out on its own, and it is the same reason pos° and >1° downstream can be written purely as shape unifications.
null° and cons° come from (aux kanren micro), not from (aux kanren arith), so the first two assertions pin the library shapes everything else is built on. If cons° ever stopped being (=° c (cons a d)), every (=° `(,a . ,d) n) in chapters 7 and 8 would still compile and would quietly mean something else.
(define (test/car°+cdr° _)
(⊦= '(()) (μkanren-run (q 3 #t) (null° q)))
(⊦= '((1 (2 3)))
(μkanren-run
(q 3 #t)
(fresh° (a d) (cons° a d '(1 2 3)) (=° q (list a d)))))
(⊦= '(a) (μkanren-run (q 3 #t) (car° '(a b c) q)))
(⊦= '((b c)) (μkanren-run (q 3 #t) (cdr° '(a b c) q)))
(⊦= '((1 2 3))
(μkanren-run
(q 3 #t)
(fresh° (a d) (car° '(1 2 3) a) (cdr° '(1 2 3) d) (=° q (cons a d)))))
(⊦= '((x . α)) (μkanren-run (q 3 #t) (car° q 'x)))
(⊦= '((α y z)) (μkanren-run (q 3 #t) (cdr° q '(y z))))
(⊦= '() (μkanren-run (q 3 #t) (car° '() q)))
(⊦= '() (μkanren-run (q 3 #t) (cdr° '() q))))
((eta 0.001) (memory #(16793184 4877528 1048576)) (stdout "") (stderr ""))
test/append°: pass
Three directions of one relation. Forward it concatenates; with the second argument fresh it subtracts a known prefix; with both inputs fresh and the output ground it enumerates the four ways to cut (a b c) in two, both empty-side boundaries included. That third query asks for nine answers and gets four: the assertion is that the search is exhaustive AND terminates, which a spot check for one split would not catch.
The fourth query runs the generator direction, output fresh, and it does not terminate on its own -- it is the count that stops it. Each answer is one cons longer and the still-fresh elements appear as the same Greek letters in x and y, showing they are shared cells and not independent unknowns. That is exactly the shape exp2° leans on when it calls (append° b `(1 . ,b) b2) to double the width of a ground b.
The last case demands a prefix longer than the whole list and gets no answers. A function would have to err or truncate; a relation just has an empty answer stream, and pinning that here is what lets the arithmetic built on it treat failure as ordinary arithmetic information.
(define (test/append° _)
(⊦= '((a b c d)) (μkanren-run (q 3 #t) (append° '(a b) '(c d) q)))
(⊦= '((c d)) (μkanren-run (q 3 #t) (append° '(a b) q '(a b c d))))
(⊦= '((() (a b c)) ((a) (b c)) ((a b) (c)) ((a b c) ()))
(μkanren-run
(q 9 #t)
(fresh° (x y) (append° x y '(a b c)) (=° q (list x y)))))
(⊦= '((() (c)) ((α) (α c)) ((α β) (α β c)) ((α β γ) (α β γ c)))
(μkanren-run
(q 4 #t)
(fresh° (x y) (append° x '(c) y) (=° q (list x y)))))
(⊦= '()
(μkanren-run
(q 3 #t)
(fresh°
(x y)
(append° x y '(a b c))
(=° x '(a b c d))
(=° q (list x y))))))
((eta 0.003) (memory #(16793184 4882920 1048576)) (stdout "") (stderr ""))
test/bit-xor°+bit-and°: pass
Both truth tables in full, all four rows each, asked with a count of nine so that a fifth answer or a missing row would fail the case. These two relations are the entire arithmetic content of chapters 7 and 8 -- everything preceding them in the module is plumbing -- so a single transposed row would come back as a wrong sum ten definitions later, with nothing local to blame.
The answer ORDER is asserted too, and the two tables do not share it: upstream writes bit-and° as 00, 10, 01, 11 while bit-xor° is 00, 01, 10, 11. Each clause of these tables yields exactly one answer, so cond°'s interleaving degenerates to textual order here; that order is observable and it feeds into the order in which adder° and *° enumerate their solutions, which past the leaves is an interleaving and no longer clause order.
Run backwards from r, bit-xor° has two preimages and bit-and° has one; that asymmetry is what makes the carry bit the deterministic half of half-adder°. The final case feeds a non-bit 2 and gets nothing: the tables are closed, so these relations reject as well as generate, and a malformed bit list dies at the leaf instead of producing a plausible-looking number.
(define (test/bit-xor°+bit-and° _)
(⊦= '((0 0 0) (0 1 1) (1 0 1) (1 1 0))
(μkanren-run
(q 9 #t)
(fresh° (x y r) (bit-xor° x y r) (=° q (list x y r)))))
(⊦= '((0 0 0) (1 0 0) (0 1 0) (1 1 1))
(μkanren-run
(q 9 #t)
(fresh° (x y r) (bit-and° x y r) (=° q (list x y r)))))
(⊦= '((0 1) (1 0))
(μkanren-run (q 9 #t) (fresh° (x y) (bit-xor° x y 1) (=° q (list x y)))))
(⊦= '((1 1))
(μkanren-run (q 9 #t) (fresh° (x y) (bit-and° x y 1) (=° q (list x y)))))
(⊦= '()
(μkanren-run
(q 9 #t)
(fresh° (y r) (bit-xor° 2 y r) (=° q (list y r))))))
((eta 0.002) (memory #(16793184 4885680 1048576)) (stdout "") (stderr ""))
test/half-adder°: pass
The whole table, derived rather than written: half-adder° is just bit-xor° conjoined with bit-and°, and the enumeration order it produces is bit-xor°'s (00, 01, 10, 11), the first conjunct driving the search while the second filters. The #;-commented alternative from frame 7:12 spells the same four rows out as a table; keeping this case honest is what would expose a divergence between the two.
The last three queries run it backwards, from the outputs to the inputs, which only works because the sum and carry are related by unification and not computed: given r=0 and c=1 there is exactly one input pair that generates a carry, given r=1 and c=0 there are two, and r=1 with c=1 has none at all.
That empty answer is the point of the case. It encodes the invariant x + y = r + 2c, whose maximum is 2, so a sum bit and a carry bit can never both be set. A table with one wrong carry would still answer every forward query plausibly and would only show up as an impossible pair becoming possible here.
(define (test/half-adder° _)
(⊦= '((0 0 0 0) (0 1 1 0) (1 0 1 0) (1 1 0 1))
(μkanren-run
(q 9 #t)
(fresh° (x y r c) (half-adder° x y r c) (=° q (list x y r c)))))
(⊦= '((1 1))
(μkanren-run
(q 9 #t)
(fresh° (x y) (half-adder° x y 0 1) (=° q (list x y)))))
(⊦= '((0 1) (1 0))
(μkanren-run
(q 9 #t)
(fresh° (x y) (half-adder° x y 1 0) (=° q (list x y)))))
(⊦= '()
(μkanren-run
(q 9 #t)
(fresh° (x y) (half-adder° x y 1 1) (=° q (list x y))))))
((eta 0.002) (memory #(16793184 4887168 1048576)) (stdout "") (stderr ""))
test/full-adder°: pass
All eight rows of the table version -- the one the module keeps live because the half-adder°-based definition of frame 7:15, kept #;-commented beside it, costs three sub-goals per bit. This is the leaf of every addition, subtraction, multiplication, division and logarithm in the rest of the module, so it is the one table worth asserting exhaustively, count of seventeen and all.
The next three queries invert it on the output pair, and together they partition the eight rows by how many of b, x, y are set: three ways to reach (r c)=(1,0), three to reach (0,1), exactly one to reach (1,1), and the unlisted (0,0) is the all-zero row. That is b + x + y = r + 2c read off the answer counts, and it is the invariant gen-adder° assumes when it threads e into the next bit position.
The last case pins b=0 to the half-adder table: the same four rows, as they must be, but in a different ORDER, because the clause order of this table is bit-and°-shaped (00, 10, 01, 11) while half-adder° inherits bit-xor°'s. The two relations are extensionally equal and operationally distinct, and it is the operational half that decides the order in which plus° hands back its solutions.
(define (test/full-adder° _)
(⊦= '((0 0 0 0 0)
(1 0 0 1 0)
(0 1 0 1 0)
(1 1 0 0 1)
(0 0 1 1 0)
(1 0 1 0 1)
(0 1 1 0 1)
(1 1 1 1 1))
(μkanren-run
(q 17 #t)
(fresh° (b x y r c) (full-adder° b x y r c) (=° q (list b x y r c)))))
(⊦= '((1 0 0) (0 1 0) (0 0 1))
(μkanren-run
(q 9 #t)
(fresh° (b x y) (full-adder° b x y 1 0) (=° q (list b x y)))))
(⊦= '((1 1 0) (1 0 1) (0 1 1))
(μkanren-run
(q 9 #t)
(fresh° (b x y) (full-adder° b x y 0 1) (=° q (list b x y)))))
(⊦= '((1 1 1))
(μkanren-run
(q 9 #t)
(fresh° (b x y) (full-adder° b x y 1 1) (=° q (list b x y)))))
(⊦= '((0 0 0 0) (1 0 1 0) (0 1 1 0) (1 1 0 1))
(μkanren-run
(q 9 #t)
(fresh° (x y r c) (full-adder° 0 x y r c) (=° q (list x y r c))))))
((eta 0.004) (memory #(16793184 4888968 1048576)) (stdout "") (stderr ""))
test/build-num: pass
The numeral, fixed once for the whole suite. Bits are little-endian -- (build-num 2) is (0 1), not (1 0) -- and zero is the empty list, not (0). The quotient recursion stops at zero?, so a numeral never carries a trailing 0: that is the canonicality the last assertion pins, and it is what makes the encoding injective. One number, one term.
The last two lines are the bridge, and they are the reason every other case in this file may write its expectation as a bare bit list. plus° and *° reconstruct their answers bit by bit through gen-adder°, never by calling build-num; the assertions say the two constructions agree, term for term. Were a relation ever to answer (0 0 0 1 0) for eight -- arithmetically the same number, a different term -- it would still unify with nothing here and every literal below would be testing a different encoding than the one the relations speak.
(define (test/build-num _)
(⊦= '() (build-num 0))
(⊦= '(1) (build-num 1))
(⊦= '(0 1) (build-num 2))
(⊦= '(1 1) (build-num 3))
(⊦= '(0 0 1) (build-num 4))
(⊦= '(1 0 1) (build-num 5))
(⊦= '(0 1 1) (build-num 6))
(⊦= '(1 1 1) (build-num 7))
(⊦= '(0 0 0 1) (build-num 8))
(⊦= '(1 0 0 0 1) (build-num 17))
(⊦= '(0 1 0 1 0 1) (build-num 42))
(⊦= '(1 1 1 1 1 1 1 1) (build-num 255))
(⊦= '(0 0 0 0 0 0 0 0 1) (build-num 256))
(⊦= '(1 1 1 1 1 1 1 1) (map (lambda (n) (last (build-num n))) (iota 8 1)))
(⊦= (build-num 8)
(car (μkanren-run (r 1 #t) (plus° (build-num 3) (build-num 5) r))))
(⊦= (build-num 15)
(car (μkanren-run (r 1 #t) (*° (build-num 3) (build-num 5) r)))))
((eta 0.003) (memory #(16793184 4892952 1048576)) (stdout "") (stderr ""))
test/pos°: pass
pos° inspects no bits. Its body is the single unification (=° `(,a . ,d) n), so what it actually decides is "n has a car", and it decides it in constant time with no choice point. That it also means n > 0 is a property of the encoding, not of the relation: build-num sends zero, and only zero, to a term without a car.
The last three lines mark exactly where the two readings come apart. (0) is a non-canonical zero -- build-num never emits it -- and pos° says yes; the improper pair (1 . 2) is not a numeral at all and it says yes too; only an atom, with no car to take, fails. So pos° is a structural guard and nothing more, and the obligation to keep non-canonical junk out of it belongs to its callers -- adder°, *°, split° -- which only ever hand it a cdr of a numeral they built themselves.
(define (test/pos° _)
(⊦= '() (μkanren-run (r 2 #t) (pos° '()) (=° r 'yes)))
(⊦= '() (μkanren-run (r 2 #t) (pos° (build-num 0)) (=° r 'yes)))
(⊦= '(yes) (μkanren-run (r 2 #t) (pos° (build-num 1)) (=° r 'yes)))
(⊦= '(yes) (μkanren-run (r 2 #t) (pos° (build-num 7)) (=° r 'yes)))
(⊦= '(yes) (μkanren-run (r 2 #t) (pos° '(0)) (=° r 'yes)))
(⊦= '(yes) (μkanren-run (r 2 #t) (pos° '(1 . 2)) (=° r 'yes)))
(⊦= '() (μkanren-run (r 2 #t) (pos° 5) (=° r 'yes))))
((eta 0.001) (memory #(16793184 4894064 1048576)) (stdout "") (stderr ""))
test/>1°: pass
Same trick one bit further along: (=° `(,a ,ad . ,dd) n) demands two cars, so the numerals it accepts are exactly those of length two or more, i.e. n > 1. The two rejections are the ones that matter in adder° and *°: zero and one, the cases where the general bit-by-bit clauses would recur on a numeral with no bits left.
The improper pair separates the two guards. (1 . 2) satisfies pos° but not >1°, because the second pattern also forces the cdr to be a pair. (a b c) passes, which says again that these relations count spine cells and never look at whether the cars are bits.
(define (test/>1° _)
(⊦= '() (μkanren-run (r 2 #t) (>1° '()) (=° r 'yes)))
(⊦= '() (μkanren-run (r 2 #t) (>1° (build-num 1)) (=° r 'yes)))
(⊦= '(yes) (μkanren-run (r 2 #t) (>1° (build-num 2)) (=° r 'yes)))
(⊦= '(yes) (μkanren-run (r 2 #t) (>1° (build-num 3)) (=° r 'yes)))
(⊦= '() (μkanren-run (r 2 #t) (>1° '(1 . 2)) (=° r 'yes)))
(⊦= '(yes) (μkanren-run (r 2 #t) (>1° '(a b c)) (=° r 'yes))))
((eta 0.0) (memory #(16793184 4897712 1048576)) (stdout "") (stderr ""))
test/pos°+>1°/fresh: pass
Run backwards, neither relation enumerates. Asked for five answers each returns one, because each is a single unification: pos° instantiates n to a pair with both fields still fresh, >1° to a pair whose cdr is a pair. Conjoining the two does not add an answer, it refines the same term. This is the property the callers depend on: a guard sitting in front of a recursive clause of adder° or *° must not open a choice point, and a pos° that generated all positive numerals instead of constraining one would turn every clause that guards on it into an infinite stream.
The last line names the reifier. μkanren-run's third argument is the grounded flag: #t prints a still-fresh variable as α, β, γ in order of appearance, while #f hands back the raw lambda form. Every partially-ground expectation in this file -- here, and the α that <° and log° leave behind -- is written in the #t language.
(define (test/pos°+>1°/fresh _)
(⊦= '((α . β)) (μkanren-run (n 5 #t) (pos° n)))
(⊦= '((α β . γ)) (μkanren-run (n 5 #t) (>1° n)))
(⊦= '((α β . γ)) (μkanren-run (n 5 #t) (pos° n) (>1° n)))
(⊦= '((λ (α β) (cons α β))) (μkanren-run (n 1 #f) (pos° n))))
((eta 0.002) (memory #(16793184 4900160 1048576)) (stdout "") (stderr ""))
test/pos°/guard-in-adder°: pass
Why pos° is in adder° at all. The second clause, ((=° 0 b) (=° '() n) (=° m r) (pos° m)), does not need its guard to be true -- 0 + m = m holds for m = 0 as well -- it needs it to stay disjoint from the first clause, which already answers when m is '(). Measured on a copy of adder° with that one conjunct deleted: x + y = 0 answers ((() ()) (() ())) and () + () = r answers (() ()), the same derivation twice. The overlap is confined to zero -- x + y = 6 returns the same seven answers with or without the guard -- but a duplicate is still a lie about the search: the count argument of μkanren-run asks for n answers, not n derivations, and a relation used as a filter inside *° and /° has to be able to say "once".
The two identity directions in the last lines come out of different clauses and are worth reading together: 5 + 0 is decided by clause one with pure unification and no guard at all, 0 + 5 by clause two, which is the guarded one. Asymmetric code, symmetric answers.
(define (test/pos°/guard-in-adder° _)
(⊦= '((() ()))
(μkanren-run
(r 5 #t)
(fresh° (x y) (plus° x y (build-num 0)) (=° r (list x y)))))
(⊦= '(()) (μkanren-run (r 5 #t) (plus° '() '() r)))
(⊦= (list (build-num 5)) (μkanren-run (r 5 #t) (plus° '() (build-num 5) r)))
(⊦= (list (build-num 5)) (μkanren-run (r 5 #t) (plus° (build-num 5) '() r))))
((eta 0.001) (memory #(16793184 4904616 1048576)) (stdout "") (stderr ""))
test/plus°: pass
plus° is adder° with the carry nailed to 0, so these are the cases where the relation happens to behave like a function. Every query asks for two answers and is handed one: the eight clauses of adder° are mutually exclusive by construction, and the pos°/>1° guards are what stops 7+0 from being proved twice, once by the empty-addend clause and once through gen-adder°. A second answer here would mean a guard was dropped, not that arithmetic broke. 15+1 is the carry-propagation case: every bit of the first addend flips and the numeral grows a digit, the only forward query that drives the full-adder chain from end to end. The last line runs the very same goal with the first addend fresh -- nothing in plus° distinguishes input from output, so subtraction is already available before minus° is defined.
(define (test/plus° _)
(⊦= `(,(build-num 8))
(μkanren-run (r 2 #t) (plus° (build-num 3) (build-num 5) r)))
(⊦= `(,(build-num 7)) (μkanren-run (r 2 #t) (plus° '() (build-num 7) r)))
(⊦= `(,(build-num 7)) (μkanren-run (r 2 #t) (plus° (build-num 7) '() r)))
(⊦= '((0 1)) (μkanren-run (r 2 #t) (plus° '(1) '(1) r)))
(⊦= `(,(build-num 16))
(μkanren-run (r 2 #t) (plus° (build-num 15) (build-num 1) r)))
(⊦= `(,(build-num 17))
(μkanren-run (r 2 #t) (plus° (build-num 12) (build-num 5) r)))
(⊦= `(,(build-num 7))
(μkanren-run
(r 2 #t)
(fresh° (x) (plus° x (build-num 5) (build-num 12)) (=° r x)))))
((eta 0.006) (memory #(16793184 4906568 1048576)) (stdout "") (stderr ""))
test/adder°: pass
The carry b is a bit, not a numeral: (adder° 1 n m r) is n+m+1, and the two clauses that consume a set carry against an empty addend discharge it by rewriting it into the literal '(1) and recurring with b back at 0 -- which is why 7+0 with a carry is answered by the same code path as 7+1, and why (adder° 1 '() '() r) bottoms out at '(1). Those two self-calls, together with (adder° b '(1) n r), are exactly the calls this file wraps in δ°: they are clause-level conjuncts of a cond°, which this port once had to delay by hand; since define-relation delays every relation, the wrappers only pin the interleaving, they no longer decide termination. The last two lines ground the sum and leave the carry fresh: the bit is recovered, uniquely, from 3+4 against 8 rather than 7.
(define (test/adder° _)
(⊦= `(,(build-num 7))
(μkanren-run (r 2 #t) (adder° 0 (build-num 3) (build-num 4) r)))
(⊦= `(,(build-num 8))
(μkanren-run (r 2 #t) (adder° 1 (build-num 3) (build-num 4) r)))
(⊦= '(()) (μkanren-run (r 2 #t) (adder° 0 '() '() r)))
(⊦= '((1)) (μkanren-run (r 2 #t) (adder° 1 '() '() r)))
(⊦= `(,(build-num 8)) (μkanren-run (r 2 #t) (adder° 1 (build-num 7) '() r)))
(⊦= `(,(build-num 8)) (μkanren-run (r 2 #t) (adder° 1 '() (build-num 7) r)))
(⊦= '(1)
(μkanren-run
(b 3 #t)
(adder° b (build-num 3) (build-num 4) (build-num 8))))
(⊦= '(0)
(μkanren-run
(b 3 #t)
(adder° b (build-num 3) (build-num 4) (build-num 7)))))
((eta 0.004) (memory #(16793184 4912600 1048576)) (stdout "") (stderr ""))
test/gen-adder°: pass
gen-adder° is deliberately not symmetric. Its body insists on (=° `(,d . ,y) m) with (pos° y) and on (=° `(,c . ,z) r) with (pos° z), so the second addend and the sum must both be at least two bits wide: it adds 1+3 and refuses 3+1, 1+1 and 0+5. Those refusals are a contract with its only caller, not a defect -- adder° reaches it solely behind (=° '(1) n) or (>1° n), and hands the shapes it drops to sibling clauses, notably the one that commutes (=° '(1) m) into (adder° b '(1) n r), which is why 3+1 still answers 4 on the line below. Calling the relation directly is the only way those guards are observable at all; every other query in this file meets gen-adder° already filtered.
(define (test/gen-adder° _)
(⊦= `(,(build-num 11))
(μkanren-run (r 2 #t) (gen-adder° 0 (build-num 6) (build-num 5) r)))
(⊦= `(,(build-num 12))
(μkanren-run (r 2 #t) (gen-adder° 1 (build-num 6) (build-num 5) r)))
(⊦= `(,(build-num 4))
(μkanren-run (r 2 #t) (gen-adder° 0 (build-num 1) (build-num 3) r)))
(⊦= '() (μkanren-run (r 1 #t) (gen-adder° 0 (build-num 3) (build-num 1) r)))
(⊦= '() (μkanren-run (r 1 #t) (gen-adder° 0 (build-num 1) (build-num 1) r)))
(⊦= '() (μkanren-run (r 1 #t) (gen-adder° 0 '() (build-num 5) r)))
(⊦= `(,(build-num 4))
(μkanren-run (r 2 #t) (adder° 0 (build-num 3) (build-num 1) r))))
((eta 0.004) (memory #(16793184 4912944 1048576)) (stdout "") (stderr ""))
test/minus°: pass
minus° has no arithmetic of its own: its whole body is (plus° m k n), subtraction being addition read in another direction, and the final line reads it in a third one by leaving the subtrahend fresh. The two empty answers are the point of the case. This encoding has no negative numeral, so 3-5 is neither an error nor a distinguished value: it is the plain absence of a k with 5+k=3. Getting '() back means the search was exhausted, not abandoned -- it terminates only because the ground difference bounds adder°'s recursion -- so asking for one answer and being handed none asserts more than any of the positive lines above.
(define (test/minus° _)
(⊦= `(,(build-num 7))
(μkanren-run (r 2 #t) (minus° (build-num 12) (build-num 5) r)))
(⊦= '(()) (μkanren-run (r 2 #t) (minus° (build-num 5) (build-num 5) r)))
(⊦= `(,(build-num 7)) (μkanren-run (r 2 #t) (minus° (build-num 7) '() r)))
(⊦= '() (μkanren-run (r 1 #t) (minus° (build-num 3) (build-num 5) r)))
(⊦= '() (μkanren-run (r 1 #t) (minus° '() (build-num 1) r)))
(⊦= `(,(build-num 5))
(μkanren-run
(r 3 #t)
(fresh° (x) (minus° (build-num 12) x (build-num 7)) (=° r x)))))
((eta 0.005) (memory #(16793184 4913544 1048576)) (stdout "") (stderr ""))
test/plus°/pairs: pass
The fully relational direction, with both addends fresh, and the only case here that pins a complete answer set: eight answers are requested and five arrive, so the stream was exhausted. 4 has exactly those five ordered decompositions -- zero on either side included -- and no pair is enumerated twice. Completeness and termination are separate properties and a query that merely checks the first few answers can see neither; widen one guard in adder° and this is the assertion that notices. The order is the interleaving of cond°'s disjunction rather than magnitude, which is why 4+0 and 0+4 precede 1+3; the sum-to-6 line pins that same sequence on its first three answers without paying for the full enumeration.
(define (test/plus°/pairs _)
(⊦= '(((0 0 1) ()) (() (0 0 1)) ((1) (1 1)) ((1 1) (1)) ((0 1) (0 1)))
(μkanren-run
(r 8 #t)
(fresh° (x y) (plus° x y (build-num 4)) (=° r (list x y)))))
(⊦= '(((0 1 1) ()) (() (0 1 1)) ((1) (1 0 1)))
(μkanren-run
(r 3 #t)
(fresh° (x y) (plus° x y (build-num 6)) (=° r (list x y))))))
((eta 0.009) (memory #(16793184 4917200 1048576)) (stdout "") (stderr ""))
test/*°: pass
Nine products, each asked for with a count of two so that the assertion also pins the number of answers: *° must succeed exactly once on ground factors and then exhaust its stream, not leave a redundant branch alive. The two operands are not symmetric in the code even though the answers are: with n odd and m even the sixth clause recurs as (*° m n p), swapping the pair so the even operand is the one that gets halved by clause five. Three of the nine rows reach the seventh clause, the only one that hands the work to odd-*°: 3*5 enters it once and is the smallest odd-times-odd product, 6*7 once after clause five has halved the 6 into (*° 3 7 z), and 7*7 eight times -- depth, not path, is what that last row buys, and deleting the clause costs exactly those three of the nine their answer.
The last two are the zero clauses, and they are the only place *° answers without grounding its arguments. (*° '() m '()) has a single answer that says nothing at all about m -- it reifies as α -- while (*° n '() '()) answers twice, once from (=° '() n) and once from (pos° n), so a non-empty n comes back as the bare pair (α . β). Zero times anything is the one fact this arithmetic knows without looking at the bits.
(define (test/*° _)
(⊦= (list (build-num 0))
(μkanren-run (r 2 #t) (*° (build-num 0) (build-num 5) r)))
(⊦= (list (build-num 0))
(μkanren-run (r 2 #t) (*° (build-num 5) (build-num 0) r)))
(⊦= (list (build-num 0))
(μkanren-run (r 2 #t) (*° (build-num 0) (build-num 0) r)))
(⊦= (list (build-num 5))
(μkanren-run (r 2 #t) (*° (build-num 1) (build-num 5) r)))
(⊦= (list (build-num 5))
(μkanren-run (r 2 #t) (*° (build-num 5) (build-num 1) r)))
(⊦= (list (build-num 6))
(μkanren-run (r 2 #t) (*° (build-num 2) (build-num 3) r)))
(⊦= (list (build-num 15))
(μkanren-run (r 2 #t) (*° (build-num 3) (build-num 5) r)))
(⊦= (list (build-num 42))
(μkanren-run (r 2 #t) (*° (build-num 6) (build-num 7) r)))
(⊦= (list (build-num 49))
(μkanren-run (r 2 #t) (*° (build-num 7) (build-num 7) r)))
(⊦= '(α) (μkanren-run (m 3 #t) (*° '() m '())))
(⊦= '(() (α . β)) (μkanren-run (n 3 #t) (*° n '() '()))))
((eta 0.017) (memory #(16793184 4918800 1048576)) (stdout "") (stderr ""))
test/division-by-*°: pass
The same goal run backwards: fix the product and one factor, leave the other fresh, and *° divides. Nothing in the relation distinguishes input from output -- there is no mode declaration and no guard on which arguments are ground -- so this direction costs no extra code; what it costs is termination, and that is what these five assertions buy. Both factor positions are exercised because the clause that fires differs: with the fresh variable second the ground odd n cannot match clause five at all and the swap in clause six is what fires; with it first clause six is dead and clause five halves the fresh n instead.
The last line is the one that matters. (*° 3 m 13) has no solution, and a relational divide that cannot say so is useless: it would have to enumerate ever longer candidates for m forever. It returns the empty stream in a couple of milliseconds because a ground product bounds every recursion -- clause five insists p begin with a zero bit and shrinks it in step with n, and the seventh clause's bound-*° caps the rest.
(define (test/division-by-*° _)
(⊦= (list (build-num 4))
(μkanren-run (m 2 #t) (*° (build-num 3) m (build-num 12))))
(⊦= (list (build-num 4))
(μkanren-run (m 2 #t) (*° m (build-num 3) (build-num 12))))
(⊦= (list (build-num 3))
(μkanren-run (m 2 #t) (*° (build-num 4) m (build-num 12))))
(⊦= (list (build-num 3))
(μkanren-run (m 2 #t) (*° (build-num 5) m (build-num 15))))
(⊦= '() (μkanren-run (m 1 #t) (*° (build-num 3) m (build-num 13)))))
((eta 0.025) (memory #(16793184 4927048 1048576)) (stdout "") (stderr ""))
test/factorisation-by-*°: pass
Both factors fresh, the product ground: *° factorises. The count is twenty and only six, four, two and one answers exist, which is the whole point of the case -- the run has to walk off the end of the stream and come back. A count of six would pass even if the seventh answer took forever to refute, and that seventh step is exactly where an unbounded *° diverges.
The order is the interleaving order of the clauses, not magnitude order: the two trivial factorisations arrive first from clauses three and four, then the pairs with an even left factor, and (4 3) precedes (3 4). Five is prime and yields only the trivial pair; one yields only (1 1), which is also the statement that this arithmetic has no non-trivial divisors of one. Every answer here is fully ground -- unlike the zero clauses, factorisation of a positive numeral leaves no bit free.
(define (test/factorisation-by-*° _)
(⊦= (list (list (build-num 1) (build-num 12))
(list (build-num 12) (build-num 1))
(list (build-num 2) (build-num 6))
(list (build-num 4) (build-num 3))
(list (build-num 3) (build-num 4))
(list (build-num 6) (build-num 2)))
(μkanren-run
(r 20 #t)
(fresh° (x y) (*° x y (build-num 12)) (=° r (list x y)))))
(⊦= (list (list (build-num 1) (build-num 6))
(list (build-num 6) (build-num 1))
(list (build-num 2) (build-num 3))
(list (build-num 3) (build-num 2)))
(μkanren-run
(r 20 #t)
(fresh° (x y) (*° x y (build-num 6)) (=° r (list x y)))))
(⊦= (list (list (build-num 1) (build-num 5))
(list (build-num 5) (build-num 1)))
(μkanren-run
(r 20 #t)
(fresh° (x y) (*° x y (build-num 5)) (=° r (list x y)))))
(⊦= (list (list (build-num 1) (build-num 1)))
(μkanren-run
(r 20 #t)
(fresh° (x y) (*° x y (build-num 1)) (=° r (list x y))))))
((eta 0.037) (memory #(16793184 4924896 1048576)) (stdout "") (stderr ""))
test/odd-*°: pass
odd-*° is not a three-way product. Its contract is p = 2*(x*m) + m, the distribution of (2x+1)*m that clause seven of *° peels off when both factors are odd, and it is written as (*° x m q) followed by (plus° `(0 . ,q) m p) -- the consed zero bit being the doubling. The first three lines read 2(1*5)+5 = 15, 2(2*3)+3 = 15 and 2(3*3)+3 = 21.
The fourth line is the surprise and the reason this case exists. n occurs nowhere in the body except inside (bound-*° q p n m), so its value is never read; only its length is, and even that only as part of the budget |n|+|m|. Passing '() for n -- arithmetically absurd, since *° only ever calls this with n equal to 2x+1 -- still answers 15, because m alone is long enough to pay for q. Anyone tempted to "use" n in a rewrite is changing a different relation.
The last two lines check the direction *° actually uses it in: with p ground it is a test, and it refutes 14 rather than wandering, which is what keeps clause seven from poisoning the whole stream.
(define (test/odd-*° _)
(⊦= (list (build-num 15))
(μkanren-run
(p 2 #t)
(odd-*° (build-num 1) (build-num 3) (build-num 5) p)))
(⊦= (list (build-num 15))
(μkanren-run
(p 2 #t)
(odd-*° (build-num 2) (build-num 5) (build-num 3) p)))
(⊦= (list (build-num 21))
(μkanren-run
(p 2 #t)
(odd-*° (build-num 3) (build-num 7) (build-num 3) p)))
(⊦= (list (build-num 15))
(μkanren-run
(p 2 #t)
(odd-*° (build-num 1) (build-num 0) (build-num 5) p)))
(⊦= '(yes)
(μkanren-run
(r 2 #t)
(odd-*° (build-num 1) (build-num 3) (build-num 5) (build-num 15))
(=° r 'yes)))
(⊦= '()
(μkanren-run
(r 1 #t)
(odd-*° (build-num 1) (build-num 3) (build-num 5) (build-num 14))
(=° r 'yes))))
((eta 0.017) (memory #(16793184 4927408 1048576)) (stdout "") (stderr ""))
test/bound-*°: pass
bound-*° computes nothing. It succeeds exactly when |q| < |p| and |q| <= |n|+|m|, and the first five lines separate those two conditions: the same q and p pass with a one-bit n and a one-bit m, fail when both are empty, and pass again when the two bits are moved into m -- the recursion peels n first and falls through to m once n runs out, so only the sum of the two lengths is visible. Line two is the same length pattern written entirely in zero bits, which is arithmetic nonsense and still succeeds: the bits are never inspected.
The last four lines are why the relation exists at all. With p ground, bound-*° is a finite generator: it enumerates every list strictly shorter than p and no longer than |n|+|m|, leaving the bits fresh, so the answers reify as (), (α), (α β) and then stop; with p empty there is nothing at all. That is the fuse odd-*° lights before it calls *°: the intermediate product q is confined to a finite set before any multiplying happens. Remove this goal and *° still answers every factorisation in test/factorisation-by-*° -- it simply never admits there are no more.
(define (test/bound-*° _)
(⊦= '(yes)
(μkanren-run (r 2 #t) (bound-*° '(1 1) '(1 1 1) '(1) '(1)) (=° r 'yes)))
(⊦= '(yes)
(μkanren-run (r 2 #t) (bound-*° '(0 0) '(0 0 0) '(0) '(0)) (=° r 'yes)))
(⊦= '()
(μkanren-run (r 1 #t) (bound-*° '(1 1) '(1 1) '(1) '(1)) (=° r 'yes)))
(⊦= '()
(μkanren-run (r 1 #t) (bound-*° '(1 1) '(1 1 1) '() '()) (=° r 'yes)))
(⊦= '(yes)
(μkanren-run (r 2 #t) (bound-*° '(1 1) '(1 1 1) '() '(1 1)) (=° r 'yes)))
(⊦= '(()) (μkanren-run (q 20 #t) (bound-*° q '(1) '(1) '(1))))
(⊦= '(() (α)) (μkanren-run (q 20 #t) (bound-*° q '(1 1) '(1) '(1))))
(⊦= '(() (α) (α β)) (μkanren-run (q 20 #t) (bound-*° q '(1 1 1) '(1) '(1))))
(⊦= '() (μkanren-run (q 20 #t) (bound-*° q '() '(1) '(1)))))
((eta 0.002) (memory #(16793184 4930672 1048576)) (stdout "") (stderr ""))
test/=l°-and-<l°-measure-the-spine: pass
Five is (1 0 1) and six is (0 1 1): the same number of cells, different numbers. That pair is the whole point of this case. =l° holds in both directions and <l° in neither, because neither relation ever looks at a bit: the base cases of =l° pin '() against '() and '(1) against '(1), and its recursive clause asks only that each argument be a pair with a positive tail, leaving the leading bits a and b free. Nine is (1 0 0 1), one cell longer, and that single cell is the entire reason (<l° 5 9) succeeds. Since the representation is canonical -- the last bit of a positive numeral is always 1 -- a shorter numeral is always the smaller number, so <l° never lies about value; it is merely blind to every equal-length pair, and that missing half is exactly what <° restores.
(define (test/=l°-and-<l°-measure-the-spine _)
(⊦= '(yes)
(μkanren-run (r 1 #t) (=l° (build-num 5) (build-num 6)) (=° r 'yes)))
(⊦= '(yes)
(μkanren-run (r 1 #t) (=l° (build-num 6) (build-num 5)) (=° r 'yes)))
(⊦= '() (μkanren-run (r 1 #t) (=l° (build-num 5) (build-num 9)) (=° r 'yes)))
(⊦= '() (μkanren-run (r 1 #t) (<l° (build-num 5) (build-num 6)) (=° r 'yes)))
(⊦= '() (μkanren-run (r 1 #t) (<l° (build-num 6) (build-num 5)) (=° r 'yes)))
(⊦= '(yes)
(μkanren-run (r 1 #t) (<l° (build-num 5) (build-num 9)) (=° r 'yes)))
(⊦= '()
(μkanren-run (r 1 #t) (<l° (build-num 9) (build-num 5)) (=° r 'yes))))
((eta 0.001) (memory #(16793184 4937760 1048576)) (stdout "") (stderr ""))
test/<°-and-<=°-measure-the-value: pass
<° is <l° widened: it first tries the length test, then, for equal lengths, (=l° n m) together with (pos° x) and (plus° n x m) -- a strictly positive witness for the gap. That pos° is the whole of irreflexivity: (<° 5 5) fails only because the witness would have to be '(). The 4-against-5 line is the one that separates the two orderings in the cheapest possible way: same length, so <l° fails, yet <° succeeds through the plus° witness. <=° adds reflexivity with a bare (=° n m), a unification rather than a value comparison, so asking for four answers to (<=° 5 5) still yields one: the <° clause cannot also fire. The same bare unification is why (<=° x x) succeeds for a fresh x and leaves it unbound -- the answer is the reified α. That query is pinned at count 1 deliberately: a second answer never arrives, because the <° branch then walks <l°'s recursive clause forever on two aliased fresh spines.
(define (test/<°-and-<=°-measure-the-value _)
(⊦= '(yes)
(μkanren-run (r 1 #t) (<° (build-num 5) (build-num 6)) (=° r 'yes)))
(⊦= '() (μkanren-run (r 1 #t) (<° (build-num 6) (build-num 5)) (=° r 'yes)))
(⊦= '() (μkanren-run (r 1 #t) (<° (build-num 5) (build-num 5)) (=° r 'yes)))
(⊦= '(yes)
(μkanren-run (r 1 #t) (<° (build-num 4) (build-num 5)) (=° r 'yes)))
(⊦= '() (μkanren-run (r 1 #t) (<l° (build-num 4) (build-num 5)) (=° r 'yes)))
(⊦= '(yes)
(μkanren-run (r 1 #t) (<=° (build-num 5) (build-num 6)) (=° r 'yes)))
(⊦= '(yes)
(μkanren-run (r 4 #t) (<=° (build-num 5) (build-num 5)) (=° r 'yes)))
(⊦= '(α) (μkanren-run (r 1 #t) (fresh° (x) (<=° x x) (=° r x)))))
((eta 0.008) (memory #(16793184 4937040 1048576)) (stdout "") (stderr ""))
test/<=l°-is-not-a-value-test: pass
The trap. (<=l° 6 5) and (<=l° 5 6) both succeed -- =l° holds between them -- while (<=° 6 5) correctly fails. <=l° is a preorder on widths with no antisymmetry to lose, so substituting it for <=° buys a relation that happily proves six no greater than five, and no ground query on a length-differing pair would ever reveal it. The last two lines keep the case from being vacuous: four cells against three is still refused. This is also the only sense in which the relation is used downstream -- base-three-or-more° writes (<=l° ql q) and the discarded /° of frame 8:54 writes (<=l° mq n) -- as a bound on how wide a numeral the search may consider, never as an arithmetic comparison.
(define (test/<=l°-is-not-a-value-test _)
(⊦= '(yes)
(μkanren-run (r 1 #t) (<=l° (build-num 5) (build-num 6)) (=° r 'yes)))
(⊦= '(yes)
(μkanren-run (r 1 #t) (<=l° (build-num 6) (build-num 5)) (=° r 'yes)))
(⊦= '() (μkanren-run (r 1 #t) (<=° (build-num 6) (build-num 5)) (=° r 'yes)))
(⊦= '(yes)
(μkanren-run (r 1 #t) (<=l° (build-num 5) (build-num 9)) (=° r 'yes)))
(⊦= '()
(μkanren-run (r 1 #t) (<=l° (build-num 9) (build-num 5)) (=° r 'yes))))
((eta 0.003) (memory #(16793184 4958432 1048576)) (stdout "") (stderr ""))
test/length-orderings-enumerate-shapes: pass
Run with the second argument fresh, the length orderings answer with shapes, not numbers, and that is what makes them cheap. (=l° 5 m) has exactly one answer however many are asked for: (α β 1) -- three cells, top bit forced to 1 by the '(1) base case, the two low bits free -- one answer standing for 4, 5, 6 and 7 at once. (<l° 5 m) collapses just as hard, to the improper list (α β γ δ . ε): <l° peels three cells off (1 0 1) and discharges the rest with (>1° m), whose unbound tail covers every numeral of four cells or more, so an infinite family of numbers arrives as a single terminating answer. (=l° 0 m) pins the degenerate end: zero is the only numeral of length zero. The <=l° line pins clause order -- the =l° answer comes first -- which no ground query can observe.
(define (test/length-orderings-enumerate-shapes _)
(⊦= '((α β 1)) (μkanren-run (m 5 #t) (=l° (build-num 5) m)))
(⊦= '(()) (μkanren-run (m 3 #t) (=l° '() m)))
(⊦= '((α β γ δ . ε)) (μkanren-run (m 3 #t) (<l° (build-num 5) m)))
(⊦= '((α β 1) (α β γ δ . ε)) (μkanren-run (m 3 #t) (<=l° (build-num 5) m))))
((eta 0.002) (memory #(16793184 4943856 1048576)) (stdout "") (stderr ""))
test/value-orderings-enumerate-numbers: pass
Backwards, <° is finite and complete where <l° is finite and short. Asking for eight answers below five returns four and stops: 0, 1, (α 1) and 4. The middle answer is partially ground on purpose -- α is a reified fresh variable, so that one answer is both 2 and 3, and an assertion that expected a concrete bit there would be asserting something the relation never commits to. The <l° line says which of them were free: the first three are pure length answers, and 4 is the one only the =l° plus plus° branch can produce. <=° prepends five itself, from its (=° n m) clause, ahead of the <° answers. The last line is the mirror direction and the reason this relation terminates upwards at all: one shape answer for everything four cells and wider, then the finitely many equal-length numerals above five, 6 and 7.
(define (test/value-orderings-enumerate-numbers _)
(⊦= (list '() (build-num 1) '(α 1) (build-num 4))
(μkanren-run (n 8 #t) (<° n (build-num 5))))
(⊦= (list '() (build-num 1) '(α 1))
(μkanren-run (n 6 #t) (<l° n (build-num 5))))
(⊦= (list (build-num 5) '() (build-num 1) '(α 1) (build-num 4))
(μkanren-run (n 8 #t) (<=° n (build-num 5))))
(⊦= (list '(α β γ δ . ε) (build-num 6) (build-num 7))
(μkanren-run (m 4 #t) (<° (build-num 5) m))))
((eta 0.011) (memory #(16793184 4946720 1048576)) (stdout "") (stderr ""))
test/mirrored-orderings: pass
The book never writes > or >=: /° and log° only ever ask whether something is smaller, so chapter 8 needs one direction and stops. A relation has no preferred direction though, and these four are the existing goals with their arguments crossed -- the same move the book already makes when it defines minus° as plus° read backwards. They are the one part of (aux kanren arith) that is not in the book, which is why they are pinned here rather than taken on trust.
(define (test/mirrored-orderings _)
(⊦= '(yes)
(μkanren-run (r 3 #t) (>° (build-num 9) (build-num 5)) (=° r 'yes)))
(⊦= '() (μkanren-run (r 3 #t) (>° (build-num 5) (build-num 9)) (=° r 'yes)))
(⊦= '() (μkanren-run (r 3 #t) (>° (build-num 5) (build-num 5)) (=° r 'yes)))
(⊦= '(yes)
(μkanren-run (r 3 #t) (>=° (build-num 5) (build-num 5)) (=° r 'yes)))
(⊦= '(yes)
(μkanren-run (r 3 #t) (>=° (build-num 9) (build-num 5)) (=° r 'yes)))
(⊦= '() (μkanren-run (r 3 #t) (>=° (build-num 5) (build-num 9)) (=° r 'yes)))
(⊦= '(yes)
(μkanren-run (r 3 #t) (>° (build-num 1) (build-num 0)) (=° r 'yes)))
(⊦= '() (μkanren-run (r 3 #t) (>° (build-num 0) (build-num 0)) (=° r 'yes))))
((eta 0.005) (memory #(16793184 4954944 1048576)) (stdout "") (stderr ""))
test/mirrored-orderings/length-vs-value: pass
Six is (0 1 1) and five is (1 0 1) -- same width, different value -- so this is the pair that tells the two mirrored families apart. >° says yes because six is the larger number; >l° says no because neither numeral is the longer one; and >=l° says yes on the strength of =l° alone. A reader reaching for >l° when they meant >° gets no error and no empty stream, just a quietly different question answered, which is why the distinction is asserted rather than described.
(define (test/mirrored-orderings/length-vs-value _)
(⊦= '(yes)
(μkanren-run (r 3 #t) (>l° (build-num 9) (build-num 5)) (=° r 'yes)))
(⊦= '() (μkanren-run (r 3 #t) (>l° (build-num 5) (build-num 9)) (=° r 'yes)))
(⊦= (list '(0 1 1) '(1 0 1)) (list (build-num 6) (build-num 5)))
(⊦= '(yes)
(μkanren-run (r 3 #t) (>° (build-num 6) (build-num 5)) (=° r 'yes)))
(⊦= '() (μkanren-run (r 3 #t) (>l° (build-num 6) (build-num 5)) (=° r 'yes)))
(⊦= '(yes)
(μkanren-run (r 3 #t) (>=l° (build-num 6) (build-num 5)) (=° r 'yes))))
((eta 0.002) (memory #(16793184 4949608 1048576)) (stdout "") (stderr ""))
test/mirrored-orderings/generate: pass
Crossing the arguments crosses the enumeration too, and both directions stay finite. Asked for six numerals above five the relation answers three and closes the stream: (α β γ δ . ε) for everything four cells and wider, then 6 and 7, which between them are every number greater than five. Downwards it answers four -- 0, 1, (α 1) covering both 2 and 3, and 4. >=° prepends five itself in each direction, from the (=° n m) clause of <=°. Counts of six and ten against streams of three and four are the point: they assert exhaustion, not merely the first few answers.
(define (test/mirrored-orderings/generate _)
(⊦= (list '(α β γ δ . ε) (build-num 6) (build-num 7))
(μkanren-run (n 6 #t) (>° n (build-num 5))))
(⊦= (list (build-num 5) '(α β γ δ . ε) (build-num 6) (build-num 7))
(μkanren-run (n 6 #t) (>=° n (build-num 5))))
(⊦= (list '() (build-num 1) '(α 1) (build-num 4))
(μkanren-run (m 10 #t) (>° (build-num 5) m)))
(⊦= (list (build-num 5) '() (build-num 1) '(α 1) (build-num 4))
(μkanren-run (m 10 #t) (>=° (build-num 5) m))))
((eta 0.014) (memory #(16793184 4951904 1048576)) (stdout "") (stderr ""))
test/numeral-equality-is-unification: pass
There is deliberately no =n° or ≠n° beside the four mirrored orderings. build-num is canonical -- little-endian, no trailing zero -- so two numerals denote the same number exactly when their lists unify, and (aux kanren micro)'s own =° and ≠° already decide that. A wrapper would add a name and hide which relation is doing the work. The strengths do differ, and that is worth knowing rather than wrapping away: (=° n m) on two fresh variables unifies them without making either one a numeral, whereas (<=° n m) constrains both to be numerals on the way to answering.
(define (test/numeral-equality-is-unification _)
(⊦= '(yes)
(μkanren-run (r 3 #t) (=° (build-num 5) (build-num 5)) (=° r 'yes)))
(⊦= '(yes)
(μkanren-run (r 3 #t) (≠° (build-num 5) (build-num 4)) (=° r 'yes)))
(⊦= '() (μkanren-run (r 3 #t) (≠° (build-num 5) (build-num 5)) (=° r 'yes))))
((eta 0.001) (memory #(16793184 4953560 1048576)) (stdout "") (stderr ""))
test/multiple°: pass
(multiple° a b) holds exactly when some k makes a times k equal b, and that is the entire definition -- *° supplies the search. The three failing assertions carry the weight. A relation that merely lacked an answer would look the same as one that never finished looking, and the naive reading of multiple° -- guess k, multiply, compare -- does not terminate on a non-multiple, because there is always a larger k left to try. What stops it is bound-*°, whose only job in chapter 8 is to bound that very search by the width of the product, so 100 is refused as a multiple of 7 in a tenth of a second rather than never.
(define (test/multiple° _)
(⊦= '(yes)
(μkanren-run
(r 1 #t)
(multiple° (build-num 3) (build-num 12))
(=° r 'yes)))
(⊦= '(yes)
(μkanren-run
(r 1 #t)
(multiple° (build-num 5) (build-num 5))
(=° r 'yes)))
(⊦= '(yes)
(μkanren-run
(r 1 #t)
(multiple° (build-num 1) (build-num 5))
(=° r 'yes)))
(⊦= '()
(μkanren-run
(r 1 #t)
(multiple° (build-num 3) (build-num 7))
(=° r 'yes)))
(⊦= '()
(μkanren-run
(r 1 #t)
(multiple° (build-num 4) (build-num 10))
(=° r 'yes)))
(⊦= '()
(μkanren-run
(r 1 #t)
(multiple° (build-num 7) (build-num 100))
(=° r 'yes))))
((eta 0.194) (memory #(16793184 4962536 1048576)) (stdout "") (stderr ""))
test/multiple°/divisors: pass
Run with the divisor fresh, multiple° enumerates divisors, and it closes the stream when they run out: twenty requested, six delivered for 12 -- 1, 12, 2, 4, 3, 6, every divisor exactly once and in the interleaved order *° produces them, not in increasing order. For 7 it answers 1 and 7 and stops, which is to say the same goal read backwards is a primality test; for 1 it answers only 1. Each count here is larger than the stream on purpose, so the case pins exhaustion rather than a prefix -- a multiple° that silently dropped a divisor would pass a weaker assertion.
(define (test/multiple°/divisors _)
(⊦= (map build-num '(1 12 2 4 3 6))
(μkanren-run (a 20 #t) (multiple° a (build-num 12))))
(⊦= (map build-num '(1 7))
(μkanren-run (a 10 #t) (multiple° a (build-num 7))))
(⊦= (map build-num '(1))
(μkanren-run (a 10 #t) (multiple° a (build-num 1)))))
((eta 0.027) (memory #(16793184 4957944 1048576)) (stdout "") (stderr ""))
test/multiple°/degenerate-rows: pass
The rows that a hand-written predicate gets wrong. They are not special cases in the definition -- each one falls out of a * k = b -- but they are the ones worth stating. Zero is a multiple of five, with k zero. Zero is a multiple of zero. Five is not a multiple of zero, because no k makes 0 * k five, so the relation simply has no answer where a function would have to raise. And asked which numerals divide zero -- all of them -- it does not enumerate forever: it answers () and (α . β), zero and one reified shape standing for every positive numeral, then closes. That is the payoff of a partially-ground answer: an infinite set delivered in two lines.
(define (test/multiple°/degenerate-rows _)
(⊦= '(yes)
(μkanren-run
(r 1 #t)
(multiple° (build-num 5) (build-num 0))
(=° r 'yes)))
(⊦= '(yes)
(μkanren-run
(r 1 #t)
(multiple° (build-num 0) (build-num 0))
(=° r 'yes)))
(⊦= '()
(μkanren-run
(r 1 #t)
(multiple° (build-num 0) (build-num 5))
(=° r 'yes)))
(⊦= (list '() '(α . β)) (μkanren-run (a 6 #t) (multiple° a (build-num 0)))))
((eta 0.001) (memory #(16793184 4960880 1048576)) (stdout "") (stderr ""))
test/divisor°: pass
(divisor° n d) is (multiple° d n) read from the other end. It earns its name rather than its logic: both spellings put the described numeral second, so (multiple° a b) is "b is a multiple of a" and (divisor° n d) is "d is a divisor of n", and a call site never has to untangle which way round the pair goes. The same six divisors of 12 come back, since it is the same goal.
(define (test/divisor° _)
(⊦= (map build-num '(1 12 2 4 3 6))
(μkanren-run (d 20 #t) (divisor° (build-num 12) d)))
(⊦= '(yes)
(μkanren-run
(r 1 #t)
(divisor° (build-num 12) (build-num 4))
(=° r 'yes)))
(⊦= '()
(μkanren-run
(r 1 #t)
(divisor° (build-num 12) (build-num 5))
(=° r 'yes))))
((eta 0.029) (memory #(16793184 4966472 1048576)) (stdout "") (stderr ""))
test/even°-and-odd°: pass
Parity needs no arithmetic here. The numeral is little-endian, so its first cell IS the parity bit, and these two relations only look at it -- where (multiple° (build-num 2) n) would decide the same question by searching. The pos° inside even° is canonicality rather than parity: it rejects (0), a zero written with a trailing zero, which is also why the empty list needs a clause of its own.
Backwards they are the sharpest generators in the module. Asked for five even numerals the relation answers two -- () and (0 α . β) -- and asked for five odd ones it answers exactly one, (1 . α). Two infinite sets, three answers, and the counts of five are what assert that nothing further is coming.
(define (test/even°-and-odd° _)
(⊦= '(yes) (μkanren-run (r 1 #t) (even° (build-num 0)) (=° r 'yes)))
(⊦= '(yes) (μkanren-run (r 1 #t) (even° (build-num 6)) (=° r 'yes)))
(⊦= '() (μkanren-run (r 1 #t) (even° (build-num 5)) (=° r 'yes)))
(⊦= '(yes) (μkanren-run (r 1 #t) (odd° (build-num 5)) (=° r 'yes)))
(⊦= '() (μkanren-run (r 1 #t) (odd° (build-num 0)) (=° r 'yes)))
(⊦= '() (μkanren-run (r 1 #t) (odd° (build-num 6)) (=° r 'yes)))
(⊦= (list '() '(0 α . β)) (μkanren-run (n 5 #t) (even° n)))
(⊦= (list '(1 . α)) (μkanren-run (n 5 #t) (odd° n))))
((eta 0.001) (memory #(16793184 4965240 1048576)) (stdout "") (stderr ""))
test/square°: pass
(square° n m) is (*° n n m) and nothing else, but the repeated variable is the whole point: the same goal read with m ground is the integer square root, because unification is what ties the two factors together and neither position is an input. 144 comes back as 12. The fourth assertion is the one that matters -- 15 has no integer root, and the relation says so and stops, which is again bound-*° doing its work. The enumeration runs 0, 1, 4, 16, 64, 256, which is the order *° reaches them, not the order a reader expects; 9 and 25 arrive later.
(define (test/square° _)
(⊦= (build-num 25) (car (μkanren-run (m 1 #t) (square° (build-num 5) m))))
(⊦= (list (build-num 4)) (μkanren-run (n 1 #t) (square° n (build-num 16))))
(⊦= (list (build-num 12)) (μkanren-run (n 1 #t) (square° n (build-num 144))))
(⊦= '() (μkanren-run (n 1 #t) (square° n (build-num 15))))
(⊦= (map build-num '(0 1 4 16 64 256))
(μkanren-run (m 6 #t) (fresh° (n) (square° n m)))))
((eta 0.042) (memory #(16793184 4970416 1048576)) (stdout "") (stderr ""))
test/composite°: pass
A numeral is composite when it is a product of two numerals each at least two, and >1° says "at least two cells", which for a canonical numeral is exactly "at least two". Stated positively like this it stays a relation and needs nothing the module does not already have.
Its complement, prime°, needs a negation -- "no divisor other than 1 and n exists" -- and costs a good deal more; it has its own cases below. 97 is refused as composite in about a third of a second, and that refusal is most of what primality then reads.
(define (test/composite° _)
(⊦= '(yes) (μkanren-run (r 1 #t) (composite° (build-num 12)) (=° r 'yes)))
(⊦= '(yes) (μkanren-run (r 1 #t) (composite° (build-num 4)) (=° r 'yes)))
(⊦= '() (μkanren-run (r 1 #t) (composite° (build-num 7)) (=° r 'yes)))
(⊦= '() (μkanren-run (r 1 #t) (composite° (build-num 1)) (=° r 'yes)))
(⊦= '() (μkanren-run (r 1 #t) (composite° (build-num 97)) (=° r 'yes))))
((eta 0.604) (memory #(16793184 4984448 1048576)) (stdout "") (stderr ""))
test/between°: pass
Two comparisons conjoined, which with n fresh is a range. Every count here is ten against streams of four, four, one and zero, so each assertion pins the whole range and not a prefix of it. The order is 3 6 5 4 rather than 3 4 5 6 -- the interleaving of or° again -- which is worth seeing written down, because a range is the one construct a reader will assume comes out sorted. An inverted range is simply an empty stream: no error, nothing to catch.
(define (test/between° _)
(⊦= (map build-num '(3 6 5 4))
(μkanren-run (n 10 #t) (between° (build-num 3) n (build-num 6))))
(⊦= (map build-num '(0 3 1 2))
(μkanren-run (n 10 #t) (between° (build-num 0) n (build-num 3))))
(⊦= (list (build-num 5))
(μkanren-run (n 10 #t) (between° (build-num 5) n (build-num 5))))
(⊦= '() (μkanren-run (n 10 #t) (between° (build-num 6) n (build-num 3)))))
((eta 0.019) (memory #(16793184 4978096 1048576)) (stdout "") (stderr ""))
test/common-divisor°: pass
Divides one and divides the other, so with d fresh it enumerates the common divisors. 12 and 18 give 1, 2, 3 and 6, and the largest of those is their gcd -- but only a reader can see that it is the largest, because picking the greatest element of a stream is a negation again ("no common divisor is bigger") -- the same shape of problem that prime° below has to pay for. What the relation does give, cheaply, is coprimality: 7 and 13 share exactly one divisor, so the single-element stream is the answer to "are these coprime". The third line spells the interleaving out once more: 4 and 8 share 1, 4 and 2, delivered in that order.
(define (test/common-divisor° _)
(⊦= (map build-num '(1 2 3 6))
(μkanren-run
(d 20 #t)
(common-divisor° d (build-num 12) (build-num 18))))
(⊦= (map build-num '(1))
(μkanren-run (d 10 #t) (common-divisor° d (build-num 7) (build-num 13))))
(⊦= (map build-num '(1 4 2))
(μkanren-run (d 10 #t) (common-divisor° d (build-num 4) (build-num 8)))))
((eta 0.066) (memory #(16793184 4973136 1048576)) (stdout "") (stderr ""))
test/numeral°: pass
pos° and >1° constrain the SHAPE of a numeral; this one enumerates its VALUES, in increasing order, which is the first enumeration in the module that is not interleaved. A canonical numeral is the empty list or a list of bits whose last cell is 1, and numeral/pos° is that sentence. The bit° inside it is what makes the answers concrete: without it the relation would answer with shapes full of fresh variables, which is the right answer to a different question and useless as a generator.
The last two assertions are the canonicality guard from the other side. (0) and (1 0) denote 0 and 1 in a positional reading, but they are not numerals, and a generator that produced them would make prime° below enumerate the same prime twice.
(define (test/numeral° _)
(⊦= (map build-num '(0 1 2 3 4 5 6 7 8 9))
(μkanren-run (n 10 #t) (numeral° n)))
(⊦= '(yes) (μkanren-run (r 1 #t) (numeral° (build-num 12)) (=° r 'yes)))
(⊦= '() (μkanren-run (r 1 #t) (numeral° '(0)) (=° r 'yes)))
(⊦= '() (μkanren-run (r 1 #t) (numeral° '(1 0)) (=° r 'yes))))
((eta 0.002) (memory #(16793184 4981432 1048576)) (stdout "") (stderr ""))
test/prime°: pass
prime° is the one relation in the module that is not pure. (if° (composite° p) ✗° ✓°) is negation as failure: it asks whether composite° p has an answer NOW, so it is sound only when p is already ground when it runs, and numeral° in front of it is what guarantees that. The order is the definition, not a stylistic choice -- put the negation first and the goal does not return at all, because with p fresh composite° p has answers and the negation fails before the generator ever chooses a candidate.
0 and 1 are excluded by >1°, which on a canonical numeral means "at least two"; 9 and 12 by the composite° refutation. Checked against an ordinary Scheme primality test over 0 to 60, the two agree everywhere.
(define (test/prime° _)
(⊦= '(yes) (μkanren-run (r 1 #t) (prime° (build-num 2)) (=° r 'yes)))
(⊦= '(yes) (μkanren-run (r 1 #t) (prime° (build-num 7)) (=° r 'yes)))
(⊦= '(yes) (μkanren-run (r 1 #t) (prime° (build-num 97)) (=° r 'yes)))
(⊦= '() (μkanren-run (r 1 #t) (prime° (build-num 0)) (=° r 'yes)))
(⊦= '() (μkanren-run (r 1 #t) (prime° (build-num 1)) (=° r 'yes)))
(⊦= '() (μkanren-run (r 1 #t) (prime° (build-num 9)) (=° r 'yes)))
(⊦= '() (μkanren-run (r 1 #t) (prime° (build-num 12)) (=° r 'yes))))
((eta 0.689) (memory #(16793184 5005696 1048576)) (stdout "") (stderr ""))
test/prime°/generates: pass
The payoff of putting the generator first: the same goal with p fresh ENUMERATES the primes, in increasing order, by generate-and-test -- numeral° proposes 2, 3, 4, 5, ... and the negation discards the composite ones. A relation written as a test is a generator for free, which is the whole argument of the book, and it survives here even though the test itself is not pure.
It is not cheap. Each candidate pays for a full composite° refutation, so these eight cost about a third of a second and the first twenty about ten. That is why the case stops at eight: the assertion is that the enumeration is correct and ordered, and twelve more primes would only have asserted patience.
(define (test/prime°/generates _)
(⊦= (map build-num '(2 3 5 7 11 13 17 19))
(μkanren-run (p 8 #t) (prime° p))))
((eta 0.648) (memory #(16793184 4980840 1048576)) (stdout "") (stderr ""))
test/split°: pass
split° is not a shift on n: the second argument is a ruler, and the relation holds exactly when n = h·2^(|r|+1) + l with l < 2^(|r|+1). The rows read 6=1·4+2, 6=3·2+0, 13=1·8+5, 12=3·4+0. Two of them pin what that equation leaves open. Splitting 12 at width 1 answers l = '(), not '(0 0): the halves come back as numerals, and a trailing zero would not fail here but three frames later, when *° or plus° inside base-three-or-more° refuses an unnormalised operand. n = '() drives the first cond° clause and forces both halves empty, which is the base case n-wider-than-m° leans on when it splits a remainder it has not yet proved positive. The last row runs the same equation backwards and reassembles n from its halves; it terminates no matter which of n, l, h are fresh because every recursive clause eats one cell of r and every base clause demands r = '() -- the ground ruler, and nothing else, bounds the depth of the search.
(define (test/split° _)
(⊦= (list (build-num 2) (build-num 1))
(car (μkanren-run
(r 1 #t)
(fresh°
(l h)
(split° (build-num 6) '(1) l h)
(=° r (list l h))))))
(⊦= (list (build-num 0) (build-num 3))
(car (μkanren-run
(r 1 #t)
(fresh° (l h) (split° (build-num 6) '() l h) (=° r (list l h))))))
(⊦= (list (build-num 5) (build-num 1))
(car (μkanren-run
(r 1 #t)
(fresh°
(l h)
(split° (build-num 13) '(0 1) l h)
(=° r (list l h))))))
(⊦= (list (build-num 0) (build-num 3))
(car (μkanren-run
(r 1 #t)
(fresh°
(l h)
(split° (build-num 12) '(1) l h)
(=° r (list l h))))))
(⊦= (list (build-num 0) (build-num 0))
(car (μkanren-run
(r 1 #t)
(fresh° (l h) (split° '() '(1) l h) (=° r (list l h))))))
(⊦= (build-num 6)
(car (μkanren-run
(r 1 #t)
(split° r '(1) (build-num 2) (build-num 1))))))
((eta 0.002) (memory #(16793184 4981920 1048576)) (stdout "") (stderr ""))
test/split°/ruler: pass
No clause of split° ever looks at a digit of r: it is matched only against '() or `(,a . ,r^) with a fresh, so the ruler is consumed as a unary counter. The three rows split 6 at width 2 with the ruler written as the numeral 2, as the numeral 3, and as '(a b), which is not a numeral at all, and all three agree. The last row is the same fact reported by the search itself: asked which ruler splits 6 into l=2, h=1, it answers once, with (α) -- a one-cell list whose element was never constrained. That is the property n-wider-than-m° spends: it passes /°'s remainder as the ruler of both (split° n r nl nh) and (split° q r ql qh) while that remainder is still only bounded by (<° r m), not known. A tidier split° that unified r with a bit list would quietly constrain the remainder and turn long division into guessing.
(define (test/split°/ruler _)
(⊦= (list (build-num 6) (build-num 0))
(car (μkanren-run
(r 1 #t)
(fresh°
(l h)
(split° (build-num 6) '(0 1) l h)
(=° r (list l h))))))
(⊦= (list (build-num 6) (build-num 0))
(car (μkanren-run
(r 1 #t)
(fresh°
(l h)
(split° (build-num 6) '(1 1) l h)
(=° r (list l h))))))
(⊦= (list (build-num 6) (build-num 0))
(car (μkanren-run
(r 1 #t)
(fresh°
(l h)
(split° (build-num 6) '(a b) l h)
(=° r (list l h))))))
(⊦= '((α))
(μkanren-run
(r 3 #t)
(split° (build-num 6) r (build-num 2) (build-num 1)))))
((eta 0.002) (memory #(16793184 4987040 1048576)) (stdout "") (stderr ""))
test//°: pass
/° dispatches on size, and the rows cover all three of its clauses. 2/5 and 0/3 take the first: a dividend narrower than the divisor is not a recursion at all, just q='() and r=n. 5/5 takes the second, where (=l° m n) pins the quotient to 1 and plus° recovers the remainder. 17/3, 12/4 and 7/1 take the third, the only clause that reaches n-wider-than-m°. 12/4 is here because an exact division is the one case whose remainder is '(), so it is the row that would break first if (<° r m) were ever weakened to <=°, and 7/1 is the degenerate divisor on the other side, where the quotient is the dividend itself. The last row divides by zero: no clause can hold, since two of them need (<° r m) and nothing is below '(), and the point of asserting the empty stream is that the failure is finite -- the guards reject before the recursion is entered, so 5/0 costs nothing instead of hanging. Cost note: 17/3 (~60 ms) dominates this family by an order of magnitude -- 12/4 is next at ~7 ms, 7/1 costs ~3 ms and the three narrow cases are at or under 1 ms; the price is in the bit width of the operands, so widen the numbers only with a reason.
(define (test//° _)
(⊦= (list (build-num 0) (build-num 2))
(car (μkanren-run
(r 1 #t)
(fresh°
(q rem)
(/° (build-num 2) (build-num 5) q rem)
(=° r (list q rem))))))
(⊦= (list (build-num 0) (build-num 0))
(car (μkanren-run
(r 1 #t)
(fresh°
(q rem)
(/° '() (build-num 3) q rem)
(=° r (list q rem))))))
(⊦= (list (build-num 1) (build-num 0))
(car (μkanren-run
(r 1 #t)
(fresh°
(q rem)
(/° (build-num 5) (build-num 5) q rem)
(=° r (list q rem))))))
(⊦= (list (build-num 5) (build-num 2))
(car (μkanren-run
(r 1 #t)
(fresh°
(q rem)
(/° (build-num 17) (build-num 3) q rem)
(=° r (list q rem))))))
(⊦= (list (build-num 3) (build-num 0))
(car (μkanren-run
(r 1 #t)
(fresh°
(q rem)
(/° (build-num 12) (build-num 4) q rem)
(=° r (list q rem))))))
(⊦= (list (build-num 7) (build-num 0))
(car (μkanren-run
(r 1 #t)
(fresh°
(q rem)
(/° (build-num 7) (build-num 1) q rem)
(=° r (list q rem))))))
(⊦= '()
(μkanren-run
(r 1 #t)
(fresh° (q rem) (/° (build-num 5) '() q rem) (=° r (list q rem))))))
((eta 0.097) (memory #(16793184 5014752 1048576)) (stdout "") (stderr ""))
test//°/relational: pass
One equation, 17 = 3·5 + 2, asked four ways: each argument in turn left fresh while the other three are ground. Every run asks for two answers and gets one, so these assertions pin exhaustion as well as value -- the stream is not merely correct at its head, it closes, and /° is a function in all four directions on these arguments. The last two directions are the cheap ones, since q and r are what the clauses compute anyway. The first two run the long division backwards: with n or m unknown, the third clause's guards (pos° q), (<l° m n) and (<° r m) are the only thing keeping the width of the answer finite, and split° inside n-wider-than-m° has to assemble a dividend it was never given, which works only because that relation is driven by the ruler rather than by n. Recovering m is the slowest of the four at ~140 ms, five times the forward quotient.
(define (test//°/relational _)
(⊦= (list (build-num 17))
(μkanren-run (r 2 #t) (/° r (build-num 3) (build-num 5) (build-num 2))))
(⊦= (list (build-num 3))
(μkanren-run (r 2 #t) (/° (build-num 17) r (build-num 5) (build-num 2))))
(⊦= (list (build-num 5))
(μkanren-run (r 2 #t) (/° (build-num 17) (build-num 3) r (build-num 2))))
(⊦= (list (build-num 2))
(μkanren-run
(r 2 #t)
(/° (build-num 17) (build-num 3) (build-num 5) r))))
((eta 0.305) (memory #(16793184 4990040 1048576)) (stdout "") (stderr ""))
test/n-wider-than-m°: pass
n-wider-than-m° is the long-division recurrence, not division. It relates n, m, q, r whenever n = m·q + r and says nothing about the remainder being small or the quotient being positive, so on 17 and 3 it streams q=0 r=17, then q=5 r=2, then q=1 r=14, then q=4 r=5, and does not stop there -- all four satisfy the equation and only the second is a quotient. The discipline lives entirely in the caller: /°'s third clause adds (pos° q), (<l° m n) and (<° r m) before delegating, and the second assertion is the same query through /°, asking for four answers and receiving exactly one. The third assertion hands /° the first junk answer directly and watches it be refused. Anyone who inlines n-wider-than-m° into /°, or who moves a guard down into it for symmetry, gets a /° that answers q=0 r=n for every division and still passes any test that only looks at the head of the stream -- which is why this case reads four answers deep.
(define (test/n-wider-than-m° _)
(⊦= (list (list (build-num 0) (build-num 17))
(list (build-num 5) (build-num 2))
(list (build-num 1) (build-num 14))
(list (build-num 4) (build-num 5)))
(μkanren-run
(r 4 #t)
(fresh°
(q rem)
(n-wider-than-m° (build-num 17) (build-num 3) q rem)
(=° r (list q rem)))))
(⊦= (list (list (build-num 5) (build-num 2)))
(μkanren-run
(r 4 #t)
(fresh°
(q rem)
(/° (build-num 17) (build-num 3) q rem)
(=° r (list q rem)))))
(⊦= '()
(μkanren-run
(r 1 #t)
(/° (build-num 17) (build-num 3) '() (build-num 17))
(=° r 'yes))))
((eta 0.391) (memory #(16793184 5001144 1048576)) (stdout "") (stderr ""))
test/exp2°: pass
Despite the name exp2° computes no power: (exp2° n '() q) relates n to q = ⌊log₂ n⌋, and it does so structurally -- the yardstick b is doubled by (append° b `(1 . ,b) b2), which widens a numeral instead of multiplying it. The 15/16 pair is the case that earns its place: it pins the floor, and pins that the step lands exactly on the power of two. Everything log° does in base 2 rests on that.
Run backwards the measure shows how coarse it is: asking which n have ⌊log₂ n⌋ = 3 returns the whole dyadic interval [8,16) as six answers, two of them partially ground -- (0 α 1 1) stands for 12 and 14, (1 α 1 1) for 13 and 15. A bit the search never had to decide is left as a variable rather than split into two answers, and nine answers were requested against six that exist, so the enumeration is complete and terminating, not truncated.
(define (test/exp2° _)
(define (⌊log2⌋ n) (car (μkanren-run (q 1 #t) (exp2° (build-num n) '() q))))
(⊦= (build-num 0) (⌊log2⌋ 1))
(⊦= (build-num 1) (⌊log2⌋ 2))
(⊦= (build-num 2) (⌊log2⌋ 5))
(⊦= (build-num 3) (⌊log2⌋ 8))
(⊦= (build-num 3) (⌊log2⌋ 15))
(⊦= (build-num 4) (⌊log2⌋ 16))
(⊦= '((0 0 0 1) (1 0 0 1) (0 1 0 1) (0 α 1 1) (1 1 0 1) (1 α 1 1))
(μkanren-run (n 9 #t) (exp2° n '() (build-num 3)))))
((eta 0.014) (memory #(16793184 4998608 1048576)) (stdout "") (stderr ""))
test/log°/base-two: pass
log° special-cases base two with the clause (=° '(0 1) b), which performs no arithmetic at all: it reads q off exp2° and then uses split° to cut n at that position for the remainder. Hence none of these five queries costs more than twenty milliseconds where the matching base-three query costs eighty, and the weight is carried by the two non-exact rows, 9 = 2³ + 1 and 12 = 2³ + 4: they are the assertions that would survive nothing, since r reaches them only through split°. 8 and 16 are exact powers whose remainder stays '() however split° misbehaves, and 1 never enters this clause at all -- (pos° dd) demands three bits, so n = 1 is answered by the first clause as q = 0, r = n - 1.
Asking for four answers of log° 12 2 and getting exactly one is the contract, not an accident. The clause commits to q = ⌊log₂ n⌋, after which r is a function of it, so the base-two path is deterministic -- unlike the small frames below, where the same query shape has two answers.
(define (test/log°/base-two _)
(define (q&r k n b)
(μkanren-run
(r k #t)
(fresh°
(q rem)
(log° (build-num n) (build-num b) q rem)
(=° r (list q rem)))))
(⊦= `((,(build-num 0) ,(build-num 0))) (q&r 1 1 2))
(⊦= `((,(build-num 3) ,(build-num 0))) (q&r 1 8 2))
(⊦= `((,(build-num 3) ,(build-num 1))) (q&r 1 9 2))
(⊦= `((,(build-num 3) ,(build-num 4))) (q&r 4 12 2))
(⊦= `((,(build-num 4) ,(build-num 0))) (q&r 2 16 2)))
((eta 0.05) (memory #(16793184 5000776 1048576)) (stdout "") (stderr ""))
test/log°/small-frames: pass
The first four clauses of log° are the non-recursive ones and each fails differently. n ≤ b (3 in base 7) answers q = 0, r = n - 1, because b⁰ = 1 is subtracted, not b. At n = b clauses one and two overlap and log° is honestly nondeterministic: 5 in base 5 answers both 5 = 5¹ + 0 and 5 = 5⁰ + 4, and then stops. Four answers were asked for and two exist, which is the real assertion -- the overlap is exactly two-fold and does not leak into the recursive clause.
Bases 1 and 0 are the frames that exist only to keep log° total. Since 1^q = 1 and 0^q = 0 for every positive q, the clauses constrain q with nothing but (pos° q) and it comes back reified as (α . β) -- a pair with both halves fresh, which is pos° and nothing more. Expecting the Greek letters is expecting log° to decline to enumerate: a future guard that forced q to a concrete numeral here would turn one answer into infinitely many.
(define (test/log°/small-frames _)
(define (q&r k n b)
(μkanren-run
(r k #t)
(fresh°
(q rem)
(log° (build-num n) (build-num b) q rem)
(=° r (list q rem)))))
(⊦= `((,(build-num 0) ,(build-num 2))) (q&r 4 3 7))
(⊦= `((,(build-num 1) ,(build-num 0)) (,(build-num 0) ,(build-num 4)))
(q&r 4 5 5))
(⊦= `(((α . β) ,(build-num 4))) (q&r 3 5 1))
(⊦= `(((α . β) ,(build-num 5))) (q&r 3 5 0)))
((eta 0.007) (memory #(16793184 5005288 1048576)) (stdout "") (stderr ""))
test/log°/base-three-or-more°: pass
Every base that is not 0, 1 or 2 falls through to base-three-or-more°, the most expensive relation in the file: before it commits to a q it brackets b^q ≤ n < b^(q+1) by widths, calling exp2° twice, /° twice and repeated-mul° twice. Nine in base three costs about 80 ms against 5 ms for the base-two clause; that ratio, not the two answers, is why every base-three case in this suite is a one-digit number.
9 and 10 are chosen as a pair so that the exact and the inexact answer share a q, and 10 is asked for four answers to pin that q is the largest exponent with b^q ≤ n: 10 = 3¹ + 7 is arithmetically true and is not an answer -- exhausting that proof costs 300 ms against 85 ms for the first one. The third assertion calls base-three-or-more° directly and gets the same answer, pinning that log°'s last clause delegates the result whole instead of adjusting it -- so a guard added around the call may not change what comes back.
(define (test/log°/base-three-or-more° _)
(define (q&r k n b)
(μkanren-run
(r k #t)
(fresh°
(q rem)
(log° (build-num n) (build-num b) q rem)
(=° r (list q rem)))))
(⊦= `((,(build-num 2) ,(build-num 0))) (q&r 1 9 3))
(⊦= `((,(build-num 2) ,(build-num 1))) (q&r 4 10 3))
(⊦= `((,(build-num 2) ,(build-num 0)))
(μkanren-run
(r 1 #t)
(fresh°
(q rem)
(base-three-or-more° (build-num 9) (build-num 3) q rem)
(=° r (list q rem))))))
((eta 0.671) (memory #(16793184 5007312 1048576)) (stdout "") (stderr ""))
test/repeated-mul°: pass
repeated-mul° is the naive fold n^q = n^(q-1) · n that base-three-or-more° leans on, and its two base clauses carry all the risk. q = 0 answers 1 only for positive n: the (pos° n) guard is the sole reason (repeated-mul° '() '() nq) does not assert 0⁰ = 1. And 1^5 = 1 is the case where the accumulator never grows, so it fails loudly if the recursion counts down on the wrong argument.
Both backward directions terminate on this same definition, for different reasons. q from 3^q = 27 runs because (plus° q1 '(1) q) is a relation and subtracts as happily as it adds; n from n³ = 27 runs because *° factorises, and it terminates only because bound-*° bounds the factors by the width of the ground product.
(define (test/repeated-mul° _)
(define (n^q n q)
(car (μkanren-run
(nq 1 #t)
(repeated-mul° (build-num n) (build-num q) nq))))
(⊦= (build-num 1) (n^q 3 0))
(⊦= (build-num 3) (n^q 3 1))
(⊦= (build-num 27) (n^q 3 3))
(⊦= (build-num 16) (n^q 2 4))
(⊦= (build-num 1) (n^q 1 5))
(⊦= `(,(build-num 3))
(μkanren-run (q 1 #t) (repeated-mul° (build-num 3) q (build-num 27))))
(⊦= `(,(build-num 3))
(μkanren-run (n 1 #t) (repeated-mul° n (build-num 3) (build-num 27)))))
((eta 0.056) (memory #(16793184 5009864 1048576)) (stdout "") (stderr ""))
test/exp°: pass
exp° has no body of its own -- it is (log° n b q '()), exponentiation read as a logarithm with no remainder -- so every use pays whatever log° charges for that base. 2⁵ is a few milliseconds down the base-two clause; 3³ is about 0.4 s through base-three-or-more° and is the slowest assertion in this file. It is also asserted a second time, via repeated-mul° above, on purpose: base-three-or-more° reaches 27 using repeated-mul°, and agreement between the two readings is the cheapest available check that the bracketing is not off by one.
The two backward runs are the interesting ones. (exp° 2 q 32) is a discrete logarithm and needs no help. (exp° b 2 9) is an integer square root, and it works only because exp° pins the remainder to '(): with the remainder left fresh the same query answers (() (1 0 0 1)) and ((1) (0 0 0 1)) first -- bases 0 and 1 satisfy log° for every n -- and only then 3. Zero remainder is exactly the filter that removes the degenerate bases.
(define (test/exp° _)
(define (b^q b q)
(car (μkanren-run (n 1 #t) (exp° (build-num b) (build-num q) n))))
(⊦= (build-num 1) (b^q 2 0))
(⊦= (build-num 32) (b^q 2 5))
(⊦= (build-num 27) (b^q 3 3))
(⊦= `(,(build-num 5))
(μkanren-run (q 1 #t) (exp° (build-num 2) q (build-num 32))))
(⊦= `(,(build-num 3))
(μkanren-run (b 1 #t) (exp° b (build-num 2) (build-num 9)))))
((eta 0.75) (memory #(16793184 5013008 1048576)) (stdout "") (stderr ""))
(aux kanren date): relations over instants in time
An instant is a numeral, and nothing else
A date, in (aux kanren date), is a POSIX time -- the count of seconds since 1970-01-01T00:00:00Z -- held as the little-endian bit list that build-num produces in (aux kanren arith). Not a record, not a tagged vector, not a new datatype: the SAME canonical numeral, so that every relation of that module already applies to an instant and this one contributes names and a calendar rather than a representation. '() is 1970-01-01T00:00:00Z, and it is a FLOOR and not an origin -- the numeral is unsigned, so there is nothing underneath it and no instant before the epoch can be named at all. That single decision is what the whole module is arranged around, and the cases below are arranged around its consequences.
The consequences were MEASURED, at the magnitudes a date query actually uses, and they are not symmetric. A current instant such as 1760000000 is a 31-bit numeral; 86400 is 17 bits; a day-count since the epoch is 15. At 31 bits <°, <=°, plus° and minus° cost a handful of milliseconds and run in every direction, while *° costs seconds and /° of an instant by 86400 NEVER FINISHED -- it was killed after TEN MINUTES. That is not a performance note. It is the statement that the calendar cannot be reached by relational division, so a design that tries is not slow, it is broken.
Layer 1 is pure; everything calendrical is guarded
So the module is two halves with an explicit boundary, and the cases below are grouped to make that boundary visible. Ordering, durations, shifts and bounded enumeration are PURE relations -- before°, after°, same-instant°, elapsed°, shift°, within°, stride°, stride/≤°, span° -- with no project° anywhere between the caller and the answer, no groundness precondition, and every mode available. elapsed° and shift° are one goal, (plus° t d u), read from different sides; running it backwards is how subtraction is spelled, because the module contains no subtraction of its own.
Calendar conversion is the other half, and every relation in it is project°-GUARDED: it reads the substitution when the goal runs, and where the relevant side is ground it escapes to Scheme -- Howard Hinnant's days-from-civil / civil-from-days, integer-only and table-free -- and unifies the result. This is the move prime° already makes in (aux kanren arith), used for a stronger reason: there, the guard is an optimisation over a relation that would merely be slow; here, in the ground-instant direction, it is the difference between the relation existing and not existing.
;; LAYER 1 -- pure. No project°. Every mode, a few milliseconds.
(define-relation (before° t u) (<° t u))
(define-relation (shift° t d u) (plus° t d u))
;; LAYER 2 -- the seam, project°-guarded. t = d*86400 + sod.
;; The `else' branch IS the pure definition, and it is sound, complete and
;; productive -- at small magnitudes. The guard adds two fast paths over it
;; and changes NO answer in any mode; it only changes the clock.
(define-relation (day+second° t d sod)
(project° ((t* t) (d* d) (s* sod))
(let ((T (numeral->number t*)) (DS (numerals->numbers (list d* s*))))
(cond
(T ...) ; escape: /° of an instant by 86400 does not terminate
(DS ...) ; escape: *° at this magnitude costs seconds
(else (fresh° (p) (<° sod DAY) (*° d DAY p) (plus° p sod t)))))))What the guard costs the caller is a MODE OBLIGATION, and it is stated in the cases rather than assumed: because the branch is chosen by looking at instantiation at the moment the goal runs, conjunction ORDER is now part of the meaning. A goal that grounds t must be written before iso°, not after it. Groundness is decided by numeral->number, positive typing over the cells rather than (not (var? x)), so a half-built numeral like (1 0 . β) is correctly NOT taken for ground and falls to the open branch instead of being decoded as though its tail were empty.
The seam, and why weekdays stride
One relation crosses between the two magnitudes, day+second°, and it is the only place in the module where 86400 is written. Everything calendrical sits above it and never sees a 31-bit number again: civil°, day-of-week°, the seven weekday names and the window relations all speak DAY-COUNTS. That is the load-bearing decision. At 15 bits the open fallback of a guarded relation costs a millisecond an answer, so "neither side ground" ENUMERATES REAL DATES instead of being undefined; at 31 bits the same fallback would have to walk two billion seconds.
Weekday enumeration is the headline feature and it is a STRIDE precisely so that it never needs the modulo that would need that division. A weekday is not computed by dividing a day-count by seven -- /° on a day-count was measured at 2.9 s, and multiple° as a divisibility test gave no answer at all after three minutes on a negative case. Instead each weekday has an ANCHOR, the smallest day-count carrying it, and the generator is repeated addition from there:
;; 1970-01-01 is day 0 and a THURSDAY -- verified below against
;; (chicken time posix), which is the one fact no relation can witness for itself.
;; So the first Monday of the epoch is day 4 = 1970-01-05 = unixtime 345600.
(define weekday-epoch-day '#(3 4 5 6 0 1 2)) ; sunday .. saturday
;; GENERATOR ONLY: with x fresh, strictly increasing, ~1 ms an answer.
;; With x ground and OFF the stride it steps past x forever -- measured.
(define-relation (stride° base step x)
(cond°
((=° x base))
((fresh° (next) (plus° base step next) (δ° (stride° next step x))))))
;; The same progression with a ground CEILING, and the ceiling is the whole
;; reason it terminates on a MISS. That is what a test needs.
(define-relation (stride/≤° base step hi x)
(cond°
((=° x base) (<=° base hi))
((fresh° (next) (plus° base step next) (<=° next hi)
(δ° (stride/≤° next step hi x))))))Both relations are pure layer 1, and the cases pin the difference between them, because it is the difference between an enumeration and a decision procedure. day-of-week° takes the other way out for its test direction: with the day-count ground it never strides at all, it escapes, which is why (monday° 20370) and the first four Mondays cost the same nothing.
Reading the expected values
Every expectation was read off a real run, and several of them are written in an order that is not the calendar's. cond° is or° and or° INTERLEAVES, so a dense enumeration comes out permuted: a four-second span° answers 400, 401, 403, 402, and stride/≤° answers 4, 11, 25, 18 where stride° answers 4, 11, 18, 25. Sorting those expectations would hide from a reader the one thing they must know before building a calendar on top of the module, which is that chronology is their job and not the solver's.
Queries ask for more answers than exist wherever the stream is meant to close, so the assertion pins EXHAUSTION and not merely correctness -- a four-second window asked for nine answers hands back four. And an expectation of '() is never decoration. A relation that cannot decide a negative case does not fail, it diverges, and a diverging case prints nothing at all, because the suite reports only once every case has finished. So each '() below is the assertion that a miss TERMINATES: that (monday° thursday-day-count) refuses instead of striding past it forever, that an inverted window is empty instead of silently swapping its bounds, and that a date which does not exist has zero solutions instead of a neighbour's.
A handful of modes are therefore deliberately absent, each named in the case that would have carried it: within° with a fresh middle, stride° as a test, a comparison with its LATER side fresh, and leap-year° on 1900. They diverge, or they answer an infinite family, or -- for 1900 -- they answer correctly for the wrong reason, the epoch floor rather than the century rule; and a suite cannot assert a hang. Where a mode is dropped the prose says what it does instead, and the closing form that answers the same question is tested in its place.
test/before°+after°: pass
None of the five comparisons has a body: before° is <°, after° is <° with its arguments crossed, same-instant° is =°. So what these lines pin is not arithmetic -- (aux kanren arith) already owns that -- but the CROSSING and the strictness, which nothing else in the module would notice if they were wrong: layers 3 and 4 never compare instants. Swap the two arguments of after° and only the fourth line here fails. The first line is the anchor the rest of the file leans on: it reads build-instant back as a plain unixtime, so every later (build-instant 2025 10 9 ...) may be written for a human and still be a claim about 1760000400.
The reflexive pair is the case worth keeping. (before° t t) must FAIL and (not-after° t t) must SUCCEED, and they differ by one clause: <=° is (or° (=° n m) (<° n m)). Drop that =° clause and not-after° silently becomes before° -- no error, no wrong number, just every closed window in the module quietly losing its endpoints. The two boundary lines of test/within°+span° and the base clause of stride/≤° are exactly the things that would then break, three layers away from the edit.
The epoch pair says that the empty numeral is 1970-01-01T00:00:00Z and that it is a FLOOR, not an origin: (before° '() t) holds for every instant this module can name and (before° t '()) holds for none. The representation is unsigned; there is nothing underneath.
The last line reads a comparison BACKWARDS, which is the whole reason these are relations and not predicates: with the earlier side fresh and the later side ground, (not-after° t 3) enumerates 3, 0, 1, 2 and closes. Ground answers, in cond°'s interleaving -- the =° clause of <=° comes first, so the ceiling arrives before the values below it. The numeral is tiny on purpose: the identical query at instant magnitude has 1.76 billion answers, which is why the module tells callers to bound a fresh side with span° rather than with a comparison. Nothing in this clause is project°-guarded -- layer 1 contains no project° at all -- so the caller pays no groundness precondition and gets every mode; the 15 ms a ground comparison costs at 31 bits is the whole bill.
(define (test/before°+after° _)
(⊦= `(,(build-num 1760000400))
(μkanren-run (t 2 #t) (same-instant° t (build-instant 2025 10 9 9 0 0))))
(⊦= '(yes)
(μkanren-run
(q 2 #t)
(=° q 'yes)
(before°
(build-instant 2025 10 9 9 0 0)
(build-instant 2025 10 9 17 30 0))))
(⊦= '()
(μkanren-run
(q 2 #t)
(=° q 'yes)
(before°
(build-instant 2025 10 9 17 30 0)
(build-instant 2025 10 9 9 0 0))))
(⊦= '(yes)
(μkanren-run
(q 2 #t)
(=° q 'yes)
(after°
(build-instant 2025 10 9 17 30 0)
(build-instant 2025 10 9 9 0 0))))
(⊦= '()
(μkanren-run
(q 2 #t)
(=° q 'yes)
(before°
(build-instant 2025 10 9 9 0 0)
(build-instant 2025 10 9 9 0 0))))
(⊦= '(yes)
(μkanren-run
(q 2 #t)
(=° q 'yes)
(not-after°
(build-instant 2025 10 9 9 0 0)
(build-instant 2025 10 9 9 0 0))
(not-before°
(build-instant 2025 10 9 9 0 0)
(build-instant 2025 10 9 9 0 0))
(same-instant°
(build-instant 2025 10 9 9 0 0)
(build-instant 2025 10 9 9 0 0))))
(⊦= '()
(μkanren-run
(q 2 #t)
(=° q 'yes)
(same-instant°
(build-instant 2025 10 9 9 0 0)
(build-instant 2025 10 9 17 30 0))))
(⊦= '(yes)
(μkanren-run
(q 2 #t)
(=° q 'yes)
(before° '() (build-instant 2025 10 9 9 0 0))))
(⊦= '()
(μkanren-run
(q 2 #t)
(=° q 'yes)
(before° (build-instant 2025 10 9 9 0 0) '())))
(⊦= `(,(build-num 3) ,(build-num 0) ,(build-num 1) ,(build-num 2))
(μkanren-run (t 9 #t) (not-after° t (build-num 3)))))
((eta 0.133) (memory #(12582912 3987240 1048576)) (stdout "") (stderr ""))
test/elapsed°: pass
elapsed° is plus° with the names changed, and the first three lines are one goal read three ways: the duration between two instants (12 ms), the later instant from the earlier plus a duration (3 ms), the earlier instant from the later (7 ms). A duration relation that only ran forwards would need a subtraction, and there is none in this module -- the backward reads are not a bonus, they are how subtraction is spelled.
Zero is an answer, not a failure. (elapsed° t d t) returns the one-answer stream (()) -- a stream containing the empty numeral -- and the distinction between that and () is the entire case. Put a pos° on the duration, as a reader tempted to forbid "no time passing" might, and this line turns into an empty stream while every other line in the clause keeps passing.
The negative case is the encoding speaking, and it is the one behaviour a caller from any other date library will guess wrong. (elapsed° later d earlier) does not answer -604800, and does not raise: it is an EMPTY STREAM, because plus° cannot prove later + d = earlier for any numeral d. Same for (elapsed° t d '()). A caller who wants a distance must order the pair first with the previous clause; this relation will not tell them which way round they were. Note that a failing query is still a 13 ms search, not a type check -- the goal is run, it just proves nothing.
Measured from the epoch, the duration IS the instant: (elapsed° '() d t) answers t itself. That line is the representation stated as a theorem, and it is what licenses every other relation in layer 1 to treat instants and durations as the same kind of numeral. The last line leaves BOTH instants fresh with only the duration ground: productive, 2 ms, (0,60) (1,61) (2,62) (3,63) -- it neither hangs nor errors, because plus° has no modes. What it has is magnitudes, and that stream is useful only where the numerals are small.
(define (test/elapsed° _)
(⊦= `(,(build-num 30600))
(μkanren-run
(d 2 #t)
(elapsed°
(build-instant 2025 10 9 9 0 0)
d
(build-instant 2025 10 9 17 30 0))))
(⊦= `(,(build-num 1760031000))
(μkanren-run
(u 2 #t)
(elapsed° (build-instant 2025 10 9 9 0 0) (seconds 30600) u)))
(⊦= `(,(build-num 1760000400))
(μkanren-run
(t 2 #t)
(elapsed° t (seconds 30600) (build-instant 2025 10 9 17 30 0))))
(⊦= '(())
(μkanren-run
(d 2 #t)
(elapsed°
(build-instant 2025 10 9 9 0 0)
d
(build-instant 2025 10 9 9 0 0))))
(⊦= '()
(μkanren-run
(d 2 #t)
(elapsed°
(build-instant 2025 10 9 17 30 0)
d
(build-instant 2025 10 9 9 0 0))))
(⊦= `(,(build-num 1760000400))
(μkanren-run (d 2 #t) (elapsed° '() d (build-instant 2025 10 9 9 0 0))))
(⊦= '()
(μkanren-run (d 2 #t) (elapsed° (build-instant 2025 10 9 9 0 0) d '())))
(⊦= `((,(build-num 0) ,(build-num 60))
(,(build-num 1) ,(build-num 61))
(,(build-num 2) ,(build-num 62))
(,(build-num 3) ,(build-num 63)))
(μkanren-run
(q 4 #t)
(fresh° (t u) (=° q (list t u)) (elapsed° t (build-num 60) u)))))
((eta 0.066) (memory #(12582912 3993768 1048576)) (stdout "") (stderr ""))
test/shift°: pass
shift° and elapsed° are the SAME relation under two names -- both are (plus° t d u) -- and the last line proves it by running a shift° query in elapsed°'s mode and getting the same 30600 the previous clause got. The two names exist for the call site, not for the solver; if one of them ever grows a body of its own, that line is what notices.
The duration builders are LAYER 0 -- plain Scheme, evaluated while the goal tree is being built -- and the seventh line asserts their numerals directly because that is a unit conversion nothing else would catch: (hours 8) is 28800 and (weeks 1) is 604800, and a seconds/hour that drifted would simply move every appointment in silence. They are Scheme and not relations on purpose: (*° d (build-num 3600)) at instant magnitude costs SECONDS, so multiplying by a constant must never reach the relational layer. Multiplying in CHICKEN before the goal exists costs nothing.
The backward shift is subtraction without a subtraction: (shift° t (days 1) u) with u ground recovers the instant a day earlier in 7 ms. The same goal with all three ground is a TEST and decides in 0 ms -- the false line is there so that the mode is asserted rather than assumed, because a relation that answered (yes) to a wrong shift would be a filter that passes everything. (seconds 0) shifts nothing, which is the same ()-is-a-numeral fact as the zero duration above, read from the other side. Everything here is pure; there is no project° between the caller and the answer, so no line in this clause has a groundness precondition to violate.
(define (test/shift° _)
(⊦= `(,(build-num 1760029200))
(μkanren-run
(u 2 #t)
(shift° (build-instant 2025 10 9 9 0 0) (hours 8) u)))
(⊦= `(,(build-num 1760002200))
(μkanren-run
(u 2 #t)
(shift° (build-instant 2025 10 9 9 0 0) (minutes 30) u)))
(⊦= `(,(build-num 1760605200))
(μkanren-run
(u 2 #t)
(shift° (build-instant 2025 10 9 9 0 0) (weeks 1) u)))
(⊦= `(,(build-num 1759944600))
(μkanren-run
(t 2 #t)
(shift° t (days 1) (build-instant 2025 10 9 17 30 0))))
(⊦= `(,(build-num 1760000400))
(μkanren-run
(u 2 #t)
(shift° (build-instant 2025 10 9 9 0 0) (seconds 0) u)))
(⊦= '()
(μkanren-run
(q 2 #t)
(=° q 'yes)
(shift°
(build-instant 2025 10 9 9 0 0)
(days 1)
(build-instant 2025 10 9 17 30 0))))
(⊦= (list (build-num 28800)
(build-num 1800)
(build-num 86400)
(build-num 604800)
(build-num 0))
(list (hours 8) (minutes 30) (days 1) (weeks 1) (seconds 0)))
(⊦= `(,(build-num 30600))
(μkanren-run
(d 2 #t)
(shift°
(build-instant 2025 10 9 9 0 0)
d
(build-instant 2025 10 9 17 30 0)))))
((eta 0.037) (memory #(12582912 3991328 1048576)) (stdout "") (stderr ""))
test/within°+span°: pass
within° is between°, used here only as a TEST -- all three arguments ground, about 30 ms at instant magnitude. The two boundary lines are the reason the case exists: the window is CLOSED, so an instant equal to lo and an instant equal to hi are both in it. between° is (and° (<=° lo n) (<=° n hi)); make either of those strict and exactly these two lines fail while the midpoint and the outside line keep passing. An inverted window, lo after hi, is EMPTY -- it fails, in 18 ms, rather than diverging or quietly swapping the bounds for the caller -- and a point window still contains its point.
span° exists because within° with a fresh middle does not close: between° yields the window and then keeps counting past hi forever. That mode is not asserted here and cannot be; asserting it means hanging the file. What is asserted is that span° answers the same question and STOPS: a four-second window asked for nine answers hands back four, a point window hands back one, and an inverted window hands back none. The over-asking is the assertion -- it pins exhaustion, not merely correctness.
The order is 1760000400, 401, 403, 402, and it is written down exactly that way on purpose. cond° is or° and or° INTERLEAVES, so a dense span comes out permuted; sorting the expectation would hide from the reader the one thing they need to know before building a calendar on top of it, which is that chronology is their job and not the solver's. The last line is the composition that makes an enumeration usable: a span° generating and a before° filtering, 269 ms, two survivors. It is also the cost warning -- roughly 50 ms per second of window at 31 bits, which is why the widest window in this file is four seconds and why the calendar layers stride over day-counts instead of instants.
(define (test/within°+span° _)
(⊦= '(yes)
(μkanren-run
(q 2 #t)
(=° q 'yes)
(within°
(build-instant 2025 10 9 9 0 0)
(build-instant 2025 10 9 12 0 0)
(build-instant 2025 10 9 17 30 0))))
(⊦= '(yes)
(μkanren-run
(q 2 #t)
(=° q 'yes)
(within°
(build-instant 2025 10 9 9 0 0)
(build-instant 2025 10 9 9 0 0)
(build-instant 2025 10 9 17 30 0))))
(⊦= '(yes)
(μkanren-run
(q 2 #t)
(=° q 'yes)
(within°
(build-instant 2025 10 9 9 0 0)
(build-instant 2025 10 9 17 30 0)
(build-instant 2025 10 9 17 30 0))))
(⊦= '()
(μkanren-run
(q 2 #t)
(=° q 'yes)
(within°
(build-instant 2025 10 9 9 0 0)
(build-instant 2025 10 10 12 0 0)
(build-instant 2025 10 9 17 30 0))))
(⊦= '()
(μkanren-run
(q 2 #t)
(=° q 'yes)
(within°
(build-instant 2025 10 9 17 30 0)
(build-instant 2025 10 9 12 0 0)
(build-instant 2025 10 9 9 0 0))))
(⊦= '(yes)
(μkanren-run
(q 2 #t)
(=° q 'yes)
(within°
(build-instant 2025 10 9 9 0 0)
(build-instant 2025 10 9 9 0 0)
(build-instant 2025 10 9 9 0 0))))
(⊦= `(,(build-num 1760000400)
,(build-num 1760000401)
,(build-num 1760000403)
,(build-num 1760000402))
(μkanren-run
(x 9 #t)
(span° (build-num 1760000400) (build-num 1760000403) x)))
(⊦= `(,(build-num 1760000400))
(μkanren-run
(x 4 #t)
(span° (build-instant 2025 10 9 9 0 0)
(build-instant 2025 10 9 9 0 0)
x)))
(⊦= '()
(μkanren-run
(x 4 #t)
(span° (build-instant 2025 10 9 17 30 0)
(build-instant 2025 10 9 9 0 0)
x)))
(⊦= `(,(build-num 1760000400) ,(build-num 1760000401))
(μkanren-run
(x 9 #t)
(span° (build-num 1760000400) (build-num 1760000404) x)
(before° x (build-num 1760000402)))))
((eta 1.001) (memory #(12582912 4003888 1048576)) (stdout "") (stderr ""))
test/stride°+stride/≤°: pass
The two relations differ by a ceiling and that difference is the whole clause. stride° is the GENERATOR: four hourly instants from 09:00, strictly increasing, 9 ms. It has no last answer and therefore cannot be asked a question -- given a ground x that is not on the stride it steps past it forever -- so that mode is documented in the module and deliberately absent here.
stride/≤° carries the bound explicitly, and the MISS is the line that matters: 17:30 is not on an hourly stride from 09:00, and the query returns () in 200 ms instead of running out of memory. Delete the (<=° next hi) conjunct from the recursive clause and that line does not fail -- it HANGS, and a hanging case prints nothing at all, because the suite reports only once every case has finished. The hit line pairs with it so that a relation which simply failed always would not pass for a working test. The last line pins the stricter base clause: (=° x base) is guarded by (<=° base hi), so a base already past the ceiling emits NOTHING, where a base-only clause would emit one answer outside the window it was given.
The nine-answer enumeration is also the price list. Four answers unbounded cost 9 ms; nine answers bounded cost 382 ms, about 53 ms a step, because the ceiling adds a <=° that is itself a search over a 31-bit numeral. An order of magnitude for termination is the right trade -- an enumeration that does not close is not an enumeration -- but it is also, precisely, why every calendrical enumeration in this module strides over DAY-COUNTS at 15 bits and crosses to instants only at the seam. These five lines are the last ones in the file that are pure: from day+second° upward, every relation is project°-guarded and the caller starts paying attention to which side is ground.
(define (test/stride°+stride/≤° _)
(⊦= `(,(build-num 1760000400)
,(build-num 1760004000)
,(build-num 1760007600)
,(build-num 1760011200))
(μkanren-run
(x 4 #t)
(stride° (build-instant 2025 10 9 9 0 0) (hours 1) x)))
(⊦= `(,(build-num 1760000400)
,(build-num 1760004000)
,(build-num 1760007600)
,(build-num 1760011200)
,(build-num 1760014800)
,(build-num 1760018400)
,(build-num 1760022000)
,(build-num 1760025600)
,(build-num 1760029200))
(μkanren-run
(x 12 #t)
(stride/≤°
(build-instant 2025 10 9 9 0 0)
(hours 1)
(build-instant 2025 10 9 17 30 0)
x)))
(⊦= '(yes)
(μkanren-run
(q 2 #t)
(=° q 'yes)
(stride/≤°
(build-instant 2025 10 9 9 0 0)
(hours 1)
(build-instant 2025 10 9 17 0 0)
(build-instant 2025 10 9 17 0 0))))
(⊦= '()
(μkanren-run
(q 2 #t)
(=° q 'yes)
(stride/≤°
(build-instant 2025 10 9 9 0 0)
(hours 1)
(build-instant 2025 10 9 17 30 0)
(build-instant 2025 10 9 17 30 0))))
(⊦= '()
(μkanren-run
(x 4 #t)
(stride/≤°
(build-instant 2025 10 9 17 30 0)
(hours 1)
(build-instant 2025 10 9 9 0 0)
x))))
((eta 1.276) (memory #(12582912 4006864 1048576)) (stdout "") (stderr ""))
test/civil°: pass
The calendar, both ways round, on the dates where an off-by-one hides: day 0, a recent day, the three days 19781-19783 that bracket a leap day, the first day of a year, and the pair 11016/11017 -- 2000-02-29 and 2000-03-01 -- which is where civil-from-days rolls over a 400-year era. Hinnant's algorithm shifts the year to start in March precisely so that the leap day is the LAST day of the era, so 11016 and 11017 sit on opposite sides of the 146097-day division; an era boundary computed one day out would answer every other case in this file correctly. 157113 is 2400-02-29, the next such boundary, and the day-count there is 18 bits rather than 15.
Every query asks for FIVE answers and gets one. That is the uniqueness assertion: the civil calendar is a bijection between day-counts and (y,m,d) triples, and a relation that offered a second solution -- or that failed to close its stream -- would be relating a date to something other than its day.
The five empty answers are the case's real content. days-from-civil is total: handed 2100-02-29 it returns a day-count, the one belonging to 2100-03-01, and handed 2025-04-31 it returns 2025-05-01. civil° does not pass that on. It recomputes the fields from the day-count it just derived and fails unless they are the ones it was given, so a date that does not exist has ZERO solutions instead of a neighbour's. 2100 is the century rule, 2023 the plain non-leap year, 13 an impossible month, April 31 an impossible day, and 1969-12-31 the epoch floor -- the numeral of (aux kanren arith) is unsigned, so the negative day-count is not representable and the same guard rejects it.
What this costs the caller: civil° is project°-guarded, so the two fast directions here read their argument as a ground numeral and leave through Scheme. The guard is an optimisation over a total relation and not a mode declaration -- with everything fresh the else branch puts numeral° in front and enumerates the calendar -- but the price of the escape is that a PARTIALLY ground numeral is not ground: numeral->number returns #f for (1 0 . β), which is how the guard avoids answering from a term it has not fully seen, and which means a half-solved day-count falls into generate-and-test rather than into a wrong answer.
The same decoder draws the other edge of the type. A trailing 0 cell makes a list no numeral at all -- (numeral° '(1 0)) fails, and no relation of (aux kanren arith) answers for it -- so numeral->number refuses (0) and (1 0) as it refuses a partial term. Decoding them instead would let the guard answer 1970-01-01 for (0) and treat (1 0) as a second spelling of day 1, where the pure branch the guard stands in for answers nothing. Nor may the term fall to that branch: in most modes the pure branch GENERATES numerals and compares each with (1 0), which never matches and never ends. A term that is bound so that it can never become a numeral -- (1 0), (0), foo -- is therefore refused by every guard before any branch runs, in every mode: the day-count of a date, its weekday, its ISO spelling, the seam, the clock. Only a PARTIAL term such as (1 0 . β), which may still become a numeral, reaches the pure branch.
(define (test/civil° _)
(⊦= (list (map build-num '(1970 1 1)))
(μkanren-run
(q 5 #t)
(fresh° (y m d) (civil° (build-num 0) y m d) (=° q (list y m d)))))
(⊦= (list (map build-num '(2025 10 9)))
(μkanren-run
(q 5 #t)
(fresh° (y m d) (civil° (build-num 20370) y m d) (=° q (list y m d)))))
(⊦= (list (map build-num '(2024 2 28)))
(μkanren-run
(q 5 #t)
(fresh° (y m d) (civil° (build-num 19781) y m d) (=° q (list y m d)))))
(⊦= (list (map build-num '(2024 2 29)))
(μkanren-run
(q 5 #t)
(fresh° (y m d) (civil° (build-num 19782) y m d) (=° q (list y m d)))))
(⊦= (list (map build-num '(2024 3 1)))
(μkanren-run
(q 5 #t)
(fresh° (y m d) (civil° (build-num 19783) y m d) (=° q (list y m d)))))
(⊦= (list (map build-num '(2025 1 1)))
(μkanren-run
(q 5 #t)
(fresh° (y m d) (civil° (build-num 20089) y m d) (=° q (list y m d)))))
(⊦= (list (map build-num '(2000 2 29)))
(μkanren-run
(q 5 #t)
(fresh° (y m d) (civil° (build-num 11016) y m d) (=° q (list y m d)))))
(⊦= (list (map build-num '(2000 3 1)))
(μkanren-run
(q 5 #t)
(fresh° (y m d) (civil° (build-num 11017) y m d) (=° q (list y m d)))))
(⊦= (list (map build-num '(2400 2 29)))
(μkanren-run
(q 5 #t)
(fresh°
(y m d)
(civil° (build-num 157113) y m d)
(=° q (list y m d)))))
(⊦= `(,(build-num 0))
(μkanren-run
(q 5 #t)
(civil° q (build-num 1970) (build-num 1) (build-num 1))))
(⊦= `(,(build-num 19782))
(μkanren-run
(q 5 #t)
(civil° q (build-num 2024) (build-num 2) (build-num 29))))
(⊦= `(,(build-num 20089))
(μkanren-run
(q 5 #t)
(civil° q (build-num 2025) (build-num 1) (build-num 1))))
(⊦= `(,(build-num 11016))
(μkanren-run
(q 5 #t)
(civil° q (build-num 2000) (build-num 2) (build-num 29))))
(⊦= `(,(build-num 157113))
(μkanren-run
(q 5 #t)
(civil° q (build-num 2400) (build-num 2) (build-num 29))))
(⊦= '()
(μkanren-run
(q 5 #t)
(civil° q (build-num 2100) (build-num 2) (build-num 29))))
(⊦= '()
(μkanren-run
(q 5 #t)
(civil° q (build-num 2023) (build-num 2) (build-num 29))))
(⊦= '()
(μkanren-run
(q 5 #t)
(civil° q (build-num 2025) (build-num 13) (build-num 1))))
(⊦= '()
(μkanren-run
(q 5 #t)
(civil° q (build-num 2025) (build-num 4) (build-num 31))))
(⊦= '()
(μkanren-run
(q 5 #t)
(civil° q (build-num 1969) (build-num 12) (build-num 31))))
(⊦= '(0 1 #f #f #f #f)
(map numeral->number '(() (1) (0) (1 0) (0 1 0) (1 0 . β))))
(⊦= '()
(μkanren-run
(q 5 #t)
(fresh° (y m d) (civil° '(0) y m d) (=° q (list y m d)))))
(⊦= '()
(μkanren-run
(q 5 #t)
(fresh° (y m d) (civil° '(1 0) y m d) (=° q (list y m d)))))
(⊦= '() (μkanren-run (w 5 #t) (day-of-week° '(1 0) w)))
(⊦= '() (μkanren-run (q 5 #t) (=° q 'yes) (day-of-week° '(1 0) 'monday)))
(⊦= '()
(μkanren-run
(q 5 #t)
(fresh° (d s) (day+second° '(1 0) d s) (=° q (list d s)))))
(⊦= '() (μkanren-run (q 5 #t) (iso° '(1 0) q)))
(⊦= '() (μkanren-run (q 5 #t) (weekday° '(1 0) q)))
(⊦= '()
(μkanren-run
(q 5 #t)
(fresh° (h m s) (clock° '(0) h m s) (=° q (list h m s)))))
(⊦= '() (μkanren-run (q 5 #t) (civil° q '(1 0) '(1) '(1))))
(⊦= '() (μkanren-run (q 5 #t) (on-day° q '(1 0))))
(⊦= '() (μkanren-run (q 5 #t) (=° q 'yes) (day-of-week° 'foo 'monday))))
((eta 0.005) (memory #(12582912 4004928 1048576)) (stdout "") (stderr ""))
test/day+second°: pass
One relation, t = d·86400 + sod, and it is the only place in the module where 86400 is written. Everything calendrical is above it and never sees a 31-bit number: the last assertion is the whole argument for the seam, spelled in bits. A current instant is a 31-bit numeral and a day-count is 15, and what that buys is not speed. Relational division of an instant by 86400 was measured NOT TO TERMINATE -- killed after ten minutes -- so in the ground-instant direction the escape to Scheme is not an optimisation, it is the difference between the relation working and not existing. In the other direction the pure branch would pay a *° of a 15-bit day-count by a 17-bit day, which a prototype measured at 2.4 s for one product; the guard answers in 2 ms.
2400-02-29T00:00:00Z is carried through both directions on purpose. It is a 34-bit instant, past every plausible fixnum-sized assumption and past the era boundary, and it is decoded and reassembled exactly. midnight° is asserted beside it because it is nothing but this relation with sod pinned to '() -- which is what makes it the one composition over the seam with no bad mode, since a ground zero on one side means the guard always has something to read.
The rejected line is sod = 86400, one second past the end of a day. It must fail: the relation is a division with a remainder, and a remainder equal to the divisor would make the encoding non-unique -- (1, 86400) and (2, 0) would name the same instant, and a day-count would no longer determine a date. The (<° sod DAY) conjunct is what forbids it, and it is present in the guarded branch as well as in the pure one.
The four-answer query is the guard's else branch, running with nothing ground at all: the pure definition, (fresh° (p) (<° sod DAY) (*° d DAY p) (plus° p sod t)), productive in 2 ms. Asserting it here is what makes the project° above honest -- the guard changes the clock and not the answer set. The ORDER is the µKanren interleaving and not chronology, which is why 86400 arrives before 1.
(define (test/day+second° _)
(⊦= (list (map build-num '(20370 32000)))
(μkanren-run
(q 5 #t)
(fresh°
(d s)
(day+second° (build-num 1760000000) d s)
(=° q (list d s)))))
(⊦= (list (map build-num '(19781 86399)))
(μkanren-run
(q 5 #t)
(fresh°
(d s)
(day+second° (build-num 1709164799) d s)
(=° q (list d s)))))
(⊦= (list (map build-num '(157113 0)))
(μkanren-run
(q 5 #t)
(fresh°
(d s)
(day+second° (build-num 13574563200) d s)
(=° q (list d s)))))
(⊦= `(,(build-num 1760000000))
(μkanren-run
(q 5 #t)
(day+second° q (build-num 20370) (build-num 32000))))
(⊦= `(,(build-num 13574563200))
(μkanren-run (q 5 #t) (day+second° q (build-num 157113) (build-num 0))))
(⊦= `(,(build-num 1709164800))
(μkanren-run (q 5 #t) (midnight° q (build-num 19782))))
(⊦= `(,(build-num 13574563200))
(μkanren-run (q 5 #t) (midnight° q (build-num 157113))))
(⊦= '()
(μkanren-run (q 5 #t) (day+second° q (build-num 1) (build-num 86400))))
(⊦= (map (lambda (row) (map build-num row))
'((0 0 0) (86400 1 0) (1 0 1) (172800 2 0)))
(μkanren-run
(q 4 #t)
(fresh° (t d s) (day+second° t d s) (=° q (list t d s)))))
(⊦= '(15 18 31 34)
(map (lambda (n) (length (build-num n)))
'(20370 157113 1760000000 13574563200))))
((eta 0.016) (memory #(12582912 4016056 1048576)) (stdout "") (stderr ""))
test/date-time°: pass
The oracle is written out inside the case, and it shares no line of code with the module: it counts years from 1970 by 365 or 366, then months off a twelve-entry length table, while (aux kanren date) reaches the same answer through Hinnant's era arithmetic, where the leap rule appears only as the 146097-day period and February's length is never written down anywhere. Two implementations that agree on all nine instants, in both directions, are agreeing about the Gregorian calendar and not about a shared mistake. The agreement is asserted as a loop rather than as literals so that the oracle, not this file, is what the relation is measured against; the four literal lines after it are there so a reader can see actual numbers, and the first assertion pins the oracle itself to the nine timestamps.
The spread is chosen so that each entry can fail alone: the epoch; a recent instant with a non-zero clock; 2024-02-28T23:59:59Z, the last second before a leap day; noon ON the leap day; the day after it; a year boundary at midnight, where the day-of-year resets; and the 2000-02-29 / 2000-03-01 pair that straddles a 400-year era, plus 2400-02-29 at 34 bits to show the era arithmetic is periodic and not a fixed offset.
The three empty answers say that the fields direction VALIDATES. 2100-02-29 is a date the century rule deletes and civil° rejects; 25:00:00 is not a clock reading; 23:59:60 is a leap second, and this module is POSIX time, where every day is exactly 86400 seconds long, so it must have no instant at all. A relation that normalised any of the three would answer with a plausible instant an hour or a day away, and nothing downstream would notice.
The two shift° lines are the leap day tested through arithmetic rather than through the calendar: one day added to 2024-02-28T12:00:00Z lands on February 29, and the same addition in 2023 lands on March 1. The shift itself is pure layer 1 -- plus° on a 31-bit numeral, a few milliseconds -- and it knows nothing about months; it is the decode that has to place the result. This is the composition a caller actually writes, and it would still typecheck with a calendar that had February wrong.
What the guard costs the caller: date-time° has no arithmetic of its own, only a project° that chooses the ORDER of one conjunction -- with t ground it splits first, so both decoders see a ground input; with the fields ground it decodes first, so the seam is handed a ground (day, second-of-day) and never multiplies two logic variables. The last query is the mode neither branch is optimised for, with only the year pinned, and it is included to assert that the answer set is still real dates: 1970-01-01T00:00:00Z, then 1970-01-02T00:00:00Z, then 1970-01-01T00:00:01Z. That is the interleaving of the day-count and second-of-day streams, NOT chronological order, and any expectation written here by reasoning rather than by running would have had the second and third answers the other way round.
(define (test/date-time° _)
(define (leap? y)
(and (zero? (modulo y 4))
(or (not (zero? (modulo y 100))) (zero? (modulo y 400)))))
(define (month-length y m)
(case m
((1 3 5 7 8 10 12) 31)
((4 6 9 11) 30)
(else (if (leap? y) 29 28))))
(define (oracle-fields t)
(let year ((ds (quotient t 86400)) (y 1970))
(if (>= ds (if (leap? y) 366 365))
(year (- ds (if (leap? y) 366 365)) (+ y 1))
(let month ((ds ds) (m 1))
(if (>= ds (month-length y m))
(month (- ds (month-length y m)) (+ m 1))
(let ((sod (modulo t 86400)))
(list y
m
(+ ds 1)
(quotient sod 3600)
(quotient (modulo sod 3600) 60)
(modulo sod 60))))))))
(define (oracle-instant y mo d hh mm ss)
(let year ((yy 1970) (ds 0))
(if (< yy y)
(year (+ yy 1) (+ ds (if (leap? yy) 366 365)))
(let month ((m 1) (ds ds))
(if (< m mo)
(month (+ m 1) (+ ds (month-length y m)))
(+ (* 86400 (+ ds d -1)) (* 3600 hh) (* 60 mm) ss))))))
(define spread
(list 0
1760000000
1709164799
1709208000
1709251200
1735689600
951782400
951868800
13574563200))
(define (fields t)
(map numeral->number
(car (μkanren-run
(q 5 #t)
(fresh°
(y mo d hh mm ss)
(date-time° (build-num t) y mo d hh mm ss)
(=° q (list y mo d hh mm ss)))))))
(define (instant y mo d hh mm ss)
(map numeral->number
(μkanren-run
(q 5 #t)
(date-time°
q
(build-num y)
(build-num mo)
(build-num d)
(build-num hh)
(build-num mm)
(build-num ss)))))
(⊦= spread
(list (oracle-instant 1970 1 1 0 0 0)
(oracle-instant 2025 10 9 8 53 20)
(oracle-instant 2024 2 28 23 59 59)
(oracle-instant 2024 2 29 12 0 0)
(oracle-instant 2024 3 1 0 0 0)
(oracle-instant 2025 1 1 0 0 0)
(oracle-instant 2000 2 29 0 0 0)
(oracle-instant 2000 3 1 0 0 0)
(oracle-instant 2400 2 29 0 0 0)))
(for-each (lambda (t) (⊦= (oracle-fields t) (fields t))) spread)
(for-each
(lambda (t) (⊦= (list t) (apply instant (oracle-fields t))))
spread)
(⊦= '(1970 1 1 0 0 0) (fields 0))
(⊦= '(2024 2 29 12 0 0) (fields 1709208000))
(⊦= '(2400 2 29 0 0 0) (fields 13574563200))
(⊦= '(1709251200) (instant 2024 3 1 0 0 0))
(⊦= '()
(μkanren-run
(q 5 #t)
(date-time°
q
(build-num 2100)
(build-num 2)
(build-num 29)
(build-num 0)
(build-num 0)
(build-num 0))))
(⊦= '()
(μkanren-run
(q 5 #t)
(date-time°
q
(build-num 2024)
(build-num 2)
(build-num 29)
(build-num 25)
(build-num 0)
(build-num 0))))
(⊦= '()
(μkanren-run
(q 5 #t)
(date-time°
q
(build-num 2024)
(build-num 2)
(build-num 29)
(build-num 23)
(build-num 59)
(build-num 60))))
(⊦= (map build-num '(2024 2 29 12 0 0))
(car (μkanren-run
(q 5 #t)
(fresh°
(t y mo d hh mm ss)
(shift° (build-instant 2024 2 28 12 0 0) (days 1) t)
(date-time° t y mo d hh mm ss)
(=° q (list y mo d hh mm ss))))))
(⊦= (map build-num '(2023 3 1 12 0 0))
(car (μkanren-run
(q 5 #t)
(fresh°
(t y mo d hh mm ss)
(shift° (build-instant 2023 2 28 12 0 0) (days 1) t)
(date-time° t y mo d hh mm ss)
(=° q (list y mo d hh mm ss))))))
(⊦= (map (lambda (row) (map build-num row))
'((0 1 1 0 0 0) (86400 1 2 0 0 0) (1 1 1 0 0 1)))
(μkanren-run
(q 3 #t)
(fresh°
(t mo d hh mm ss)
(date-time° t (build-num 1970) mo d hh mm ss)
(=° q (list t mo d hh mm ss))))))
((eta 0.042) (memory #(12582912 4017648 1048576)) (stdout "") (stderr ""))
test/leap-year°: pass
leap-year° has no arithmetic of its own. Its body is (fresh° (d) (civil° d y '(0 1) '(1 0 1 1 1))) -- a year is a leap year exactly when the 29th of February is a date -- so this case is really asking whether civil°'s round-trip guard implements the 4/100/400 rule. 2024 is the plain rule, 2100 and 2200 are the centuries it deletes, 2000 and 2400 are the ones the 400 rule gives back. Take away the recomputation in civil° and all seven answer yes, because days-from-civil is happy to hand back the day-count of March 1.
1968 answers NO although 1968 is a leap year, and that is not a bug -- it is the epoch floor, asserted so that no reader mistakes it for one. The numeral of (aux kanren arith) is unsigned, 1968-02-29 has a negative day-count, and civil° fails on it. So leap-year° is a decision procedure only for years from 1970 on; before that it answers no for a reason that has nothing to do with leap years. 1900, the century rule's headline case, is therefore unreachable through the relation, and the four civil-from-days lines pin it one layer down instead, on plain Scheme where negative day-counts exist: 1900-02-29 comes back as 1900-03-01 and is not a date, while 1968-02-29 and 2000-02-29 come back unchanged and are. The two 146097 lines are the same rule stated as a period -- four hundred Gregorian years are exactly 146097 days, twice over, which is the identity Hinnant's era arithmetic is built on and the reason there is no leap-year branch anywhere in the kernel.
The lengths are computed by the RELATIONS, not read off a table. year° and month° answer with the first and last day-count of the window -- month° by way of a twelve-row next-month° successor table and civil° on the first of the following month -- and the two plus° goals then measure it, inclusive of both endpoints. That subtraction is pure layer 1 at 15 to 18 bits, about 7 ms a query. February 2024 is 29 days and February 2100 is 28 without either number appearing in the module, which is the strongest available statement that the calendar is derived and not tabulated; and because the window is a relation over numerals rather than a pair of Scheme integers, the same goals run with the year left fresh.
(define (test/leap-year° _)
(define (year-length y)
(map numeral->number
(μkanren-run
(q 5 #t)
(fresh°
(lo hi hi+1 len)
(year° (build-num y) lo hi)
(plus° hi '(1) hi+1)
(plus° lo len hi+1)
(=° q len)))))
(define (february-length y)
(map numeral->number
(μkanren-run
(q 5 #t)
(fresh°
(lo hi hi+1 len)
(month° (build-num y) (build-num 2) lo hi)
(plus° hi '(1) hi+1)
(plus° lo len hi+1)
(=° q len)))))
(⊦= '(yes) (μkanren-run (r 5 #t) (leap-year° (build-num 1972)) (=° r 'yes)))
(⊦= '(yes) (μkanren-run (r 5 #t) (leap-year° (build-num 2000)) (=° r 'yes)))
(⊦= '(yes) (μkanren-run (r 5 #t) (leap-year° (build-num 2024)) (=° r 'yes)))
(⊦= '(yes) (μkanren-run (r 5 #t) (leap-year° (build-num 2400)) (=° r 'yes)))
(⊦= '() (μkanren-run (r 5 #t) (leap-year° (build-num 2025)) (=° r 'yes)))
(⊦= '() (μkanren-run (r 5 #t) (leap-year° (build-num 2100)) (=° r 'yes)))
(⊦= '() (μkanren-run (r 5 #t) (leap-year° (build-num 2200)) (=° r 'yes)))
(⊦= '() (μkanren-run (r 5 #t) (leap-year° (build-num 1968)) (=° r 'yes)))
(⊦= '() (μkanren-run (r 5 #t) (leap-year° (build-num 1900)) (=° r 'yes)))
(⊦= '(1900 3 1) (civil-from-days (days-from-civil 1900 2 29)))
(⊦= '(1968 2 29) (civil-from-days (days-from-civil 1968 2 29)))
(⊦= '(2000 2 29) (civil-from-days (days-from-civil 2000 2 29)))
(⊦= '(2100 3 1) (civil-from-days (days-from-civil 2100 2 29)))
(⊦= 146097 (- (days-from-civil 2000 3 1) (days-from-civil 1600 3 1)))
(⊦= 146097 (- (days-from-civil 2400 3 1) (days-from-civil 2000 3 1)))
(⊦= '(366) (year-length 1972))
(⊦= '(365) (year-length 2025))
(⊦= '(366) (year-length 2000))
(⊦= '(365) (year-length 2100))
(⊦= '(366) (year-length 2400))
(⊦= '(29) (february-length 2024))
(⊦= '(28) (february-length 2025))
(⊦= '(29) (february-length 2000))
(⊦= '(28) (february-length 2100))
(⊦= '(29) (february-length 2400)))
((eta 0.116) (memory #(12582912 4018248 1048576)) (stdout "") (stderr ""))
test/weekday°/epoch: pass
The anchor every other weekday case stands on, and the one fact in the module that nothing inside the module can check. weekday-epoch-day is #(3 4 5 6 0 1 2) -- the smallest day-count carrying each weekday -- and every generator below starts from one of those seven offsets. Rotate the vector by one and the module stays perfectly self-consistent: monday° would agree with day-of-week°, which would agree with weekend°, and all three would be a day out. Only an outside witness can say so, which is why the first two rows call (chicken time posix) rather than anything in (aux kanren date): field 6 of seconds->utc-time is the weekday with 0 for Sunday, and it reads 4 for the epoch and 1 for 345600.
The rest is the same claim made from inside, at each of the three magnitudes the module speaks. 1970-01-01 is a Thursday, so 1970-01-05 is day-count 4 and instant 345600; (monday° d) with d fresh offers 4 as its very first answer, so the stride anchor and the calendar agree; and midnight° carries day 4 back up to 345600, closing the loop between the day-count layer and the instant layer. The last row is day 3, the Sunday before: five answers were asked for and none came, which is a miss that TERMINATES -- see test/weekday-names°/refuse.
(define (test/weekday°/epoch _)
(⊦= 4 (vector-ref (seconds->utc-time 0) 6))
(⊦= 1 (vector-ref (seconds->utc-time 345600) 6))
(⊦= 'thursday (weekday-of-day 0))
(⊦= 'monday (weekday-of-day 4))
(⊦= (build-num 4) (build-day 1970 1 5))
(⊦= (build-num 345600) (build-instant 1970 1 5))
(⊦= (map build-num '(3 4 5 6 0 1 2))
(map weekday-anchor
'(sunday monday tuesday wednesday thursday friday saturday)))
(⊦= (build-num 7) WEEK)
(⊦= '(monday) (μkanren-run (w 2 #t) (weekday° (build-num 345600) w)))
(⊦= (list (build-num 4)) (μkanren-run (d 1 #t) (monday° d)))
(⊦= (list (build-num 345600))
(μkanren-run (t 2 #t) (midnight° t (build-num 4))))
(⊦= '(yes) (μkanren-run (q 2 #t) (=° q 'yes) (thursday° (build-num 0))))
(⊦= '() (μkanren-run (q 5 #t) (=° q 'yes) (monday° (build-num 3)))))
((eta 0.001) (memory #(12582912 4027656 1048576)) (stdout "") (stderr ""))
test/day-of-week°: pass
One relation, three modes, and three different mechanisms answering them -- which is what project° buys and what it costs. With the day-count ground the goal ESCAPES to Scheme and unifies the answer, so the test is 0 ms and the relational alternatives are all worse: /° on a day-count was measured at 2.9 s, striding from the epoch to 2025 at 15.5 s, and multiple° as a divisibility test gave no answer at all after three minutes on a negative case. With the WEEKDAY ground instead it is a pure unbounded stride° from that weekday's epoch anchor, about a millisecond an answer and genuinely increasing -- 4, 11, 18, 25, 32 for Monday, 3, 10, 17, 24, 31 for Sunday, each seven apart from its anchor. With neither ground numeral° proposes a day-count and the escape names its weekday, so the relation is TOTAL: no error, no hang, just the calendar in order from the epoch. That branch is for a FRESH weekday only: a w bound to a typo such as mon, Monday or the string "monday" is no weekday name and never will be, so the relation refuses it at once -- generating day-counts to refute it one re-entry at a time would never end.
What the guard costs the caller is that the branch is chosen by looking at instantiation AT THE MOMENT THE GOAL RUNS, so conjunction order is now part of the meaning. The groundness test is numeral->number, positive typing over the cells rather than (not (var? x)), so a half-built day-count like (1 0 . β) is correctly NOT taken for ground and falls to the generate-and-test branch instead of being decoded as if the tail were empty. The last row is the both-ground mode: a wrong weekday is refused by unification, in no time and with no search, which is the whole reason the next case terminates.
(define (test/day-of-week° _)
(⊦= '(thursday)
(μkanren-run (w 2 #t) (day-of-week° (build-day 2025 10 9) w)))
(⊦= (map build-num '(4 11 18 25 32))
(μkanren-run (d 5 #t) (day-of-week° d 'monday)))
(⊦= (map build-num '(3 10 17 24 31))
(μkanren-run (d 5 #t) (day-of-week° d 'sunday)))
(⊦= (list (list (build-num 0) 'thursday)
(list (build-num 1) 'friday)
(list (build-num 2) 'saturday)
(list (build-num 3) 'sunday))
(μkanren-run
(q 4 #t)
(fresh° (d w) (=° q (list d w)) (day-of-week° d w))))
(⊦= '()
(μkanren-run
(q 5 #t)
(=° q 'yes)
(day-of-week° (build-day 2025 10 9) 'monday)))
(⊦= '(() () ())
(map (lambda (w) (μkanren-run (d 1 #t) (day-of-week° d w)))
'(mon Monday "monday"))))
((eta 0.01) (memory #(12582912 4024056 1048576)) (stdout "") (stderr ""))
test/weekday-names°: pass
The seven names the module is for, each a line of sugar over day-of-week° and inheriting both of its directions for nothing. The first row runs all seven against 2025-10-09 and exactly one answers, which is the partition property: the seven relations are mutually exclusive and jointly exhaustive over day-counts, and a table that had drifted would show up here as two hits or none. The second row is the diagonal, 20366 to 20372 -- 2025-10-05 to 2025-10-11, a full week beginning on a Sunday -- and it is the row that pins WHICH name goes with which offset. Test a single name and any cyclic rotation of weekday-names passes; test all seven in order against seven consecutive days and only the true assignment does.
The generators read the anchors straight out of weekday-epoch-day: Fridays are 1, 8, 15, 22 and Saturdays 2, 9, 16, 23, because 1970-01-02 was a Friday and 01-03 a Saturday. The last row is the unit trap, and it is written down rather than merely warned about because nothing else in the module will catch it. These relations take a DAY-COUNT, not an instant. Handing one a unixtime is not an error and does not fail: 1760000000 days after the epoch is 4820686-05-02, and the module cheerfully reports it a Sunday. weekday° is the relation that takes an instant; these seven are a layer below it, and midnight° is the lift.
(define (test/weekday-names° _)
(⊦= '(() () () () (yes) () ())
(map (lambda (r)
(μkanren-run (q 2 #t) (=° q 'yes) (r (build-day 2025 10 9))))
(list sunday°
monday°
tuesday°
wednesday°
thursday°
friday°
saturday°)))
(⊦= '((yes) (yes) (yes) (yes) (yes) (yes) (yes))
(map (lambda (r d) (μkanren-run (q 2 #t) (=° q 'yes) (r (build-num d))))
(list sunday°
monday°
tuesday°
wednesday°
thursday°
friday°
saturday°)
'(20366 20367 20368 20369 20370 20371 20372)))
(⊦= (map build-num '(1 8 15 22)) (μkanren-run (d 4 #t) (friday° d)))
(⊦= (map build-num '(2 9 16 23)) (μkanren-run (d 4 #t) (saturday° d)))
(⊦= '(sunday)
(μkanren-run (w 2 #t) (day-of-week° (build-num 1760000000) w))))
((eta 0.007) (memory #(12582912 4023680 1048576)) (stdout "") (stderr ""))
test/weekday-names°/refuse: pass
The case the whole design is arranged around: a weekday name used as a test on a date that is NOT that weekday must fail, and must fail in finite time. 2025-10-09 is a Thursday, so monday° and sunday° refuse it and weekend° refuses the Friday after; each asks for twenty answers and receives none, in no measurable time. An assertion of '() is the only kind that can distinguish failure from divergence, and only by being run: a goal that hangs never gets as far as disagreeing with an expectation.
It is not a free property. The generator direction of these relations IS an unbounded stride, and what happens when that stride is asked to serve as a test was measured: (stride° base step x) with x ground and off the stride steps past it forever, because nothing in the recursive clause compares the running value to x. The three stride/≤° rows are the two ways out written side by side. A ceiling makes the stride terminate on a miss -- 18 is on 4+7k and answers, 19 is not and the stream simply ends -- and that is the relation to reach for when a stride must decide. day-of-week° takes the other way out: with the day-count ground it never strides at all, it escapes, which is why 4, 11, 18, 25 and "is 20370 a Monday" cost the same nothing.
The last two rows also pin the ORDER, because the two relations enumerate the same set and do not agree on sequence. stride° walks 4, 11, 18, 25; stride/≤° answers 4, 11, 25, 18. The ceiling comparison sits inside the recursive clause, so the answers come back in the interleaving of or° rather than in the calendar's. Anything downstream that assumed a bounded stride was sorted is wrong, and the module says so.
(define (test/weekday-names°/refuse _)
(⊦= '() (μkanren-run (q 20 #t) (=° q 'yes) (monday° (build-day 2025 10 9))))
(⊦= '() (μkanren-run (q 20 #t) (=° q 'yes) (sunday° (build-day 2025 10 9))))
(⊦= '()
(μkanren-run (q 20 #t) (=° q 'yes) (weekend° (build-day 2025 10 10))))
(⊦= '(yes)
(μkanren-run
(q 3 #t)
(=° q 'yes)
(stride/≤° (build-num 4) (build-num 7) (build-num 25) (build-num 18))))
(⊦= '()
(μkanren-run
(q 3 #t)
(=° q 'yes)
(stride/≤° (build-num 4) (build-num 7) (build-num 25) (build-num 19))))
(⊦= (map build-num '(4 11 25 18))
(μkanren-run
(x 9 #t)
(stride/≤° (build-num 4) (build-num 7) (build-num 25) x)))
(⊦= (map build-num '(4 11 18 25))
(μkanren-run (x 4 #t) (stride° (build-num 4) (build-num 7) x))))
((eta 0.055) (memory #(12582912 4030560 1048576)) (stdout "") (stderr ""))
test/weekend°: pass
The two filters, over the same week as above: 20366 is a Sunday and 20372 a Saturday, 20370 a Thursday, and each relation refuses what the other accepts. The content of both definitions is CONJUNCTION ORDER. The disjunction that pins w comes first, so that with the day-count fresh day-of-week° still sees a ground weekday and takes its stride branch; write the two goals the other way round and the guard finds nothing ground, falls to generate-and-test, and enumerates every day-count in the calendar in order to keep two-sevenths of them. Both readings are sound and only one returns in time, which is the recurring price of a project°-guarded relation: its callers have to be written for the mode they want.
workday° spells out its five rows rather than negating the weekend with ≠° for the same reason -- a disequality CONSTRAINS w without GROUNDING it, so the guard would still see a fresh weekday and the generator direction would be lost. The last three rows are what that direction actually looks like, and they are pinned because they are not what a reader expects. Weekends come out 2, 3, 9, 10, 16, 17: two streams interleaving so cleanly they look sorted. Workdays come out 4, 5, 6, 0, 1 -- the five anchors, in the order the or° lists them, so Monday's 4 before Thursday's 0 -- and then 11, 7, 12, 18, 13. Five interleaved streams are visibly not a chronology, and a filter does not preserve the order of what it filters.
(define (test/weekend° _)
(⊦= '(yes) (μkanren-run (q 2 #t) (=° q 'yes) (weekend° (build-num 20372))))
(⊦= '(yes) (μkanren-run (q 2 #t) (=° q 'yes) (weekend° (build-num 20366))))
(⊦= '() (μkanren-run (q 3 #t) (=° q 'yes) (weekend° (build-num 20370))))
(⊦= '(yes) (μkanren-run (q 2 #t) (=° q 'yes) (workday° (build-num 20370))))
(⊦= '() (μkanren-run (q 3 #t) (=° q 'yes) (workday° (build-num 20372))))
(⊦= (map build-num '(2 3 9 10 16 17)) (μkanren-run (d 6 #t) (weekend° d)))
(⊦= (map build-num '(4 5 6 0 1)) (μkanren-run (d 5 #t) (workday° d)))
(⊦= (map build-num '(4 5 6 0 1 11 7 12 18 13))
(μkanren-run (d 10 #t) (workday° d))))
((eta 0.014) (memory #(12582912 4031912 1048576)) (stdout "") (stderr ""))
test/weekday-name°: pass
Seven unifications in a cond°, the only entirely pure relation in this group, and the one the guarded ones lean on. The first row asks for NINE and gets seven: the stream CLOSES, which is the property that matters and the reason a count larger than the answer set is the right thing to write here. A generator put in front of a guarded relation has to terminate, or the guarded relation's open mode terminates no better than the hang it was meant to avoid. The prefix of three fixes the order as the clause order, Sunday first, matching weekday-names and weekday-epoch-day index for index.
Used the other way it is a membership test, and funday gets zero answers rather than quietly being accepted as an eighth weekday -- the same guard as weekday-name?, which is what every project° in the calendar layer consults before it trusts a symbol. The last row is the idiom the relation exists for, and it is prime°'s discipline from (aux kanren arith) transplanted: where a mode would otherwise be undefined, put a GENERATOR in front of the guard instead of raising an error. Seven candidates are proposed, the ground day-count filters six away, Thursday survives. day-of-week/within° does exactly this in its fallback branch, and it must generate the WEEKDAY and not the day-count: generating the answer instead leaves w fresh on re-entry, the fallback fires again, and that version was measured hanging.
(define (test/weekday-name° _)
(⊦= '(sunday monday tuesday wednesday thursday friday saturday)
(μkanren-run (w 9 #t) (weekday-name° w)))
(⊦= '(sunday monday tuesday) (μkanren-run (w 3 #t) (weekday-name° w)))
(⊦= '(yes) (μkanren-run (q 3 #t) (=° q 'yes) (weekday-name° 'monday)))
(⊦= '() (μkanren-run (q 3 #t) (=° q 'yes) (weekday-name° 'funday)))
(⊦= '(thursday)
(μkanren-run
(w 3 #t)
(weekday-name° w)
(day-of-week° (build-day 2025 10 9) w))))
((eta 0.001) (memory #(12582912 4032208 1048576)) (stdout "") (stderr ""))
test/weekday-midnight°: pass
The headline query at instant magnitude, and the one place where the two bounds of the window cross the seam DIFFERENTLY. day+second° floors, which is right for hi -- the last midnight not after hi falls on hi's own day -- and wrong for lo: Monday noon floors to Monday, whose midnight is twelve hours BEFORE the window opens. So a lo past midnight is ceiled to the next day-count, and the rows walk that edge: from midnight itself the Monday is in, from noon or from one second past it is out, and a window that opens one second after a Monday midnight and closes one second before the next holds no Monday midnight at all. The last row is the same fact as a test, and it terminates on the miss because the window bounds the stride.
(define (test/weekday-midnight° _)
(define (mondays lo hi)
(map (lambda (t) (instant->iso (numeral->number t)))
(μkanren-run (t 9 #t) (weekday-midnight° 'monday lo hi t))))
(⊦= '("2025-10-06T00:00:00Z"
"2025-10-13T00:00:00Z"
"2025-10-20T00:00:00Z"
"2025-10-27T00:00:00Z")
(mondays (build-instant 2025 10 6) (build-instant 2025 10 31)))
(⊦= '("2025-10-13T00:00:00Z" "2025-10-20T00:00:00Z" "2025-10-27T00:00:00Z")
(mondays (build-instant 2025 10 6 12 0 0) (build-instant 2025 10 31)))
(⊦= '("2025-10-13T00:00:00Z")
(mondays (build-instant 2025 10 6 0 0 1) (build-instant 2025 10 13)))
(⊦= '()
(mondays
(build-instant 2025 10 6 0 0 1)
(build-instant 2025 10 12 23 59 59)))
(⊦= '()
(μkanren-run
(q 3 #t)
(=° q 'yes)
(weekday-midnight°
'monday
(build-instant 2025 10 6 12 0 0)
(build-instant 2025 10 31)
(build-instant 2025 10 6)))))
((eta 0.362) (memory #(12582912 4104608 1048576)) (stdout "") (stderr ""))
test/instant->iso: pass
The epoch is asserted as a literal string because it is the one instant every other case in this file is measured from: (instant->iso 0) is "1970-01-01T00:00:00Z" exactly, and the numeral of that instant is '(), so the encoding's zero and the calendar's origin are the same object. An epoch off by one day would leave every relation in the module self-consistent and every string in it wrong.
1735787045 is in here for one reason: it is 2025-01-02T03:04:05Z, the instant whose month, day, hour, minute and second are ALL single digits at once. It is the only shape that catches the bug this kind of code always has -- a bare ~a on a field that happens to be 5 -- and the field-by-field substring line names which field lost its zero rather than making a reader diff two twenty-character strings. The padding is not cosmetic: it is what makes lexicographic order agree with chronological order, so a sorted list of these strings is a sorted list of instants, and "2025-1-2" would break that silently while still reading correctly to a human. The width assertion is the cheap standing guard: an ISO instant here is TWENTY characters, T at index 10 and Z at index 19, and those offsets are exactly the ones iso->instant slices at.
The last four lines pin the far edge honestly. zero-pad is string-pad, which keeps the RIGHT-hand end of a string too long for the field: (zero-pad 12345 2) is "45". So the year is four digits or it is a lie: padded blindly, the year 10000 -- one second past the last assertion above -- would read "0000-01-01T00:00:00Z" and 12025-03-14T09:00:00Z would read "2025-03-14T09:00:00Z", a well-formed string that the parser takes back as a DIFFERENT instant. So the formatter answers #f past 9999, as the parser does on a string it cannot read, and iso° turns that into zero answers. The supported range is [1970, 9999], and it is asserted here rather than left to a reader's assumption.
(define (test/instant->iso _)
(⊦= "1970-01-01T00:00:00Z" (instant->iso 0))
(⊦= "2025-01-02T03:04:05Z" (instant->iso 1735787045))
(⊦= '("2025" "01" "02" "03" "04" "05")
(let ((s (instant->iso 1735787045)))
(list (substring s 0 4)
(substring s 5 7)
(substring s 8 10)
(substring s 11 13)
(substring s 14 16)
(substring s 17 19))))
(⊦= '(#\T #\Z)
(let ((s (instant->iso 1735787045)))
(list (string-ref s 10) (string-ref s 19))))
(⊦= '("1970-01-01T00:00:00Z"
"1970-01-01T00:00:01Z"
"1970-01-01T00:00:59Z"
"1970-01-01T00:01:00Z"
"1970-01-01T00:59:59Z"
"1970-01-01T01:00:00Z"
"1970-01-01T23:59:59Z"
"1970-01-05T00:00:00Z"
"2000-02-29T00:00:00Z"
"2025-10-09T08:53:20Z"
"2038-01-19T03:14:07Z")
(map instant->iso
'(0
1
59
60
3599
3600
86399
345600
951782400
1760000000
2147483647)))
(⊦= '(20 20 20 20)
(map (lambda (t) (string-length (instant->iso t)))
'(0 1735787045 1760000000 253402300799)))
(⊦= '("00" "05" "59" "1970" "0999" "45")
(list (zero-pad 0 2)
(zero-pad 5 2)
(zero-pad 59 2)
(zero-pad 1970 4)
(zero-pad 999 4)
(zero-pad 12345 2)))
(⊦= "9999-12-31T23:59:59Z" (instant->iso 253402300799))
(⊦= #f (instant->iso 253402300800))
(⊦= #f (instant->iso 317311462800))
(⊦= '() (μkanren-run (s 2 #t) (iso° (build-num 317311462800) s))))
((eta 0.0) (memory #(12582912 4039256 1048576)) (stdout "") (stderr ""))
test/iso->instant: pass
The parse direction on well-formed input, and then the statement that the two string functions are inverses. Both of them are plain Scheme over plain integers -- no goal, no numeral, no project° -- and that is the whole point of testing them apart from iso°: the relation does nothing but choose between these two functions, so anything wrong with the format is wrong here first, where a failure names a number instead of a stream.
The spread is chosen at the boundaries where a carry is made or dropped, because an arithmetic slip inside civil-from-days or the second-of-day split shows up there and nowhere else: 0 and 1; 59 and 60, the minute; 86399 and 86400, the day, which is the seam the whole module is built around; 345600, the first Monday of the epoch; 951782400, 2000-02-29, a leap day in the century year that IS a leap year; 1735787045, the all-single-digit instant again, now read back; and 2147483647, the signed 32-bit ceiling, which is a 31-bit numeral and the largest instant anyone is likely to hand this module by accident. Round-tripping through the string and comparing integers is what makes the assertion legible; comparing strings would pass just as well for a formatter and parser that agreed on the same wrong calendar, which is why the calendar itself is cross-checked against (chicken time posix) elsewhere in this suite and not here.
(define (test/iso->instant _)
(⊦= 0 (iso->instant "1970-01-01T00:00:00Z"))
(⊦= 1735787045 (iso->instant "2025-01-02T03:04:05Z"))
(⊦= 1760000000 (iso->instant "2025-10-09T08:53:20Z"))
(⊦= 1709208000 (iso->instant "2024-02-29T12:00:00Z"))
(⊦= '(0
1
59
60
86399
86400
345600
951782400
1735787045
1760000000
2147483647)
(map (lambda (t) (iso->instant (instant->iso t)))
'(0
1
59
60
86399
86400
345600
951782400
1735787045
1760000000
2147483647))))
((eta 0.001) (memory #(12582912 4041936 1048576)) (stdout "") (stderr ""))
test/iso->instant/rejects: pass
What happens on malformed input, said once and for all: #f, never a condition and never a neighbouring instant. The thirteen strings are one row each of the three checks the parser makes, and the distinction between them is the interesting part. SHAPE is decided by one template, iso-shape = "dddd-dd-ddTdd:dd:ddZ" -- an ASCII digit at every d, that exact separator elsewhere -- and that is what refuses a space separator, a missing Z, an offset of "+01:00", a truncated string and the empty one. The second row is the same check on the strings that have the right LENGTH and the wrong characters: a stray separator, a sign, a decimal point. string->number would read +1 as a month and 2. as a second, so a parser that checked only the length, the T and the Z turned "2025-+1-09T08:53:20Z" into 2025-01-09 -- a neighbouring instant, the one outcome this case forbids. Everything here is UTC by construction, so an offset is not converted, it is rejected; that is a design decision and this line is where it is written down. RANGE refuses hour 25, minute 60 and second 60 before any calendar arithmetic runs, so a leap second has no representation.
The middle four are the ones that would otherwise be silent. 2025-02-30, 2025-04-31 and 2100-02-29 all pass the range test -- the month is in [1,12], the day in [1,31] -- and days-from-civil will happily give each of them a day-count, one that belongs to March 2, May 1 and March 1. The parser catches them by mapping that day-count BACK with civil-from-days and demanding the original triple: the calendar is a bijection, so a tuple the forward map never returns is not a date. Without that round trip every one of these four would parse to a wrong instant that no later assertion could distinguish from a right one -- and the century rule would be untested, 2100 being divisible by 100 and not by 400, hence not a leap year, unlike 2000 in the case above. The pre-epoch string is refused for a different reason: it is a perfectly good ISO instant with no numeral to become, because the numeral of (aux kanren arith) is unsigned. A non-string argument is refused by the string? guard, so a caller who passes an instant by mistake gets #f rather than a type error -- which is why callers must check the result, and why iso° turns exactly this #f into ✗°.
(define (test/iso->instant/rejects _)
(⊦= '(#f #f #f #f #f #f #f #f #f #f #f #f #f)
(map iso->instant
'("2025-02-30T00:00:00Z"
"2100-02-29T00:00:00Z"
"2025-13-01T00:00:00Z"
"2025-04-31T00:00:00Z"
"2025-10-09T25:00:00Z"
"2025-10-09T00:60:00Z"
"2025-10-09T00:00:60Z"
"1969-12-31T23:59:59Z"
"2025-10-09 08:53:20Z"
"2025-10-09T08:53:20"
"2025-10-09T08:53:20+01:00"
"not a date at all!!"
"")))
(⊦= '(#f #f #f #f #f #f #f)
(map iso->instant
'("2025x10-09T08:53:20Z"
"2025-10x09T08:53:20Z"
"2025-10-09T08!53:20Z"
"2025-10-09T08:53?20Z"
"2025-+1-09T08:53:20Z"
"+025-10-09T08:53:20Z"
"2025-10-09T08:53:2.Z")))
(⊦= '() (μkanren-run (t 2 #t) (iso° t "2025-+1-09T08:53:20Z")))
(⊦= #f (iso->instant 1760000000)))
((eta 0.0) (memory #(12582912 4046032 1048576)) (stdout "") (stderr ""))
test/iso°: pass
The relation, in the two modes a caller actually writes, and each of them asks for TWO answers so that the assertion also says the stream closes: an instant has one spelling and a spelling has one instant. Every query here is a millisecond or less, because neither direction does any relational arithmetic at all -- iso° is a project° and a cond° over two string functions. Note the second group's expectations are written (build-num 1760000000), not thirty-one bits: the answer is a term, and test/build-num in microkanren-arith.scm has already pinned that the two constructions agree. The epoch answers (()) -- a one-answer stream whose single answer is the empty numeral.
What the project° costs the caller is a MODE OBLIGATION, and it is the reason these three groups are separate. The guard reads the substitution when the goal runs, so it is the conjunction ORDER that decides which branch is taken: a goal that grounds t must be written before iso°, not after it, or the relation falls through to the open branch and enumerates instead of computing. Being ground is tested by numeral?, positively, so a partially instantiated instant counts as unknown and no bits already fixed are consulted. In exchange the caller gets something a pure relation could not give at all: formatting needs /° on a whole unixtime, and the brief's measurement is that that division does not terminate.
With both sides ground the goal is a TEST, and the last two lines of that group say what it tests. One second off is zero answers, which is the useful half. The other half is that "2025-1-2T3:4:5Z" -- the same instant, spelled without the padding -- is ALSO zero answers, because the ground-t branch wins the cond° and unifies against the canonical string. Equality here is string equality on one chosen spelling, not equality of dates, and a caller comparing strings from elsewhere must normalise them first. The final line is the same refusal in relational clothing: a malformed string gives an empty stream -- the goal simply fails, it does not raise, and it does not answer with a nearby instant.
(define (test/iso° _)
(⊦= '("2025-10-09T08:53:20Z")
(μkanren-run (s 2 #t) (iso° (build-num 1760000000) s)))
(⊦= '("1970-01-01T00:00:00Z") (μkanren-run (s 2 #t) (iso° (build-num 0) s)))
(⊦= '("2025-01-02T03:04:05Z")
(μkanren-run (s 2 #t) (iso° (build-num 1735787045) s)))
(⊦= (list (build-num 1760000000))
(μkanren-run (t 2 #t) (iso° t "2025-10-09T08:53:20Z")))
(⊦= (list (build-num 0))
(μkanren-run (t 2 #t) (iso° t "1970-01-01T00:00:00Z")))
(⊦= (list (build-num 1735787045))
(μkanren-run (t 2 #t) (iso° t "2025-01-02T03:04:05Z")))
(⊦= '(yes)
(μkanren-run
(q 2 #t)
(=° q 'yes)
(iso° (build-num 1760000000) "2025-10-09T08:53:20Z")))
(⊦= '()
(μkanren-run
(q 2 #t)
(=° q 'yes)
(iso° (build-num 1760000000) "2025-10-09T08:53:21Z")))
(⊦= '()
(μkanren-run
(q 2 #t)
(=° q 'yes)
(iso° (build-num 1735787045) "2025-1-2T3:4:5Z")))
(⊦= '(() () () () ())
(map (lambda (s) (μkanren-run (t 1 #t) (iso° t s)))
'("2025-02-30T00:00:00Z"
"2025-13-01T00:00:00Z"
"1969-12-31T23:59:59Z"
"2025-10-09T08:53:20+01:00"
"not a date at all!!"))))
((eta 0.002) (memory #(12582912 4050016 1048576)) (stdout "") (stderr ""))
test/iso°/round-trip: pass
The same eight instants out through one branch of iso° and back in through the other, at the numeral level rather than the integer level. test/iso->instant already pinned that the two string functions invert each other; what this pins is that the RELATION wires them up in the right direction and builds a canonical term out of the result. A cond° whose branches were swapped, or a parse branch that unified str with its own input, or a numeral built by some path other than number->numeral, would each leave the function-level assertions perfectly green and fail right here. It is eight queries a direction and still under a millisecond each.
The last two lines are the open mode -- neither side ground -- and the reason to assert it at all is that the alternatives were a failure and a hang. Instead date-time° generates an instant, the goal re-enters with t now ground, and the guard's fast branch formats it: the stream is an enumeration of REAL instants, each one a string this file's parser would accept. The order is the µKanren interleaving and it is NOT chronological -- day-count and second-of-day interleave, so the answers arrive 0, 86400, 1, 172800, which is 1970-01-01, 01-02, then back to 00:00:01 on the 1st. The paired assertion is written with a project° precisely so that the reader sees the numbers next to the strings and cannot mistake the sequence for a sorted one. This order is pinned as OBSERVED, not as promised: it is a fact about or°'s interleaving, it is what a caller will actually see, and nobody should build a chronological listing on it -- span° and weekday-midnight° are the relations that bound a window.
(define (test/iso°/round-trip _)
(⊦= '("1970-01-01T00:00:00Z"
"1970-01-01T00:00:01Z"
"1970-01-05T00:00:00Z"
"1970-01-01T23:59:59Z"
"2000-02-29T00:00:00Z"
"2025-01-02T03:04:05Z"
"2025-10-09T08:53:20Z"
"2038-01-19T03:14:07Z")
(map (lambda (t) (car (μkanren-run (v 1 #t) (iso° (build-num t) v))))
'(0 1 345600 86399 951782400 1735787045 1760000000 2147483647)))
(⊦= '(0 1 345600 86399 951782400 1735787045 1760000000 2147483647)
(map (lambda (t)
(numeral->number
(car (μkanren-run (u 1 #t) (iso° u (instant->iso t))))))
'(0 1 345600 86399 951782400 1735787045 1760000000 2147483647)))
(⊦= '("1970-01-01T00:00:00Z"
"1970-01-02T00:00:00Z"
"1970-01-01T00:00:01Z"
"1970-01-03T00:00:00Z"
"1970-01-02T00:00:01Z")
(μkanren-run (s 5 #t) (fresh° (t) (iso° t s))))
(⊦= '((0 "1970-01-01T00:00:00Z")
(86400 "1970-01-02T00:00:00Z")
(1 "1970-01-01T00:00:01Z")
(172800 "1970-01-03T00:00:00Z"))
(μkanren-run
(q 4 #t)
(fresh°
(t s)
(iso° t s)
(project° ((t* t)) (=° q `(,(numeral->number t*) ,s)))))))
((eta 0.011) (memory #(12582912 4051704 1048576)) (stdout "") (stderr ""))
(aux kanren micro show): a presentation layer for µkanren answers
The engine answers a query with a reified λ-expression: faithful, but the cons spine hides the shape of the term and the constraint store shows up as executable assertions. (aux kanren micro show) splits that answer in a datum and a list of constraints, then renders both as a table, as a Mermaid graph of the term (where hash-consing makes sharing visible) and, optionally, as a profile of how many suspensions the engine had to force before each answer showed up.
test/repr->datum: pass
(define (test/repr->datum _)
(⊦= '(α z) (μkanren-repr->datum '(cons α (cons 'z '()))))
(⊦= 42 (μkanren-repr->datum 42))
(⊦= '#(α 3) (μkanren-repr->datum '(vector α 3))))
((eta 0.0) (memory #(12582912 2496368 1048576)) (stdout "") (stderr ""))
test/form->constraint: pass
(define (test/form->constraint _)
(⊦= '(≠ α list) (μkanren-form->constraint '(begin (deny (equal? α 'list)))))
(⊦= '(≠ (α β) (list quote))
(μkanren-form->constraint
'(begin (deny (and (equal? α 'list) (equal? β 'quote))))))
(⊦= '(symbol? α)
(μkanren-form->constraint '(assert (every (μ v (symbol? v)) (list α)))))
(⊦= '(absento closure α)
(μkanren-form->constraint '(assert (absent? 'closure α))))
(⊦= '(absento (1 2) (1 . α))
(μkanren-form->constraint '(assert (absent? '(1 2) (cons 1 α))))))
((eta 0.0) (memory #(12582912 2497592 1048576)) (stdout "") (stderr ""))
test/string/short: pass
(define (test/string/short _)
(⊦= "(\"a b\" sym)" (->string/short (list "a b" 'sym)))
(⊦= "(#\\\" \"a b\" |x y| \"q\\\" \")"
(->string/short (list #\" "a b" (string->symbol "x y") "q\" ")))
(⊦= "'quote" (->string/short ''quote))
(⊨ (and (substring-index
"| 1 | `\"a \\| b\"` |"
(μkanren-run/markdown (q 3) (=° q "a | b")))
#t)))
((eta 0.0) (memory #(12582912 2491248 1048576)) (stdout "") (stderr ""))
test/occurrences: pass
(define (test/occurrences _)
(⊦= 2 (μkanren-datum-occurrences '((α z) z (α β)) 'α))
(⊦= 1 (μkanren-datum-occurrences '((α z) z (α β)) 'β))
(⊦= 0 (μkanren-datum-occurrences '((α z) z (α β)) 'γ)))
((eta 0.0) (memory #(12582912 2492496 1048576)) (stdout "") (stderr ""))
test/answer: pass
(define (test/answer _)
(let1 (a (car (°->answers (fresh° (q) (=° q (list 'z 'z))))))
(⊦= '(z z) (μkanren-answer->datum a))
(⊦= '() (μkanren-answer->constraints a))
(⊨ (μkanren-answer-ground? a))))
((eta 0.0) (memory #(12582912 2494136 1048576)) (stdout "") (stderr ""))
test/append°: pass
Two altitudes, from the same answers. The variables view keeps a value whole and hangs the unknowns it is still free in off it, labelling each edge with how many times that unknown occurs; the cells view opens the term up into the DAG it really is, where equal subterms are hash-consed so that sharing is visible.
(μkanren-run (l 5 #f) (fresh° (a d) (append° a d l)))
5 answers.
| # | answer |
|---|---|
| 1 | α |
| 2 | (α . β) |
| 3 | (α β . γ) |
| 4 | (α β γ . δ) |
| 5 | (α β γ δ . ε) |
flowchart LR
n0(("l"))
n1["α"]
n2(("α"))
n3["(α . β)"]
n4(("α"))
n5(("β"))
n6["(α β . γ)"]
n7(("α"))
n8(("β"))
n9(("γ"))
n10["(α β γ . δ)"]
n11(("α"))
n12(("β"))
n13(("γ"))
n14(("δ"))
n15["(α β γ δ . ε)"]
n16(("α"))
n17(("β"))
n18(("γ"))
n19(("δ"))
n20(("ε"))
n0 -->|1| n1
n1 -->|×1| n2
n0 -->|2| n3
n3 -->|×1| n4
n3 -->|×1| n5
n0 -->|3| n6
n6 -->|×1| n7
n6 -->|×1| n8
n6 -->|×1| n9
n0 -->|4| n10
n10 -->|×1| n11
n10 -->|×1| n12
n10 -->|×1| n13
n10 -->|×1| n14
n0 -->|5| n15
n15 -->|×1| n16
n15 -->|×1| n17
n15 -->|×1| n18
n15 -->|×1| n19
n15 -->|×1| n20
class n0 query
class n15,n10,n6,n3,n1 value
class n20,n19,n18,n17,n16,n14,n13,n12,n11,n9,n8,n7,n5,n4,n2 var
classDef query fill:#ebfbee,stroke:#2f9e44,stroke-width:2px;
classDef value fill:#ffffff,stroke:#495057;
classDef var fill:#fff3bf,stroke:#f08c00,stroke-width:2px;
classDef atom fill:#e7f5ff,stroke:#1971c2;
classDef cell fill:#f8f9fa,stroke:#868e96;
classDef constraint fill:#ffe3e3,stroke:#e03131,stroke-dasharray:4 3;
classDef answer fill:#ebfbee,stroke:#2f9e44,stroke-width:2px;flowchart LR
subgraph a1["answer 1"]
direction LR
n0(("α"))
end
subgraph a2["answer 2"]
direction LR
n1[["cons"]]
n2(("α"))
n3(("β"))
n1 -->|car| n2
n1 -->|cdr| n3
end
subgraph a3["answer 3"]
direction LR
n4[["cons"]]
n5(("α"))
n6[["cons"]]
n7(("β"))
n8(("γ"))
n4 -->|car| n5
n6 -->|car| n7
n6 -->|cdr| n8
n4 -->|cdr| n6
end
subgraph a4["answer 4"]
direction LR
n9[["cons"]]
n10(("α"))
n11[["cons"]]
n12(("β"))
n13[["cons"]]
n14(("γ"))
n15(("δ"))
n9 -->|car| n10
n11 -->|car| n12
n13 -->|car| n14
n13 -->|cdr| n15
n11 -->|cdr| n13
n9 -->|cdr| n11
end
subgraph a5["answer 5"]
direction LR
n16[["cons"]]
n17(("α"))
n18[["cons"]]
n19(("β"))
n20[["cons"]]
n21(("γ"))
n22[["cons"]]
n23(("δ"))
n24(("ε"))
n16 -->|car| n17
n18 -->|car| n19
n20 -->|car| n21
n22 -->|car| n23
n22 -->|cdr| n24
n20 -->|cdr| n22
n18 -->|cdr| n20
n16 -->|cdr| n18
end
class n24,n23,n21,n19,n17,n15,n14,n12,n10,n8,n7,n5,n3,n2,n0 var
class n22,n20,n18,n16,n13,n11,n9,n6,n4,n1 cell
classDef query fill:#ebfbee,stroke:#2f9e44,stroke-width:2px;
classDef value fill:#ffffff,stroke:#495057;
classDef var fill:#fff3bf,stroke:#f08c00,stroke-width:2px;
classDef atom fill:#e7f5ff,stroke:#1971c2;
classDef cell fill:#f8f9fa,stroke:#868e96;
classDef constraint fill:#ffe3e3,stroke:#e03131,stroke-dasharray:4 3;
classDef answer fill:#ebfbee,stroke:#2f9e44,stroke-width:2px;(define (test/append° _)
(let1 (answers
(°->answers (take° 5 (fresh° (l) (fresh° (a d) (append° a d l))))))
(⊦= '(α (α . β) (α β . γ) (α β γ . δ) (α β γ δ . ε))
(map μkanren-answer->datum answers))))
((eta 0.001) (memory #(12582912 2509000 1048576)) (stdout "") (stderr ""))
test/peano°/shared: pass
With share: 'all every ground subterm is shared by the whole answer set, so a family such as the Peano numerals collapses into a single spine that each answer points into: the diagram grows linearly, not quadratically.
6 answers.
| # | answer |
|---|---|
| 1 | z |
| 2 | (s z) |
| 3 | (s (s z)) |
| 4 | (s (s (s z))) |
| 5 | (s (s (s (s z)))) |
| 6 | (s (s (s (s (s z))))) |
flowchart LR
n0(("q"))
n1["z"]
n2["(s z)"]
n3["(s (s z))"]
n4["(s (s (s z)))"]
n5["(s (s (s (s z))))"]
n6["(s (s (s (s (s z)))))"]
n0 -->|1| n1
n0 -->|2| n2
n0 -->|3| n3
n0 -->|4| n4
n0 -->|5| n5
n0 -->|6| n6
class n0 query
class n6,n5,n4,n3,n2,n1 value
classDef query fill:#ebfbee,stroke:#2f9e44,stroke-width:2px;
classDef value fill:#ffffff,stroke:#495057;
classDef var fill:#fff3bf,stroke:#f08c00,stroke-width:2px;
classDef atom fill:#e7f5ff,stroke:#1971c2;
classDef cell fill:#f8f9fa,stroke:#868e96;
classDef constraint fill:#ffe3e3,stroke:#e03131,stroke-dasharray:4 3;
classDef answer fill:#ebfbee,stroke:#2f9e44,stroke-width:2px;flowchart LR
n0["'z"]
n1("answer 1")
n2[["cons"]]
n3["'s"]
n4[["cons"]]
n5(["()"])
n6("answer 2")
n7[["cons"]]
n8[["cons"]]
n9("answer 3")
n10[["cons"]]
n11[["cons"]]
n12("answer 4")
n13[["cons"]]
n14[["cons"]]
n15("answer 5")
n16[["cons"]]
n17[["cons"]]
n18("answer 6")
n1 --> n0
n2 -->|car| n3
n4 -->|car| n0
n4 -->|cdr| n5
n2 -->|cdr| n4
n6 --> n2
n7 -->|car| n3
n8 -->|car| n2
n8 -->|cdr| n5
n7 -->|cdr| n8
n9 --> n7
n10 -->|car| n3
n11 -->|car| n7
n11 -->|cdr| n5
n10 -->|cdr| n11
n12 --> n10
n13 -->|car| n3
n14 -->|car| n10
n14 -->|cdr| n5
n13 -->|cdr| n14
n15 --> n13
n16 -->|car| n3
n17 -->|car| n13
n17 -->|cdr| n5
n16 -->|cdr| n17
n18 --> n16
class n5,n3,n0 atom
class n17,n16,n14,n13,n11,n10,n8,n7,n4,n2 cell
class n18,n15,n12,n9,n6,n1 answer
classDef query fill:#ebfbee,stroke:#2f9e44,stroke-width:2px;
classDef value fill:#ffffff,stroke:#495057;
classDef var fill:#fff3bf,stroke:#f08c00,stroke-width:2px;
classDef atom fill:#e7f5ff,stroke:#1971c2;
classDef cell fill:#f8f9fa,stroke:#868e96;
classDef constraint fill:#ffe3e3,stroke:#e03131,stroke-dasharray:4 3;
classDef answer fill:#ebfbee,stroke:#2f9e44,stroke-width:2px;(define (test/peano°/shared _))
((eta 0.0) (memory #(12582912 2519688 1048576)) (stdout "") (stderr ""))
test/variables-view: pass
(define (test/variables-view _)
(let* ((answers (°->answers (take° 2 (fresh° (q) (eval-exp° q '() q)))))
(g (μkanren-answers->mermaid answers #:view 'variables #:var 'q)))
(⊨ (and (substring-index "((\"q\"))" g) #t))
(⊨ (and (substring-index "|×6|" g) #t))
(⊨ (and (substring-index "{{\"(symbol? α β)\"}}" g) #t))))
((eta 0.286) (memory #(12582912 2529296 1048576)) (stdout "") (stderr ""))
test/sharing: pass
The variable α occurs in two different components of the answer: in the graph it is one node with two parents.
1 answer.
| # | answer |
|---|---|
| 1 | ((α z) z (α β)) |
flowchart LR
n0(("q"))
n1["((α z) z (α β))"]
n2(("α"))
n3(("β"))
n0 -->|1| n1
n1 -->|×2| n2
n1 -->|×1| n3
class n0 query
class n1 value
class n3,n2 var
classDef query fill:#ebfbee,stroke:#2f9e44,stroke-width:2px;
classDef value fill:#ffffff,stroke:#495057;
classDef var fill:#fff3bf,stroke:#f08c00,stroke-width:2px;
classDef atom fill:#e7f5ff,stroke:#1971c2;
classDef cell fill:#f8f9fa,stroke:#868e96;
classDef constraint fill:#ffe3e3,stroke:#e03131,stroke-dasharray:4 3;
classDef answer fill:#ebfbee,stroke:#2f9e44,stroke-width:2px;flowchart LR
subgraph a1["answer 1"]
direction LR
n0[["cons"]]
n1[["cons"]]
n2(("α"))
n3[["cons"]]
n4["'z"]
n5(["()"])
n6[["cons"]]
n7[["cons"]]
n8[["cons"]]
n9[["cons"]]
n10(("β"))
n1 -->|car| n2
n3 -->|car| n4
n3 -->|cdr| n5
n1 -->|cdr| n3
n0 -->|car| n1
n6 -->|car| n4
n8 -->|car| n2
n9 -->|car| n10
n9 -->|cdr| n5
n8 -->|cdr| n9
n7 -->|car| n8
n7 -->|cdr| n5
n6 -->|cdr| n7
n0 -->|cdr| n6
end
class n10,n2 var
class n5,n4 atom
class n9,n8,n7,n6,n3,n1,n0 cell
classDef query fill:#ebfbee,stroke:#2f9e44,stroke-width:2px;
classDef value fill:#ffffff,stroke:#495057;
classDef var fill:#fff3bf,stroke:#f08c00,stroke-width:2px;
classDef atom fill:#e7f5ff,stroke:#1971c2;
classDef cell fill:#f8f9fa,stroke:#868e96;
classDef constraint fill:#ffe3e3,stroke:#e03131,stroke-dasharray:4 3;
classDef answer fill:#ebfbee,stroke:#2f9e44,stroke-width:2px;(define (test/sharing _))
((eta 0.0) (memory #(12582912 2514688 1048576)) (stdout "") (stderr ""))
test/quine: pass
The smallest quine of the relational interpreter. An answer too wide for a table cell gets a block of its own, pretty-printed with the reader's abbreviations — 'quote, not (quote quote). Grounding it with °->list/ground would silently drop its three constraints; here they stay, under the term and as chips on the variable they restrict. The bar chart counts the suspensions the engine forced before handing out the answer.
1 answer.
answer 1
((λ (α) (list α (list 'quote α))) '(λ (α) (list α (list 'quote α))))
constraints: (≠ α closure), (≠ α list), (≠ α quote), (symbol? α)
flowchart LR
n0(("q"))
n1["((λ (α) (list α (list 'quote α))) '(λ (α) (list<br/>α (list 'quote α))))"]
n2(("α"))
n3{{"(≠ α closure)"}}
n4{{"(≠ α list)"}}
n5{{"(≠ α quote)"}}
n6{{"(symbol? α)"}}
n0 -->|1| n1
n1 -->|×6| n2
n2 -.-> n3
n2 -.-> n4
n2 -.-> n5
n2 -.-> n6
class n0 query
class n1 value
class n2 var
class n6,n5,n4,n3 constraint
classDef query fill:#ebfbee,stroke:#2f9e44,stroke-width:2px;
classDef value fill:#ffffff,stroke:#495057;
classDef var fill:#fff3bf,stroke:#f08c00,stroke-width:2px;
classDef atom fill:#e7f5ff,stroke:#1971c2;
classDef cell fill:#f8f9fa,stroke:#868e96;
classDef constraint fill:#ffe3e3,stroke:#e03131,stroke-dasharray:4 3;
classDef answer fill:#ebfbee,stroke:#2f9e44,stroke-width:2px;flowchart LR
subgraph a1["answer 1"]
direction LR
n0[["cons"]]
n1[["cons"]]
n2["'λ"]
n3[["cons"]]
n4[["cons"]]
n5(("α"))
n6(["()"])
n7[["cons"]]
n8[["cons"]]
n9["'list"]
n10[["cons"]]
n11[["cons"]]
n12[["cons"]]
n13[["cons"]]
n14[["cons"]]
n15["'quote"]
n16[["cons"]]
n17[["cons"]]
n18[["cons"]]
n19[["cons"]]
n20["'closure"]
n21{{"symbol?"}}
n1 -->|car| n2
n4 -->|car| n5
n4 -->|cdr| n6
n3 -->|car| n4
n8 -->|car| n9
n10 -->|car| n5
n12 -->|car| n9
n14 -->|car| n15
n16 -->|car| n15
n16 -->|cdr| n6
n14 -->|cdr| n16
n13 -->|car| n14
n13 -->|cdr| n4
n12 -->|cdr| n13
n11 -->|car| n12
n11 -->|cdr| n6
n10 -->|cdr| n11
n8 -->|cdr| n10
n7 -->|car| n8
n7 -->|cdr| n6
n3 -->|cdr| n7
n1 -->|cdr| n3
n0 -->|car| n1
n18 -->|car| n15
n19 -->|car| n1
n19 -->|cdr| n6
n18 -->|cdr| n19
n17 -->|car| n18
n17 -->|cdr| n6
n0 -->|cdr| n17
n5 -. ≠ .-> n20
n5 -. ≠ .-> n9
n5 -. ≠ .-> n15
n5 -.-> n21
end
class n5 var
class n20,n15,n9,n6,n2 atom
class n19,n18,n17,n16,n14,n13,n12,n11,n10,n8,n7,n4,n3,n1,n0 cell
class n21 constraint
classDef query fill:#ebfbee,stroke:#2f9e44,stroke-width:2px;
classDef value fill:#ffffff,stroke:#495057;
classDef var fill:#fff3bf,stroke:#f08c00,stroke-width:2px;
classDef atom fill:#e7f5ff,stroke:#1971c2;
classDef cell fill:#f8f9fa,stroke:#868e96;
classDef constraint fill:#ffe3e3,stroke:#e03131,stroke-dasharray:4 3;
classDef answer fill:#ebfbee,stroke:#2f9e44,stroke-width:2px;xychart-beta title "suspensions forced per answer" x-axis "answer" ["1"] y-axis "forced" bar [14261]
(define (test/quine _))
((eta 0.065) (memory #(12582912 2526448 1048576)) (stdout "") (stderr ""))
test/blocks: pass
(define (test/blocks _)
(let1 (md (°->markdown
(take° 1 (fresh° (q) (eval-exp° q '() q)))
#:title
"quine"
#:var
'q
#:diagram
#f))
(⊨ (and (substring-index "### answer 1" md) #t))
(⊨ (and (substring-index "((λ (α) (list α (list 'quote α)))" md) #t))
(⊨ (and (substring-index
"constraints: `(≠ α closure)`, `(≠ α list)`"
md)
#t))))
((eta 0.068) (memory #(12582912 2525712 1048576)) (stdout "") (stderr ""))
test/window°: pass
When every answer is a ground tuple of the same length the report spreads it over one column per field, which is what a relational query deserves: this is the PostgreSQL window function example, computed by window°.
10 answers.
| # | depname | empno | salary | avg |
|---|---|---|---|---|
| 1 | develop | 7 | 4200 | 5020 |
| 2 | develop | 8 | 6000 | 5020 |
| 3 | develop | 9 | 4500 | 5020 |
| 4 | develop | 10 | 5200 | 5020 |
| 5 | develop | 11 | 5200 | 5020 |
| 6 | personnel | 2 | 3900 | 3700 |
| 7 | personnel | 5 | 3500 | 3700 |
| 8 | sales | 1 | 5000 | 14600/3 |
| 9 | sales | 3 | 4800 | 14600/3 |
| 10 | sales | 4 | 4800 | 14600/3 |
(define (test/window° _))
((eta 0.0) (memory #(12582912 2554096 1048576)) (stdout "") (stderr ""))
test/markdown: pass
(define (test/markdown _)
(let1 (md (μkanren-run/markdown (l 4) (fresh° (a d) (append° a d l))))
(⊨ (string? md))
(⊨ (and (substring-index "| 2 | `(α . β)` |" md) #t))
(⊨ (and (substring-index "```mermaid" md) #t))
(⊨ (and (substring-index "classDef query" md) #t))
(⊨ (and (substring-index "|car|" md) #t))
(μkanren-markdown->file! md "microkanren-show")))
((eta 0.001) (memory #(12582912 2543048 1048576)) (stdout "") (stderr ""))
test/markdown/tuples: pass
(define (test/markdown/tuples _)
(let1 (md (μkanren-run/markdown (q 1) (=° q (list 1 2))))
(⊨ (and (substring-index "| # | answer |" md) #t))
(⊭ (substring-index "| c0 |" md)))
(⊭ (substring-index "| c0 |" (μkanren-run/markdown (q 1) (=° q (iota 36)))))
(⊨ (and (substring-index
"| # | a | b |"
(μkanren-run/markdown/table (q 1) '(a b) (=° q (list 1 2))))
#t))
(⊨ (and (substring-index
"| # | c0 | c1 |"
(μkanren-run/markdown
(q 2)
(or° (=° q (list 1 2)) (=° q (list 3 4)))))
#t)))
((eta 0.0) (memory #(12582912 2534160 1048576)) (stdout "") (stderr ""))
test/markdown/query: pass
(define (test/markdown/query _)
(let* ((md (μkanren-run/markdown (q 3) (=° q 1)))
(query (with-input-from-string
(substring md (+ 10 (substring-index "```scheme\n" md)))
read)))
(⊦= '(μkanren-run (q 3 #f) (=° q 1)) query)
(⊦= '((λ () 1)) (eval query)))
(⊦= '(code/scheme (μkanren-run (q 3 #f) (=° q 1)))
(car (μkanren-run/sxml (q 3) (=° q 1)))))
((eta 0.0) (memory #(12582912 2537800 1048576)) (stdout "") (stderr ""))
(aux kanren unionfind): a miniKanren whose substitution is a union-find
test/vars-generation: pass
(define (test/vars-generation _)
(⊭ (equal? (V 'V0) (V/gensym)))
(⊭ (equal? (V 'V₁) (V/gensym)))
(⊭ (equal? (V/gensym) (V/gensym)))
(let* ((v₅ (variable->symbol (V/gensym))) (v₆ (variable->symbol (V/gensym))))
(⊨ (V/subscripted? v₅))
(⊨ (and (V/subscripted? v₆) (not (eq? v₅ v₆))))))
((eta 0.0) (memory #(12582912 3269960 1048576)) (stdout "") (stderr ""))
test/tautologies: pass
(define (test/tautologies _)
(⊦= '() (stream:->list (run ✗)))
(⊭ (run/with-symbols #t ✗))
(⊦= '((#t 0)) (stream:->list (run ✓)))
(⊨ (and (run/with-symbols #t ✓) #t))
(⊦= '() (stream:->list (run (≡ 2 3))))
(⊭ (run/with-symbols #t (≡ 2 3)))
(⊦= '(#t) (run/with-symbols ∞ (≡ 3 3)))
(⊦= '() (run/with-symbols ∞ (fresh (v) ✗)))
(⊦= '(#t) (run/with-symbols ∞ (fresh (v) ✓)))
(⊦= '(#t) (run/with-symbols ∞ (fresh (v) (≡ v 3))))
(⊦= '() (run/with-symbols ∞ (fresh (v) (∧ (≡ v 3) (≡ v 4))))))
((eta 0.0) (memory #(12582912 3283768 1048576)) (stdout "") (stderr ""))
test/vars-≡-sharing: pass
(define (test/vars-≡-sharing _)
(⊦= '(3) (run/with-symbols ∞ (v) (≡ v 3)))
(⊦= '(3) (run/with-symbols ∞ (v) (≡ 3 v)))
(⊦= '(3) (run/with-symbols ∞ (v) (≡ '(3 4) `(,v 4))))
(⊦= (list `(,(R '▢ 0) 0)) (stream:->list (run (v) ✓)))
(⊦= '(▢₀) (run/with-symbols ∞ (v) ✓))
(⊦= '((▢₀ ▢₁)) (run/with-symbols ∞ (v w) ✓))
(⊦= '((▢₀ ▢₀)) (run/with-symbols ∞ (v w) (≡ v w)))
(⊦= '((▢₀ ▢₀) 0) (run/with-symbols #t (v w) (≡ v w)))
(⊦= '((▢₀ ▢₀ ▢₁)) (run/with-symbols ∞ (v w x) (≡ v w)))
(⊦= '((▢₀ ▢₀ ▢₁ ▢₂)) (run/with-symbols ∞ (v w x y) (≡ v w)))
(⊦= '((▢₀ ▢₁ ▢₂ ▢₀ ▢₁)) (run/with-symbols ∞ (a b c d e) (∧ (≡ d a) (≡ e b))))
(⊦= '((▢₀ (((▢₀))))) (run/with-symbols ∞ (v w) (≡ `(((,v))) w))))
((eta 0.001) (memory #(12582912 3278232 1048576)) (stdout "") (stderr ""))
test/list-destructuring: pass
(define (test/list-destructuring _)
(⊦= '(()) (run/with-symbols ∞ (v) (null° v)))
(⊦= '(0) (run/with-symbols ∞ (l) (car° '(0 1 2 3) l)))
(⊦= '((1 2 3)) (run/with-symbols ∞ (l) (cdr° '(0 1 2 3) l)))
(⊦= '((3 4)) (run/with-symbols ∞ (v w) (cons° v 4 `(3 unquote w))))
(⊦= '(#t) (run/with-symbols ∞ (fresh (w) (pair° `(3 unquote w)))))
(⊦= '((▢₀ . ▢₁)) (run/with-symbols ∞ (w) (pair° w))))
((eta 0.0) (memory #(12582912 3281416 1048576)) (stdout "") (stderr ""))
test/cond°: pass
(define (test/cond° _)
(⊦= '(tea cup) (run/with-symbols ∞ (v) (tea-cup° v)))
(⊦= '((split pea) (red bean)) (run/with-symbols ∞ (v w) (split-pea° v w)))
(⊦= '((tea ▢₀) (#f tea) (cup ▢₀) (#f cup))
(run/with-symbols ∞ (v w) (split-pea₁° v w))))
((eta 0.001) (memory #(12582912 3282928 1048576)) (stdout "") (stderr ""))
test/list°: pass
(define (test/list° _)
(⊦= '() (run/with-symbols ∞ (list° 3)))
(⊦= '(#t) (run/with-symbols ∞ (list° '())))
(⊦= '(#t) (run/with-symbols ∞ (list° '())))
(⊦= '(#t) (run/with-symbols ∞ (list° '(3 4))))
(⊦= '(() (▢₀) (▢₀ ▢₁) (▢₀ ▢₁ ▢₂) (▢₀ ▢₁ ▢₂ ▢₃))
(run/with-symbols 5 (l) (list° l))))
((eta 0.001) (memory #(12582912 3288232 1048576)) (stdout "") (stderr ""))
test/append°: pass
(define (test/append° _)
(⊨ (and (run/with-symbols #t (append° '(0 1 2) '(3 4 5) '(0 1 2 3 4 5))) #t))
(⊦= '(#t) (run/with-symbols ∞ (append° '(0 1 2) '(3 4 5) '(0 1 2 3 4 5))))
(⊦= '((0 1 2 3 4 5)) (run/with-symbols ∞ (v) (append° '(0 1 2) '(3 4 5) v)))
(⊦= '((() (0 1 2 3 4 5))
((0) (1 2 3 4 5))
((0 1) (2 3 4 5))
((0 1 2) (3 4 5))
((0 1 2 3) (4 5))
((0 1 2 3 4) (5))
((0 1 2 3 4 5) ()))
(run/with-symbols ∞ (v w) (append° v w '(0 1 2 3 4 5))))
(⊦= '(((0 1 2 3 4 5) ())
((1 2 3 4 5) (0))
((2 3 4 5) (0 1))
((3 4 5) (0 1 2))
((4 5) (0 1 2 3))
((5) (0 1 2 3 4))
(() (0 1 2 3 4 5)))
(run/with-symbols ∞ (v w) (append° w v '(0 1 2 3 4 5)))))
((eta 0.002) (memory #(12582912 3283280 1048576)) (stdout "") (stderr ""))
test/always°-never°: pass
(define (test/always°-never° _)
(⊦= '(▢₀) (run/with-symbols 1 (v) always°))
(⊦= '(▢₀ ▢₀ ▢₀ ▢₀ ▢₀) (run/with-symbols 5 (v) always°))
(⊦= '(onion onion onion onion onion)
(run/with-symbols 5 (v) (∧ (≡ v 'onion) always°)))
(⊦= '() (run/with-symbols 1 (v) (∧ (≡ v 'garlic) ✓ (≡ v 'onion))))
(let ((g₀ (λ (v)
(∧ (cond°/§ ((≡ v 'garlic) always°) ((≡ v 'onion)))
(≡ v 'onion))))
(g₁ (λ (v)
(∧ (cond°/§ ((≡ v 'garlic) always°) ((≡ v 'onion) ✓))
(≡ v 'onion))))
(g₂ (λ (v)
(∧ (cond°/§ ((≡ v 'garlic) always°) ((≡ v 'onion) always°))
(≡ v 'onion)))))
(⊦= '(onion) (run/with-symbols 1 (v) (g₀ v)))
(⊦= '(onion onion onion onion onion) (run/with-symbols 5 (v) (g₂ v)))
(⊦= '() (run/with-symbols 1 (v) (∧ ✗ never°)))
(⊦= '(▢₀) (run/with-symbols 1 (v) (cond°/§ (✓) (never°))))))
((eta 0.0) (memory #(12582912 3296344 1048576)) (stdout "") (stderr ""))
test/dyck°: pass
(define (test/dyck° _)
(⊦= '(()
(○ ●)
(○ ○ ● ●)
(○ ● ○ ●)
(○ ○ ○ ● ● ●)
(○ ● ○ ○ ● ●)
(○ ○ ● ● ○ ●)
(○ ● ○ ● ○ ●)
(○ ○ ● ○ ● ●)
(○ ● ○ ○ ○ ● ● ●)
(○ ○ ● ● ○ ○ ● ●)
(○ ● ○ ● ○ ○ ● ●)
(○ ○ ○ ● ● ● ○ ●)
(○ ● ○ ○ ● ● ○ ●)
(○ ○ ● ● ○ ● ○ ●)
(○ ● ○ ● ○ ● ○ ●)
(○ ○ ○ ○ ● ● ● ●)
(○ ● ○ ○ ● ○ ● ●)
(○ ○ ● ● ○ ○ ○ ● ● ●)
(○ ● ○ ● ○ ○ ○ ● ● ●)
(○ ○ ○ ● ● ● ○ ○ ● ●)
(○ ● ○ ○ ● ● ○ ○ ● ●)
(○ ○ ● ● ○ ● ○ ○ ● ●)
(○ ● ○ ● ○ ● ○ ○ ● ●)
(○ ○ ● ○ ● ● ○ ●)
(○ ● ○ ○ ○ ● ● ● ○ ●)
(○ ○ ● ● ○ ○ ● ● ○ ●)
(○ ● ○ ● ○ ○ ● ● ○ ●)
(○ ○ ○ ● ● ● ○ ● ○ ●)
(○ ● ○ ○ ● ● ○ ● ○ ●)
(○ ○ ● ● ○ ● ○ ● ○ ●)
(○ ● ○ ● ○ ● ○ ● ○ ●)
(○ ○ ● ○ ○ ● ● ●)
(○ ● ○ ○ ○ ○ ● ● ● ●)
(○ ○ ● ● ○ ○ ● ○ ● ●)
(○ ● ○ ● ○ ○ ● ○ ● ●)
(○ ○ ○ ● ● ● ○ ○ ○ ● ● ●)
(○ ● ○ ○ ● ● ○ ○ ○ ● ● ●)
(○ ○ ● ● ○ ● ○ ○ ○ ● ● ●)
(○ ● ○ ● ○ ● ○ ○ ○ ● ● ●)
(○ ○ ● ○ ● ● ○ ○ ● ●)
(○ ● ○ ○ ○ ● ● ● ○ ○ ● ●))
(run/with-symbols 42 (α) (dyck° α))))
((eta 0.03) (memory #(12582912 4853072 1048576)) (stdout "") (stderr ""))
test/dyck°/deepening: pass
(define (test/dyck°/deepening _)
(⊦= '((() 1)
((○ ●) 7)
((○ ○ ● ●) 17)
((○ ● ○ ●) 13)
((○ ○ ○ ● ● ●) 31)
((○ ● ○ ○ ● ●) 23)
((○ ○ ● ● ○ ●) 23)
((○ ● ○ ● ○ ●) 19)
((○ ○ ● ○ ● ●) 27)
((○ ● ○ ○ ○ ● ● ●) 37)
((○ ○ ● ● ○ ○ ● ●) 33)
((○ ● ○ ● ○ ○ ● ●) 29)
((○ ○ ○ ● ● ● ○ ●) 37)
((○ ● ○ ○ ● ● ○ ●) 29)
((○ ○ ● ● ○ ● ○ ●) 29)
((○ ● ○ ● ○ ● ○ ●) 25)
((○ ○ ○ ○ ● ● ● ●) 49)
((○ ● ○ ○ ● ○ ● ●) 33)
((○ ○ ● ● ○ ○ ○ ● ● ●) 47)
((○ ● ○ ● ○ ○ ○ ● ● ●) 43)
((○ ○ ○ ● ● ● ○ ○ ● ●) 47)
((○ ● ○ ○ ● ● ○ ○ ● ●) 39)
((○ ○ ● ● ○ ● ○ ○ ● ●) 39)
((○ ● ○ ● ○ ● ○ ○ ● ●) 35)
((○ ○ ● ○ ● ● ○ ●) 33)
((○ ● ○ ○ ○ ● ● ● ○ ●) 43)
((○ ○ ● ● ○ ○ ● ● ○ ●) 39)
((○ ● ○ ● ○ ○ ● ● ○ ●) 35)
((○ ○ ○ ● ● ● ○ ● ○ ●) 43)
((○ ● ○ ○ ● ● ○ ● ○ ●) 35)
((○ ○ ● ● ○ ● ○ ● ○ ●) 35)
((○ ● ○ ● ○ ● ○ ● ○ ●) 31)
((○ ○ ● ○ ○ ● ● ●) 41)
((○ ● ○ ○ ○ ○ ● ● ● ●) 55)
((○ ○ ● ● ○ ○ ● ○ ● ●) 43)
((○ ● ○ ● ○ ○ ● ○ ● ●) 39)
((○ ○ ○ ● ● ● ○ ○ ○ ● ● ●) 61)
((○ ● ○ ○ ● ● ○ ○ ○ ● ● ●) 53)
((○ ○ ● ● ○ ● ○ ○ ○ ● ● ●) 53)
((○ ● ○ ● ○ ● ○ ○ ○ ● ● ●) 49)
((○ ○ ● ○ ● ● ○ ○ ● ●) 43)
((○ ● ○ ○ ○ ● ● ● ○ ○ ● ●) 53))
(run/with-symbols ↓ 42 (α) ((deepening 100) (dyck° α)))))
((eta 0.029) (memory #(12582912 4866576 1048576)) (stdout "") (stderr ""))
test/stacksort°: pass
(define (test/stacksort° _)
(⊦= '(((5 4 3 2 1) "((((()))))")
((4 3 2 1 5) "(((())))()")
((5 3 2 1 4) "(((()))())")
((3 2 1 4 5) "((()))()()")
((5 4 2 1 3) "(((())()))")
((4 2 1 3 5) "((())())()")
((3 2 1 5 4) "((()))(())")
((2 1 3 4 5) "(())()()()")
((5 4 3 1 2) "(((()())))")
((4 3 1 2 5) "((()()))()")
((5 2 1 3 4) "((())()())")
((3 1 2 4 5) "(()())()()")
((5 2 1 4 3) "((())(()))")
((2 1 4 3 5) "(())(())()")
((2 1 3 5 4) "(())()(())")
((1 2 3 4 5) "()()()()()")
((5 4 1 3 2) "((()(())))")
((4 1 3 2 5) "(()(()))()")
((5 3 1 2 4) "((()())())")
((1 3 2 4 5) "()(())()()")
((5 4 1 2 3) "((()()()))")
((4 1 2 3 5) "(()()())()")
((3 1 2 5 4) "(()())(())")
((1 4 3 2 5) "()((()))()")
((5 1 4 3 2) "(()((())))")
((1 2 4 3 5) "()()(())()")
((2 1 5 3 4) "(())(()())")
((1 4 2 3 5) "()(()())()")
((2 1 5 4 3) "(())((()))")
((1 2 3 5 4) "()()()(())")
((1 5 4 3 2) "()(((())))")
((5 1 3 2 4) "(()(())())")
((5 1 4 2 3) "(()(()()))")
((1 3 2 5 4) "()(())(())")
((5 1 2 4 3) "(()()(()))")
((5 1 2 3 4) "(()()()())")
((1 5 4 2 3) "()((()()))")
((1 5 3 2 4) "()((())())")
((1 2 5 4 3) "()()((()))")
((1 2 5 3 4) "()()(()())")
((1 5 2 4 3) "()(()(()))")
((1 5 2 3 4) "()(()()())"))
(map (λ (p) (list (car p) (list->string (cadr p))))
(run/with-symbols ∞ (α β) (stacksort° β α '(5 4 3 2 1))))))
((eta 0.021) (memory #(12582912 3326680 1048576)) (stdout "") (stderr ""))
test/anti-reverse: pass
(define (test/anti-reverse _)
(⊦= "(((-)))" (anti-reverse "(((-)))"))
(⊦= "(-((((-))--)-))" (anti-reverse "((-(--((-))))-)"))
(⊨ (and ((closed? anti-reverse)
'("(-(-(((-)))-)-)"
"(((-((-)--)-)))"
"(((-(-(-)-)-)))"
"(((--((-))--)))"
"(((-(--(-))-)))"))
#t)))
((eta 0.0) (memory #(12582912 3276792 1048576)) (stdout "") (stderr ""))
test/2stacksort°: pass
(define (test/2stacksort° _)
(let* ((sort-by-arranging-ways/ascending (fsort cadr <))
(permutation+#paths+paths
(λ (p) (let1 (L (map cadr (cdr p))) (list (car p) (length L) L))))
(group-by-permutation (group car permutation+#paths+paths))
(permutation+path (λ (p) (list (car p) (list->string (cadr p)))))
(map->group->sort
(○ sort-by-arranging-ways/ascending
group-by-permutation
(fmap permutation+path)))
(permutations
(map->group->sort
(run/with-symbols ∞ (α β) (|2stacksort\xb0;| β α '(3 2 1))))))
(⊦= 6 (length permutations))
(⊨ (every (λ (p) (member? p (map car permutations)))
'((1 2 3) (1 3 2) (2 1 3) (2 3 1) (3 1 2) (3 2 1))))
(⊨ (every (λ (t) (= (cadr t) (length (caddr t)))) permutations))
(⊨ (apply <= (map cadr permutations)))
(⊨ (every (λ (t)
(every (λ (path)
(let1 (cs (string->list path))
(and (= 9 (length cs))
(= 3 (length (filter (=to? #\)) cs)))
(= 3 (length (filter (=to? #\-) cs))))))
(caddr t)))
permutations))))
((eta 0.021) (memory #(12582912 3288128 1048576)) (stdout "") (stderr ""))
test/recurrence-unfolding: pass
(define (test/recurrence-unfolding _)
(⊦= '(((2 1))
((0 1) (1 1))
((-2 1) (-1 2) (0 1))
((-4 1) (-3 3) (-2 3) (-1 1))
((-6 1) (-5 4) (-4 6) (-3 4) (-2 1))
((-8 1) (-7 5) (-6 10) (-5 10) (-4 5) (-3 1))
((-10 1) (-9 6) (-8 15) (-7 20) (-6 15) (-5 6) (-4 1))
((-12 1) (-11 7) (-10 21) (-9 35) (-8 35) (-7 21) (-6 7) (-5 1))
((-14 1)
(-13 8)
(-12 28)
(-11 56)
(-10 70)
(-9 56)
(-8 28)
(-7 8)
(-6 1)))
(map (λ (n)
((○ (λ (l) (sort l (λ args (apply < (map car args)))))
(group identity (λ (p) (list (car p) (length (cdr p))))))
(car (run/with-symbols ∞ (α) (fibonacci° n 2 α)))))
(list-tabulate 9 identity)))
(⊦= '((((1 1) 1))
(((0 1) 1) ((0 0) 1))
(((-1 1) 1) ((-1 0) 2) ((-1 -1) 1))
(((-2 1) 1) ((-2 0) 3) ((-2 -1) 3) ((-2 -2) 1))
(((-3 1) 1) ((-3 0) 4) ((-3 -1) 6) ((-3 -2) 4) ((-3 -3) 1))
(((-4 1) 1)
((-4 0) 5)
((-4 -1) 10)
((-4 -2) 10)
((-4 -3) 5)
((-4 -4) 1))
(((-5 1) 1)
((-5 0) 6)
((-5 -1) 15)
((-5 -2) 20)
((-5 -3) 15)
((-5 -4) 6)
((-5 -5) 1))
(((-6 1) 1)
((-6 0) 7)
((-6 -1) 21)
((-6 -2) 35)
((-6 -3) 35)
((-6 -4) 21)
((-6 -5) 7)
((-6 -6) 1))
(((-7 1) 1)
((-7 0) 8)
((-7 -1) 28)
((-7 -2) 56)
((-7 -3) 70)
((-7 -4) 56)
((-7 -5) 28)
((-7 -6) 8)
((-7 -7) 1)))
(map (λ (n)
((○ (λ (l)
(sort l (λ args (apply (tuple/pred? >=) (map car args)))))
(group identity (λ (p) (list (car p) (length (cdr p))))))
(car (run/with-symbols ∞ (α) (tartaglia° n 1 1 α)))))
(list-tabulate 9 identity))))
((eta 1.666) (memory #(50331648 3304272 1048576)) (stdout "") (stderr ""))
test/unify-binds-variables-to-terms: pass
(define (test/unify-binds-variables-to-terms _)
(⊦= '((3 3)) (run/with-symbols ∞ (v w) (∧ (≡ v w) (≡ v 3))))
(⊦= '((3 3)) (run/with-symbols ∞ (v w) (∧ (≡ v w) (≡ w 3))))
(⊦= '((3 3)) (run/with-symbols ∞ (v w) (∧ (≡ v w) (≡ 3 v))))
(⊦= '() (run/with-symbols ∞ (v w) (∧ (≡ v w) (≡ v 3) (≡ v 4))))
(⊦= '() (run/with-symbols ∞ (v w) (∧ (≡ v 3) (≡ w 4) (≡ v w))))
(⊦= '((3 3 3)) (run/with-symbols ∞ (u v w) (∧ (≡ u v) (≡ v w) (≡ w 3))))
(⊦= '((3 3 3)) (run/with-symbols ∞ (u v w) (∧ (≡ u v) (≡ w 3) (≡ v w))))
(⊦= '(((1 2) (1 2)))
(run/with-symbols ∞ (v w) (∧ (≡ v w) (≡ w `(1 ,(add1 1))))))
(⊦= '(((▢₀ 2) (▢₀ 2)))
(run/with-symbols ∞ (v w) (fresh (x) (∧ (≡ v w) (≡ v `(,x 2)))))))
((eta 0.001) (memory #(50331648 3300520 1048576)) (stdout "") (stderr ""))
test/unify-strings: pass
(define (test/unify-strings _)
(⊦= '(#t) (run/with-symbols ∞ (≡ "ab" (string #\a #\b))))
(⊦= '() (run/with-symbols ∞ (≡ "ab" "ba")))
(⊦= '("ab") (run/with-symbols ∞ (v) (∧ (≡ v "ab") (≡ v (string #\a #\b))))))
((eta 0.0) (memory #(50331648 3288800 1048576)) (stdout "") (stderr ""))
test/conditionals: pass
(define (test/conditionals _)
(⊦= '(1) (run/with-symbols ∞ (v) (cond°/! ((≡ v 1)) ((≡ v 2)))))
(⊦= '(cup)
(run/with-symbols ∞ (v) (cond°/! ((tea-cup° v) (≡ v 'cup)) ((≡ v 2)))))
(⊦= '(tea cup) (run/with-symbols ∞ (v) (cond°/! ((tea-cup° v)) ((≡ v 2)))))
(⊦= '(2) (run/with-symbols ∞ (v) (cond°/! (✗) ((≡ v 2)))))
(⊦= '(1) (run/with-symbols ∞ (v) (cond°/!! ((≡ v 1)) ((≡ v 2)))))
(⊦= '(tea) (run/with-symbols ∞ (v) (cond°/!! ((tea-cup° v)) ((≡ v 2)))))
(⊦= '(2) (run/with-symbols ∞ (v) (cond°/!! (✗) ((≡ v 2)))))
(⊦= '(1 2) (run/with-symbols ∞ (v) (cond°/¦ ((≡ v 1)) ((≡ v 2)))))
(⊦= '(tea cup 2) (run/with-symbols ∞ (v) (cond°/¦ ((tea-cup° v)) ((≡ v 2)))))
(⊦= '(▢₀ ▢₀ ▢₀) (run/with-symbols 3 (v) (cond°/¦ (always°) ((≡ v 2)))))
(⊦= '(▢₀ 2 ▢₀) (run/with-symbols 3 (v) (cond°/§ (always°) ((≡ v 2))))))
((eta 0.001) (memory #(50331648 3286960 1048576)) (stdout "") (stderr ""))
test/deepening: pass
(define (test/deepening _)
(⊦= '((1 1)) (run/with-symbols ↓ ∞ (v) ((deepening 1) (cond°/§ ((≡ v 1))))))
(⊦= '((1 1))
(run/with-symbols ↓ ∞ (v) ((deepening 1) (cond°/§ ((≡ v 1)) ((≡ v 2))))))
(⊦= '((1 1) (2 2))
(run/with-symbols ↓ ∞ (v) ((deepening 2) (cond°/§ ((≡ v 1)) ((≡ v 2))))))
(⊦= '((#t 0)) (run/with-symbols ↓ ∞ ((deepening 0) ✓))))
((eta 0.0) (memory #(50331648 3293144 1048576)) (stdout "") (stderr ""))
test/strict-errors: pass
(define (test/strict-errors _)
(⊨ (condition-case
(begin (run/with-symbols 'all (v) (≡ v 1)) #f)
((exn) #t)))
(⊨ (condition-case (begin (force ((≡ 1 1) 'no-status)) #f) ((exn) #t)))
(⊨ (condition-case (begin (V 3) #f) ((exn) #t)))
(⊨ (condition-case (begin (R "x" 0) #f) ((exn) #t)))
(⊨ (condition-case (begin (R 'x 'y) #f) ((exn) #t)))
(⊨ (and (variable? (V 'x)) (variable? (R 'x 0)) #t)))
((eta 0.0) (memory #(50331648 3306040 1048576)) (stdout "") (stderr ""))