mk: rev-acco + rev-2o — accumulator-style reverse
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 29s
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 29s
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.
This commit is contained in:
@@ -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
|
||||
|
||||
46
lib/minikanren/tests/rev-acco.sx
Normal file
46
lib/minikanren/tests/rev-acco.sx
Normal file
@@ -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!)
|
||||
@@ -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.
|
||||
|
||||
Reference in New Issue
Block a user