Rules and Reasoning

Rules are where Argon stops looking like Rust and starts looking like its own thing. A rule says “whenever this body is true, this head holds.” The compiler turns rules into reasoning — given some facts, it derives more facts mechanically, with provenance for every conclusion.

This chapter teaches the rule grammar, the assertion variant, the three-engine reasoning pipeline, and a first look at the decidability tier ladder (Chapter 5.3 covers it in depth). References to kind / role / phase throughout the chapter are UFO metatypes — user-declared on top of Argon’s substrate per Chapter 2.1, not built-in keywords.

A first rule

pub derive ActiveLease(l: Lease) :-
    l: Lease,
    l.start_date <= today(),
    l.end_date > today()

Read in English: “for any Lease l, ActiveLease(l) holds when l’s start date has passed and its end date has not.” Whenever the engine has a Lease instance, it checks the body; if every atom holds, it derives ActiveLease(l) as a new fact.

Five things to notice:

1. derive introduces a rule item. The head is ActiveLease(l: Lease). The body follows :-.
2. The body is a conjunction. Each atom must hold for the rule to fire. The separator between atoms is , — there is no && and no and keyword inside a body.
3. Head parameters bind bare names. l in the head and body refers to the same binding. The first body atom (l: Lease) gives l its type; subsequent atoms reuse the binding. The ? prefix is reserved for body-fresh variables — those introduced by an aggregate’s iteration clause or a query’s body when no head parameter is in scope. Head parameters never carry ?.
4. <= and > are comparison operators, not subtype operators. We will meet specializes later for subtype tests.
5. today() is a context-supplied date function intended to return the date for the current evaluation context. It is referentially transparent for any given query — calling the same query at the same wall-clock instant should produce the same result. Status: the call parses and elaborates today, but a registered runtime evaluator is on the roadmap; in the current toolchain expressions involving today() are accepted by ox check and ox build but evaluation against a real wall clock is not yet wired. Use a Date literal (#2026-06-15#) when you need a concrete value to test against today.

Type-check it:

$ ox check
ox lease-tutorial v0.1.0 (./ox.toml)
ox 11 modules resolved from entry point
OI0804 ... derive rule `ActiveLease` classified at Tier 3 (value predicates)
check passed

The OI0804 info diagnostic is the tier classifier reporting where this rule landed on the seven-tier ladder. Three is the highest of the executable tiers — comparisons over value-typed fields put us in QF-LIA territory.

Body atoms — the small vocabulary

A rule body is a comma-separated list of rule atoms. Argon admits roughly a dozen atom shapes; in practice, most rules use four or five.

Type test

l: Lease

“l is a Lease.” Narrows l to instances of Lease (or a subtype). When you want to narrow further, use a more specific type:

l: ResidentialLease

The narrowing is sound — the compiler tracks that subsequent atoms see l at the narrower type. This is occurrence typing; the soundness result is stated in Chapter 5.1.

Comparison

l.end_date > today()
p.age >= 18
n == 0

The comparison operators are ==, !=, <, <=, >, >=. They lift to rule-atom position naturally; both sides can be expressions over bound variables and constants.

Status note: comparison operand-type rule. Today’s elaborator does not type-check comparison operands against each other — p.age < "twenty" where p.age: Int and the right side is a String literal is accepted silently. The operand-type rule for comparison atoms is part of the upcoming Appendix B operator audit (“Reserved for the second edition”). Tracked at sharpe-dev/orca-mvp#412.

Predicate call

HasName(p)
ActiveLease(l)

Calls a derive head as an atom. If the call’s arguments unify with a derived fact, the atom holds. This is how rules compose: one rule’s head is another rule’s body.

Negation

not Expired(l)

“There is no derivation of Expired(l).” Argon uses negation as failure under stratified semantics (Apt, Blair & Walker, Towards a Theory of Declarative Knowledge, 1988); the engine refuses to compile cyclic negation (OE0501).

Aggregate

count(t for t in lease.tenants where t: ActiveTenant) >= 1
sum(p.amount for p in payments where p.month == #2026-01-01#)

Five aggregate functions: sum, count, min, max, avg. The for ... in path clause binds the iteration variable; where atom filters per row. The result is an expression you can compare against a constant.

Status note: aggregate carrier-type rule. The carrier-type rule for sum, min, max, avg (count is intrinsically type-agnostic — it counts witnesses regardless of type) is part of the upcoming Appendix B operator audit. Today’s elaborator does not reject sum(e.note for e in entries) where e.note: String; tracked at sharpe-dev/orca-mvp#412.

The atom families above cover the everyday surface. Five more atom shapes round out the rule-body grammar; each gets its full treatment in Chapter 5, but a short example here makes them concrete. Every example below has a matching workspace under argon/examples/_catalog/ you can cd into and run.

Advanced atoms — a brief tour

Modal — box(...) necessity, diamond(...) possibility. box(<atom>) reads “in every accessible Kripke world, this atom holds”; diamond(<atom>) is its possibility dual. Both wrap any rule-body atom (type tests, comparisons, predicate calls, even other modal atoms). Today’s elaborator accepts both and preserves the wrapper in the IR; the planned tier:modal semantics evaluates them per-world. See Chapter 5.4.

pub derive BoxedPerson(p: Person) :-
    box(p: Person)

Variants: _catalog/rule-modal-box/{minimal,composition,idiom}/, _catalog/rule-modal-diamond/{minimal,composition,idiom}/.

Allen interval relations. Argon admits the thirteen Allen relations (Allen 1983) as binary infix operators between interval-shaped values: before, after, meets, met_by, overlaps, overlapped_by, during, contains, starts, started_by, finishes, finished_by, equals. Each operator classifies the rule at tier:temporal (Tier 4); execution backed by DatalogMTL is on the roadmap.

pub derive Precedes(x: E, y: E) :-
    x: E, y: E,
    x.interval before y.interval

Variants: _catalog/rule-allen-relations/ — the multi-allen variant exercises all thirteen operators in one workspace; the idiom variant shows the canonical “no-double-booking” temporal-invariant pattern.

Quantifiers — forall and exists binding forms. Binding-form quantifiers introduce a fresh-bound variable and lift the rule to tier:fol. They live inside unsafe logic { ... } blocks and require a @[budget] annotation for fairness once tier-6 execution lands.

unsafe logic {
    @[budget(heartbeats: 1000)]
    pub derive SomeLeaseHasEmptyId() :-
        exists l: Lease where l.id == ""
}

Description-Logic-style bounded restrictions (exists(path, Type), forall(path, Type)) classify at lower tiers and don’t need unsafe logic; see Chapter 5.3. Variants: _catalog/rule-quant-{exists,forall}/.

Hypothetical reasoning — hypothetical { ... } blocks. A hypothetical { ... } block declares a counterfactual scenario: a forked knowledge state in which axioms get overridden, the reasoner re-saturates, and ox check --reason reports the diff against the baseline.

let alice: Person = { id: "alice", salary: 100000 }

pub hypothetical alice_double_salary {
    let alice.salary: Int = 200000
}

Plain ox check only confirms the block parses and elaborates; the reasoner-side fork lands at ox check --reason time. Variants: _catalog/hypothetical-block/{minimal,composition-with-derive,idiom}/.

Reflection — meta() and the is-family. meta(X) returns X’s metatype as a value; the intrinsic lowers to a CoreRuleAtom::Meta and surfaces one of the IS-facts the meta-property calculus’s Stratum 0 propagates from each declaration’s metatype profile (Chapter 5.1).

pub derive person_is_kind(p: Person) :-
    p: Person,
    meta(p) == kind

The Person :: kind form is sugar for meta(Person) == kind. The companion is-family of pattern shapes (is unknown, is ambiguous(x), is timeout(x)) handles Argon’s three-valued query outcomes at match-arm level — Chapter 3.1. Variants: _catalog/rule-meta-coloncolon/, _catalog/rule-is-reasoning-outcome/.

A worked derivation

Before running the engine on the lease tutorial, walk through what the saturator does step by step. Suppose the knowledge base contains one Lease fact:

Lease(id="lease-001", start_date=2026-01-01, end_date=2027-01-01,
      tenant=alice, landlord=bob, property=p1, monthly_rent=9500)

and the rule

pub derive ActiveLease(l: Lease) :-
    l: Lease,
    l.start_date <= today(),
    l.end_date > today()

Today’s date is 2026-06-15. The engine performs forward-chaining saturation:

The engine stops at iteration 2: nothing new is derivable. The set of derived facts is the least fixed point of the rule’s immediate-consequence operator over the input facts. This is the standard fixed-point construction from Datalog; the result is unique and independent of the order in which the engine considered candidate bindings.

Why-provenance traces the result back: ActiveLease(lease-001) was derived by the rule ActiveLease/1 from the input fact Lease(lease-001, …) at the body’s three satisfied atoms. ox query active_leases --explain prints this tree.

Multiple bodies, one head

Two rules with the same head form a disjunction: the head holds if any of the bodies fires.

pub derive ExpiredLease(l: Lease) :-
    l: Lease,
    l.end_date <= today()

pub derive ExpiredLease(l: Lease) :-
    l: Lease,
    Terminated(l)

A lease is ExpiredLease if its end date has passed or if it has been explicitly terminated. The compiler treats the two rules as a single Datalog disjunction at the engine level. The provenance you get back when querying tells you which body fired.

Asserts — invariants

A rule with derive produces facts. An assert declares an invariant: a body that, if it ever fires, signals a violation.

assert positive_rent(l: Lease) :-
    l: Lease,
    l.monthly_rent <= 0
    => error("monthly_rent must be positive")

Three differences from derive:

1. The body is the violation condition. The body fires exactly when something is wrong. Read the rule above as “if a Lease exists with non-positive monthly_rent, that is the bad case.”
2. The consequence is mandatory. => error("…") — no optional consequence. The string is the error message.
3. No pub. Asserts are module-scope invariants, not exported.

Migration note: the team is exploring unifying assert and derive under a single rule shape with explicit event consequences (=> Error(...), => Warn(...), => FactDerived(...)). Today’s assert keyword stays the idiomatic form; the unified shape will land additively. See Appendix D.

Optional consequences on derive

A derive rule can carry a non-default consequence:

pub derive borderline_case(c: Case) :-
    c: Case,
    c.confidence < 0.7
    => flag_for_review("low confidence", c.id)

The escalate consequence sends a structured event to a human reviewer rather than tagging the case for asynchronous review:

pub derive low_confidence_decision(d: Decision) :-
    d: Decision,
    d.confidence < 0.5,
    not d.override_recorded
    => escalate("low-confidence decision", d.id, d.confidence)

Variants: _catalog/derive-escalate-consequence/ (minimal, composition-with-assert, idiom) and _catalog/derive-flag-for-review-consequence/ (same shapes).

The four consequence forms today:

Most rules use the implicit form. The explicit forms are for when the head’s purpose is communication or fallback, not just fact derivation.

Migration note: the consequence forms above are being unified with the assert mechanism into a single event-typed => Event(...) system, so that escalate, flag_for_review, error, and warn become user-defined event types rather than keyword forms. The semantics stay; the surface tightens. See Appendix D.

Running the reasoner

ox check does not invoke the reasoner by default. It type-checks and runs the meta-property calculus, but full saturation is opt-in:

$ ox check --reason
ox lease-tutorial v0.1.0 (./ox.toml)
   Reasoning over 4 rules + 2 asserts...
   2 derivations
check passed

The trade-off is speed: type-check is sub-100ms; reasoning takes longer because it actually saturates the rule set. You typically run ox check in editor-loop mode and ox check --reason before commits or releases.

To actually evaluate a query against a populated knowledge base:

$ ox query active_leases
   1 result.
   Lease(id="lease-001", tenant=Tenant(id="t-1"), …)

ox query --explain adds the why-tree — the chain of facts and rule firings that produced each result.

The three-engine pipeline

Argon’s reasoner is not a single algorithm. Three engines tune themselves to different rule types:

• Nous+ saturation — for tier:structural classification: subsumption, role hierarchies, partition. The Baader-style structural saturator (Baader et al., Pushing the EL Envelope, IJCAI 2005) lives in crates/nous. One implementation; two drivers — oxc::reason runs it at compile time, the Kernel runs it at runtime against the same evaluator.
• DataFrog — for tier:closure through tier:recursive: derive rules, asserts, stratified negation, disjunction (Apt, Blair & Walker 1988). One implementation in crates/datalog; two drivers — oxc::reasoning::datalog_bridge at compile time, the Kernel at runtime.
• DomainRuleEngine — for event-driven reactive rules and computations. Lives in the Kernel; runtime-only today (a compile-time driver is a development gap).

Above tier:recursive, rules parse and elaborate but do not execute. tier:fol is gated behind unsafe logic { … }; tier:modal and tier:mlt are syntax-only today.

The dispatch is automatic — you almost never have to think about which engine owns a rule. The classification surfaces through OI0804 if you want to see it.

The saturator follows a monotone-inflationary pattern: every derive rule’s body defines a monotone function on the fact set; the iterator applies the composition until quiescence. The fixpoint is finite (the lattice has finite ascending chains over a finite concept hierarchy) and unique (any two evaluation orders that respect stratification produce the same final state). Chapter 5.1 states the termination, uniqueness, and indeterminacy results in full.

The decidability tier ladder

Argon’s most distinctive design choice is making decidability a graded property, not a binary one. Every rule is classified at compile time into one of seven tiers:

The key thing: tiers 4–6 still parse and elaborate. The compiler checks them syntactically and runs the type-system; @[theorem] annotations are preserved through to the kernel as theorem markers for a future verification pipeline. What it does not do is run them at query time, because the engines for those fragments are either not yet shipped (tiers 4 and 5) or undecidable (tier 6); mechanical theorem verification itself is not yet active.

A package-wide cap lives in ox.toml’s [package] section:

[package]
name = "lease-tutorial"
version = "0.1.0"
max_tier = 3

The compiler refuses to elaborate any rule that classifies above this tier (OE1405). It is the package’s most general statement of “I will not surprise you with a query that takes forever.” The lease tutorial sits comfortably at tier 3.

Chapter 5.3 covers the full ladder, the formal classification function, @[theorem], unsafe logic, and the #[unproven] / #[assumed] test markers.

Edge cases worth knowing

• Variables must be bound. Every variable in a body needs at least one atom that binds it (a type test, a relation atom, a path traversal). Query heads with unbound variables emit OE1409; derive bodies with unbound identifiers fail name resolution.
• Order does not matter inside a rule body. Rule bodies are declarative — l: Lease, l.end_date > today() and l.end_date > today(), l: Lease mean the same thing. The engine picks an evaluation order that works.
• Rule heads cannot share a name with computes. pub derive ActiveLease(...) and pub compute ActiveLease(...) would collide. The compiler tells you up front (OE0206).
• Asserts run in ox check --reason and in tests. They do not run on every ox check (which skips reasoning for speed). Either run --reason or write a test that invokes the relevant assertion.
• today() versus --as-of-valid. Inside a query, today() resolves to the valid time at which the query is asked. To time-travel, pass --as-of-valid <RFC-3339> to the runtime. The same rule body will fire or not depending on the temporal frame (Chapter 5.4).

Putting it in the running example

Add src/rules.ar:

use lease::*

pub derive ActiveLease(l: Lease) :-
    l: Lease,
    l.start_date <= today(),
    l.end_date > today()

pub derive ExpiredLease(l: Lease) :-
    l: Lease,
    l.end_date <= today()

assert valid_dates(l: Lease) :-
    l: Lease,
    l.start_date >= l.end_date
    => error("lease start_date must be before end_date")

assert positive_rent(l: Lease) :-
    l: Lease,
    l.monthly_rent <= 0
    => error("monthly_rent must be positive")

And src/queries.ar:

use lease::*
use rules::*

pub query active_leases() -> [Lease] :-
    ?l: Lease,
    ActiveLease(?l)
    => ?l

pub query expired_leases() -> [Lease] :-
    ?l: Lease,
    ExpiredLease(?l)
    => ?l

pub query active_residential_leases() -> [ResidentialLease] :-
    ?l: ResidentialLease,
    ActiveLease(?l)
    => ?l

Notice: queries’ bodies use ?l because the head is empty (active_leases()) — ? introduces the body’s fresh variable. Derives’ heads carry the binding name explicitly (ActiveLease(l: Lease)), so the body reuses l without ?.

Update prelude.ar:

pub use metatypes::*
pub use party::*
pub use lease::*
pub use rules::*
pub use queries::*

Then:

$ ox check --reason
   Reasoning over 2 rules + 2 asserts...
check passed

The model now derives lease state and enforces lease invariants. We have the engine running over our model.

Summary

Rules are declarative: a head holds when its body’s atoms all hold. derive produces facts; assert declares invariants. Bodies use a small vocabulary of atoms — type tests, comparisons, predicate calls, negation, aggregates — and a few advanced shapes for cases that need them. Head parameters bind bare names; ? prefixes are reserved for body-fresh variables. The reasoner is a three-engine pipeline; the tier ladder makes decidability a graded property; --reason opts in at compile time, and --explain shows why-trees at runtime. The lease tutorial now has rules, asserts, and queries. Next we add operations.