From 4df277803d93c6c6683c8233e6d204791bd5265f Mon Sep 17 00:00:00 2001 From: giles Date: Fri, 8 May 2026 12:07:00 +0000 Subject: [PATCH] mk: cycle-free path search test 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. --- lib/minikanren/tests/path-cycle-free.sx | 40 +++++++++++++++++++++++++ plans/minikanren-on-sx.md | 1 + 2 files changed, 41 insertions(+) create mode 100644 lib/minikanren/tests/path-cycle-free.sx diff --git a/lib/minikanren/tests/path-cycle-free.sx b/lib/minikanren/tests/path-cycle-free.sx new file mode 100644 index 00000000..2c46e407 --- /dev/null +++ b/lib/minikanren/tests/path-cycle-free.sx @@ -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!) diff --git a/plans/minikanren-on-sx.md b/plans/minikanren-on-sx.md index d04acc87..300c3661 100644 --- a/plans/minikanren-on-sx.md +++ b/plans/minikanren-on-sx.md @@ -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.