Collections, aggregates, and data completeness

For LLMs9 sections

A fee for one order is a number from one fact. A reader’s monthly bill is a number from many: the sum of unpaid orders, their count, the average cheque. For this the core has collections and aggregates: count( stands in 745 rules across 83 packages, sum( in 71 across 23 (measured 05.09.2026). Aggregates hold three traps, all three silent: two equal sums counted as one; an empty set mistaken for zero; and an aggregate computed before what it counts has been collected.

language "law.core" version "0.2";
package tutorial.archive version "0.14.0";
namespace "urn:law:tutorial:archive";

entity Person;
entity CopyOrder;

relation copy_order(o: CopyOrder, p: Person) kind empirical;
relation order_amount(o: CopyOrder, amount: Money) kind empirical { key(o); }
relation order_paid(o: CopyOrder) kind empirical;
relation registered_reader(p: Person) kind institutional;
relation no_orders_confirmed(p: Person) kind empirical;

relation unpaid_order(o: CopyOrder) kind institutional;
relation total_due(p: Person, total: Money) kind institutional { key(p); }
relation distinct_amounts_total(p: Person, total: Money) kind institutional { key(p); }
relation naive_total(p: Person, total: Money) kind institutional { key(p); }
relation order_count(p: Person, n: Integer) kind institutional { key(p); }
relation unpaid_count(p: Person, n: Integer) kind institutional { key(p); }
relation average_order(p: Person, avg: Money) kind institutional { key(p); }
relation heavy_user(p: Person) kind institutional;

const HEAVY_ORDERS: Integer = 3;

Unpaid is not “unmarked as paid”

First — what counts as an unpaid order at all. The rule reads not order_paid(o), and that, as in the negation tutorial, requires an established negative support: an “unpaid” mark, not a missing “paid” mark.

rule UnpaidOrder strict {
    for o: CopyOrder;
    for p: Person;
    when copy_order(o, p) and not order_paid(o);
    then unpaid_order(o);
}

Facts about the order	`unpaid_order`
payment refuted	`TRUE_ONLY`
nothing about payment	`NEITHER`

Everything below sums unpaid_order — and so inherits this caution: an order the cash desk stayed silent about will not enter the debt.

A sum of positions versus a sum of values

A collect … where … generator enumerates substitutions; the aggregate counts over them. There are two forms, typed identically: collect all yields a list of positions, collect a set of distinct values.

rule TotalDue strict {
    for p: Person;
    when registered_reader(p) and count(collect o: CopyOrder where copy_order(o, p) and unpaid_order(o)) > 0;
    then total_due(p, sum(collect all a: Money, o: CopyOrder where copy_order(o, p) and unpaid_order(o) and order_amount(o, a)));
}

rule DistinctAmountsTotal strict {
    for p: Person;
    when registered_reader(p) and count(collect o: CopyOrder where copy_order(o, p) and unpaid_order(o)) > 0;
    then distinct_amounts_total(p, sum(collect a: Money, o: CopyOrder where copy_order(o, p) and unpaid_order(o) and order_amount(o, a)));
}

Unpaid orders	`total_due`	`distinct_amounts_total`
two at 1,000	`2000 KZT`	`1000 KZT`
1,000, 1,500, and a paid 2,000	`2500 KZT`	`2500 KZT`

The first row is the test from this page, byte for byte:

test "два неоплаченных заказа по 1000 — к оплате 2000" {
    given {
        context {
            decision_time @2026-04-20T09:00:00+05:00;
            knowledge_time @2026-04-20T09:00:00+05:00;
            legal_time @2026-04-20;
            timezone "Asia/Almaty";
        }
        assert registered_reader(entity_ref("urn:tutorial:ivanova")) {
            id "assert-reader";
            origin case_input;
        }
        assert copy_order(entity_ref("urn:tutorial:order1"), entity_ref("urn:tutorial:ivanova")) {
            id "assert-order-1";
            origin case_input;
        }
        assert order_amount(entity_ref("urn:tutorial:order1"), 1000 KZT) {
            id "assert-amount-1";
            origin case_input;
        }
        assert not order_paid(entity_ref("urn:tutorial:order1")) {
            id "assert-unpaid-1";
            origin case_input;
        }
        assert copy_order(entity_ref("urn:tutorial:order2"), entity_ref("urn:tutorial:ivanova")) {
            id "assert-order-2";
            origin case_input;
        }
        assert order_amount(entity_ref("urn:tutorial:order2"), 1000 KZT) {
            id "assert-amount-2";
            origin case_input;
        }
        assert not order_paid(entity_ref("urn:tutorial:order2")) {
            id "assert-unpaid-2";
            origin case_input;
        }
    }
    evaluate truth(total_due(entity_ref("urn:tutorial:ivanova"), 2000 KZT));
    expect truth_status == TRUE_ONLY;
    expect evaluation_status == COMPUTED;
}

The test name reads: “Two unpaid orders at 1,000 each — 2,000 due.”

Two orders at a thousand each gave a thousand through collect: the set of distinct values sees one value. Statics does not notice the difference — both records compile, both lower, and the undercount yields neither a refusal nor a warning: distinct_amounts_total(…, 2000 KZT) is simply NEITHER. The rule is simple: a charges total is always collect all with an entity in the generator; an entity count is collect. Guard the total with a test on two equal values, as here.

The generator’s second variable, o: CopyOrder, is not decoration: it is what tells apart two substitutions with an equal sum. Remove it and the compiler refuses: the name o in the condition is bound by nothing.

Count

rule OrderCount strict {
    for p: Person;
    when registered_reader(p);
    then order_count(p, count(collect o: CopyOrder where copy_order(o, p)));
}

rule UnpaidCount strict {
    for p: Person;
    when registered_reader(p);
    then unpaid_count(p, count(collect o: CopyOrder where copy_order(o, p) and unpaid_order(o)));
}

rule HeavyUser strict {
    for p: Person;
    when registered_reader(p) and count(collect o: CopyOrder where copy_order(o, p)) >= HEAVY_ORDERS;
    then heavy_user(p);
}

Orders	`order_count`	`unpaid_count`	`heavy_user`
three, one paid	`3`	`2`	`TRUE_ONLY`
two	`2`	—	`NEITHER`
none	`0`	`0`	`NEITHER`

count over an empty set is zero: “how many orders” is answered even when there are none. It is the only aggregate for which emptiness has a value.

An empty sum is not zero

Write a reader’s debt as one rule, without a guard:

rule NaiveTotal strict {
    for p: Person;
    when registered_reader(p);
    then naive_total(p, sum(collect all a: Money, o: CopyOrder where copy_order(o, p) and order_amount(o, a)));
}

Orders	`naive_total(Ivanova, 0 KZT)`	Document
none	`NEITHER`	`RUNTIME_ERROR`, issue `EMPTY_AGGREGATE`

An empty sum has neither a value nor a currency, and the core does not substitute zero: the rule fails, and the document of a reader without orders carries a runtime error. That is why TotalDue above stands under a count(…) > 0 guard — and the zero case, if the act provides for it, is written as a second rule:

rule TotalDueNothing strict {
    for p: Person;
    when registered_reader(p) and no_orders_confirmed(p) and count(collect o: CopyOrder where copy_order(o, p) and unpaid_order(o)) == 0;
    then total_due(p, 0 KZT);
}

Orders	`total_due(Ivanova, 0 KZT)`
none	`NEITHER`
none, the absence of orders confirmed by the cash desk	`TRUE_ONLY`

The first row is a legal choice, not a technical shortcoming. Missing order data does not mean there were no orders: the snapshot may be incomplete, the cash desk may not have sent the statement. Zero is an established fact, established either by a completeness confirmation, as here, or by a closure from the closed-world tutorial. Writing total_due(p, 0 KZT) from count(…) == 0 alone turns a gap in the evidence into a settled bill.

Average

average requires precision and a rounding mode explicitly: the mean of three sums is rarely representable.

rule AverageOrder strict {
    for p: Person;
    when registered_reader(p) and count(collect o: CopyOrder where copy_order(o, p)) > 0;
    then average_order(p, average(collect all a: Money, o: CopyOrder where copy_order(o, p) and order_amount(o, a), 2, "HALF_UP"));
}

Orders	`average_order`
1,000 and 1,500	`1250.00 KZT`
1,000, 1,000 and 1,500	`1166.67 KZT`

An aggregate waits for producers

TotalDue counts unpaid_order — a predicate that is derived, not fed. A sum’s value is correct only over a complete set: the aggregate cannot execute until all rules producing unpaid_order have run. The core guarantees this by stratification: enumerating a derived predicate is a completion edge, and the reader stands strictly above all producers. The author does not think about it until closing a loop: if unpaid_order itself reads total_due, the program cannot be ordered, and the compiler refuses — LDC-E4102.

The count(…) > 0 guard in TotalDue’s body is an exception from the same rule: a monotone aggregate guard does not shrink as the set grows, and the rule may repeat in the producers’ stratum. Reverse comparisons — count(…) == 0 in TotalDueNothing — stay a completion barrier.

Key on a computed head

total_due, order_count, average_order are declared with key(p): one value per reader. This is the corpus-wide convention for all heads an aggregate fills: if a total is fed as a case fact past the calculation, the discrepancy of two values becomes KEY_CONFLICT, not two true answers to one question.

Compiler refusals

A generator name is unbound — remove o: CopyOrder from TotalDue’s generator:

error LDC-E1317: имя "o" в generator-е comprehension §52.1 не связано ни
биндером правила, ни `let`, ни переменной самого comprehension и не
объявлено символом пакета — это свободная переменная (§188 unresolved
name)

The diagnostic reads: ‘name “o” in a comprehension generator is bound by neither the rule binder, nor let, nor the comprehension’s own variable, and is not declared as a package symbol — it is a free variable’.

A cycle through an aggregate — let UnpaidOrder read total_due:

error LDC-E4102: цикл предикатных зависимостей через unpaid_order →
total_due с ребром вида [status] — программа не стратифицируема
(§110/§191: циклам разрешены только monotone supported(P)-рёбра §65/§103)

The diagnostic reads: ‘a predicate-dependency cycle through unpaid_order → total_due with a [status]-kind edge — the program is not stratifiable: only monotone supported(P) edges are allowed to cycles’.

Both refusals belong to the language. But the collect versus collect all undercount and the empty sum are not compiler refusals — only a runtime test catches them.

The teaching archive has exhausted the core: facts, rules, negation, defeat, closure, tests, numbers, and aggregates. Next comes a real article of a real act: source and anchor.

The exercise for this page is /tutorials/exercise-aggregates/.

Documentation for Arxo. Writings — blog.arxo.io.

Anonymous visit counts on stats.arxo.io, no cookies.