Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

derive

derive-decl ::= attribute* 'pub'? 'derive' Ident '(' param-list ')'
                  ( ':-' atom-list )? ';'
atom-list   ::= atom (',' atom)*
atom        ::= predicate-call | comparison | type-test | 'not' atom | path-pattern

pub derive ancestor(d: Person, a: Person) :- ParentOf(d, a);
pub derive ancestor(d: Person, a: Person) :- ParentOf(d, p), ancestor(p, a);
pub derive senior(p: Person) :- p: Person, p.age >= 65;

// Ground-fact form (no body, concrete args): the head holds for the named terms.
pub derive iof(Type, Type);                                    // MLT* OL3
pub derive Within(usc26, usc);                                 // seed a derived predicate

Multiple derives with matching head name and arity compose as Datalog union (modulo the stratification check below). not atom is NAF, evaluated under well-founded semantics. A derive with no :- clause is bodiless, and its head arguments decide its reading:

  • Concrete arguments → a ground fact. When every head argument is a concrete term — a declared individual (Within(usc26, usc)), an enum constant, an axis value, or a type reference (iof(Type, Type)) — the bodiless derive declares that tuple as a ground fact, equivalent to :- true. This is the sanctioned way to seed ground tuples directly on a derived predicate: the seed tuples union with the head’s other derive clauses and rules over the same relation node (same name, same arity), so a recursive rule reads them and computes their closure (seeds ∪ derived-closure). A non-concrete (free-variable) argument is the error — a bodiless derive has no body to range-restrict it — and is refused with OE1342, the bodiless analogue of OE1303 (below), naming the offending argument and directing you to declare the individual or add a :- … body.
  • Type-annotated parameters → an empty predicate. A bodiless head whose arguments are typed parameters (pub derive adult(p: Person);) introduces the predicate with that signature and an initially empty extent — the introduce-empty idiom (Rule-atom grammar). Its rows arrive from later same-head derive clauses.

Every body-carrying rule must be range-restricted (safe): each variable in the head, in a negated (NAF) atom, or in a comparison/compute operand is bound by some positive body atom; an unsafe rule is refused at compile (OE1303), since an unbound variable would silently project Null or mis-evaluate.

Evaluation model. A derive program denotes the tuples its rules derive, under the semantics fixed in Reasoning: the least fixpoint of the positive program, stratified negation layered along the axis dependency graph, and — for a negation cycle no stratification can layer — the well-founded model computed by the alternating fixpoint. The surface consequences a rule author relies on:

  • Recursion through negation is accepted. A negation cycle (p :- not q, q :- not p) that strict stratification cannot layer is evaluated under well-founded semantics rather than refused. Cross-stratum, acyclic NAF is ordinary stratified negation. (OE1309 no longer fires from stratification; it survives only as the dispatch seam.)
  • Two-valued query surface. WFS is three-valued (true / false / undefined), but the engine materializes only the definitely-true extent — a paradoxical atom resolves to undefined and does not fire. A rule whose conclusion is genuinely undecided neither fires nor is denied.
  • #[brave] / stable-model semantics is out of scope (Out of scope).

Parametric (axis-generic) rules. A derive rule may be generic over a set of axes; the elaborator monomorphizes it to a finite set of concrete rules at elaboration, with no change to fixpoint semantics.

Stratified aggregates. Aggregate atoms (count, sum, max, min, avg, set_collect, …; see query) are admitted inside derive bodies when the aggregated predicate sits at a strictly lower stratum than the rule head, where the stratification dimension is a well-founded relation (typically the iof DAG, the specialization lattice, or an explicit user-declared ordering). The classic library use case is computing a derived level function over iof:

pub derive has_order(t: Entity, n: Nat) :-
    n == 1 + max { select m from t': Entity, m: Nat
                   where iof(t', t), has_order(t', m) };

The stratifier accepts this because the inner max aggregates has_order over iof-predecessors of t, and iof is well-founded. Stratified aggregates that would loop through an aggregation step on the same stratum are rejected with OE0510 NonStratifiedAggregate.

Universals over recursive predicates. A common composite pattern — a conjunction is fulfilled iff all of its children are — is a universal over the very predicate being defined:

pub derive Fulfilled(p: Conjunction, t: Instant) :-
    Instant(t), forall c: PC where childOf(p, c), Fulfilled(c, t);

This form is refused (OE1317 RecursionThroughAggregation): the forall lowers to the count-equality aggregate (Rule-atom grammar), and stratified-aggregate semantics (Faber–Pfeifer–Leone) require the aggregated predicate in a strictly-lower stratum — here Fulfilled aggregates over itself, so its SCC crosses an aggregate boundary and has no stratification. No intermediate derive helps: recursion depth follows the data (the part-whole tree), so any helper joins the same cycle. The supported phrasing is negation-as-failure double negation — ∀c.F(c) rewritten as ¬∃c.¬F(c):

pub derive HasUnfulfilledChild(p: Conjunction, t: Instant) :-
    childOf(p, c), Instant(t), not Fulfilled(c, t);
pub derive Fulfilled(p: Conjunction, t: Instant) :-
    Conjunction(p), Instant(t), not HasUnfulfilledChild(p, t);

This converts recursion-through-aggregation into recursion-through-negation, which the well-founded executor evaluates. On two-valued-total data — every child’s Fulfilled status resolves to true or false, as it does over a finite acyclic part-whole tree of leaves with definite status — the double negation derives exactly the universal’s extent, bottom-up through the tree. The honest caveat: where a child’s status is genuinely undefined under WFS, the double-negation form propagates undefined to the parent rather than guessing either way — and the two-valued surface omits undefined atoms, per the projection rule under well-founded semantics. Admitting the forall form directly (structural stratification over a provably well-founded relation) is tracked in issue #185.

Worked example — double-entry accounting (RFD 0029). Derived values and aggregate-as-term together make quantitative domains authorable. The double-entry invariant — within every journal entry, total debits equal total credits — is a check comparing two aggregates; the per-account balance is a derived value, grouped per account (the outer bound variable). The running package is examples/double_entry_v0.

pub type Account { mut name: String, }
pub type Entry   { mut memo: String, }
pub type Posting { mut amount: Decimal, mut side: String, }   // side = "D" | "C"
pub rel postedTo(posting: Posting, account: Account);
pub rel inEntry(posting: Posting, entry: Entry);

// Per-account balance = Σ debits − Σ credits, grouped per `acct`.
pub derive accountBalance(acct, bal) :- acct: Account,
    debits  = sum(p.amount for p in Posting, postedTo(p, acct), p.side == "D"),
    credits = sum(p.amount for p in Posting, postedTo(p, acct), p.side == "C"),
    bal     = debits - credits;

// The double-entry invariant — two aggregates compared, per entry.
pub check EntryNotBalanced(e: Entry) :- e: Entry,
    debits  = sum(p.amount for p in Posting, inEntry(p, e), p.side == "D"),
    credits = sum(p.amount for p in Posting, inEntry(p, e), p.side == "C"),
    debits != credits
    => Diagnostic {
        severity: Severity::Error,
        code:     "Ledger::E001",
        message:  "journal entry is not balanced — total debits must equal total credits",
    };

// A sales-tax line, rounded to cents with banker's rounding (the money default).
pub derive accountTax(acct, tax) :- acct: Account,
    debits = sum(p.amount for p in Posting, postedTo(p, acct), p.side == "D"),
    tax    = round_half_even(debits * 0.075, 2);

Every amount is an exact Decimal: sum folds rationals (no rounding), the balance subtraction is exact, and round_half_even rounds to cents exactly — 150.75 * 0.075 = 11.30625 rounds to 11.31, never an f64 artifact. The EntryNotBalanced check is an instance-level Error, so at runtime it is a delta guard: a mutation that would leave an entry unbalanced is rejected atomically (double-entry is enforced, not merely reported).

Rule-atom grammar

Bodies of derive, query from clauses, check, and unsafe logic blocks are conjunctive sequences of rule atoms. The atom shapes:

rule-body ::= rule-atom (',' rule-atom)*
rule-atom ::=
    // Negation as failure
      'not' rule-atom
    | 'not' '(' rule-atom (',' rule-atom)* ')'
    // Modal (tier:modal)
    | 'box' '(' rule-atom ')'
    | 'diamond' '(' rule-atom ')'
    // Restriction quantifiers — DL ∀R.C / ∃R.C  (tier:expressive)
    | 'forall' '(' field-path ',' type-expr ')'
    | 'exists' '(' field-path ',' type-expr ')'
    // FOL binding quantifiers — admitted at tier:fol (inside unsafe logic)
    | 'forall' Ident ':' type-expr 'where' rule-body
    | 'exists' Ident ':' type-expr 'where' rule-body
    // Aggregate as atom, optionally compared (paren form, Expression grammar)
    | aggregate (comp-op expr)?
    // Subquery as atom, optionally compared (brace form, `query`)
    | subquery (comp-op expr)?
    // Reflection
    | meta-call (comp-op expr)?
    | path '::' Ident                                // sugar for meta(path) == Ident
    // Predicate call with optional outcome / comparison suffix
    | path '(' rule-arg (',' rule-arg)* ')'
        ('is' outcome-suffix | comp-op expr)?
    // Role invocation with closure (+ = transitive, * = reflexive-transitive)
    | field-path ('+'|'*') '(' Ident (':' type-expr)? ')'
    | field-path '(' Ident (':' type-expr)? ')'
    // Type test and `is` sugar
    | field-path ':' type-expr
    | field-path 'is' ('not'? 'unknown' | type-expr | Ident)
    // Specialization
    | field-path '<:' field-path
    // Binding — single `=`, distinct from the comparison `==` (RFD 0029)
    | Ident '=' expr
    // Comparison — RHS is a full expression (Expression grammar)
    | field-path comp-op expr
    // Membership — RHS is a full expression (set, list, or range)
    | field-path 'not'? 'in' expr
    // Bare-path Boolean test
    | field-path

field-path     ::= Ident ('.' name)*
rule-arg       ::= expr | expr comp-op expr
outcome-suffix ::= 'not'? ('ambiguous'|'unknown'|'timeout') ('(' Ident ')')?

Binding atoms (x = expr, RFD 0029). A rule body may bind a fresh variable to the value of an expression: x = expr (single =) is assignment, distinct from the comparison x == e (double =, a filter). expr ranges over bound variables, literals, field projections (t.income), exact arithmetic over the numeric tower, the rounding builtins (Expression grammar), and aggregate expressions. This is the established Datalog/Soufflé assignment concept and is what lets a rule head carry a derived value:

pub derive Tax(t, owed) :- appliesTo(b, t), owed = t.income * b.rate;

The binding introduces a fresh variable, and is range-restricted. Two distinct refusal paths, never a silent Null:

  • Freshness (OE1335 BindingLhsAlreadyBound). The left-hand side x must be a new name. If x is already bound — by a prior positive predicate atom, a head parameter bound elsewhere, a projection, an aggregate result, or an earlier binding — the = would silently degrade into an equality filter (x joined against the computed value) rather than a binding. It is refused, naming x, with the directed hint: use == to compare, or pick a fresh name. This is the path a rebind x = x + 1 takes when x is otherwise bound (e.g. by a body predicate) — the LHS is not fresh.
  • Range restriction (OE1303 RuleNotRangeRestricted). x = expr binds x positively iff every variable in expr is itself positively bound. An unbound right-hand-side variable, or a pure self-reference / cycle among binding atoms where the result variable is bound by nothing else (x = x + 1 as the only binder of x; x = y, y = x), leaves x unbound under the binding fixpoint and is refused as unsafe.

So x = x + 1 refuses either way — via OE1335 when x is already bound elsewhere (freshness), or via OE1303 when x has no other binder (range restriction) — and the two codes name the two genuinely different errors.

Aggregates as bindable terms (RFD 0029). Because an aggregate is a bindable expression, comparing two aggregates — the double-entry sum(debits) == sum(credits) invariant — is simply binding each and comparing the bound variables:

pub derive balanced(e) :- e: Entry,
    debits  = sum(p.amount for p in Posting, inEntry(p, e), p.side == "D"),
    credits = sum(p.amount for p in Posting, inEntry(p, e), p.side == "C"),
    debits == credits;

The aggregate source extends the comprehension form: after for x in Source, a comma-separated list of additional body atoms (relation atoms, comparisons, type tests) refines the fold’s domain, and variables from the outer rule body are visible inside. That visibility is the grouping — the group key is the set of outer bound variables free in the aggregate, the standard Datalog reading. pub derive balance(acct, s) :- acct: Account, s = sum(p.amount for p in Posting, postedTo(p, acct)); groups per acct. A binding is not a comprehension trailing-atom form — sum(w for u in T, …, w = u.v) is refused with OE1336 BindingInComprehension, which directs you to project the value into the fold directly (sum(u.v for u in T, …)) or to bind in the outer rule body and aggregate the bound variable. The brace form (sum { … }) stays count/exists-only; a value aggregate in brace form is refused with OE1331 ValueAggregateBraceForm, which directs to the comprehension form. The SQL-ish group by … having is not built; it refuses with OE0007 carrying the binding-form rewrite. (Aggregates evaluate over the definitely-true extent: an aggregate folding over a relation with well-founded-undefined atoms is refused at runtime with OE1332 AggregateOverUndefined rather than silently treating undefined as false. The refusal is whole-relation, not per-group; three-valued aggregate intervals are tracked under issue #250.)

Empty-group semantics — a deliberate split. When a group is empty (the fold sees no rows), the aggregators divide by role:

  • sum, count, count_distinct emit a value for the empty group — 0. An additive/cardinality fold has a well-defined identity (the empty sum is zero, the empty count is zero), so the grouped row is produced with that identity value.
  • min, max, avg drop the row — they have no value over an empty set (there is no least/greatest element, and the mean is 0/0), so no grouped row is produced for an empty group rather than fabricating one.

This split is load-bearing for the double-entry invariant. sum(debits) == sum(credits) must catch an entry that has credits but no debits: because sum emits 0 for the empty debit side, the comparison is 0 == credits, which fails and flags the entry as unbalanced. Were sum to drop the empty group, the row would vanish and the imbalance would pass silently. The examples/double_entry_v0 package relies on exactly this behavior.

Conjunction between atoms uses ,. NAF uses the not keyword. Disjunction is not inline — write separate derive rules with the same head and arity; the union composes structurally. The same-head idiom is derive-only: a check head carries payload identity (its => Diagnostic { severity, code, message } report, its guard classification, its violation relation), so two checks sharing one head would cross-talk and are refused at elaboration (OE1328 DuplicateCheckHead) — rename one check, or express the disjunction through a shared derive predicate whose same-head clauses union, read by a single check. (Trait check members are unaffected: each impl’s monomorphized member rule is qualified by its impl target and keeps a distinct head, Trait atom.) The RHS of comparison atoms is a full expression (Expression grammar); inside that expression context, && / || / ! apply normally.

Payloadless enum constants. In value position, a path of the form EnumName::VariantName denotes the canonical enum value when the variant has no payload. This is distinct from the standalone rule atom sugar path :: Ident above, which means meta(path) == Ident. Payload-carrying variants require constructor semantics and are not constants by themselves.

Predicate resolution. The head of every predicate-call atom (path '(' … ')') must resolve to a declared predicate in scope — a rel, a concept used as a classification predicate, a derive / query head, a trait rule member (qualified Trait::member(...), or bare when exactly one provider is in lexical scope; subject to the coverage gate, Resolution), a pub fact / pub not_fact predicate, a fn, or a reflection intrinsic (iof, specializes, meta, extent, implements). check heads are not consumable: checks are observers only (Purity ladder) — their violation sets never populate the IDB — so a body atom resolving to a check head (module-level or trait check member) is refused with OE1329 CheckHeadConsumed; derive from the underlying body predicates instead (factor the violation pattern into a pub derive head read by both the check and the consuming rule). This applies to the predicate atoms of derive and check bodies and to both the body and head atoms of bridge rules (Bridge rules). An unresolved head is OE0223 RuleReferencesUnknownPredicate, the rule-body analogue of the pub fact obligation OE0220 (RFD 0004). A resolved atom is further checked for arity (OE0225) and — where both the argument’s type and the declared parameter type are concretely known — argument type (OE0226, sound under multiple classification: it fires only on provable disjointness). This is independent of the world assumption: the world assumption governs the truth value of instances of a declared predicate (under the CWA default an unasserted instance is false; under an #[world(open)] concept it is unknown/Can, World assumptions (CWA / OWA)) — it never admits an undeclared predicate name. To introduce a predicate that is intentionally empty until populated, declare it (pub rel P(...), or a bodiless pub derive P(...); head). ox check enforces this, and ox build refuses to emit an artifact for a program containing an unresolved predicate.

pub fact targets a base predicate, never a derived one. A derive / query head is a valid rule-body atom (it is in the resolution set above), but it is not a valid pub fact target. pub fact asserts into an extensional relation (a concept-as-classification or a pub rel); a derived predicate’s extent is intensional — computed by rule derivation. A pub fact P(...) whose P is a pub derive / pub query head is refused with OE0239 FactReferencesDerivedPredicate: the asserted seed tuple would key a different relation node than the rule head reads, so it would silently drop out of the rule’s fixpoint — the derive would evaluate to a result that omits the asserted tuples (no error, wrong answer). To give a derived predicate ground tuples that participate in its derivation, use one of two sanctioned forms, and OE0239’s help names both:

  • A bodiless pub derive P(args); clause over concrete arguments (derive). The seed tuple is itself a derive clause on P, so it shares P’s relation node and participates directly in P’s fixpoint — the simplest way to seed P itself.
  • A base relation the rule reads — declare pub rel Base(...), seed it with pub fact Base(...), and add a clause pub derive P(...) :- Base(...). Use this when the seed tuples are themselves a reusable extensional predicate.

Either keeps P a single-origin intensional head (the same rule Build pipeline and .oxbin enforces for a foreign-placed-vs-derived relation, OE1246). (A pub fact over a check head is the ordinary OE0220 — a check head is observer-only, not a predicate at all.)

Build loud-gate. More broadly, ox build refuses (writing no .oxbin) any derive / query rule the engine does not evaluate — an unsupported quantifier shape, a nested or non-count-class aggregate, not <aggregate>, an unsupported type-test or meta-eq (OE1311–OE1315). Argon refuses rather than emit an artifact that would silently mis-derive; see Build pipeline and .oxbin.

Modal atoms (box(...), diamond(...)) carry Kripke-frame semantics over the standpoint and classification frames described in Modal operators. The elaborator statically discharges the common case (type-classification atoms whose target is introduced by a fixed metatype — membership constant, RFD 0027 D6) and routes the remainder to a modal reasoner over std::kripke. Modal atoms are admitted only at tier:modal; lower tiers reject them.

Restricted universals (forall v: T where Body, Head). In the where body the last atom is the consequent (Head) and all preceding atoms are the domain restriction (Body). The quantifier holds iff every domain element also satisfies the consequent — it lowers to the count-equality count{ v : Body, Head } == count{ v : Body } (the domain-and-consequent count equals the domain count). The type annotation T is the static sort of v; the runtime domain comes from the where Body, so the Body must restrict v with a membership or predicate atom (e.g. member(g, v) or v in g.items) — Body, not T, bounds the count. An empty domain (count{ v : Body } == 0) makes the universal vacuously true (0 == 0), deriving the head — classical restricted-∀ semantics. The encoding needs at least a domain atom and a consequent (≥2 where atoms); the paren restriction form forall(path, T), the exists-binder form, and a single-atom where refuse with OE1315 (App. C).

Allen interval relations (before, meets, overlaps, during, starts, finishes, and their reciprocals) are not substrate operators. They are provided by the std::allen library (RFD 0024), defined over the Date / Duration value layer (Temporal substrate) — ordinary predicates over interval endpoints, not parser-level syntax.

Three atom shapes in the grammar above parse-refuse rather than silently mis-derive:

  • Role closure field-path ('+'|'*') '(' … ')' (e.g. p.knows+(q: Person)). The base role-invocation form field-path '(' Ident (':' type-expr)? ')' is accepted; the transitive (+) / reflexive-transitive (*) closure suffix refuses with OE0001. Express transitive reachability through a recursive derive head.
  • Axis sugar path '::' Ident (x :: T, i.e. meta(x) == T). Write the meta(x) == T comparison atom directly; the :: rule-atom shorthand refuses. (In value position EnumName::Variant is unaffected — see the payloadless-enum-constant note above.)
  • Range membership field-path 'not'? 'in' <range> (p.v in 1..10). The set/list RHS of in is accepted; a lo..hi range RHS refuses (OE0001 on ..). Write the two-sided comparison p.v >= 1, p.v <= 10 instead.

Temporal rule atoms

Argon’s bitemporal substrate (Temporal substrate) admits metric temporal operators in rule bodies — the DatalogMTL fragment with stratified negation over the integer timeline.

Any atom may be qualified by a valid-time point or interval: atom at t (a single VT point), atom during [t1, t2] (a closed VT interval), atom since t (the open interval [t, ∞]).

Six prefix metric operators address past and future. Their interval bounds are durations (0, N with a unit ns…y, or inf/∞):

box_minus     [a, b] (φ)         // φ held at every past point in [a, b]
diamond_minus [a, b] (φ)         // φ held at some past point in [a, b]
box_plus      [a, b] (φ)         // φ holds at every future point in [a, b]
diamond_plus  [a, b] (φ)         // φ holds at some future point in [a, b]
since         [a, b] (φ, ψ)      // φ has held since ψ within [a, b]
until         [a, b] (φ, ψ)      // φ holds until ψ within [a, b]

Two shortcuts expand to [0, ∞] intervals: ever atom (some past or future point; needs tier: expressive for the disjunction) and always atom (every point; tier: recursive).

Side-by-side modal (box/diamond) and metric temporal atoms in one body compose additively. Nesting one family inside the other is refused at tier: recursive and routed to tier: fol — see Tier ladder for the decidability rule (OE0712).