Recursion under a live defeat plane

Area: Defeasible reasoning Teaches: a recursive rule (transitive closure) still computes its full fixpoint when the module also carries a defeat plane — the defeasibility transform attributes each clause’s contribution over the converged support, so a recursive clause sees its own prior tuples. Prerequisites: lex specialis, and recursive derive rules (transitive closure). Run: ox build examples/defeasible_recursion_v0 && ox derive examples/defeasible_recursion_v0 reach

The presence of a single #[default]/#[defeats] pair anywhere in a module switches its entire evaluation onto the Governatori defeasibility transform rather than the classical Datalog fast path. A recursive rule must keep working under that transform. This example pins that property: a transitive closure, evaluated next to an unrelated defeat plane, must still be whole.

What to read in graph.ar

A standard recursive transitive closure over a 3-edge chain a → b → c → d:

pub derive reach(x: Node, y: Node) :- edge(x, y);
pub derive reach(x: Node, z: Node) :- reach(x, y), edge(y, z);

The recursive clause feeds on its own prior output — (a,c) needs (a,b) and (b,c) to already be in reach.

An unrelated defeat plane — a #[default] head attacked by a #[defeats] edge — on a different predicate entirely. Its only job here is to make has_defeat_plane() true so the whole module evaluates through the defeasibility transform:

#[default]
#[label(presumed)]
pub derive flagged(n: Node) :- Node(n);

#[defeats(flagged(n))]
pub derive cleared(n) :- edge(n, n);

cleared requires a self-loop edge(n, n); the chain has none, so the defeat never actually fires. It exists purely to activate the transform that the recursive closure must survive.

Running it

The graph is shipped as pub fact data (no mutations), so the runner is ox derive … reach rather than a scenario. Over a → b → c → d the closure is the six reachable pairs:

derive(reach): 6 tuple(s)
  (a,b) (a,c) (a,d)
  (b,c) (b,d)
  (c,d)

The transitive pairs (a,c), (b,d), (a,d) are exactly the ones the recursive clause derives from reach’s own prior tuples — the contributions a naive per-clause defeat attribution would drop if it cleared the head before attributing support. Six tuples, not three: the closure is whole under the live defeat plane.

This example is compiled and run in CI; the full six-pair closure under the defeat plane is pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs), so a regression in the defeasibility transform breaks the build rather than silently under-deriving.

Source

The package’s real Argon source, transcluded from the files this corpus compiles — what you read here is exactly what CI builds.

root.ar

//! Recursion under a live defeat plane (RFD 0028 — the F1 regression).
//!
//! A self-recursive `#[default]`-bearing module must still compute the
//! full transitive closure. The defeasibility transform attributes each
//! clause's contribution over the CONVERGED support catalog — never a
//! cleared head — so a recursive clause sees its own prior tuples and
//! transitive closure does not silently under-derive.

mod graph;

graph.ar

//! Transitive closure of a 3-edge chain (a→b→c→d), evaluated inside a
//! module that carries a live defeat plane.
//!
//! The chain: edge(a,b), edge(b,c), edge(c,d).
//!
//! `reach` is the standard recursive transitive closure:
//!     reach(x, y) :- edge(x, y);                       // base
//!     reach(x, z) :- reach(x, y), edge(y, z);          // recursive step
//!
//! Over a→b→c→d the closure is the six pairs
//!     {(a,b),(b,c),(c,d),(a,c),(b,d),(a,d)}.
//!
//! The defeat plane below (a `#[default]` clause attacked by a
//! `#[defeats]` edge, on an unrelated head) makes `has_defeat_plane()`
//! true, so `reach` is evaluated through the Governatori compilation
//! transform rather than the classical fast path. The F1 bug cleared
//! the head before per-clause attribution, dropping every transitive
//! pair the recursive clause needed its own prior tuples to derive
//! (it returned only {(a,b),(b,c),(c,d)} with no diagnostic). The fix
//! attributes per clause over the converged support catalog, so the
//! recursive clause derives (a,c),(b,d),(a,d) and the closure is whole.

pub type Node {}

pub rel edge(x: Node, y: Node);

// The graph: a → b → c → d.
pub fact Node(a)
pub fact Node(b)
pub fact Node(c)
pub fact Node(d)

pub fact edge(a, b)
pub fact edge(b, c)
pub fact edge(c, d)

// Transitive closure — the recursive head under test.
// ANCHOR: reach
pub derive reach(x: Node, y: Node) :- edge(x, y);
pub derive reach(x: Node, z: Node) :- reach(x, y), edge(y, z);
// ANCHOR_END: reach
// ── The live defeat plane (unrelated to `reach`) ──────────────────
// A standalone `#[default]` head attacked by a `#[defeats]` edge. This
// activates the defeasibility transform for the whole module so `reach`
// is evaluated through it — the path the F1 bug corrupted.
// ANCHOR: defeat
#[default]
#[label (presumed)]
pub derive flagged(n: Node) :- Node(n);

#[defeats (flagged(n))]
pub derive cleared(n) :- edge(n, n);
// ANCHOR_END: defeat
pub query closure() -> reach;