mk: cyclic-graph behaviour test — motivates Phase 7 tabling
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 28s

Demonstrates the naive-patho behaviour on a 2-cycle (a <-> b, plus
b -> c). Without Phase-7 tabling, the search produces ever-longer
paths: (a b), (a b a b), (a b a b a b), ... `run 5` truncates to a
finite prefix; `run*` diverges. Documenting this as a regression-style
test gives Phase 7 a concrete starting point.

3 new tests, 331/331 cumulative.
This commit is contained in:
2026-05-08 11:19:29 +00:00
parent 2d51a8c4ea
commit 16fe22669a
2 changed files with 53 additions and 0 deletions

View File

@@ -0,0 +1,48 @@
;; lib/minikanren/tests/cyclic-graph.sx — demonstrates the naive-patho
;; behaviour on a cyclic graph. Without Phase-7 tabling/SLG, the search
;; produces ever-longer paths revisiting the cycle. `run n` truncates;
;; `run*` would diverge.
(define cyclic-edges (list (list :a :b) (list :b :a) (list :b :c)))
(define cyclic-edgeo (fn (x y) (membero (list x y) cyclic-edges)))
(define
cyclic-patho
(fn
(x y path)
(conde
((cyclic-edgeo x y) (== path (list x y)))
((fresh (z mid) (cyclic-edgeo x z) (cyclic-patho z y mid) (conso x mid path))))))
;; --- direct edge ---
(mk-test
"cyclic-direct"
(run 1 q (cyclic-patho :a :b q))
(list (list :a :b)))
;; --- runs first 5 paths from a to b: bare edge, then increasing
;; numbers of cycle traversals (a->b->a->b, etc.) ---
(mk-test
"cyclic-enumerates-prefix-via-run-n"
(let
((paths (run 5 q (cyclic-patho :a :b q))))
(and
(= (len paths) 5)
(and
(every? (fn (p) (= (first p) :a)) paths)
(every? (fn (p) (= (last p) :b)) paths))))
true)
(mk-test
"cyclic-finds-c-via-cycle-or-direct"
(let
((paths (run 3 q (cyclic-patho :a :c q))))
(and
(>= (len paths) 1)
(some (fn (p) (= p (list :a :b :c))) paths)))
true)
(mk-tests-run!)

View File

@@ -173,6 +173,11 @@ _(none yet)_
_Newest first._
- **2026-05-08** — **Cyclic graph behaviour test (motivates Phase 7 tabling)**:
Demonstrates that naive patho on a 2-cycle generates ever-longer paths.
`run 5` truncates to a finite prefix; `run*` would diverge. This is
exactly the test case Phase 7 (tabled / SLG resolution) is designed
to fix. 3 new tests, 331/331 cumulative.
- **2026-05-08** — **numbero / stringo / symbolo (type predicates)**: ground-only
type tests via project. Compose with `membero` for type-filtered enumeration:
`(fresh (x) (membero x (1 "a" 2 "b" 3)) (numbero x) (== q x))``(1 2 3)`.