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.