Investigative Report: Making Oscillation Risk Visible in Ampersand

Status: unpublished research. This is a working research note, not a peer-reviewed publication. It records a literature study and the design and validation of the Stage-1 oscillation-risk analysis now in the compiler. Sections 1–5 are the literature analysis; sections 6–7 document the implementation and the open questions.

Literature-grounded analysis and plan. Search id 1; 17 references in literature_search.csv. In-text citations use the symbolic keys [@cite_key]; the full reference for each key is listed under References at the end.

---

0. What this report does

The oscillation guide (docs/guides/oscillations/README.md) establishes that an oscillation (Maximum reruns exceeded) is the runtime telling you that, given the data, your automated rules are jointly unsatisfiable. It also states the open problem: we cannot mathematically predict from the code whether an oscillation will occur, but we would like to make the risk of one visible.

This report reads the literature on that exact question, reformulates the problem in the vocabulary the literature uses, weighs the candidate methods against each other, and ends with an advised approach for Ampersand.

---

1. Interpreting the problem through the literature

The same phenomenon — a repair loop that may never reach a fixpoint — has been studied independently in four communities. Each gives Ampersand a precise name for one facet of the ExecEngine.

1.1 The ExecEngine repair loop extends the chase

The closest formal match is the chase from database dependency theory. The chase is a fixpoint procedure that repeatedly enforces dependencies on an instance, inserting tuples (possibly with fresh nulls) and equating values until no dependency is violated [@Fagin2005DataExchange; @Onet2013ChaseProcedure]. Two dependency kinds drive it, and they line up one-to-one with Ampersand's {EX} primitives:

Chase dependency	Ampersand {EX} primitive	Effect
TGD (tuple-generating, often existential)	InsAtom, InsPair, NewStruct	adds facts (a fresh atom = a fresh null)
EGD (equality-generating)	MrgAtoms	equates two atoms
(no standard analogue)	DelPair, DelAtom	removes facts

The FC5 case is textbook: the create-rule eppoCodeMaaktOrganisme is an existential TGD (it invents a fresh Organisme), and the merge-rule OrganismeUniekeEPPO is an EGD (it equates two Organisme atoms). "Maximum reruns exceeded" is exactly non-termination of the chase. This matters because chase termination is the single most-studied version of our question, and crucially it is studied data-independently: the standard criteria guarantee termination for every instance [@Fagin2005DataExchange].

A caveat that shapes the whole analysis. The match is an extension, not an identity: the chase only ever adds and equates; it never retracts. Ampersand's DelPair/DelAtom have "no standard analogue" (last table row) precisely because the chase has none. This matters because the two kinds of {EX} give rise to two distinct non-termination causes:

• create-driven non-termination — a generating dependency (InsAtom/NewStruct, possibly with MrgAtoms) keeps inventing fresh atoms (the FC5 loop). This is the chase's own termination problem, and the tool for it is chase acyclicity (§3.2);
• delete-driven oscillation — a Del/Mrg repair undoes what another repair created, so the combined operator is non-monotone (the insdel loop, RAP's role web). The chase cannot exhibit this; the right tool is the monotonicity/stratification view of §1.4 / §3.4.

Keeping these apart matters later: the implemented Stage 1 (§6) and its convergence certificate (§6.5) target the delete-driven class, while the create-driven class is the subject of the still-future weak-acyclicity work (§4, §7). Conflating them is the easiest way to misread what the analysis does and does not guarantee.

1.2 The ExecEngine is also an active (ECA) rule system

Viewed operationally, the ExecEngine is an active database: each automated rule is an event–condition–action rule whose action can re-trigger other rules [@Paton1999ActiveDB]. This community framed precisely our three questions — is a rule set guaranteed to terminate, to reach a unique final state (confluence), and to produce a unique observable behaviour — and answered them by static analysis of the rule set [@Aiken1995StaticAnalysis]. This is the literature that gives us the rule-level dependency graph and the language of "rules that re-trigger each other," which is also how the guide already reasons ("Rules fixed in last run", "a write that feeds another antecedent").

1.3 The ExecEngine is also a graph-rewriting system

An Ampersand population is a labelled graph (atoms = nodes, pairs = edges), and every {EX} action is a graph rewrite. In that setting termination and confluence are the standard well-behavedness properties, and critical-pair analysis detects pairs of rules that conflict — one rule disabling or undoing what another did [@Lambers2006ConflictDetection]. That is precisely the guide's "opposing actions" signature (one rule adds a fact, another removes/merges it on the same relation or atom).

1.4 The unifying lens: monotonicity and stratification

Underneath all three views is one distinction the guide already draws: monotone (insert-only) repair converges to a least fixpoint by Knaster–Tarski/Kleene, whereas delete/merge make the repair operator non-monotone and it can cycle. Logic programming made this operational long ago: build the predicate dependency graph with positive and negative edges; if no cycle runs through a negative edge, the program is stratified and has a well-defined, terminating semantics [@Apt1988DeclarativeKnowledge]. Translated to Ampersand: a repair that removes or merges (DelPair, DelAtom, MrgAtoms) is a negative-polarity edge; a cycle through a negative edge is the formal signature of oscillation risk. This single idea reappears as "no special-edge cycle" in the chase (§2) and as "no triggering cycle" in active rules (§1.2).

---

2. A more precise statement of the problem

The literature lets us sharpen the original question into something implementable.

Given a set R of automated rules, each a relation-algebra inclusion antecedent ⊆ consequent with a repair script of {EX} primitives, construct a static analysis A(R), computed from the rule text alone (data-independent), such that:

1. Soundness for termination (no false "safe"). If A(R) reports safe, then for every population the ExecEngine repair loop terminates. (This is exactly the guarantee weak acyclicity gives the chase [@Fagin2005DataExchange].)
2. Explanatory risk reports. When A(R) cannot certify safety, it returns the minimal set of mutually-triggering rules and the relation(s)/atom(s) on which opposing writes meet — i.e. it reproduces, statically and before any data is loaded, the "Rules fixed in last run" diagnosis the runtime gives after the fact.
3. Conservative by design. False positives (flagging a safe rule set as risky) are acceptable; false negatives (missing a real oscillation) are not.

Two consequences follow directly from the abstracts.

(a) We cannot ask for an exact decision — and now we know why. Joosten proves that entailment over invariants written with composition, converse and intersection of binary relations (with equality) — the core idea behind languages such as Ampersand — is undecidable; his "graph saturation" procedure is therefore only a semi-decision procedure that need not terminate [@Joosten2018GraphSaturation]. The same verdict comes from the chase: termination is undecidable in general [@Deutsch2008ChaseRevisited; @Greco2011StratificationCriteria]. So the guide's claim ("we cannot mathematically predict oscillation from the code") is not a gap in our cleverness; it is a theorem. The only coherent goal is a sound over-approximation: a sufficient condition for termination whose negation we surface as risk. This is the design stance every method below shares.

(b) "Risk" has two distinguishable structural causes, matching the guide's two signatures:

• a triggering cycle — rule A's repair feeds rule B's antecedent and vice versa (§1.2); and
• an opposing-write conflict — within such a cycle, at least one edge is negative (a Del/Mrg undoes an Ins), which is what turns a benign monotone cycle into a non-monotone, potentially oscillating one (§1.4).

A useful analysis must detect the cycle and its polarity, because a purely positive (monotone) cycle still converges by Knaster–Tarski and must not be flagged — otherwise the analysis drowns the user in false alarms.

Scope of the soundness guarantee (as currently implemented). Requirement (3) — never miss a real oscillation — is met for the delete-driven class (§1.1): every cycle whose non-termination would come from opposing Ins/Del writes is either flagged or provably convergent. It is not yet met for the create-driven class: a rule re-triggered purely by the existence of a freshly created atom (e.g. I[C] |- r repaired by InsAtom;C) is not modelled (§6.3), so such an existential, chase-style non-termination can currently be reported "safe" — a known false negative. Closing it is exactly the weak-acyclicity work of §4/§7. Until then, read "safe" as "safe against delete-driven oscillation".

---

3. The candidate methods, compared on equal footing

Four families of methods can supply A(R). They differ mainly in granularity (do they reason about whole rules or about individual relation positions?), which drives their precision (false-positive rate) and cost.

3.1 Rule-level triggering / activation graph (active databases)

Build a directed graph with one node per automated rule; an edge A → B when A's action can change a relation occurring in B's antecedent. No cycle ⇒ guaranteed termination; a cycle is a necessary condition for non-termination [@Aiken1995StaticAnalysis]. The refined triggering graph prunes edges where the action cannot actually re-satisfy the other rule's condition, removing spurious cycles [@Urban1999RefinedTriggering], and later refinements delete still more edges that cannot lead to actual re-execution, certifying termination for strictly more rule sets [@Couchot2002ImprovingRTG]. An algebraic reformulation expresses the test in terms of properties of the action operators (e.g. commutativity ⇒ confluence) rather than syntax [@Baralis2000AlgebraicApproach], and modularization keeps it tractable on large rule sets [@Baralis1996Modularization].

• + Granularity matches the user's mental model and the guide's diagnosis exactly: it names rules. Cheap to compute; cycle detection on a small graph.
• + The algebraic variant is the natural way to lift the test onto relation-algebra operators, and Ampersand already manipulates rules as relation-algebra terms.
• − Coarse: it over-approximates at the rule level, so it flags cycles that the data can never actually drive — more false positives than position-level analysis.
• − Plain triggering graphs ignore polarity; without the signed refinement (§1.4) they flag monotone cycles that always converge.

3.2 Position-level acyclicity (the chase)

Build a dependency graph over relation positions (argument slots). Mark edges that carry a freshly invented value ("special"/existential edges). Weak acyclicity = no cycle through a special edge ⇒ the chase terminates on every instance [@Fagin2005DataExchange]. Successively more permissive criteria certify strictly larger classes: stratification and c-stratification [@Deutsch2008ChaseRevisited], super-weak acyclicity [@Marnette2009GeneralizedSchemaMappings], and a unifying local-stratification hierarchy with rewriting techniques that massage a rule set so more criteria apply [@Greco2011StratificationCriteria; @CuencaGrau2013AcyclicityNotions]. Critically for us, most early criteria ignore EGDs; later work shows EGDs (= MrgAtoms) materially affect termination and gives criteria that exploit them [@Calautti2016EGDChaseTermination]. A complementary line keeps reasoning decidable even when the chase does not terminate, via structural restrictions such as guardedness [@Cali2013TamingChase].

• + Strongest precision: position-level value-flow analysis flags far fewer safe sets than rule-level graphs. Decidable in polynomial time for several criteria [@Marnette2009GeneralizedSchemaMappings].
• + EGD-aware variants target exactly the create-vs-merge interaction that caused FC5 [@Calautti2016EGDChaseTermination].
• + Soundness-for-all-instances is the literal form of requirement (1) in §2.
• − Granularity is positions, not rules; turning a "special-edge cycle" back into a human-readable "these two rules collide" report needs extra work.
• − Heavier to implement: it requires modelling each {EX} script as TGD/EGD bodies and tracking value provenance across positions.

3.3 Critical-pair analysis (graph rewriting)

Enumerate the minimal population fragments on which two rules conflict — one rule's rewrite disables or undoes another's. No critical pairs ⇒ local confluence (Newman's lemma); the AGG tool computes these automatically [@Lambers2006ConflictDetection].

• + Directly formalises the guide's "opposing actions" signature; tells you which two repairs undo each other and on what overlap.
• + Aims at confluence (unique result), a property the rule-level and position-level termination tests do not directly give.
• − Critical-pair enumeration is combinatorially heavier and is about confluence, not primarily termination; on its own it does not bound the number of reruns.
• − Tooling lives in the model-transformation world; porting to Ampersand's relation-algebra rewrites is a non-trivial bridge.

3.4 Signed dependency graph / stratification (logic programming)

The conceptual unifier of §1.4: a predicate (here: relation) dependency graph with positive and negative edges; a cycle through a negative edge means unstratified and is the formal risk signature [@Apt1988DeclarativeKnowledge].

• + Captures the one thing the bare triggering graph misses — polarity — and does so with almost no extra machinery.
• + Explains why monotone rule sets are always safe (Knaster–Tarski), so it naturally suppresses the false alarms of §3.1.
• − Stratification by itself is a yes/no property; it does not localise which atoms nor bound reruns. It is best used as a refinement layer on top of §3.1, not standalone.

3.5 Comparison summary

Method	Granularity	Precision (fewer false +)	Cost	Names colliding rules?	EGD/merge-aware?	Gives confluence?
3.1 Triggering graph [@Aiken1995StaticAnalysis; @Urban1999RefinedTriggering]	rule	low–medium	low	yes	only if encoded	partial (algebraic [@Baralis2000AlgebraicApproach])
3.2 Chase acyclicity [@Fagin2005DataExchange; @Calautti2016EGDChaseTermination]	position	high	medium–high	not directly	yes	no
3.3 Critical pairs [@Lambers2006ConflictDetection]	rule-pair + graph overlap	high (for conflict)	high	yes	yes	yes
3.4 Signed graph / stratification [@Apt1988DeclarativeKnowledge]	relation/rule	refinement only	very low	yes (as layer)	yes (sign of Mrg)	no

No single row dominates. The pragmatic reading: 3.1 + 3.4 give the cheapest, most explanatory first cut; 3.2 (EGD-aware) buys precision exactly where Ampersand bleeds; 3.3 is the principled future answer for confluence.

---

4. Selection: an advised approach for Ampersand

Given the trade-offs, a single layered analysis built in stages dominates any one method used alone. Each stage is independently shippable and strictly increases precision.

Stage 0 — Frame and classify (concept work, no code). Adopt the chase as the official semantics of the ExecEngine [@Fagin2005DataExchange; @Joosten2018GraphSaturation], and classify each {EX} primitive once: Ins*/NewStruct = monotone (positive), Del* = non-monotone (negative), MrgAtoms = EGD (negative). This classification is the input to every later stage and is already implicit in the guide.

Stage 1 — Signed, refined rule-level triggering graph (primary, user-facing). Combine §3.1 and §3.4. Nodes are automated rules. Add edge A → B when A's repair writes a relation that occurs in B's antecedent; label the edge + if A only inserts into it and − if A can delete-or-merge it [@Aiken1995StaticAnalysis; @Apt1988DeclarativeKnowledge]. Prune edges that cannot actually re-trigger B, as in the refined triggering graph and its later refinements [@Urban1999RefinedTriggering; @Couchot2002ImprovingRTG]. Report a risk for every cycle that contains at least one − edge, naming the rules and the shared relation — statically reproducing the runtime's "Rules fixed in last run." Purely positive cycles are not flagged, because monotone repair converges (Knaster–Tarski). Use the algebraic operator view to compute edge labels directly from the relation-algebra terms [@Baralis2000AlgebraicApproach], and modularize per pattern to scale [@Baralis1996Modularization].

Why first: highest value-to-effort ratio. It speaks in rules (the user's and the guide's language), it is cheap, and with the sign refinement it already separates the dangerous non-monotone cycles from the harmless monotone ones. Its known weakness is false positives.

Stage 2 — precision layer (two independent sub-goals). Stage 1's only weakness is false positives, and they have two distinct causes (§1.1), each needing its own tool. It is clearest to treat Stage 2 as two separable pieces:

Stage 2a — convergence certificate for the delete-driven class (implemented, see §6.5). The opposing-write cycles Stage 1 flags are mostly benign maintenance: a relation kept equal to a definition (ENFORCE :=, the Determine/Remove idiom, complementary-guard toggles) or a delete-only cleanup. These converge for a stratification reason, not a value-flow one [@Apt1988DeclarativeKnowledge], so they are certified with a signed, relation-level argument (delete-only ⇒ well-founded descent; R := D with D invariant ⇒ per-pair convergence). No value-flow modelling is needed; this is why it shipped first after Stage 1.

Stage 2b — EGD-aware position-level acyclicity for the create-driven class (future). For the cycles that remain, run a weak-acyclicity / local-stratification check on the underlying TGD/EGD encoding, with MrgAtoms treated as a first-class EGD [@Fagin2005DataExchange; @Greco2011StratificationCriteria; @Calautti2016EGDChaseTermination]. If the cycle is weakly acyclic (no fresh value flows around it), downgrade it from "risk" to "safe." This is the FC5 discriminator: the create→merge cycle is not weakly acyclic because the merge's EGD feeds a fresh organism back into the create rule's antecedent. The same machinery closes the §6.3 soundness gap (existential InsAtom triggering), so 2b is both a precision and a soundness improvement for the create-driven class.

Why this split: the two sub-goals attack different false positives (resp. different missed oscillations) and rest on different theory; 2a is cheap and rule-level, 2b needs value-flow modelling. Conflating them (the earlier framing of "Stage 2 = weak acyclicity") hides that the delete-driven false positives — the bulk of what RAP and SIAM hit — are already addressable without the heavier value-flow machinery.

Stage 3 (optional, research) — Critical-pair confluence and native saturation. For rule sets that pass termination but where order-independence matters, add critical-pair analysis to certify confluence [@Lambers2006ConflictDetection], and use Joosten's graph saturation as the executable reference semantics that defines "triggers" precisely in Ampersand's own relation algebra [@Joosten2018GraphSaturation]. Where neither termination nor confluence can be shown, guardedness-style restrictions indicate which rule shapes remain well-behaved [@Cali2013TamingChase].

What this deliberately is not. It is not a decision procedure — that is impossible [@Joosten2018GraphSaturation; @Deutsch2008ChaseRevisited]. It is a sound over-approximation: "safe" is a guarantee; "risk" is an honest "I cannot rule out an oscillation here, and these are the colliding rules." That is precisely what the guide asks for.

---

5. Conclusions and advice

1. The problem is solved in principle, not by us first. The ExecEngine repair loop is a chase over TGDs (Ins*/NewStruct) and EGDs (MrgAtoms) [@Fagin2005DataExchange; @Onet2013ChaseProcedure], equivalently an active-rule system [@Aiken1995StaticAnalysis; @Paton1999ActiveDB] and a graph-rewriting system [@Lambers2006ConflictDetection; @Joosten2018GraphSaturation]. Each community already offers a data-independent, syntactic termination test. Ampersand can adopt one rather than invent one.

2. Exact prediction is provably out of reach, so aim for a sound over-approximation. The undecidability is established both in Ampersand's own relation algebra [@Joosten2018GraphSaturation] and for the chase [@Deutsch2008ChaseRevisited]. This justifies the guide's framing and sets the realistic target: certify safe soundly, and otherwise emit an explanatory risk.

3. Advice — build it in two shippable stages. Start with the signed, refined rule-level triggering graph (Stage 1): it is cheap, it speaks in rules, and the positive/negative edge labelling already encodes the monotone-vs-non-monotone insight the guide teaches [@Aiken1995StaticAnalysis; @Urban1999RefinedTriggering; @Apt1988DeclarativeKnowledge; @Baralis2000AlgebraicApproach]. Then add the EGD-aware weak-acyclicity check (Stage 2) to prune false positives on exactly the create-vs-merge interaction that caused the FC5 oscillations [@Calautti2016EGDChaseTermination; @Fagin2005DataExchange; @Greco2011StratificationCriteria]. Treat critical-pair confluence and graph saturation as a later research track [@Lambers2006ConflictDetection; @Joosten2018GraphSaturation].

4. Pedagogical bonus. The signed-cycle report is the static twin of the guide's runtime "Rules fixed in last run" message. Shipping it would let Ampersand warn a modeller about an oscillation before a single row is loaded — turning the guide's after-the-fact diagnosis into design-time feedback, which is the stated goal.

---

6. Stage 1 — implementation and validation (2026-06-06)

Stage 1 is implemented in the compiler. This section records what was built, the design decisions taken, and how the result was validated, so that the choices are auditable and Stage 2 can build on them.

6.1 What was built

A new module Ampersand.FSpec.Oscillation computes the signed, refined rule-level triggering graph and emits one compiler warning per risky cycle. It runs inside pCtx2Fspec (in Ampersand.FSpec.ToFSpec.CreateFspec), right after the existing Cartesian-product check, so the analysis runs on every command that builds an FSpec — check, validate, proto. The warning is constructed by mkOscillationWarning in the central CtxError module, alongside the other compiler warnings. The analysis is always on (not gated behind --verbose), because oscillation risk is a design-time concern the modeller should always see.

The graph is built as follows.

• Nodes are the automated rules: the rules maintained by the ExecEngine role (fRoleRuls). Invariants and human-role process rules are excluded, because only the ExecEngine repairs data automatically and can therefore loop.
• Writes per rule. Each rule's VIOLATION repair script is parsed from its PairView by splitting the concatenated text segments on the {EX} marker and then on ;. The function name and the relation/concept names are always literal text in a {EX} instruction (they can never be computed from an expression), so this text-level parse is robust even though the atom-value arguments are expression segments. Each instruction maps to signed writes, following the classification of Stage 0: InsPair → positive write on the named relation; DelPair → negative write; MrgAtoms;C → both a positive and a negative write on every relation on concept C (a merge re-routes pairs: it removes (b,x) and adds (a,x)); DelAtom;C → negative write on every relation on C; InsAtom;C/NewStruct;C → positive writes on the relations on C. "Relations on C" is restricted to the relations actually read by some automated rule, since only those can carry an edge.
• Edges. There is an edge A → B, signed with A's write, whenever a write of A can increase B's set of violations. Which writes can do so is decided by the monotonicity refinement (§6.2). The edge is negative iff the triggering write deletes or merges.
• Risk. The graph's strongly-connected components are computed (Data.Graph). A component is reported iff it is cyclic and contains at least one internal negative edge. A purely positive (insert-only) cycle converges to a least fixpoint by Knaster–Tarski and is deliberately not flagged.

6.2 The monotonicity refinement, and why it is essential

A bare triggering graph — "edge A → B whenever A writes a relation that occurs in B" — flags far too much. The decisive example: a uniqueness rule key;key~ |- I[E] repaired by MrgAtoms;E. The merge writes key, and the rule reads key, so the bare graph draws a negative self-loop and reports every uniqueness rule in every model as an oscillation risk. That is a false alarm: a merge strictly reduces the number of atoms, so it always terminates on its own.

The fix is the refinement that the literature attaches to Stage 1 ("prune edges that cannot actually re-trigger B", §3.1, §4). A rule a |- c is violated by the pairs in a - c, so its violation set grows only when a relation that occurs positively in a - c grows, or one that occurs negatively shrinks. We compute, by a standard polarity walk over the relation-algebra term (composition, union, intersection, Kleene and converse preserve sign; difference flips its right argument; complement flips; residuals and the diamond are treated conservatively as both signs), the set of signs with which each relation occurs in a - c. An insert can re-trigger B only on a relation that occurs positively there; a delete only on one that occurs negatively. In the uniqueness example key occurs only positively in key;key~, so the merge's delete cannot grow the rule's own violations — the self-loop disappears, exactly as it should.

6.3 Design decisions and deliberate deviations

• Soundness target: whole rule expression, not only the antecedent. §2 and §4 phrase the edge as "A writes a relation in B's antecedent". We use B's whole expression (antecedent and consequent), because a repair that shrinks B's consequent also creates a violation of B. Restricting to the antecedent would miss those triggers — a false negative, which requirement (3) forbids. The monotonicity walk already handles antecedent and consequent with the correct signs, so this is the natural sound reading.
• Reporting granularity: strongly-connected components. We report one warning per SCC that contains a negative edge, rather than enumerating elementary cycles. An SCC is exactly the "minimal set of mutually-triggering rules" of requirement (2), it is cheap and deterministic, and every negative edge inside an SCC lies on some cycle. Enumerating individual elementary cycles (finer, but exponential in the worst case) is left for later.
• Atom-level effects modelled through relations. Merge, delete-atom and insert-atom are modelled by their effect on the relations on the concept, which is how oscillations actually propagate (the FC5 loop runs through voorkeursNaam and eppoCode). We do not model the rarer trigger in which the bare existence of a fresh atom violates a rule phrased purely on I[C] or V (e.g. I[C] |- r) without any relation pair changing. InsAtom almost always comes paired with an InsPair that does the real triggering, so this keeps the analysis simple at a small, documented soundness cost. See the open question in §7.
• No --verbose gate. Unlike the Cartesian-product warning, the risk warning is always emitted. It is a design-time signal, not a performance hint.

6.4 Validation

The two guide reproductions and ten purpose-built fixtures probe the analysis. The fixtures live in two sibling directories under testing/oscillation/ whose testinfo.yaml asserts the verdict via the exit code (see the box below): risk/ expects exit 45 (a flagged oscillation), safe/ expects exit 0 (certified convergent).

Script	Automated rules	Expected	Result
docs/guides/oscillations/oscillatie-buggy.adl	maakOrganisme, uniekeCode, uniekeNaam	risk	risk — one SCC of all three, naming the voorkeursNaam/eppoCode collisions
docs/guides/oscillations/oscillatie-fixed.adl	same names, code-driven creation + maakSynoniem	risk (see note)	risk — same SCC
testing/oscillation/risk/insdel-cycle.adl	an InsPair/DelPair pair on one relation	risk (exit 45)	risk — names the light collision
testing/oscillation/risk/create-merge-cycle.adl	an InsAtom create vs a MrgAtoms merge (FC5)	risk (exit 45)	risk — create↔merge SCC
testing/oscillation/safe/mono-cycle.adl	two insert-only rules in a cycle	no risk (exit 0)	silent
testing/oscillation/safe/merge-alone.adl	one MrgAtoms uniqueness rule	no risk (exit 0)	silent
testing/oscillation/safe/delete-only.adl	a delete-only cycle on p/q	no risk (exit 0)	silent (§6.5, refinement a)
testing/oscillation/safe/delatom-cleanup.adl	a DelAtom orphan-cleanup self-cycle	no risk (exit 0)	silent (§6.5, refinement a)
testing/oscillation/safe/functional-maintenance.adl	an R := D pair and a complementary-guard toggle	no risk (exit 0)	silent (§6.5, refinement b)
testing/oscillation/safe/enforce-assignment.adl	a real ENFORCE r := expr statement	no risk (exit 0)	silent (§6.5, refinement b)
testing/oscillation/safe/guarded-maintenance.adl	a deleter guarded by a composition	no risk (exit 0)	silent (§6.5, refinement b)
testing/oscillation/safe/bounded-maintenance.adl	insert-region ⊆ allow-region (not =)	no risk (exit 0)	silent (§6.5, ⊆-extension)

How the regression asserts the verdict. Oscillation findings are warnings, which do not change the exit code, so a plain ampersand check (exit 0 on any warning) cannot tell a flagged script from a silent one. The --fail-on-oscillation flag closes this: when set, a detected oscillation risk exits with the dedicated code 45 (OscillationRiskDetected), while a clean run still exits 0. Each directory's testinfo.yaml runs ampersand check --fail-on-oscillation and asserts the matching code (45 in risk/, 0 in safe/). So a change that silences a real oscillation (a risk/ script dropping to exit 0) or introduces a false positive (a safe/ script rising to exit 45) now fails the regression — the verdict, not just type-checking, is machine-checked. The flag is off by default, so normal use is unaffected.

The two negative cases (mono-cycle, merge-alone) confirm the analysis is not the trivial "flag every cycle": the monotone cycle and the standalone merge rule are both correctly left silent. The insdel-cycle case confirms a genuine non-monotone cycle is caught.

Note on oscillatie-fixed.adl. Stage 1 does flag the fixed script, and this is the correct Stage-1 behaviour rather than a bug. The fix in the guide (code-driven creation) makes the rules terminate for a value-flow reason: after the merge, the code still has an Organisme, so the create rule's antecedent stays empty. A signed rule-level graph cannot see that — voorkeursNaam still occurs negatively in the create rule's consequent, so the merge's delete is, at the rule level, a possible re-trigger. Certifying the fixed script safe is exactly the job of Stage 2 (EGD-aware weak acyclicity), which §4 introduces for precisely this discriminator. Stage 1 honestly reports "I cannot rule out an oscillation here"; Stage 2 will downgrade it to "safe". This matches the staged design and the undecidability result: a sound over-approximation must over-flag, and Stage 2 is where the false positive is removed.

6.5 Stage 2a — a sound convergence certificate for the delete-driven class (2026-06-23)

Two sound refinements were added to Ampersand.FSpec.Oscillation, both pruning false positives before the risk test of §6.1. Each is a sufficient condition for termination, so soundness (no missed oscillation, requirement (3)) is preserved.

Stage 2a, refinement (a) — delete-only components terminate. A strongly-connected component whose rules perform no monotone (insert/grow) write only ever shrinks the population. The state space under set inclusion is finite and the combined repair operator is monotone decreasing, so it reaches a fixpoint by well-founded descent — the exact dual of the Knaster–Tarski argument that §1.4 gives for insert-only cycles. Such a component is no longer flagged, even though every edge in it is negative. (MrgAtoms counts as a positive write, so a component containing a merge is not delete-only and stays subject to the full test.)

Stage 2a, refinement (b) — functionally maintained relations converge. A relation R that is written by at least one inserter and one deleter is functionally maintained when there is a relation-free expression D, invariant within the component (no component rule writes a relation occurring in D), such that every inserter has the form D |- R (so it only ever adds R-pairs inside D) and every deleter allows R exactly on D (so it only ever removes R-pairs outside D; the deleter's guard is irrelevant to soundness). The per-pair argument is decisive: D-pairs are only inserted, ¬D-pairs are only deleted, so no pair is ever both inserted and deleted and R converges. The opposing writes on such an R cannot oscillate, so its triggering edges are pruned. Deleters written in the equivalent disjointness forms a |- I - R and a |- -R are solved to the bounds I - a and -a respectively, so complementary-guard toggles (e.g. visible := I - invisible) are certified as well.

The invariance condition is what keeps genuine recursion flagged: when R's definition D mentions a relation that the same component also rewrites (e.g. SIAM's mutually-defined accPerson/accPersonRef, or the session-role web where allowed and active roles feed each other), D is not invariant, the certificate does not apply, and the risk is reported as before. This is exactly local stratification (§1.4, §3.4): R sits in its own stratum, defined from a lower, invariant one.

Validation. The regression fixtures (§6.4) now assert the verdict via the exit code: risk/ (the insdel and create-merge cycles) must exit 45, safe/ (mono-cycle, merge-alone, delete-only, delatom-cleanup, functional-maintenance, enforce-assignment, guarded-maintenance) must exit 0. All eleven pass. On the RAP4 source the oscillation warnings drop from nine to three: the two genuine mutually-recursive risks (the accPersonRef definition cycle and the session-role web) are still flagged, together with one residual (the Sequence first/last/empty trio, see §7).

Containment, not just equality (2026-06-24). The certificate was generalised from "every bound is the same D" to the weaker, still-sound obligation it actually needs: there is a relation-free, component-invariant D with every inserter's insert-region ⊆ D and every deleter's allow-region ⊇ D. We never materialise D; we check the equivalent pairwise insert-region ⊆ allow-region with a sound, deliberately incomplete syntactic test subExpr (reflexivity; A - X ⊆ A; A ∩ X ⊆ A; A ∪ X ⊆ B iff both; A ⊆ B ∪ X; A ⊆ B;V / V;B and A ⊆ B*/B⁺ since each only grows B; converse congruence). Equality is the special case insert-region = D = allow-region. The ⊆ test additionally certifies bounded maintenance — e.g. the Sequence first/last items, which are set only for a non-empty sequence (itemInSeq - …), a subset of the region the emptiness rule allows (itemInSeq~;V). On the RAP4 source this clears that residual, taking the warnings from nine to two; the two that remain are the genuine mutually-recursive risks (the accPersonRef definition cycle and the session-role web), whose bounds mention a relation the same component rewrites, so invariance fails and they stay flagged — correctly.

What this is still not. It is not the full EGD-aware weak-acyclicity check of §4 (§2b): it reasons about delete-driven convergence, not about freshly invented atoms. The create-driven class (existential InsAtom, the FC5 loop) remains the subject of §2b.

7. Open questions for the next session

0. Containment-based maintenance — done (2026-06-24). The Sequence first/last/empty trio is now certified: the certificate checks insert-region ⊆ allow-region with a sound syntactic subExpr, not just bound equality (see §6.5). Regression fixture safe/bounded-maintenance.adl locks it in. Remaining option: subExpr is intentionally incomplete; add lemmas only as real models demand them, keeping each one provably sound.

1. Bare-atom triggering (the §6.3 soundness gap). Should Stage 1 also model the trigger where a freshly created atom violates a rule phrased on I[C]/V with no relation pair involved? Doing so soundly reintroduces the merge/delete self-loop noise unless handled with care. The pragmatic choice was to leave it to Stage 2 (which tracks atom/value provenance anyway). Confirm this is acceptable, or ask for it in Stage 1.

2. Whether to flag oscillatie-fixed.adl now. Stage 1 flags it (correctly, see §6.4). If that is judged too noisy before Stage 2 lands, an interim option is to lower the fixed-script-style false positives by also requiring the cycle's negative edge to be a merge/delete of a relation the partner rule can re-create — but that starts to anticipate Stage 2. Preference?

3. Severity and gating. The risk is emitted as a normal compiler warning, always on. Should it instead be --verbose-gated (like the Cartesian-product warning), or promoted to something more prominent?

4. Wording and locale. The warning text is English and points to docs/guides/oscillations/README.md. Is that the right destination, and is English right given the FC5 audience?

5. Verdict-level regression — done (2026-06-24). The testing/oscillation/ suite no longer merely type-checks: the --fail-on-oscillation flag (exit code 45) lets the risk/ and safe/ directories assert each fixture's verdict through the exit code (§6.4). A change that silences a real oscillation or introduces a false positive now fails CI. Remaining option: a finer HSpec test on the exposed oscillationWarnings could additionally assert which rules are named in each warning, not just that a warning occurs — useful if the report wording or grouping is ever refactored.

---

References

The in-text citations use symbolic keys of the form [@Key]. The full references follow, ordered alphabetically by key; each ends with a resolvable DOI link. (GitHub and Docusaurus do not render Pandoc/BibTeX-style citations, so this list is maintained by hand. The machine-readable source is literature_search.csv, search id 1.)

• [@Aiken1995StaticAnalysis] Aiken, A., Hellerstein, J.M., Widom, J. (1995). Static analysis techniques for predicting the behavior of active database rules. ACM Transactions on Database Systems 20(1), 3–41. doi:10.1145/202106.202107
• [@Apt1988DeclarativeKnowledge] Apt, K.R., Blair, H.A., Walker, A. (1988). Towards a theory of declarative knowledge. In: Minker, J. (ed.) Foundations of Deductive Databases and Logic Programming, Morgan Kaufmann, pp. 89–148. doi:10.1016/B978-0-934613-40-8.50006-3
• [@Baralis1996Modularization] Baralis, E., Ceri, S., Paraboschi, S. (1996). Modularization techniques for active rules design. ACM Transactions on Database Systems 21(1), 1–29. doi:10.1145/227604.227605
• [@Baralis2000AlgebraicApproach] Baralis, E., Widom, J. (2000). An algebraic approach to static analysis of active database rules. ACM Transactions on Database Systems 25(3), 269–332. doi:10.1145/363951.363954
• [@Calautti2016EGDChaseTermination] Calautti, M., Greco, S., Molinaro, C., Trubitsyna, I. (2016). Exploiting equality generating dependencies in checking chase termination. Proceedings of the VLDB Endowment 9(5), 396–407. doi:10.14778/2876473.2876475
• [@Cali2013TamingChase] Calì, A., Gottlob, G., Kifer, M. (2013). Taming the infinite chase: Query answering under expressive relational constraints. Journal of Artificial Intelligence Research 48, 115–174. doi:10.1613/jair.3873
• [@Couchot2002ImprovingRTG] Couchot, A. (2002). Improving the refined triggering graph method for active rules termination analysis. In: Advances in Databases and Information Systems (ADBIS), LNCS 2435, pp. 191–204. doi:10.1007/3-540-45495-0_16
• [@CuencaGrau2013AcyclicityNotions] Cuenca Grau, B., Horrocks, I., Krötzsch, M., Kupke, C., Magka, D., Motik, B., Wang, Z. (2013). Acyclicity notions for existential rules and their application to query answering in ontologies. Journal of Artificial Intelligence Research 47, 741–808. doi:10.1613/jair.3949
• [@Deutsch2008ChaseRevisited] Deutsch, A., Nash, A., Remmel, J. (2008). The chase revisited. In: Proceedings of PODS 2008, pp. 149–158. doi:10.1145/1376916.1376938
• [@Fagin2005DataExchange] Fagin, R., Kolaitis, P.G., Miller, R.J., Popa, L. (2005). Data exchange: semantics and query answering. Theoretical Computer Science 336(1), 89–124. doi:10.1016/j.tcs.2004.10.033
• [@Greco2011StratificationCriteria] Greco, S., Spezzano, F., Trubitsyna, I. (2011). Stratification criteria and rewriting techniques for checking chase termination. Proceedings of the VLDB Endowment 4(11), 1158–1168. doi:10.14778/3402707.3402750
• [@Joosten2018GraphSaturation] Joosten, S.J.C. (2018). Finding models through graph saturation. Journal of Logical and Algebraic Methods in Programming 100, 98–112. doi:10.1016/j.jlamp.2018.06.005
• [@Lambers2006ConflictDetection] Lambers, L., Ehrig, H., Orejas, F. (2006). Efficient detection of conflicts in graph-based model transformation. Electronic Notes in Theoretical Computer Science 152, 97–109. doi:10.1016/j.entcs.2006.01.017
• [@Marnette2009GeneralizedSchemaMappings] Marnette, B. (2009). Generalized schema-mappings: from termination to tractability. In: Proceedings of PODS 2009, pp. 13–22. doi:10.1145/1559795.1559799
• [@Onet2013ChaseProcedure] Onet, A. (2013). The chase procedure and its applications in data exchange. In: Data Exchange, Integration, and Streams, Dagstuhl Follow-Ups, vol. 5, pp. 1–37. doi:10.4230/DFU.Vol5.10452.1
• [@Paton1999ActiveDB] Paton, N.W., Díaz, O. (1999). Active database systems. ACM Computing Surveys 31(1), 63–103. doi:10.1145/311531.311623
• [@Urban1999RefinedTriggering] Urban, S.D., Tschudi, M.K., Dietrich, S.W., Karadimce, A.P. (1999). Active rule termination analysis: an implementation and evaluation of the refined triggering graph method. Journal of Intelligent Information Systems 12(2–3), 215–243. doi:10.1023/A:1026430919467

Reading copies: the open-access PDF of Joosten2018GraphSaturation, together with the open-access items Cali2013TamingChase, Onet2013ChaseProcedure and CuencaGrau2013AcyclicityNotions, are archived under copies/; the remaining items are retrieved through the OU library (see literature_search/worklist.md).