Derivation

derive

A derive rule defines a relation by a condition instead of by listing its members. The head holds for any binding of the variables that makes the body hold:

senior(p) :- p: Person, p.age >= 65;

senior(p) holds for every Person whose age is at least 65. Two properties take this past a stored view.

A rule may name itself, so a relation can recurse. Transitive closure is the canonical case — reachability over a directed graph, computed from a base case and a recursive step:

reach(x, y) :- edge(x, y);
reach(x, z) :- reach(x, y), edge(y, z);

The first rule is the base case: a direct edge is reachable. The second recurses — if x reaches y and an edge runs from y to z, then x reaches z. Rules with the same head and arity combine by union, so the two clauses together define reach as “a direct edge, or one edge past something already reachable.” Over the chain a → b → c → d the closure is the six reachable pairs, including the three the base edges never state. This is the computation plain SQL joins cannot express and recursive SQL strains to.

A rule body may also negate — not P — and may quantify, compare, and aggregate. Every body must be range-restricted: each variable in the head, in a negated atom, or in a comparison must be bound by some positive atom in the body. An unbound variable would project nothing meaningful, so an unsafe rule is refused at build (OE1303) rather than silently producing a wrong answer.

The stratified fixpoint

A set of derive rules computes by a fixpoint, and the substrate proves both that it terminates and that the answer is unique. The engine tracks, for each predicate and individual, a three-valued status — is, not, or can (unknown) — starting with everything can and filling in the other two. Rules fall into three internal categories the modeler never writes but whose separation explains the guarantee:

• Positive rules only ever turn can into is.
• Negation rules — those using not — read a finished positive result and turn can into not.
• Constraint rules observe and emit diagnostics; they change no status.

Predicates are sorted into strata by their dependencies. Within a stratum the engine runs every positive rule to a fixpoint, then applies negation once against that completed result, then moves up. Termination follows from monotonicity: positive work only adds is, negation only adds not, and doing all the positive work before any negation keeps the two from contradicting each other. The count of remaining can values strictly decreases, so the process halts in a bounded number of steps with one answer. The Rust engine runs this as a semi-naive evaluator.

Recursion through negation

Stratification handles negation that crosses between strata — one predicate’s negation reading another, already-finished one. Negation inside a cycle it cannot: p :- not q together with q :- not p has no stratified answer, because whichever rule runs first decides the result. Argon does not reject such a program. It falls to well-founded semantics — the Van Gelder–Ross–Schlipf alternating fixpoint — under which a paradoxical atom comes out undefined: neither asserted nor denied. An undefined atom does not fire.

This is not a corner case to be tolerated; it is how arbitration is modeled. Argon by Example schedules a robot’s plan in robot_plan_execution, where two conflicting actions cannot both run. An action is scheduled when it is applicable and not challenged; an action is challenged when a conflicting action is itself scheduled. So scheduled recurses through its own negation by way of challenged — exactly the win-move game on the conflict graph — and the two predicates form one negation-cyclic component the engine evaluates by well-founded semantics. An asymmetric conflict, where one action has priority, resolves to a definite winner: the uncontested action is scheduled and its rival is challenged and absent. A symmetric conflict, two actions deadlocked with no tiebreak, is undefined under the well-founded model — both are absent from scheduled and from challenged, the observable signature of a standoff.

The well-founded model is three-valued; the current surface is two-valued. The engine materializes the definitely-true extent, the sound projection for conditional obligations. Surfacing undefined as a distinct query result is a later increment, which the reference tracks under derive. A second semantics, stable models behind a #[brave] attribute, is designed but not built — writing the attribute refuses loudly today rather than parsing green and doing nothing.

Bounded universals and aggregates

A rule can demand that every element of a domain satisfy a condition. forall f: Fluent where pre(a, f), holds(f) holds for an action a exactly when every precondition of a holds initially — the genuine universal, not “some precondition holds.” It lowers to a count-equality: the number of preconditions that hold equals the number of preconditions, so an empty domain is vacuously true. The reference gives the encoding under derive.

A body can also count and compare. exists { Person(p) } is the bare Boolean form, true when the body has any solution at all. count { Person(p) } >= 3 binds a cardinality and filters on it. The comprehension forms — sum, min, max, avg, and count with a projection — also run in derive and query bodies, and because an aggregate is a bindable expression, two of them can be compared directly. Argon by Example classifies a workforce by cardinality in aggregate_count_v0 and totals ledger postings in double_entry_v0.