datalog: dl-walk handles circular substitutions without infinite loop (257/257)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 27s

Bug: dl-walk would infinite-loop on a circular substitution
(e.g. A→B and B→A simultaneously). The walk endlessly chased
the cycle. This couldn't be produced through dl-unify (which has
cycle-safe behavior via existing bindings), but raw dl-bind calls
or external manipulation of the subst dict could create it.

Fix: dl-walk now threads a visited-names list through the
recursion. If a variable name is already in the list, the walk
stops and returns the current term unchanged. Normal chained
walks are unaffected (A→B→C→42 still resolves to 42).

1 new unify test verifies circular substitutions don't hang.
This commit is contained in:
2026-05-11 07:20:20 +00:00
parent a9e4eea334
commit 9a16f27075
4 changed files with 32 additions and 11 deletions

View File

@@ -129,6 +129,15 @@
((s2 (dl-unify (quote Y) (quote tom) s1)))
(dl-walk (quote X) s2)))
(quote tom))
;; Walk with circular substitution must not infinite-loop.
;; Cycles return the current term unchanged.
(dl-ut-test!
"walk circular subst no hang"
(let ((s (dl-bind (quote B) (quote A)
(dl-bind (quote A) (quote B) (dl-empty-subst)))))
(dl-walk (quote A) s))
(quote A))
(dl-ut-test!
"apply subst on tuple"
(let