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.

OverviewBoundariesCorpus formsPitfalls

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)

Show syntax reference

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

Grammar

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:

Grammar

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):

Grammar

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.

Arxo 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):

Output

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, defeasible rules, facts and evidence, negation and truth statuses, time.