From 6fc155ddd82cdb6b687b761f9387c495de4ecdce Mon Sep 17 00:00:00 2001 From: giles Date: Fri, 8 May 2026 11:51:51 +0000 Subject: [PATCH] =?UTF-8?q?mk:=20rev-acco=20+=20rev-2o=20=E2=80=94=20accum?= =?UTF-8?q?ulator-style=20reverse?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit rev-acco is the standard tail-recursive reverse with an accumulator; rev-2o starts the accumulator at the empty list. Faster than the appendo-driven reverseo for forward queries because there is no nested appendo per element. Trade-off: rev-acco is asymmetric. The accumulator's initial-empty cannot be enumerated backwards the way reverseo does, so reverseo is still the right choice when both directions matter. A test verifies rev-2o and reverseo agree on forward queries. 6 new tests, 422/422 cumulative. --- lib/minikanren/relations.sx | 12 ++++++++- lib/minikanren/tests/rev-acco.sx | 46 ++++++++++++++++++++++++++++++++ plans/minikanren-on-sx.md | 1 + 3 files changed, 58 insertions(+), 1 deletion(-) create mode 100644 lib/minikanren/tests/rev-acco.sx diff --git a/lib/minikanren/relations.sx b/lib/minikanren/relations.sx index b2b837a8..ca2abf09 100644 --- a/lib/minikanren/relations.sx +++ b/lib/minikanren/relations.sx @@ -66,13 +66,23 @@ ((nullo l) (nullo r)) ((fresh (a d res-rev) (conso a d l) (reverseo d res-rev) (appendo res-rev (list a) r)))))) +(define + rev-acco + (fn + (l acc result) + (conde + ((nullo l) (== result acc)) + ((fresh (a d acc-prime) (conso a d l) (conso a acc acc-prime) (rev-acco d acc-prime result)))))) + +(define rev-2o (fn (l result) (rev-acco l (list) result))) + (define palindromeo (fn (l) (fresh (rev) (reverseo l rev) (== l rev)))) + (define prefixo (fn (p l) (fresh (rest) (appendo p rest l)))) (define suffixo (fn (s l) (fresh (front) (appendo front s l)))) - (define subo (fn diff --git a/lib/minikanren/tests/rev-acco.sx b/lib/minikanren/tests/rev-acco.sx new file mode 100644 index 00000000..6733fe9a --- /dev/null +++ b/lib/minikanren/tests/rev-acco.sx @@ -0,0 +1,46 @@ +;; lib/minikanren/tests/rev-acco.sx — accumulator-style reverse. +;; +;; Faster than reverseo for forward queries (no quadratic appendos). +;; Trade-off: rev-acco is asymmetric (acc=initial-empty for the public +;; interface), so it does not cleanly run backwards in run* the way +;; reverseo does. + +(mk-test "rev-2o-empty" (run* q (rev-2o (list) q)) (list (list))) + +(mk-test + "rev-2o-singleton" + (run* q (rev-2o (list 7) q)) + (list (list 7))) + +(mk-test + "rev-2o-three" + (run* q (rev-2o (list 1 2 3) q)) + (list (list 3 2 1))) + +(mk-test + "rev-2o-five" + (run* + q + (rev-2o (list 1 2 3 4 5) q)) + (list (list 5 4 3 2 1))) + +(mk-test + "rev-2o-strings" + (run* q (rev-2o (list "a" "b" "c") q)) + (list (list "c" "b" "a"))) + +(mk-test + "rev-2o-reverseo-agree" + (let + ((via-reverseo (first (run* q (reverseo (list 1 2 3 4 5) q)))) + (via-rev-2o + (first + (run* + q + (rev-2o + (list 1 2 3 4 5) + q))))) + (= via-reverseo via-rev-2o)) + true) + +(mk-tests-run!) diff --git a/plans/minikanren-on-sx.md b/plans/minikanren-on-sx.md index 07f05f2c..5307dc9c 100644 --- a/plans/minikanren-on-sx.md +++ b/plans/minikanren-on-sx.md @@ -173,6 +173,7 @@ _(none yet)_ _Newest first._ +- **2026-05-08** — **rev-acco / rev-2o**: accumulator-style reversal — faster than appendo-driven reverseo for forward queries because no quadratic appendos. Trade-off: rev-acco is asymmetric (cannot run cleanly backward in run*). 6 new tests, 422/422 cumulative. - **2026-05-08** — **even-i / odd-i (intarith)**: ground-only parity goals via project. Composes with membero for filtered enumeration: -> . 5 new tests, 416/416 cumulative. - **2026-05-08** — **selecto**: classic miniKanren "choose an element + rest". Direct base (l = (x . rest)) plus skip-head recurse. Enumerates all (element, rest) splits in run*; runs forward, backward, mid-pipeline. 6 new tests, 411/411 cumulative. - **2026-05-08** — **subo (contiguous sublist)**: Two appendos chained — l = front ++ s ++ back. Goal order matters: appendo on the ground l first, so the search is finitary; then constrain front. 7 new tests, 405/405 cumulative.