Markdown for LLMs

Expressions and quantities: const, function, arithmetic, aggregates

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

# Expressions and quantities: const, function, arithmetic, aggregates

**In one sentence:** these constructs answer the
question "how to compute a value without leaving the norm", with no external
computation. Take them when a norm needs a number and a measure: a named value
(`const`), a named computation (`function`), a threshold and a rate (comparison
and arithmetic), a unit and a dimension (magnitudes), a summary
over a set (aggregates) and explicit rounding (`round`/`div_round`).

Values are computed inside the norm: named constants and functions, exact arithmetic over quantities, and explicit rounding — no silent conversions.

## 1. When to take it and when not to

| Instead of | Selection rule |
|---|---|
| Expression vs judgment | A threshold in the body (`n >= 10`) is an expression over data: the machine computes. A disputable reading of a norm ("manifestly excessive", "good cause") is the judgment channel: a human decides, the machine awaits the verdict. A number is an expression, an assessment is a judgment |
| `round` vs `div_round` | Rounding a finished value — `round(v, precision, mode)`. Division with rounding — `div_round(a, b, precision, mode)` as one operation over the exact quotient, not a composition of two: `round(x / y, …)` fails with `INEXACT_DIVISION` before `round` ever sees it |
| `collect` vs `collect all` | Counting entities — `collect` (`Set`, distinct values). Summarizing charges — always `collect all` (`List`, positions): two equal incomes in a `Set` are one element, and `sum` silently undercounts. Statics cannot see the difference — guard it with a test on two equal facts |
| `const` vs case fact | Program immutables (rate, threshold, benchmark) — `const`. Mutable legal facts are `assert` with `origin`, not a constant: case facts are not modelled with `const` |

## Grammar: comparisons, quantifiers, collections (EBNF verbatim from the grammar)

Comparisons are a formula conjunct (`==`/`!=` only in formulas; `in` removed, unary `!` removed):

```ebnf
comparison              = relational_expression,
                          comparison_operator,
                          relational_expression ;
comparison_operator     = relational_operator | "==" | "!=" ;
relational_expression   = additive_expression,
                          [ relational_operator, additive_expression ] ;
(* Errata E-0070: оператор `in` снят из relational_operator — членство
   выражается квантором `exists … in … where` §52; парсер формы не разбирал. *)
relational_operator     = "<" | "<=" | ">" | ">=" ;
additive_expression     = multiplicative_expression,
                          { ( "+" | "-" ), multiplicative_expression } ;
multiplicative_expression
                        = unary_expression,
                          { ( "*" | "/" | "mod" ), unary_expression } ;
(* Errata E-0070: унарный `!` снят — отрицание пишется словом `not`
   (proposition) либо инверсией сравнения; лексер `!` вне `!=` отвергает. *)
unary_expression        = [ "+" | "-" ], postfix_expression ;
```

Quantifiers over a collection:

```ebnf
quantifier              = existential_quantifier | universal_quantifier ;
existential_quantifier  = "exists", identifier, "in", expression,
                          "where", formula ;
universal_quantifier    = "forall", identifier, "in", expression,
                          "satisfies", formula ;
```

Collections — `collect` (`Set`) and `collect all` (`List`):

```ebnf
comprehension_expression
                        = "collect", [ "all" ], identifier, ":", type_ref,
                          { ",", identifier, ":", type_ref },
                          "where", formula ;
```
## 2. Minimal example

Package `research.expressions.rounded_share`: a rate constant, a percent and explicit
rounding. Salary 100 000 KZT, bonus — a quarter under `HALF_UP`, monthly
share — a twelfth under the policy.

```law
const BONUS_RATE: Decimal = 25 percent;

rule Bonus strict {
    for e: Employee; for s: Money;
    when salary(e, s);
    then bonus(e, round(s * BONUS_RATE, 2, "HALF_UP"));
}

rule MonthlyShare strict {
    for e: Employee; for s: Money;
    when salary(e, s);
    then monthly_share(e, div_round(s, 12.0, 2, "HALF_UP"));
}
```

Case facts: `salary(urn:case:research:expressions:ali, 100000 KZT)` with
`origin case_input`. Query: `evaluate truth(bonus(…, 25000 KZT))`.

Observed engine answer (installed `law`, semantics `law.core/0.2`):

```text
law test research.expressions.rounded_share: мир research.expressions.rounded_share
  ok   [research.expressions.rounded_share#authored] tests/01-bonus-computed.lawtest / urn:query:research-expressions-01
  ok   [research.expressions.rounded_share#authored] tests/02-no-salary.lawtest / urn:query:research-expressions-02
итого: 2 проверено, 2 прошли, 0 не прошли, 0 не исполнены; код 0
```

`law engine check` — `check OK`, no warnings. Sensitivity:
removing the `salary` fact changes the expectation from `TRUE_ONLY` to `NEITHER`
(`tests/02-no-salary.lawtest`) — the example is not vacuous.

Nearest wrong outcome (verified by reading the dividend table): divisor `12` instead of `12.0` — `Money / Integer` is not
in the dividend table, statics answer `LDC-E2108`. The reverse would be the
mistake: expecting the integer to silently "promote" to decimal — there are no
implicit conversions.

## 3. Example by domain

- **Law:** England-and-Wales intestacy (package `gb.statute.administration_of_estates_act_1925`, England and Wales) —
  function `fixed_net_sum() -> Money = FixedNetSum`: an A3 parameter read with
  a witness at every use; nearby — the norm's exact fraction
  `(v - c - sum) * (1 / 2)` (see `corpus-forms.md`).
- **Standard/protocol:** the SI unit dictionary (package `units.si`, units pack) — `pub unit kg dimension
  Mass scale 1 / 1`: the unit dictionary all magnitude
  arithmetic rests on; conversion — only `convert`, tag attachment — `with_unit`.
- **Religion:** zakat on money (package `fiqh.zakat`, Islamic jurisprudence) —
  `div_round(w, 40.0, 2, "HALF_UP")`: one fortieth as explicit division under
  a policy, not the `w * 0.025` approximation.
- **Science:** medication ordering (package `med.medication_order`, medical corpus) — `const
  MillilitreEdinitsa: Quantity = 1 ml`: a named benchmark making the
  "volume → dimensionless number" transition explicit; the rule below multiplies a dose
  by a counter `n * q` (`Integer * Quantity`).
- **Teaching case:** `research.expressions.counted_threshold` — the same device in
  miniature: the `FULL_CREW` threshold as `const`, the `count(collect …) >=
  FULL_CREW` guard in the body, the `sum(collect all …)` summary over positions;
  three equal 50 000 KZT payouts guard the silent-undercount trap.

## 4. How the engine answers

Table — observed runs of this directory's examples (installed `law`,
semantics `law.core/0.2`):

| Facts | Question | Answer | Why |
|---|---|---|---|
| `salary(ali, 100000 KZT)` | `bonus(ali, 25000 KZT)` | `TRUE_ONLY` | `100000 × 0.25` exact, `round` under `HALF_UP` |
| no facts | `bonus(ali, 25000 KZT)` | `NEITHER` | `salary` premise not established; the expression does not invent the base |
| `salary(ali, 100000 KZT)` | `monthly_share(ali, 8333.33 KZT)` | `TRUE_ONLY` | `div_round(s, 12.0, 2, "HALF_UP")` — one operation over the exact quotient |
| three members, payouts 3 × 50000 | `crew_bonus(crew1)` | `TRUE_ONLY` | `count == 3 >= FULL_CREW` |
| two members | `crew_bonus(crew1)` | `NEITHER` | `count >= 3` guard false; below threshold — silence |

- In `proof` a term value is published computed: the result stands there
  (`25000 KZT`), not the expression tree; argument supports enter the
  rule-application proof.
- In `why_not` an unfired guard gives `NEITHER`: the expression does not name
  the silence cause — it names the missing premise.
- The `monthly_share(ali, 8333.33 KZT)` line was separately verified on a scratch
  copy of the package (same `law test`, a third trial file, 3/3): `100000 / 12 =
  8333.333…`, `HALF_UP` at two places gives `8333.33`. The trial is not in the
  shipment — it adds no sensitivity to the example.
- The `crew_payroll` summary is crew-sensitive in the same order:
  removing a member removes their payout from `collect all`, and the previously true
  total becomes `NEITHER` — the summary does not "remember" the departed.
- Execution refusals (`TYPE_ERROR`, `CURRENCY_MISMATCH`, `INEXACT_DIVISION`,
  `DIVISION_BY_ZERO`, `EMPTY_AGGREGATE`) are presented as case issues, not as
  a whole-conclusion refusal: the rule does not fire, the rest continue.
- `BOTH` in an `if`-term condition gives `CONFLICTED_CONDITION`, `NEITHER` —
  keeps missing/external issues and picks no branch.

Outcomes (earlier scenarios):

| Facts | Question | Answer | Why |
|---|---|---|---|
| two incomes of 100,000 each | `household_income(h, 200 000 KZT)` | `TRUE_ONLY` | `collect all` — two positions |
| same | `household_income_distinct(h, 100 000 KZT)` | `TRUE_ONLY` | `collect` — one value |
| same | `household_income_distinct(h, 200 000 KZT)` | `NEITHER` | silent undercount: neither refusal nor warning |
| two members | `household_size(h, 2)`; `member_share(h, a, 1 / 2)`; `half_share(h, a)` | `TRUE_ONLY` | `count`; `1 / 2` and `2 / 4` are one `Rational` |
| tenure 12 / 3 | `senior(a)` / `senior(b)` | `TRUE_ONLY` / `NEITHER` | guard `n >= 10`; below threshold — silence |
| `grade(a, Senior)`; tenure 12 | `senior_by_grade(a)`; `even_years(a)` | `TRUE_ONLY` | member equality; `12 mod 2 == 0` |
| signature `23:01+01:00` | `signed_at_moment(a)` | `TRUE_ONLY` | guard `== 22:01Z` — the same moment |
| salary 100,000 | `bonus(a, 25 000 KZT)`; `monthly_salary(a, 8 333.33 KZT)` | `TRUE_ONLY` | `round`, `div_round` under `HALF_UP` |
| `a` is senior | `any_member_senior(h)` / `all_members_senior(h)` | `TRUE_ONLY` / `NEITHER` | `exists` / `forall` over `collect` |
| member `c` with no income | `household_income(h2, 0 KZT)` | `RUNTIME_ERROR` | `EMPTY_AGGREGATE`: an empty sum is not zero |

A term value is asked with a `DATA` query (`evaluate -7 mod 3` → `2`, Euclidean remainder; `evaluate 7 / 2` → `Rational 7/2`); refusals — with an `expect issue(CODE)` observation (`CURRENCY_MISMATCH`, `INEXACT_DIVISION`, `DIVISION_BY_ZERO`, `TYPE_ERROR`).

Money, shares, and functional lookup — the second half of the earlier expression scenarios (every row below is a documented outcome):

| Term / facts | Question | Answer | Why (test) |
|---|---|---|---|
| — | `pow(2, 10) + abs(-24) + min(3, 5)` | DATA `1051` | std terms ("power, absolute, minimum") |
| — | `100 KZT * (1 / 4) + div_round(100 KZT, 3.0, 2, "HALF_UP")` | DATA `58.33 KZT` | exact share plus division under a policy ("money for a share under a policy") |
| — | `7 / 2` | DATA `Rational 7/2`, no `INEXACT_DIVISION` | exact fraction ("7 / 2 is an exact Rational") |
| — | `1 + 1 / 2` | `TYPE_ERROR` | counter and share do not add ("Integer + Rational") |
| — | `1000 KZT + 5 USD`, `100 KZT / 5 USD` | `CURRENCY_MISMATCH` | different currencies ("money in different currencies" ×2) |
| — | `100 KZT / 3.0`, `100 KZT * (1 / 3)` | `INEXACT_DIVISION` | inexact quotient without a policy ("Money / Decimal inexact", "Money * Rational inexact") |
| — | `15 mg / 1 mg` | DATA `15.0` | same-unit share ("Quantity of one unit") |
| — | `15 mg / 1 kg` | `TYPE_ERROR` | different units ("Quantities of different units") |
| — | `7 mod 0` | `DIVISION_BY_ZERO` | zero ("mod by zero") |
| — | `250 KZT / 1000 KZT` | DATA `0.25` — a share, not money | ("Money / Money of one currency is a share") |
| — | `25 percent` | DATA exact `Decimal 0.25` | ("percent is an exact Decimal") |
| — | `convert(...)` | DATA `3000 m` | conversion only by explicit conversion ("convert is explicit conversion") |
| — | `let`/`if`/`match` | DATA (e.g. `6`) | layers and analysis ("let and if are expressions", "layers through let") |
| salary/fund | `prorated_salary`, `salary_per_worked_month`, `two_thirds_of_salary`, `member_bonus` | `TRUE_ONLY` | one rounding over the exact result ("months out of twelve", "variable divisor", "two thirds", "same proportion") |
| head + income | `head_income` | `TRUE_ONLY` | the set's single value ("only: the head's single income") |
| head + two incomes | `head_income` | `NEITHER`, `RUNTIME_ERROR` | two distinct values — conflict, not choice ("only: two distinct values") |

## 5. Common mistakes

1. Summarizing charges via `collect` instead of `collect all` — silent
   undercount on equal values (`pitfalls.md`, item 1).
2. Dividing money by a whole number (`div_round(s, 12, …)`) — `LDC-E2108`
   (`pitfalls.md`, item 4).
3. `round` without `precision`/`mode` — `LDC-E2116`; percent of type `Percentage`
   instead of `Decimal` — `LDC-E2101` (`pitfalls.md`, item 5).
4. Mixing currencies and units (`1000 KZT + 5 USD`, `500 kg > 100 m`) — `check`
   stays silent, execution answers `CURRENCY_MISMATCH`/`TYPE_ERROR`
   (`pitfalls.md`, item 6).
5. Double rounding (`round` over a `div_round` total) — divergence from
   the norm (`pitfalls.md`, item 8).
6. Bare domain constant in a term — `LDC-E1330`, constant cycle —
   `CYCLIC_CONSTANT` (`pitfalls.md`, items 9–10).

## 6. References

- Neighbouring pages: [strict rules](/constructs/rule-strict/),
  [defeasible rules](/constructs/rule-defeasible-unless/),
  [facts and evidence](/constructs/facts-and-evidence/),
  [negation and truth statuses](/constructs/negation-and-status/),
  [time](/constructs/time/).