Recursion through Clingo() emits scrambled iteration frames — cycle evaluates one round regardless of @Recursive; functional predicates in recursive SCCs generally mishandled

[ludaesch]

Found while preparing experiments for the ASPOCP'26 paper (Skvortsov, Xia, Garg, Bowers, Ludäscher). Logica @ GitHub main (2026-08-06), clingo 5.8.1, DuckDB 1.5.5, macOS; installed via pip install git+https://github.com/EvgSkv/logica in a fresh venv.

Summary

A recursive cycle that passes through a Clingo() call is evaluated for exactly one round — the feedback edge is effectively cut — at every @Recursive budget. Inspecting the generated SQL shows the unroller does attempt to unfold the cycle, but emits a scrambled frame graph: several iteration-frame tables are CREATE TABLE'd twice from different inputs and overwrite each other mid-execution. A no-Clingo control with the same shape (functional predicate inside the SCC) fails outright with a DuckDB binder error, suggesting the root cause is general: recursion through functional (=) predicates in an SCC.

Repro 1 — one round instead of iteration

@Engine("duckdb", clingo: {time_limit: ∞, models_limit: ∞});

# Candidates: "i", and the successor (one more "i") of anything picked.
In(x) distinct :- x == "i" | Out(y), x == y ++ "i";

# ASP fragment: free choice; union over all models = all candidates.
Pick(x) couldbe :- Cand(x);

M() = Clingo(["Pick", "Cand"],
             List{ClingoFact("Cand", [x]) :- In(x)});

Out(x) distinct :-
  ExtractClingoCall(x, predicate: "Pick", model_id:) = M();

logica grow.l run Out → {"i"} (one round).

Control without the solver (same growth recursion):

@Engine("duckdb");
In(x) distinct :- x == "i" | In(y), x == y ++ "i", Length(y) < 20;

→ "i" … "iiiii" (normal iterative evaluation). Adding @Recursive(In, 12) or (24) to the Clingo version adds exactly one _ifr frame to the plan and never changes the result.

Evidence: the generated frame graph is incoherent

logica grow.l print Out emits frames In_ifr0..4, M_ifr0..4, Out_ifr1..4, and the feedback edge is present (In_ifr4 reads Out_ifr3.col0 || 'i') — so this is not a deliberate cut. But mapping each CREATE TABLE to the tables it reads gives three interleaved chains:

In_ifr1 (base) -> M_ifr2 -> Out_ifr3 -> In_ifr4 -> M_ifr3
M_ifr0 (base)  -> Out_ifr1 -> In_ifr2 -> M_ifr3      (M_ifr3 created 2nd time)
In_ifr0 (base) -> M_ifr1 -> Out_ifr2 -> In_ifr3 -> M_ifr4
Out_ifr3 <- M_ifr3, M_ifr4                            (Out_ifr3 created 2nd time)
final SELECT <- Out_ifr3, M_ifr3, M_ifr4

M_ifr3, In_ifr3, and Out_ifr3 are each created twice with different inputs; sequential execution silently overwrites, and the final answer reads from mixed chains.

Repro 2 — same shape without Clingo doesn't even bind

@Engine("duckdb");
In(x) distinct :- x == "i" | Out(y), x == y ++ "i";
F() = List{x :- In(x)};
Out(x) distinct :- x in F(), Length(x) < 6;

→ _duckdb.BinderException: Binder Error: UNNEST not supported here

So the pure functional-predicate-in-SCC case errors, while the Clingo case produces running-but-wrong SQL.

Suggested fix

Until the unroller supports SCCs containing functional predicates (and Clingo() calls in particular): detect and reject them at compile time with a clear message. Silent one-round evaluation is the worst outcome — the ASPOCP camera-ready now documents the current behavior as "mutual recursion across the boundary is currently not iterated."

Smaller issues found in the same session (can file separately if useful)

1. Empty List{ClingoFact(...) :- ...} (zero rows) makes the facts argument NULL and Clingo() silently returns NULL — no error, no models.
2. ~P(x) over fact-fed predicates in a cantbe rule makes the dependency check demand a synthesized internal predicate: "Predicate MustPick depends on IsNull but IsNull was not requested."
3. Count{...} shouldbe passes the compiler but generates ASP that clingo rejects with "parsing failed" (only Max/Min are documented for optimization).
4. Docs/paper use @Engine("duckdb", clingo: {time_limit: inf, ...}) but the parser only accepts ∞ — inf fails with "Could not understand arguments of annotation."

🤖 Generated with Claude Code

https://claude.ai/code/session_01NA7AvfwRmaHjWwcsFgbxo4

[ludaesch]

Follow-up after Evgeny's report that @Recursive(In, 5) yields i … iiiiiii ("recursion works"): we re-ran the repro across the states we can reach, and we get materially different behavior on each. Config matrix (all: macOS, clingo 5.8.1):

Logica state	query	result
main as of ~Aug 5 (last pip-installable commit), duckdb 1.5.5	run Out, @Recursive(In,{4,12,24})	one round ({"i"})
same	run Out, @Recursive(In,5)	two rounds ({"i","ii"})
same	run In, @Recursive(In,3..10) sweep	capped at two rounds for every n
head 7d96853 ("Supporting list aggregation", Aug 6 08:04 PDT), duckdb 1.5.5	run In / run Out, @Recursive(In,5)	Binder Error: UNNEST not supported here
head 7d96853, duckdb 1.1.3	same	same binder error

So on the states we can reach, we never see more than two rounds, and pushed head currently crashes on the repro. Two questions that would pin this down:

1. Which commit is your run on (git rev-parse HEAD), and does it include local changes? Ours suggests your tree is ahead of 7d96853.
2. Which runner — CLI logica <file> run In, or the notebook/colab path — and which duckdb version?

Also possibly relevant: head 7d96853 has no setup.py/pyproject.toml, so pip install git+https://github.com/EvgSkv/logica currently fails ("does not appear to be a Python project") — if that's not intentional restructuring, it bites anyone installing from git.

If your working tree already fixes the unrolling — excellent, that's exactly the outcome we hoped the report would trigger; the matrix above then documents what the released/pushed states do in the meantime.

🤖 Generated with Claude Code

https://claude.ai/code/session_01NA7AvfwRmaHjWwcsFgbxo4

[ludaesch]

Reconciled — Evgeny is right, and the divergence is now precisely located: it's two execution paths, not versions or machines.

run_in_terminal (concertina driver, diamond/portal iteration) — works. Reproduced on pushed head 7d96853, duckdb 1.1.3: logica grow-r5.l run_in_terminal In iterates M_diamond 5/5, Out_diamond 5/5 and returns i … iiiiii. Recursion through the Clingo() boundary behaves exactly as intended under this engine. We simply didn't know this command existed — apologies for the noise about "one round."

run / static compilation — still the bug. Everything in the original report applies to the default run path: scrambled iteration frames with duplicate CREATE TABLEs on the last pip-installable main (~Aug 5), and Binder Error: UNNEST not supported here on head (duckdb 1.1.3 and 1.5.5). Suggested resolution updated accordingly: have run/run_to_csv delegate recursive-through-Clingo programs to the driver, or reject them with a pointer to run_in_terminal — silent wrong results being the worst outcome.

One new driver failure while testing: a flip-flop variant where the fragment's output suppresses its next input fails in the driver at the portal-table stage with the same UNNEST binder error (duckdb 1.1.3 and 1.5.5, head):

@Engine("duckdb", clingo: {time_limit: ∞, models_limit: ∞});
@Recursive(Out, 6);

Seed("p");
Blocked(x) distinct :- Out(x) | x == "dummy";

Pick(x) couldbe :- Cand(x);
CantPick() cantbe :- Pick(x), Blk(x);

M() = Clingo(["Pick", "Cand", "CantPick", "Blk"],
             List{ClingoFact("Cand", [x]) :- Seed(x)}
             ++ List{ClingoFact("Blk", [x]) :- Blocked(x)});

Out(x) distinct :-
  ExtractClingoCall(x, predicate: "Pick", model_id:) = M();

logica flip5.l run_in_terminal Out → Binder Error: UNNEST not supported here creating Out_portal / unnesting M_portal.logica_value. This one is interesting semantically: if the driver handles it, the program oscillates (picked ⇒ blocked ⇒ unpicked ⇒ …), i.e. exactly the non-stabilizing case your stabilization semantics is for — would love to see what the diamond engine reports for it.

🤖 Generated with Claude Code

https://claude.ai/code/session_01NA7AvfwRmaHjWwcsFgbxo4