mk: cycle-free path search test
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 44s

Mitigation for the cyclic-graph divergence (see tests/cyclic-graph.sx).
Threads a `visited` accumulator through the recursion; each candidate
next-step is gated by `nafc (membero z visited)`. Terminates on graphs
with cycles, no Phase-7 tabling required for the simple acyclic-path
query.

Demonstrates a viable alternative to tabling for the common case where
the user wants finite path enumeration over a graph with cycles.

3 new tests, 449/449 cumulative.
This commit is contained in:
2026-05-08 12:07:00 +00:00
parent 58d78de32a
commit 4df277803d
2 changed files with 41 additions and 0 deletions

View File

@@ -0,0 +1,40 @@
;; lib/minikanren/tests/path-cycle-free.sx — cycle-free reachability search.
;;
;; Threads a "visited" accumulator through the recursion, using nafc +
;; membero to prevent revisiting nodes. Demonstrates how to make the
;; cyclic-graph divergence problem (see tests/cyclic-graph.sx) tractable
;; for graphs with cycles, without invoking Phase-7 tabling.
(define
cf-edges
(list (list :a :b) (list :b :a) (list :b :c) (list :c :d) (list :d :a))) ; another cycle
(define cf-edgeo (fn (from to) (membero (list from to) cf-edges)))
(define
patho-no-cycles
(fn
(x y visited path)
(conde
((cf-edgeo x y) (nafc (membero y visited)) (== path (list x y)))
((fresh (z mid v-prime) (cf-edgeo x z) (nafc (membero z visited)) (conso z visited v-prime) (patho-no-cycles z y v-prime mid) (conso x mid path))))))
(define cf-patho (fn (x y path) (patho-no-cycles x y (list x) path)))
(mk-test
"cycle-free-finds-finitely"
(let
((paths (run* q (cf-patho :a :d q))))
(and
(>= (len paths) 1)
(every? (fn (p) (and (= (first p) :a) (= (last p) :d))) paths)))
true)
(mk-test
"cycle-free-direct-edge"
(run* q (cf-patho :a :b q))
(list (list :a :b)))
(mk-test "cycle-free-no-self-loop" (run* q (cf-patho :a :a q)) (list))
(mk-tests-run!)

View File

@@ -173,6 +173,7 @@ _(none yet)_
_Newest first._
- **2026-05-08** — **cycle-free path search**: mitigation for the cyclic-graph divergence — thread a accumulator through the recursion, gate each step with nafc + membero on visited. Terminates on graphs with cycles; no Phase-7 tabling required for the simple case. 3 new tests, 449/449 cumulative.
- **2026-05-08** — **removeo-allo**: removes every occurrence of x (vs rembero, which removes only the first). Three conde clauses: empty -> empty; head matches -> skip and recurse; head differs (nafc) -> keep and recurse. 5 new tests, 446/446 cumulative.
- **2026-05-08** — **btree-walko (matche showcase)**: walks a binary tree (:leaf v) | (:node l r) and emits each leaf value via conde. Demonstrates matche dispatch on tagged-list patterns, recursion through both branches via conde, and run* enumerating all 5 leaves of a small tree. 4 new tests, 441/441 cumulative.
- **2026-05-08** — **swap-firsto**: swap the first two elements of a list. Built via four conso constraints. Self-inverse on length-2+ lists; runs forward and backward. 6 new tests, 437/437 cumulative.