RFD 0003 — Reasoner backend dispatch

• State: discussion
• Opened: 2026-05-27
• Decides: how multiple reasoning backends (semi-naive, SLG, DBSP, SMT, Kripke, Kora-extension) compose under one Engine interface; the dispatch policy for per-stratum routing; the registration discipline; the modeler-facing diagnostic surface for unsupported-tier rules.

Question

Argon’s tier ladder admits seven distinct reasoning tiers (§10.1: structural, closure, expressive, recursive, fol, modal, metaorder). No single algorithm handles all seven — semi-naive Datalog handles stratified recursive; SLG tabling handles expressive; DBSP handles recursive under IVM; SMT handles fol; Kripke tableau handles modal; Kora-EL handles a slice of OWL profile semantics. How do these backends compose under one engine interface? What does the dispatcher do? When does the modeler see backend choices vs not?

Context

What’s already in place

Phase 1 of the reasoner is shipped (oxc-reasoning crate, ~530 LOC of evaluator + classifier + scaffolding). The keystone test passes: derive adult(p) :- Person(p), hasAge(p, n), n >= 18 derives the right facts end-to-end.

The current shape:

Engine
  ├── executors: Vec<Box<dyn TierExecutor>>   (registration-ordered)
  └── run_rules(...) — dispatches each rule to the first executor
                       whose supported_tiers() contains the rule's
                       classified tier.

TierExecutor trait
  ├── name(&self) -> &'static str
  ├── supported_tiers(&self) -> TierSet
  └── execute(stratum, input) -> ReasoningResult<RelationCatalog>

The single MVP implementation SemiNaiveExecutor advertises {Structural, Closure, Recursive}. The dispatcher is one-deep: pick the first executor that supports the tier. Per-rule tier comes from RuleDeclBody.main_tier, populated by oxc-instantiate::tier_classify::classify_body.

Where this falls short

The “first executor that supports the tier” policy works for the trivial case (one executor) but doesn’t say what happens when:

1. Multiple executors claim the same tier (e.g., SemiNaive and DBSP both handle recursive). Which wins? Order-of-registration is the current answer; that’s an implicit policy with no surface.

2. A rule’s body spans multiple tiers (e.g., a recursive rule that joins against an expressive qualified-cardinality predicate). Today the rule’s main_tier is the max of its atoms’ tiers — so the whole rule goes to whatever handles the max. That’s correct semantically but ignores stratification: the lower-tier sub-rule could run on the cheaper engine, results then fed into the higher-tier engine.

3. Cross-backend data exchange — every backend produces RelationCatalog (Z-set BTreeMaps). Good for composition; the next stratum reads from the prior stratum’s output. But what if a backend uses internally-different data (DBSP’s arrangements vs SLG’s tabled tables)? The exchange happens at stratum boundaries via RelationCatalog; backend internals stay private.

4. The modeler’s diagnostic surface — OE1305 (TierNotYetImplemented) is reserved but emission sites aren’t wired. When does the modeler see it? At build time (the rule’s tier exceeds any registered backend) or at query time (the rule’s classified tier is unsupportable)?

5. Optional backends (Kora-extension) — std::owl is a stdlib package that brings in the Kora-EL / Kora-DL backend. How does that get registered? Is it an explicit Engine::with_executor call, or implicit on import std::owl?

Decision

The dispatch model: per-stratum, registration-ordered, with explicit OE1305 emission

1. Strata are the unit of dispatch. The physical plan (PhysicalPlan) carries a Vec<Stratum>. Each stratum has a tier (the max of its rules’ tiers). The dispatcher picks one executor per stratum and runs it.

2. Registration order = preference order. Executors are pushed onto Engine::executors in registration order. The dispatcher picks the first executor whose supported_tiers() contains the stratum’s tier. This makes the policy explicit and modeler-controllable via build configuration.

3. OE1305 emits at build time, not query time. When oxc-instantiate classifies a rule and the workspace’s configured backends don’t claim its tier, the build fails with OE1305. The modeler sees the error at compile time, before any runtime invocation.

4. Backend registration is workspace configuration. Backends are declared in ox.toml (or the equivalent), not in source code. Default workspaces register SemiNaiveExecutor only. Adding SLG, SMT, etc. is an explicit opt-in via:

   [reasoning]
   executors = ["semi-naive", "slg-tabled"]
   

   Kora-extension is enabled by import std::owl in source, which adds kora-el (and kora-dl) to the executor list automatically.

5. Cross-backend exchange is the shared RelationCatalog. All backends produce and consume RelationCatalog (Z-set BTreeMap). Internal representations (DBSP arrangements, SLG tabled solutions) are private. Composition happens at stratum boundaries: stratum N’s output catalog is stratum N+1’s input catalog.

The seven backends, mapped

Composition rules:

• DBSP wins over SemiNaive when both are registered: register DBSP first so the dispatcher picks it. DBSP is a strictly more powerful evaluator (handles IVM, deltas, retractions natively); SemiNaive becomes a fallback for environments where DBSP can’t be deployed.
• Kora-extension only handles its declared tier slice. It doesn’t claim recursive even though some EL rules look Datalog-shaped — Kora’s optimizations are OWL-specific and don’t generalize. The dispatcher uses Kora only for rules tagged as DL-shaped (a future RuleDeclBody field).

What the modeler sees

The modeler does not see backend names in source code. Rules are tier-classified by the compiler; backend selection is a deployment concern.

The modeler does see OE1305 when a rule’s tier exceeds the workspace’s configured backends. The diagnostic suggests which backend would handle it:

error[OE1305]: rule `complex_query` classified at tier `expressive` —
              no registered executor handles this tier
  --> demo.ar:42:1
  |
  | pub derive complex_query(p) :- ...
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  |
  = note: enable the `slg-tabled` executor in ox.toml:
        [reasoning]
        executors = ["semi-naive", "slg-tabled"]

The TierExecutor trait — refined

#![allow(unused)]
fn main() {
pub trait TierExecutor: Send + Sync {
    fn name(&self) -> &'static str;
    fn supported_tiers(&self) -> TierSet;

    /// Execute one stratum. Reads from `input` (current state +
    /// prior strata's outputs); returns the stratum's catalog delta.
    fn execute(
        &self,
        stratum: &Stratum,
        input: &RelationCatalog,
    ) -> ReasoningResult<RelationCatalog>;

    /// Optional: backend-specific cost estimate for a stratum.
    /// Returned values are comparable across backends (smaller = preferred).
    /// Default impl returns `f64::INFINITY` (never prefer).
    fn estimate_cost(&self, _stratum: &Stratum, _input: &RelationCatalog) -> f64 {
        f64::INFINITY
    }
}
}

The estimate_cost method is the hook for cost-based dispatch (v2). v1 uses pure registration-order dispatch; v2 may evolve to “pick the registered executor whose cost estimate is lowest.” Deferred to a follow-up RFD.

Stratum boundary policy

The optimizer is responsible for stratification: walk the rule dependency graph, partition into SCCs, topologically sort the SCCs into strata. Each stratum is single-tier (max of its rules). NAF is stratified across stratum boundaries (sound).

Inter-stratum NAF (a rule in stratum N+1 uses not p(...) where p is populated in stratum N) is the standard stratified-WFS case. Intra-stratum NAF is a cycle and either:

• Handled by the backend if the backend supports WFS (SLG does; SemiNaive doesn’t beyond stratification).
• Rejected with OE1309 (StratificationNafCycle) at build time.

Rationale

Why per-stratum, not per-rule

A real-world workload has many rules at different tiers. Dispatching per-rule means launching the backend’s per-call overhead for each. Per-stratum amortizes: the backend sees all its rules, can build its own internal arrangements once, run them all to fixpoint within its scope.

This matches DataFusion’s pattern (which inspired the architecture): each ExecutionPlan node runs to completion in one backend context; data flows between nodes via the shared columnar format. Argon’s analog: each stratum runs in one backend context; catalogs flow between strata via the shared Z-set format.

Why registration order, not declared priority

A priority: i32 field on TierExecutor would let backends declare their own preference order. Rejected because:

• It distributes the dispatch logic — each backend needs to know its place in the ordering vs other backends.
• It introduces a coordination problem when two backends claim the same priority.
• Registration order achieves the same expressivity (push backends in the desired order) without per-backend coordination.

Workspace configuration (ox.toml’s [reasoning].executors = [...]) makes the order explicit and modeler-visible. That’s the right surface for the policy decision.

Why OE1305 at build time, not query time

The alternative is lazy: register backends; at query time, if no backend handles the tier, fail. Rejected because:

• A modeler shouldn’t ship an .oxbin that they don’t know is unrunnable. Build-time emission catches it early.
• The set of registered backends is a deployment property; the modeler knows it at build configuration time.
• “Build it, ship it, then it fails when the user runs it” is a bad UX for a system whose virtue is “deterministic builds give you runtime guarantees.”

Why workspace-config, not in-source backend selection

Source code shouldn’t say “use SLG for this rule.” Two reasons:

• The modeler should describe what they want derived, not how to derive it. That’s the entire point of declarative semantics.
• Backend choice is deployment policy. A test workspace uses SemiNaive; a production workspace uses DBSP + SLG. Same source code, different deployment.

The exception: std::owl is a stdlib package that brings in OWL semantics. Importing it implicitly enables Kora-extension because the modeler is asking for OWL-shape reasoning. This isn’t “backend selection”; it’s “load this semantics extension.”

Why DBSP wins over SemiNaive when both registered

DBSP handles every workload SemiNaive handles, plus retractions and IVM. It’s strictly more powerful. Once DBSP is mature (Phase-4-of-RFD-0001 or later), the natural default is “use DBSP if available, fall back to SemiNaive otherwise.” Registration order encodes this: push DBSP first.

SemiNaive stays in the stack because:

• It has no external dependencies (DBSP needs the timely dataflow runtime).
• It’s simpler to reason about correctness in.
• It’s the reference implementation that other backends can be tested against.

Why Kora is “extension” not “default”

Argon’s substrate is OWL-neutral. Baking OWL-specific optimizations into the default executor stack would couple Argon to OWL semantics — which RFD 0001 and the broader architecture explicitly avoid.

Kora becomes available when a modeler imports std::owl. That import is a deliberate statement: “I want OWL semantics for this part of my model.” The Kora backend then handles those rules; non-OWL rules go through the default backends.

Alternatives considered

Alt 1: Single mega-engine

One backend handles all tiers via dispatched algorithms internally. Examples in prior art: SWRL-DL engines that switch between Datalog and tableau internally.

Rejected: kills modularity. Adding a new backend (SLG, DBSP) requires modifying the mega-engine. Cross-engine testing becomes impossible.

Alt 2: Runtime backend resolution

Backends register themselves via plugin discovery at runtime; the engine probes for capability.

Rejected: introduces dynamic-loading complexity Rust doesn’t natively support and Argon doesn’t need. All known backends are statically-known at build time.

Alt 3: Backend per rule mode

derive rules go to one backend, query rules to another, etc.

Rejected: backend choice is about tier (what features the rule uses), not mode (what kind of declaration it is). A derive rule and a query rule with the same body should run on the same backend.

Alt 4: First-class cost-based dispatch from v1

estimate_cost is mandatory; dispatcher picks the lowest-cost backend per stratum.

Rejected for v1: backends don’t yet have meaningful cost models. SemiNaive’s cost estimate is fact-count; DBSP’s would involve arrangement-sharing analysis. Without a calibrated cost surface, “lowest cost” is noise. Registration-order is honest about the v1 state. Cost-based dispatch becomes v2 once enough backends ship to make calibration meaningful.

Consequences

Code structure

The Engine and TierExecutor trait already exist (oxc-reasoning/src/executor/mod.rs). This RFD codifies the existing API; minor refinements needed:

• Add estimate_cost default method (deferred-use API).
• Add workspace configuration support (ox.toml parsing for [reasoning]).
• Wire OE1305 emission from oxc-instantiate::tier_classify when the configured backends don’t cover the classified tier.

Diagnostic surface

OE1305 emission gains a structured “suggest enabling X backend” hint. Requires the diagnostic system to know which backends could handle which tiers — a static table in oxc-diagnostics or oxc-reasoning::backend_registry.

Each future backend’s commit

Each new backend lands as:

1. A new module in oxc-reasoning::executor::{name}.rs implementing TierExecutor.
2. Registration plumbing in workspace config.
3. Backend-specific tests showing the keystone-equivalent for its tier (e.g., SLG’s keystone is a recursive-aggregate rule like count over a stratified-NAF derived predicate).
4. An interop test showing the backend composes cleanly with SemiNaive at stratum boundaries.

Kora vendoring decision

Per the earlier session decision: when we bring in Kora, we vendor the code into oxc-reasoning::executor::kora and own the implementation. We don’t depend on the upstream kora-* crates. This isolates Argon from Kora’s design choices and lets us evolve the embedded reasoner independently.

The vendoring is an explicit one-time copy; subsequent changes happen in Argon’s tree. If upstream Kora improves substantially, we re-vendor with a documented migration. This matches the pattern other projects use for embedded engines (e.g., rust-analyzer’s vendored libraries).

Open questions

• Stratum boundary policy with retractions: when a fact is retracted in stratum N, the retraction must propagate to stratum N+1’s derived facts. The current RelationCatalog exchange is a snapshot, not a delta stream. For DBSP this is solved natively (it IS the delta stream); for SemiNaive we recompute. Architecturally clean; performance-cost matters for large stores. Defer to the DBSP integration RFD.

• Workspace config schema: ox.toml’s [reasoning] section needs a concrete schema. Reserve the section now; nail down the schema when the second backend (DBSP or SLG, whichever lands first) makes it necessary.

• Per-rule backend override: should the modeler ever be able to say “use SemiNaive for this rule even though DBSP is registered”? Possible use cases: debugging (compare backends on the same rule), workload-specific tuning. Defer; revisit when a real use case emerges.

• Backend feature negotiation: a backend may support a tier but not a specific feature (e.g., SemiNaive supports recursive but not recursive with aggregates). How does the dispatcher know? Either (a) backends advertise feature support more granularly than tier, or (b) the classifier bumps tiers when specific features are used (e.g., aggregates always classify as expressive). The current classifier does (b); the trade-off is granularity vs simplicity. Probably keep (b) for v1.

• Dynamic backend selection by data characteristics: e.g., “use DBSP if the input cardinality is over 10M; use SemiNaive otherwise.” Cost-based dispatch (v2) addresses this. Out of scope for v1.

• Modal + temporal interaction: when temporal qualifiers nest inside modal operators (or vice versa), the relevant tier is modal per §10.1. Which backend handles? KripkeExecutor in the design; verify when the temporal-substrate work track lands the temporal evaluator.