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.)
  • Four-valued query surface. WFS is three-valued (true / false / undefined). The engine materializes the definitely-true extent as the head’s rows — a paradoxical atom resolves to undefined and does not fire downstream rules — and the head’s undefined tuples surface on the query/derive read as Can rows, by default (drop-but-count under the opt-in K3 projection; see the envelope contract under well-founded semantics). A rule whose conclusion is genuinely undecided neither fires nor is denied — and the read says so (Can) instead of omitting it.
  • #[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 surface reports the parent as a Can row rather than omitting it, per the four-valued 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 ')')?

The truth qualifier R(arguments) is unknown selects R’s well-founded-undefined tuples. These are tuples left neither definitely true nor definitely false by a recursion-through-negation component (Truth values). The component must finish first: the stratifier places the consumer in a higher stratum and then reads R’s undefined companion. A consumer that feeds back into R’s component is refused with OE1441, because it would inspect an incomplete result. Move that consumer into a separate pub derive that does not feed back into R. is not unknown, payload-binding is unknown(x), and path-headed x is unknown also refuse with OE1441; only a predicate call identifies the companion, and a complement requires an explicit finite domain. The multi-valued suffixes is both(a, b) / is ambiguous(a) / is timeout(a) remain the separate OE1349 refusal. This qualifier does not classify ordinary open-world absence; it reads only the WFS companion materialized by evaluation.

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.)

The value aggregates are numeric folds (RFD 0016): sum / avg / min / max lift every projected value into the exact-rational domain — min / max included, so no orderable-but-non-numeric projection (a Date, a String) is admissible either. A projection whose declared type is statically non-numeric — a temporal value, a String, a Bool, an entity or structured value — refuses at ox check / ox build with OE1433 AggregateProjectionNotNumeric, naming the projection expression, its type, and the fold’s numeric domain; a non-numeric value that reaches the fold only dynamically raises the same OE1433 loudly at runtime. count folds cardinality and admits any projection.

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). Entity-typed positions additionally carry a declared-sort discipline (OE1432 RuleAtomArgSortMismatch): a logic variable whose declared sort — its head-parameter annotation, a body sort guard x : T, or a unary concept-membership atom T(x) — is <:-incomparable with the position’s declared parameter concept is refused. This is deliberately not a disjointness proof (multiple classification can still make the join non-empty at runtime); it is the signature-level discipline: an atom whose declared sorts are incomparable can only succeed through a multi-classification the program never states, and in practice compiles to a silently-empty join. Both <: directions pass (a subtype in a supertype slot is subsumption; a supertype in a subtype slot narrows, exactly as an x : T occurrence-typing test narrows), and asserting the second sort in the body (x : T or T(x)) licenses the atom. A predicate declared in several clauses — one per admissible sort — licenses an argument comparable with any clause’s parameter concept at that position, and a clause leaving the position unannotated admits anything there. Sorts a variable merely picks up by occupying other predicates’ argument slots are classification evidence, not declarations, and never trigger the refusal. 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.

Relation-value application. A rule-body variable whose value is proven to range over a finite, exhaustive set of declared relations may itself stand in predicate position — r(p, c) where r is such a variable. The proof comes from the same body: a specializes(r, Parent) atom pins r to the Parent specialization family (relations are first-class citizens of the <: graph, so specializes ranges over declared relations exactly as it ranges over concepts); an equality with a relation literal (r == Home) pins a singleton; rel/arm reflection atoms pin by metarel or endpoint signature. The application lowers to a static dispatch over the proven candidate set — reading the dispatch at selector r equals applying the concrete relation r names.

If you only want the union of a relation family, do not use this — query the parent relation directly. Every subrelation’s tuples flow into each ancestor relation’s extent by declared subsumption (the RFD 0005 closure, materialized at seeding). A rule body naming Loc already ranges over Home, Work, and any member added later, with no dispatch and no domain proof. Relation-value application earns its cost only when the parent query would erase information you need — see the cases below.

pub type Person;
pub type City;

pub rel Loc(p: Person, c: City);
pub rel Home(p: Person, c: City) <: Loc;
pub rel Work(p: Person, c: City) <: Loc;

// UNION — no relation-value application. `Home` and `Work` tuples flow
// into `Loc` by subsumption, so the parent query already unions them.
pub derive anyLoc(p: Person, c: City) :- Loc(p, c);

The motivating case is provenance: you need to know which member of the family a tuple came from. The parent query collapses the family to one relation and erases that; a relation-valued selector keeps it, because specializes(kind, IncomeItem) binds kind to each member and kind(p, a) reads the tuple through it — so kind stands in the output as which relation each row was declared in, kept as a value.

pub type Person;

pub rel IncomeItem(mut p: Person, amount: Int);
pub rel Wages(mut p: Person, amount: Int)    <: IncomeItem;
pub rel Interest(mut p: Person, amount: Int) <: IncomeItem;

pub fact Person(alice);
pub fact Person(bob);
pub fact Wages(alice, 50000);
pub fact Interest(alice, 1200);
pub fact Wages(bob, 30000);

// PROVENANCE — `kind` is a relation-valued output column.
pub derive report(p: Person, kind, a: Int) :-
    specializes(kind, IncomeItem), kind(p, a);

// UNION — the plain parent query; same rows, no `kind` column.
pub derive total(p: Person, a: Int) :- IncomeItem(p, a);

Read what the selector is, row by row. Built as a standalone file and queried with ox derive, report produces (verbatim):

derive(report): 6 tuple(s)
  (#i7582462787275748164, <anonymous>::IncomeItem, 1200)
  (#i7582462787275748164, <anonymous>::IncomeItem, 50000)
  (#i7582462787275748164, <anonymous>::Interest, 1200)
  (#i7582462787275748164, <anonymous>::Wages, 50000)
  (#i8648907253816210642, <anonymous>::IncomeItem, 30000)
  (#i8648907253816210642, <anonymous>::Wages, 30000)

The first column is the Person identity, printed as its stable content-addressed handle — #i7582… is alice, #i8648… is bob. The middle column is the relation each row was declared in — Wages, Interest, IncomeItem are relation values, not strings (a standalone file elaborates its relations under <anonymous>, so a member prints <anonymous>::Wages; inside a multi-module package it is the module path, e.g. model::Wages). Every concrete row also appears under IncomeItem itself: specializes is reflexive (a relation is a kind of itself) and the RFD 0005 closure copies each child tuple up into the parent’s extent, so the family selector legitimately witnesses both the leaf and the ancestor. The plain parent query total produces the same underlying rows without the category column — (#i7582…, 1200), (#i7582…, 50000), (#i8648…, 30000) — and nothing downstream can recover which member each came from once the union has merged them. That recovery is the entire reason to apply a relation-valued selector instead of naming the parent.

For one row per concrete member — dropping the reflexive parent witnesses — exclude the parent in the body (kind != IncomeItem narrows the proven domain; the specializes atom still supplies it, so the finite-domain proof holds):

pub type Person;

pub rel IncomeItem(mut p: Person, amount: Int);
pub rel Wages(mut p: Person, amount: Int)    <: IncomeItem;
pub rel Interest(mut p: Person, amount: Int) <: IncomeItem;

pub fact Person(alice);
pub fact Wages(alice, 50000);
pub fact Interest(alice, 1200);

// Leaf-only provenance: exclude the reflexive parent witness.
pub derive reportLeaf(p: Person, kind, a: Int) :-
    specializes(kind, IncomeItem), kind != IncomeItem, kind(p, a);

reportLeaf drops the IncomeItem rows, leaving one (p, kind, a) per concrete member — (#i7582…, <anonymous>::Interest, 1200), (#i7582…, <anonymous>::Wages, 50000) (again #i7582… is alice).

The generalized family query — each row once, by construction

The kind != IncomeItem idiom above is a workaround for a specific over-return: the bare specializes(kind, IncomeItem), kind(p, a) reads every candidate’s closed extent, and the parent’s closed extent already holds a copy of every member’s tuples (the RFD 0005 closure), so each concrete row surfaces twice — once under its declaring member, once under the reflexive parent. The canonical family query — the via sugar — names the family in one atom and reads each member’s own extent, so every row is returned once, under its declaring relation, by construction — no exclusion idiom, no dedup.

via is the spelling you write; it desugars to a generalized specializes atom that is the same query written out:

Parent( args ) via k   ≡   specializes( k( _… ) , Parent( args ) )

Each example below is shown as a pair — the via form and the equivalent generalized specializes form — with one shared meaning and one shared output; the two spellings produce byte-identical rows (a differential test pins this end to end). Every block parses on this branch; every output is ox build + ox derive, verbatim. The shared fixture:

pub type Person;

pub rel IncomeItem(mut p: Person, amount: Int);
pub rel Wages(mut p: Person, amount: Int)    <: IncomeItem;
pub rel Interest(mut p: Person, amount: Int) <: IncomeItem;

pub fact Person(alice);
pub fact Person(bob);
pub fact Wages(alice, 50000);
pub fact Interest(alice, 1200);
pub fact Wages(bob, 30000);
// A tuple asserted DIRECTLY on the parent relation — it arrives under
// `kind = IncomeItem`, not under any leaf member.
pub fact IncomeItem(alice, 500);

// A second family: engagements between an audit firm and its clients.
pub type Firm;
pub type Company;
pub rel Engagement(firm: Firm, client: Company);
pub rel AuditEngagement(firm: Firm, client: Company)      <: Engagement(firm = firm, client = client);
pub rel ConsultingEngagement(firm: Firm, client: Company) <: Engagement(firm = firm, client = client);
pub fact Firm(deloitte);
pub fact Firm(kpmg);
pub fact Company(acme);
pub fact Company(beta);
// deloitte both audits AND consults for acme; kpmg only audits beta.
pub fact AuditEngagement(deloitte, acme);
pub fact ConsultingEngagement(deloitte, acme);
pub fact AuditEngagement(kpmg, beta);

// ── Provenance: for each income row, also give me the relation it was
//    declared in. `via` (canonical) and its generalized form are one query.
pub derive report_via(p: Person, kind, a: Int) :-
    IncomeItem(p, a) via kind;
pub derive report_gen(p: Person, kind, a: Int) :-
    specializes(kind(p, a), IncomeItem(p, a));

// ── Guard as meaning: the same rows, but exclude tuples asserted directly
//    on the parent relation itself.
pub derive leaf_via(p: Person, kind, a: Int) :-
    IncomeItem(p, a) via kind, kind != IncomeItem;
pub derive leaf_gen(p: Person, kind, a: Int) :-
    specializes(kind(p, a), IncomeItem(p, a)), kind != IncomeItem;

// ── Multi-witness, witnesses DIFFER: the same firm serves the same client
//    under two different engagement categories — a firm may not both audit
//    and consult for one client (auditor independence).
pub derive independence_via(firm: Firm, client: Company) :-
    Engagement(firm, client) via k1, Engagement(firm, client) via k2, k1 != k2;
pub derive independence_gen(firm: Firm, client: Company) :-
    specializes(k1(firm, client), Engagement(firm, client)),
    specializes(k2(firm, client), Engagement(firm, client)), k1 != k2;

// ── Multi-witness, witness JOINS: two different people with income of the
//    SAME category — the witness `kind` is an ordinary join variable, shared
//    across both atoms rather than compared unequal.
pub derive sameCategory_via(p1: Person, p2: Person, kind) :-
    IncomeItem(p1, a1) via kind, IncomeItem(p2, a2) via kind, p1 != p2;
pub derive sameCategory_gen(p1: Person, p2: Person, kind) :-
    specializes(kind(p1, a1), IncomeItem(p1, a1)),
    specializes(kind(p2, a2), IncomeItem(p2, a2)), p1 != p2;

Provenance — for each income row, also give me the relation it was declared in. report_via and report_gen return the same rows: each family tuple exactly once — the three leaf rows and the directly-asserted parent row, under IncomeItem:

derive(report_via): 4 tuple(s)      # report_gen is byte-identical
  (#i7582462787275748164, <anonymous>::IncomeItem, 500)
  (#i7582462787275748164, <anonymous>::Interest, 1200)
  (#i7582462787275748164, <anonymous>::Wages, 50000)
  (#i8648907253816210642, <anonymous>::Wages, 30000)

Guard as meaning — the same, but only rows declared on a leaf member. leaf_via and leaf_gen add kind != IncomeItem and both drop the directly-asserted parent row:

derive(leaf_via): 3 tuple(s)        # leaf_gen is byte-identical
  (#i7582462787275748164, <anonymous>::Interest, 1200)
  (#i7582462787275748164, <anonymous>::Wages, 50000)
  (#i8648907253816210642, <anonymous>::Wages, 30000)

Note what the guard now means. Under the old bare closed-extent read, kind != IncomeItem corrected an artifact — it discarded the reflexive duplicate rows the closure copied up into the parent. Under the own-extent read those duplicates never exist, so the same guard now states a choice: exclude facts asserted directly on the parent relation (they arrive with kind = IncomeItem) and keep only the leaf members. Under the old read the guard corrected an artifact; under the family query it states a meaning — report includes the IncomeItem, 500 row, leaf excludes it.

Multi-witness, witnesses differ — the same firm serves the same client under two DIFFERENT engagement categories — a firm may not both audit and consult for one client. independence_via and independence_gen bind two witnesses over the same firm/client pair and require them distinct; only deloitte/acme qualifies (both audit and consult), kpmg/beta has one engagement kind:

derive(independence_via): 1 tuple(s)   # independence_gen is byte-identical
  (#i7895632145248339177, #i1312706375208229289)

The two handles are deloitte and acme. The parent query cannot express this. Engagement(f, c), Engagement(f, c) is the same union self-joined on itself — it holds whenever the firm has any engagement with the client, and two audit engagements alone would satisfy it. Only the witness distinguishes the categories: k1 != k2 demands two rows from different declaring relations, which is exactly “audit and also consult”.

The independence rule needs a proper-member guard when the parent carries direct facts. via is reflexive: a tuple asserted directly on Engagement arrives in the parent’s own extent with witness = Engagement. The fixture above has no direct-parent engagements, so its output is exact — but on a schema where firms are also recorded through a bare Engagement fact, a firm/client with one real member engagement plus a direct parent fact carries two distinct witnesses (Engagement and the member), and the rule above spuriously flags it though only one real engagement category exists. Add the same “exclude direct parent assertions” guard the reportLeaf example uses — k1 != Engagement, k2 != Engagement — so only genuine member categories count:

pub derive independence_unguarded(firm: Firm, client: Company) :-
    Engagement(firm, client) via k1, Engagement(firm, client) via k2, k1 != k2;
pub derive independence_guarded(firm: Firm, client: Company) :-
    Engagement(firm, client) via k1, Engagement(firm, client) via k2,
    k1 != k2, k1 != Engagement, k2 != Engagement;

With AuditEngagement(kpmg, beta) and a direct Engagement(kpmg, beta), the unguarded rule returns two rows — the genuine deloitte/acme and the spurious kpmg/beta — while the guarded rule returns only the genuine pair:

derive(independence_unguarded): 2 tuple(s)
derive(independence_guarded): 1 tuple(s)

Multi-witness, witness joins — two different people with income of the SAME category. Here the witness is an ordinary join variable — kind is shared across both atoms, not compared unequal. sameCategory_via and sameCategory_gen return the person pairs sharing a category (alice and bob both have Wages; each ordering appears once):

derive(sameCategory_via): 2 tuple(s)   # sameCategory_gen is byte-identical
  (#i7582462787275748164, #i8648907253816210642, <anonymous>::Wages)
  (#i8648907253816210642, #i7582462787275748164, <anonymous>::Wages)

The identity handles: #i7582… is alice, #i8648… is bob; the witness column is the relation each row was declared in, kept as a value (a standalone file elaborates under <anonymous>).

The legacy bare form, for contrast. The pre-existing two-argument specializes(kind, IncomeItem), kind(p, a) reads every candidate’s closed extent — so the parent’s closure copies surface alongside the members, returning each leaf row twice and the direct parent tuples once, seven rows for this fixture:

derive(report_bare): 7 tuple(s)
  (#i7582462787275748164, <anonymous>::IncomeItem, 500)
  (#i7582462787275748164, <anonymous>::IncomeItem, 1200)
  (#i7582462787275748164, <anonymous>::IncomeItem, 50000)
  (#i7582462787275748164, <anonymous>::Interest, 1200)
  (#i7582462787275748164, <anonymous>::Wages, 50000)
  (#i8648907253816210642, <anonymous>::IncomeItem, 30000)
  (#i8648907253816210642, <anonymous>::Wages, 30000)

This is the behavior the via / generalized own-extent form replaces: the three tiers are the bare two-argument form (legacy, closed extents, duplicates), the via sugar (canonical, own extents, each row once), and the generalized specializes form (via’s meaning, written out — identical rows).

Why the member frame is not a user spelling. The generalized specializes(k(memberArgs), Parent(parentArgs)) atom bounds k to the family, applies k in its own argument frame, and constrains the tuple in the parent’s frame; for an identity family the two frames have the same width, shared variables thread a column through both, and the correspondence is the declared subsumption mapping, never visual column position. The parent frame is information-complete — the mapping rules forbid dropped child ends, so every value a member carries is available in the parent frame. A member frame therefore binds nothing the parent frame does not already bind, which is why via plus the parent atom expresses every practical family query and the generalized form appears only as via’s desugar. The member frame becomes independently expressive only if subsumption mappings that drop a child’s ends are ever admitted — an open design question — at which point the general form is already specified and via remains its all-wildcard special case.

Rule of thumb. The parent atom alone is the union; + via k is the union plus which one; the generalized specializes(k(...), Parent(...)) form is the meaning of via, written out.

The via sugar reaches mapped members too — a member joined by a non-identity (argument-mapped) edge, whether a rename, a constant pin, or a subsort cast. A via family query reads such a member’s own extent and presents the rows in the parent’s frame, with the pinned / renamed / cast ends filled by the mapping and the answering member bound to the witness. The generalized specializes form with an explicit member frame still refuses (OE1416) for a non-identity member: that form ties the member frame positionally to the member’s own ends, which is sound only for an equal-arity identity member — it points the modeler at via, which is frame-agnostic. The witness member position must be a plain variable (OE1415 otherwise); the member frame’s width must match the parent’s arity (OE1414) and the parent frame’s width must match the parent relation’s declared arity (OE1418). A via k clause on an explicit specializes(...) atom is a misuse — via is itself the sugar for a specializes query — and refuses with OE1419; write one spelling or the other, not both.

A mapped family reads cleanly through via. With WagesUSA(p, a) <: IncomeItem(p, a, c = USD) (a constant pin), an incomeSource view over the parent family binds each row’s currency through the pin and its witness through the edge — no member-frame spelling, no dispatch:

use std::core::{type, rel};
pub type Person;
pub type Currency;
pub const USD: Currency;
pub rel IncomeItem(mut p: Person, mut amount: Int, mut c: Currency);
pub rel WagesUSA(mut p: Person, mut amount: Int) <: IncomeItem(p = p, amount = amount, c = USD);

pub fact Person(alice);
pub fact Currency(USD);
pub fact WagesUSA(alice, 500);

// Reads the mapped member through φ: `c` is filled by the pin, `kind` by the edge.
pub derive incomeSource(p: Person, a: Int, c: Currency, kind) :- IncomeItem(p, a, c) via kind;

incomeSource(alice, 500, USD, WagesUSA)

The USD came from the pin (the member never stores it), and kind is WagesUSA — the member that answered.

Don’t-care ends in a family query — the anonymous wildcard _. A parent frame does not have to bind every end. When you only want which member answered — not the amount, not the currency — write _ for each end you don’t care about. This is the natural query for provenance: “who has income, and from which kind of source?” ignores the figures entirely. The wildcard is a genuine don’t-care in the family-query frame, one anonymous slot per _, so an all-_-but-one frame is not mistaken for a lower-arity query.

The fixture carries a pinned member (WagesUSA, currency pinned to USD) and an identity member (ForeignIncome, currency passed through):

use std::core::{type, rel};
pub type Person;
pub type Currency;
pub const USD: Currency;
pub const EUR: Currency;
pub rel IncomeItem(mut p: Person, mut amount: Int, mut c: Currency);
pub rel WagesUSA(mut p: Person, mut amount: Int) <: IncomeItem(p = p, amount = amount, c = USD);
pub rel ForeignIncome(mut p: Person, mut amount: Int, mut c: Currency) <: IncomeItem(p = p, amount = amount, c = c);

pub fact Person(alice);
pub fact Person(bob);
pub fact Currency(USD);
pub fact Currency(EUR);
pub fact WagesUSA(alice, 500);
pub fact ForeignIncome(bob, 300, EUR);

// Who has income, and from which kind? Amount and currency are don't-cares.
pub derive whoHasIncome(p, kind) :- IncomeItem(p, _, _) via kind;
// Keep the amount, still ignore the (pinned or passed-through) currency.
pub derive amountAndKind(p, a, kind) :- IncomeItem(p, a, _) via kind;

whoHasIncome drops both figure ends and returns one row per person with the answering member — alice earns WagesUSA, bob earns ForeignIncome:

derive(whoHasIncome): 2 tuple(s)
  (#i7582462787275748164, <anonymous>::WagesUSA)
  (#i8648907253816210642, <anonymous>::ForeignIncome)

amountAndKind keeps the amount and still ignores the currency — useful precisely because the currency is pinned on WagesUSA (the member never stores it) and passed through on ForeignIncome; a single _ reads across both shapes without naming a column that one member fills by a pin and the other by an end:

derive(amountAndKind): 2 tuple(s)
  (#i7582462787275748164, 500, <anonymous>::WagesUSA)
  (#i8648907253816210642, 300, <anonymous>::ForeignIncome)

#i7582… is alice, #i8648… is bob. The wildcard behaves the same in a via family query as in a plain parent atom: it matches any value and binds nothing.

A subsumption edge may not drop a child end — use a derive view instead. A mapping must reference every declared child end (a rename or a cast source; a child end may feed several parent ends — a diagonal — but never none). Dropping one is refused at the declaration with OE1421:

use std::core::{type, rel};
pub type Person;
pub type Currency;
pub type Text;
pub const USD: Currency;
pub rel IncomeItem(mut p: Person, mut amount: Int, mut c: Currency);
pub rel Bad(mut p: Person, mut amount: Int, mut note: Text) <: IncomeItem(p = p, amount = amount, c = USD);
//                                          ^ OE1421 — child end `note` is referenced by no filler

OE1421: subsumption of `Bad` onto `IncomeItem` drops child end `note` — dropping an end inside a subsumption edge would merge distinct `Bad` facts (differing only at `note`) into one `IncomeItem` row, so it is refused. Fix, in order: (1) if `Bad` genuinely belongs to the `IncomeItem` family, reference every child end in the filler list (a rename or a cast source; a diagonal may reference one child end at several parent ends); (2) if a lossy projection is intended, write a derive rule instead — a projection VIEW is not family membership, e.g. `pub derive view(p, a) :- Bad(p, a, _);`

Why every child end must be referenced (φ-injectivity). The mapping φ translates each child tuple to a parent image. A dropped end makes φ non-injective: two child tuples that differ only at the dropped end collapse to the same parent image with no declared meaning for the collapse, and — because a relation’s extent is a set — merge into one parent row that any aggregate over the family then counts once. Worse, the §D4 withdrawal cascade relies on the child identity the dropped end carried — a distinction the collapse erases at the parent image, so the cascade can no longer tell the two child tuples apart. Requiring every child end (each fed to at least one parent end) keeps φ injective on the distinct-child-tuple part of the domain, which is exactly what family membership must preserve. A diagonal is still injective: reusing one child end at several parent ends duplicates a value into the image but discards nothing.

The derive view is the honest spelling of a lossy projection. The OE1421 remedy — pub derive view(p, a) :- Bad(p, a, _); — is a rule, not a family edge, so it is explicit that it forgets note and is not Bad’s membership in a family. It also makes the merge visible where it happens: two Bad facts that agree on (p, a) and differ only in note project to one view row.

use std::core::{type, rel};
pub type Person;
pub type Text;
pub rel Bad(mut p: Person, mut amount: Int, mut note: Text);

pub fact Person(alice);
pub fact Text(memoA);
pub fact Text(memoB);
pub fact Bad(alice, 500, memoA);
pub fact Bad(alice, 500, memoB);

pub derive view(p: Person, a: Int) :- Bad(p, a, _);

view(alice, 500)

One row, not two — the two notes are projected away by the derive, exactly the merge a dropped-end edge would have performed silently. A dedicated projection marker on a subsumption edge (a surface way to declare “this edge intentionally forgets an end”) is a reserved design under consideration in the mapped-relation-subsumption design record and is not yet a surface form; until it lands, the derive view is the spelling.

Multiplicity is a schema choice, and aggregates read it. The merge above is the same set-membership rule an aggregate obeys: whether a family sum double-counts two payments is decided by the schema, not the query. A relation Payment(mut p: Person, mut amount: Int) with two facts Payment(alice, 500) twice holds one proposition and sums to 500; add a distinguishing source end — Payment(mut p: Person, mut amount: Int, mut src: Source) with s1/s2 — and the two payments are distinct rows summing to 1000. This is the same trap the relations chapter draws out for family images; the fix is identical (keep a distinguishing end, do not pin it away). Grouping such an aggregate by the family witness is not yet expressible: a via clause is not admitted inside an aggregate comprehension, and threading the witness through an intermediate derive trips the finite-domain proof on the selector column — so per-witness totals are computed today by aggregating each leaf member directly, not by grouping a parent-family sum on kind.

Two clarifications on the selector. kind is an ordinary rule variable, not a keyword — name it anything (r, src, which). And it takes no type annotation: like every rule variable its type is inferred from where it stands — appearing as the family member in specializes(kind, IncomeItem) constrains it to that family, the compiler establishes the complete closed set of member relations at build time (the finite-domain proof; a selector it cannot pin to a finite exhaustive set is refused with OE1386, below), and refuses the rule if it cannot.

Two further cases need the selector in body position, not the head. Per-member differentiated logic — the same selector applied twice, or joined against a per-member table, so the rule branches on which relation matched (specializes(kind, Loc), kind(p, c), priority(kind, n)). Families not modeled by subsumption — members collected by a rel/arm/meta reflection atom (a shared metarel or endpoint signature) rather than a <: edge, where no single parent relation exists to query. A pinned singleton (r == Home) reads exactly one relation’s tuples and is the degenerate case of the same dispatch:

pub type Person;
pub type City;

pub rel Home(p: Person, c: City);

// Singleton: equality with the relation literal `Home` pins `r`, so
// the application reads exactly `Home`'s tuples.
pub derive homed(p: Person, c: City) :- r == Home, r(p, c);

The candidate set must be statically proven — Argon refuses rather than guess a domain or evaluate an open dispatch. A selector bound only by a constraint that proves no finite exhaustive set (an inequality binds r as a value variable but enumerates nothing) is refused with OE1386:

pub type Person;
pub type City;

pub rel Loc(p: Person, c: City);

// `r != Loc` binds `r` but proves no finite exhaustive relation domain.
pub derive anywhere(p: Person, c: City) :- r != Loc, r(p, c);

A value proven not to denote a relation (pinned to an Int, a String, a struct value, …) applied in predicate position is refused with OE1387:

pub type Person;
pub type City;

pub rel Loc(p: Person, c: City);

// `r` is pinned to the integer 3 — not a relation value.
pub derive anywhere(p: Person, c: City) :- r == 3, r(p, c);

A negated relation-value application must be safe: the selector and every tuple argument must be positively range-restricted outside the negation. An argument (or the selector) bound only inside the not is refused with OE1391:

pub type Person;
pub type City;

pub rel Loc(p: Person, c: City);
pub rel Home(p: Person, c: City) <: Loc;

// `c` appears ONLY inside the negation — the negated dispatch is unsafe.
pub derive unhoused(p: Person) :- p : Person, specializes(r, Loc), not r(p, c);

The remaining refusals in the family are structural, and each guards against a silent misderivation the dispatch would otherwise produce:

  • An application whose argument count matches no candidate’s arity is OE1388. With the wrong tuple width there is no coherent pairing of arguments to a candidate’s columns, so a dispatch built anyway would read misaligned columns (or an always-empty relation) — a wrong answer, not an error.
  • An argument category-incompatible with a candidate’s declared endpoint is OE1389 (e.g. a text literal against an Int column). Such a candidate can never match the tuple; dispatching over it would either drop rows the modeler expected or force a type-incoherent join, again silently.
  • A family containing a relation not lexically accessible from the applying module is OE1390. A dispatch that silently dropped the inaccessible candidate would change the rule’s meaning based on visibility — the family it reads would depend on who is looking, so the whole application is refused rather than narrowed.
  • A candidate whose signature metadata (arity, endpoints, visibility) is unavailable to the build — a relation carried by an artifact too old to record it — is OE1393. The dispatch cannot be proven sound without that metadata, so Argon refuses rather than guess it (App. C).

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).