docs← Back to article

Markdown for LLMs

Collections, aggregates, and data completeness

The source Markdown for this article. Copy it into your assistant or download it as a text file.

Download this articlePlain text ↗
# Collections, aggregates, and data completeness

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.

```law
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](/tutorials/negation/), requires an established negative
support: an "unpaid" mark, not a missing "paid" mark.

```law
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.

```law
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:

```law
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

```law
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:

```law
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**:

```law
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](/tutorials/closed-world/). 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.

```law
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:

```text
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`:

```text
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.

## Next

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](/tutorials/real-article-source/).

The exercise for this page is [/tutorials/exercise-aggregates/](/tutorials/exercise-aggregates/).