RFD 0011 — Aggregate semantics under OWA

• State: discussion
• Opened: 2026-05-29
• Decides: how aggregate atoms (sum, count, min, max, avg, set_collect, …) evaluate under OWA when filter or input cells carry Can verdicts; the per-mode default semantics (query / derive / check / fn); the diagnostic surface that makes the projection observable rather than silent; the aggregation-metadata envelope that surfaces interval bounds and excluded-cell counts at every data-system boundary; resolves RFD 0007 OQ3.

Question

Argon admits aggregate atoms in rule bodies and query bodies (§6.6, §7.3.1, §7.4): sum(i.value for i in income where i.taxable) > threshold and friends. Under OWA, the filter predicate i.taxable can evaluate to Can (per RFD 0007’s required-field-under-OWA lift). The substrate has not specified what aggregates do with Can-valued cells.

The spec at §12.2 has only one nearby sentence: “Set / list / record projections: Can-valued cells are omitted from the result set.” Applied literally to aggregates this is silent fail-closed at the filter — Can-cells get dropped, the sum is a definite number, the comparison yields a definite verdict, and the modeler never learns that the answer depended on uncertain data they did not see. This is the SQL-NULL bug at scale. For a language whose primary contract is “OWA semantics done right,” it is an unacceptable default.

But the formal-correctness response (the elaborator forces the modeler to declare an aggregate-Can handling at every site) is hostile to the 90% case: writing reports, dashboards, and analytics queries should feel like SQL, not like coursework on three-valued logic.

This RFD picks the semantics that gives Argon both: SQL-like ergonomics in the default case, OWA-sound interval semantics in the substrate, and a never-silent projection at the surface.

Context

The motivating Slack thread (Almeida + Almeida, 2026-05-28 → 2026-05-29)

Gustavo Ladeira (Sharpe) extended the discussion of RFD 0007 with a concrete query:

pub kind Income {
    taxable: Bool?,
    value:   Money,
}

pub query AllIncome() -> [Income] :- i: Income, select i

pub derive TotalTaxableIncomeExceedsThreshold(threshold: Money) :-
    sum(i.value for i in AllIncome() where i.taxable) > threshold

He asked: “does the derive resolve to Can if both lines below hold simultaneously?

sum(i.value for i in AllIncome() where i.taxable == true) <= threshold
sum(i.value for i in AllIncome() where (i.taxable == true) || (not exists i.taxable)) > threshold

He had derived the interval-bound semantics for monotone aggregates in his own message: lower bound = sum over confirmed-true filter; upper bound = sum over confirmed-true OR Can filter; verdict is Can exactly when the threshold falls in the open interval. The spec did not have a rule giving him that semantics.

João Paulo Almeida (UFES) had separately raised the structural-vs-epistemic ambiguity of Bool? (RFD 0007’s motivating point), which compounds: under structural-optional Bool?, Gustavo’s None-cells are not taxable (a positive fact of absence) and the aggregate is definite by structural exclusion; under epistemic Bool + OWA, missing taxable lifts to Can and the interval semantics is what he wants. RFD 0007 resolved the surface ambiguity. This RFD resolves what happens once the Can-cells reach an aggregator.

Substrate readiness

• Aggregate grammar is in §6.6 / §7.3.1 (atom shape: aggregate (comp-op expr)?; expression shape: aggregate ::= ('sum'|'count'|'min'|'max'|'avg') '(' expr ('for' Ident 'in' expr ('where' expr)?)? ')').
• Aggregate runtime is not yet implemented. oxc-reasoning/src/compile/rule.rs:78 returns RuleCompileError::AggregateNotYet. The semi-naive executor classifies aggregates at the expressive tier (§10.1) and rejects them; no execution path exists. This RFD is greenfield design, not a behavior change.
• Lean mechanization has no Reasoning/Aggregate.lean. The Truth4 substrate (Foundation/Truth4.lean) + the K3 conjunction in Reasoning/Fixpoint.lean give the operators an aggregate semantics can build on; the aggregate-specific theorems do not yet exist.
• Truth4 projection is documented at §12.2: K3 fail-closed projection (Pietz–Rivieccio Exactly-True) folds Can → false for Bool, omits Can-cells from set/list/record results. This RFD threads the aggregate question through that projection rule without contradicting it.

Why the obvious answers fail

Three semantics, evaluated independently:

No single option covers all aggregator kinds. The decision is to combine them with type-driven projection, so the modeler picks the level of sophistication via the result type while the substrate always evaluates soundly.

Decision

Three rules, applied in order. Each rule is one click away from the next; the modeler picks the level at which they want to engage with Can.

Rule 1 — The substrate evaluates aggregates in Truth4

Under OWA, an aggregate agg(expr for x in S where φ(x)) evaluates over a Truth4-tagged set:

{ x ∈ S : φ(x) ∈ {Is, Can} }

— with each element marked by its filter verdict. The aggregator’s behavior on this tagged set depends on its monotonicity class:

Monotone aggregators (interval bounds)

For sum over non-negative values, count, set_collect:

lower = agg over { x : φ(x) is Is(true) }
upper = agg over { x : φ(x) is Is(true) or Can }

For sum over signed values, the bounds are sign-partitioned: lower = sum(Is) + sum(negative-valued Can cells); upper = sum(Is) + sum(positive-valued Can cells). This is monotone in each sign-class independently and computable in a single pass.

The aggregator returns the Truth4-lifted interval — internally a pair (lower, upper) carried as Truth4Of<T> with bounds metadata.

Non-monotone aggregators (propagating)

For min, max, avg, percentile, string_join, count distinct:

if { x : φ(x) is Can } is empty:
    result = agg over { x : φ(x) is Is(true) }    // definite verdict
else:
    result = Can                                   // any Can in filter set
                                                    // propagates to whole result

These aggregators have non-monotone bounds (min(A ∪ B) ≤ min(A) and the upper bound depends on Can-cell values that aren’t known), so interval semantics gives vacuous bounds in the worst case. Propagating is the only sound default that doesn’t over-claim; modelers who want sharper semantics narrow the filter explicitly to Is-only.

Aggregator-kind taxonomy

The classification is fixed at the aggregator-kind level, not per-call.

Rule 2 — The surface projection is type-driven

The Truth4-tagged aggregate result propagates until it hits a typed boundary (the declared return type of the enclosing query/derive/fn, the head of a derive, the predicate of an if/match, the membership-witness of a refinement clause). At the boundary, the §12.2 K3 fail-closed projection fires, governed by the boundary’s declared type:

A modeler switches between ergonomic and sound semantics by changing one type annotation:

// Ergonomic: SQL-like; projects Can → false at Bool boundary.
pub query QuarterlyOK() -> Bool {
    sum(i.value for i in income where i.taxable) > threshold
}

// Sound: preserves three-way verdict for caller.
pub query QuarterlyOK() -> Truth4Of<Bool> {
    sum(i.value for i in income where i.taxable) > threshold
}

For derive rule heads, the same dial applies via the head type. A pub derive Foo(p: Person) is Truth4Of<Bool> rule populates a Truth4-aware IDB relation; consumers reading Foo(p) get Is | Not | Can directly.

Rule 3 — The projection is never silent

Two pieces ensure the modeler always sees the soundness picture, no matter which projection they chose.

3a. Per-projection diagnostic

Every fail-closed projection at an aggregate boundary emits a diagnostic with the interval bounds and excluded-cell count. The diagnostic level depends on the mode:

The diagnostic carries:

14:5: info[OW0613]: aggregate filter projection fail-closed
  |
14 |   sum(i.value for i in income where i.taxable) > threshold
  |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  | filter `i.taxable` may evaluate to Can; verdict projects to Bool with
  | Can → false (Pietz–Rivieccio Exactly-True, §12.2). Interval bounds for
  | this materialization: [$1,234,567.00, $1,256,789.00]; 5 Can-cells.
  |
help: change return type to Truth4Of<Bool> to preserve Can verdict:
  pub query QuarterlyOK() -> Truth4Of<Bool> { … }
help: or filter explicitly to suppress this diagnostic:
  ... where i.taxable is Is(true)              // fail-closed, explicit
  ... where i.taxable is Is(true) or Can       // include unknowns
help: silence per-rule with #[allow(aggregate_fail_closed)]

The diagnostic is suppressible per-site with #[allow(aggregate_fail_closed)]; in check mode, the diagnostic is OE0614 (error) and the only opt-out is #[check(fail_closed)] on the check declaration, which makes the soundness loss explicit at the check site.

3b. Per-result metadata envelope

Every aggregate query result, regardless of projection target, carries an aggregation_metadata envelope alongside the projected value. The envelope is always present when the aggregate’s filter set could have been Can-valued; it is absent when the aggregate is provably Can-free.

JSON shape (REST / wire format):

{
    "value": true,
    "aggregation_metadata": {
        "result_type": "Bool",
        "projected_from": "Truth4Of<Bool>",
        "projected_verdict": "Is(true)",
        "interval": { "lower": 1234567.00, "upper": 1256789.00 },
        "excluded_can_cells": 5,
        "excluded_can_value_bounds": { "lower": 22222.00, "upper": 22222.00 },
        "verdict_robust": true
    }
}

verdict_robust = true iff the projected verdict would be the same across every completion of the Can-cells. When false, the modeler / auditor / dashboard sees that the answer depended on the projection — exactly the SQL-NULL bug made visible.

CLI presentation (ox query):

$ ox query QuarterlyOK
true

(aggregate: 5 of 100 income rows had Can-valued `taxable`;
            bounds [$1,234,567, $1,256,789];
            verdict robust to all completions)

ox query --explain prints the full envelope; standard text mode prints a one-line summary when excluded_can_cells > 0. The envelope is computed during the substrate’s Truth4 evaluation (the bounds are already needed for monotone aggregators), so the runtime cost is one allocation per aggregate, not an extra pass.

Per-mode default summary

Worked example — Gustavo’s case

After this RFD lands, Gustavo’s pattern, with the epistemic-Bool surface (per RFD 0007) and the sound-three-verdict return type:

pub kind Income {
    taxable: Bool,                // required + OWA — epistemic reading
    value:   Money,
}

pub query AllIncome() -> [Income] :- i: Income, select i

pub derive TotalTaxableIncomeExceedsThreshold(threshold: Money)
        is Truth4Of<Bool> :-
    sum(i.value for i in AllIncome() where i.taxable) > threshold

The substrate’s monotone-sum evaluates to Truth4Of<Money> with bounds [lower, upper] per Rule 1. The comparison > threshold lifts pointwise:

threshold <  lower            → Is(true)    // every completion exceeds
threshold >= upper            → Is(false)   // no completion exceeds
lower <= threshold < upper    → Can         // depends on which Can-cells are taxable

The head type Truth4Of<Bool> preserves the verdict (Rule 2). Consumers read TotalTaxableIncomeExceedsThreshold(threshold) and pattern-match on the three outcomes. No diagnostic fires (Rule 3) — the modeler chose the sound path explicitly.

If Gustavo had written is Bool on the head, the verdict projects fail-closed (Can → false), the diagnostic fires at warning level (derive mode), and the materialized IDB record carries false for the Can-case threshold. The metadata envelope on the query result still shows the bounds and Can-cell count.

Rationale

Why “substrate sound, surface projected” rather than “force the modeler”

The earlier draft of this design (A1+B1 from the Slack discussion) made the elaborator hard-error at every where-clause that could be Can, requiring the modeler to declare an aggregate-Can handling explicitly. This was formally correct but practically hostile: every aggregate over OWA data in a routine query would error until the modeler annotated. Argon’s contract as a practical data systems language requires that day-to-day analytics queries — reports, dashboards, ad-hoc SQL-like exploration — feel like SQL with one knob upgraded, not like a three-valued-logic seminar.

The substrate-Truth4 + surface-projected design separates the two concerns. The substrate always evaluates with Truth4 fidelity (the OWA-soundness contract is preserved regardless of what the modeler writes). The surface projection is type-driven: the modeler picks ergonomic Bool or sound Truth4Of via the return type, with the type-system change costing one character. The “never silent” rule ensures the modeler is informed about the projection at every fail-closed site without being blocked. This is the design SQL should have had.

Why the per-mode default split

query is the analytics surface — ergonomics-first. derive populates the IDB and propagates downstream; an unsound derive contaminates many subsequent rules. check is compliance — a check that silently fails-closed and misses a violation is the worst possible failure mode for the system. The diagnostic level escalates monotonically with the cost of silent-wrong: info → warning → error.

This is symmetric with how Rust handles Result<T, E>: ignoring the error is allowed but loud (#[must_use] warning by default), and the language never forces you to handle every case at every call site. The “you must handle this” boundary is at the typed-result boundary, not at every intermediate computation.

Why the metadata envelope is always-present (not opt-in)

The bounds and Can-cell counts are computed by the substrate regardless (they’re load-bearing for the monotone interval evaluation). Surfacing them at the result boundary is near-free. Making them opt-in (?metadata=true) would mean most data-system consumers — dashboards, CSV exports, REST clients — never see them, and the SQL-NULL bug returns silently. Always-present means the auditor / debugger / pipeline-engineer always has the evidence; the cost is a few extra bytes per result.

The CLI’s one-line summary (only printed when excluded_can_cells > 0) keeps the common-case output clean while still being honest. ox query --explain shows the full envelope.

Why interval semantics, not propagation, for monotone aggregators

Propagation (any Can → whole result Can) is sound but loses real conclusions. When sum-over-Is alone already exceeds threshold, the verdict is definitively Is(true) regardless of the Can-cells; propagation would still say Can and the modeler / system / auditor would get a less informative answer than the data supports. Interval semantics extracts the maximum signal from the partial data without over-claiming.

For non-monotone aggregators, interval semantics gives vacuous bounds (e.g., min with Can-cells could be anything in the Can-cells’ value range); propagation is the right default there because the alternative is bounds that don’t constrain. The taxonomy fixes the classification per-aggregator-kind so modelers don’t have to reason about which gets which.

Alternatives considered

A. Silent fail-closed (the SQL-NULL default, what §12.2 implies today)

Can-cells dropped from filter set; aggregate produces a definite verdict; modeler never told. Rejected. Reproduces the SQL-NULL bug at the OWA scale. Argon’s substrate guarantees OWA-soundness; a surface that silently violates the guarantee defeats the language’s central pitch.

B. Hard-error at every aggregate over Can-potential filter (the original A1+B1)

Elaborator refuses to compile until the modeler annotates the aggregate with one of is Is(true) / is Can / propagating. Rejected. Hostile to practical analytics — every query against OWA-required field must annotate; the migration cost from existing codebases is enormous; the friction undermines the data-system-as-product story.

C. Always-Truth4Of return type

Aggregators always return Truth4Of<T>; modelers must pattern-match to extract a value. Rejected. Most aggregator results are immediately compared or summed downstream where the ergonomic fail-closed projection is what the modeler wants; forcing Truth4Of<T> everywhere is the same hostile-friction problem as B.

D. Per-call annotation in the aggregate body

sum(i.value for i where i.taxable mode=interval) > threshold. Rejected. Annotation is at the wrong site — the modeler’s intent is about the projection, not the aggregator. The return type is the natural place to declare it.

E. Two-pass query model (run with one semantics, switch interactively)

ox query defaults to fail-closed; modeler runs ox query --reanalyze sound if they want to see the Can-case. Rejected. Doesn’t work for batch / programmatic consumers, and the modeler doesn’t know to ask the second time unless something cues them. The always-present metadata envelope (Rule 3b) gives the same effect without the second invocation.

F. Defer entirely

Wait until the aggregate executor lands (oxc-reasoning::AggregateNotYet) and decide then. Rejected. The executor needs this decision before it can be implemented; the design space has been actively explored; settling now means the implementation doesn’t ship with an ad-hoc choice. RFD 0007 OQ3 already promised follow-on; this is it.

Consequences

What lands

Substrate impact

• One new theorem in Reasoning/Aggregate.lean: for any monotone aggregator A over a filter predicate φ, the interval [A(Is), A(Is ∪ Can)] is a sound over-approximation of every completion of the KB. Proven by induction on the K3 fixpoint already established in Reasoning/Fixpoint.lean.
• No change to subsumption_axiom, iof_assertion, relation_tuple wire formats. The metadata envelope is computed at query time, not stored.
• No change to the Z-set Storage model. Aggregates are evaluated over materialized relation extents, which already carry the Truth4 tags from the underlying fixpoint.

Modeler impact

• Routine analytics queries compile unchanged; behavior is SQL-NULL fail-closed but with bounded transparency via the metadata envelope and the info-level diagnostic.
• Soundness opt-in is a one-character type change (Bool → Truth4Of<Bool>).
• check rules get stricter default — modelers writing compliance checks must engage with Can or explicitly opt out, which is the right default for compliance.
• Existing rules that compiled under the unimplemented-aggregate path will compile under this RFD with the same surface; behavior change vs the unimplemented baseline is the addition of the diagnostic and the metadata envelope.

Tooling impact

• ox query shows aggregate summaries by default when Can-cells were excluded.
• ox query --explain shows full metadata envelopes.
• LSP can surface the diagnostic inline; debuggers can read the envelope.
• REST adapters return the envelope alongside results; clients can ignore it or render it.

Compatibility

The aggregate executor is a new implementation; there is no prior behavior to preserve. The grammar surface is unchanged. The metadata envelope is additive; consumers that don’t read it see the same JSON shape they would have seen.

Open questions

OQ1 — Aggregator-kind monotonicity classification under user-defined aggregators

When modelers register custom aggregators via pub aggregate (a future grammar surface for plugin aggregators), how do they declare the monotonicity class? Likely via attribute (#[monotone] / #[propagating]) on the aggregator declaration. Out of scope for this RFD; document when the custom-aggregator surface lands.

OQ2 — Aggregate-of-aggregate composition

What does sum(count(j.value for j in i.children) for i in roots()) look like under partial Can data? The inner aggregator produces a Truth4Of<Nat> interval per row; the outer aggregator over a sequence of intervals needs an interval composition rule. For monotone outer aggregators over interval-valued inputs, the composition is sum-of-bounds — pointwise interval arithmetic. Specify in the Reasoning/Aggregate.lean mechanization; document examples in §7.4.

OQ3 — Interaction with temporal aggregates (§6.10.5 + §7.3.2)

DatalogMTL operators since/until combined with aggregates. Under OWA + temporal Can, the interval bounds need to factor in the temporal extent. The temporal substrate’s three-valued evaluation (§6.10.5) composes pointwise; the aggregate’s interval semantics composes monotonically; the combined semantics needs verification. Likely lands in a follow-on RFD on temporal-aggregate semantics.

OQ4 — #[brave] mode interaction

§7.3 admits #[brave] for stable-model semantics. Under brave + OWA, aggregates need to evaluate across stable models. Each stable model produces a definite verdict; the aggregate result is the join across models. Out of scope; document when the brave-semantics RFD is written.

OQ5 — Metadata envelope schema versioning

The envelope is a wire-format addition; future fields (additional bounds, multiple Can-cell categorizations) require a schema version. Adopt the oxc-protocol versioning policy from RFD 0001; envelope carries a version: 1 field.

OQ6 — Persistent aggregate caching under metadata

Salsa-cached aggregate results need to track the metadata envelope; cache invalidation when Can-cells are resolved (via subsequent insert facts) must re-fire dependent aggregates. Likely a small extension to the Salsa cache key but worth verifying with the oxc-runtime Salsa wiring.

References

• RFD 0007 — Missing-value semantics under OWA §OQ3 — the open question this RFD resolves
• §6.6 (aggregate expression grammar), §6.9 (CWA/OWA), §6.10.5 (Kleene truth tables), §7.3.1 (rule-atom aggregates), §7.3 line 72 (“stratified aggregates”), §7.4 (query mode), §12.2 (K3 fail-closed projection)
• oxc-reasoning/src/compile/rule.rs:78 — AggregateNotYet (the implementation site)
• Foundation/Truth4.lean, Foundation/Projection.lean, Reasoning/Fixpoint.lean — substrate mechanization this RFD builds on
• Faber, W., Pfeifer, G., Leone, N. (2011). Semantics and complexity of recursive aggregates in answer set programming. Artificial Intelligence — the stratification rule §7 cites
• Pietz, A. & Rivieccio, U. (2013). Nothing but the truth. Journal of Philosophical Logic — the K3 fail-closed projection
• Belnap, N. (1977). A useful four-valued logic — the underlying bilattice
• Almeida, J.P.A. (UFES) & Ladeira, G. (Sharpe), Slack thread, 2026-05-28 → 2026-05-29 — the motivating discussion