Default solver: install-time recursion on NAF over recursive predicate

[hierophantos]

Summary

A solve form (using the default, non-WF solver) against a clause whose body contains (not (P ...)) where P is a recursive predicate triggers an install-time infinite recursion in install-conjunction ↔ install-clause-propagators-inner. The user sees memory growth + CPU pegged + eventually OOM or stack exhaustion.

The well-founded solver (solve-with wf-solver) handles the same program correctly. So the workaround exists — but the default solver should not silently loop on a structurally common program shape.

Severity: correctness. The user's program produces no answer, no error message, just hangs (or OOMs).

Reproduction

Save as bug-naf-recursive.prologos:

ns prologos.bug.naf-recursive

defr edge [?from ?to]
  || "a" "b"
     "b" "c"
     "c" "d"
     "b" "e"

defr vertex [?v]
  || "a" "b" "c" "d" "e" "f"

defr path [?from ?to]
  &> (edge from to)
  &> (edge from mid) (path mid to)

defr unreachable-from-a [?x]
  &> (vertex x) (not (path "a" x))

solve (unreachable-from-a x)

Run via process-file:

racket -e '(require "driver.rkt") (process-file "bug-naf-recursive.prologos")'

Expected: [{:x "a"} {:x "f"}] — a is unreachable from itself (no self-edge); f is isolated.

Actual: process hangs at install time, growing memory until OOM or user-break. Stack trace on user-break shows:

relations.rkt:2383:0: install-clause-propagators-inner
relations.rkt:2190:0: install-conjunction
relations.rkt:2383:0: install-clause-propagators-inner
relations.rkt:2190:0: install-conjunction
... (loops indefinitely)

Workaround

solver wf-solver
  :semantics well-founded

;; ... same defr declarations ...

solve-with wf-solver (unreachable-from-a x)

The well-founded engine handles install-time correctly. The non-NAF query solve (path \"a\" dest) against the same recursive path works fine (no NAF triggers the bug).

Initial hypothesis

The architecture comment at relations.rkt:2010 states:

"At S0: allocate assumption, register in NAF-pending cell. The NAF goal does NOT install inner goal propagators at S0. Inner goal installation happens on a FORK at S1 (clean isolation)."

The [(not) ...] case in install-goal-propagator (lines 2001–2049) honors this — it allocates the NAF assumption and writes to NAF-pending without installing the negated predicate's clauses inline.

So the loop isn't from the NAF-case branch directly. Likely candidates:

1. Default solver doesn't enable tabling early enough. install-clause-propagators (line 2333) breaks recursion via the table-consumer path (lines 2361–2362), but only when ctx + tabling are set up. The wf-solver appears to register tables proactively; the default solver may not, so the recursive (path mid to) reference inside path's own body falls through to install-clause-propagators-inner re-installing the clauses.

2. An eager pass installs all referenced predicates before the NAF handler can defer.

3. (not ...) is dispatched through a non-[(not)] code path in some installation site that doesn't honor the deferral comment.

The fact that the wf-solver path works means the underlying machinery is there; one code path is not honoring the stratification.

Fix paths considered

Approach	Effort	Notes
(A) Fail-fast: detect at install time, emit clear error pointing at wf-solver	1–2 hours	UX-only fix; no semantic improvement. Lowest risk.
(B) Default solver registers tables for recursive predicates upfront	half-day to day	Eliminates the loop. Adds default tabling overhead; may interact with :tabling :off configs.
(C) Locate + patch the actual recursion source	2–4 hours total (1–2 hr tracing + 30 min fix + verify)	Cleanest; aligns with the stated architecture (line 2010 comment). Likely a small site once located.
(D) Comprehensive: deferred-NAF universal across all solvers	1–2 days	Most principled. Could surface adjacent install-path issues. Worth doing if broader cleanup is warranted.

Recommended: (C). Tracing approach: eprintf instrumentation at lines 2190 and 2383 to print goal kinds + names on entry; the recursion's call chain on the failing program will reveal the site that doesn't honor the NAF deferral.

Surfacing context

Found while building the propagator-network demo for the upcoming meeting with Prof. J. B. Nation (commit 73f7aff9). The demo program needed solve-with wf-solver to install successfully. The architecture comments suggest the design intends stratified NAF to work universally; this is a single-path bug, not a missing feature.

Acceptance for fix

• Failing reproduction (above) installs and produces [{:x \"a\"} {:x \"f\"}] under default solve.
• No regression in solve-with wf-solver semantics.
• Test added to tests/ covering NAF over a recursive predicate.
• Existing acceptance file (examples/2026-03-14-wfle-acceptance.prologos) continues to pass.