nb-15 — Quantities and dimensions

← Course mapChapter 15 / 25 · Mathematics branch

Math branch, needs beginner only (nb-01: First permit: facts, a rule and a question → nb-02: Why a missing fact is not a refusal → nb-03: Exceptions and conflicting rules → nb-04: The permit fee). All law is fictional; every depot, truck route and load record is synthetic and unofficial. No real municipal deployment or legal-validity claims. Engine law 0.1.0, semantics law.core/0.2.

Situation

Northbridge runs a depot scale for road-maintenance trucks. Two readings arrive on the same morning: truck A reports a trip length of 5 kilometres, truck B reports an axle load of 22 kilowatts of auxiliary draw. The clerk’s register has one threshold for “heavy load” (44, in metres of wire-equivalent test load) and one for “long trip” (1000 metres). The clerk asks two questions: is truck A heavy, and is either trip long? The trap is that the readings carry different dimensions — length versus power — and the numbers 5 and 22 mean nothing until each is reduced to a plain number in a named unit.

This article shows the 0.2 mechanism for that reduction. A reading such as 5 km is kept as one value — number glued to unit — until an explicit step converts it and reduces it to a plain number the threshold can judge. You will run that two-step chain for the heavy and long verdicts, then for conversions and custom unit tags. Each new term is introduced where it is first used.

Prerequisites

nb-01: First permit: facts, a rule and a question: facts, strict rules, truth statuses (TRUE_ONLY means established, NEITHER means established neither way), law test as the way to check a claim. nb-04: The permit fee: Money comparison against a threshold — the same shape as the scalar comparison here, but Money needs no conversion step.

New here: quantities with units, explicit conversion, and the two-rule meld/scalar chain — each introduced where it first appears below.

Minimal example

All fragments are excerpts: package header, imports and unrelated rules cut. Identifiers as written.

Excerpt 1 — the meld/scalar chain (from packs/examples/language-demo/math02/package.law, rules LoadScalar and HeavyLoad). A head computation derives a scalar relation from each quantity fact; a second rule compares the bare variable against a Rational threshold.

rule LoadScalar(q: Quantity) strict {
    when load_q(q);
    then load_scalar(scalar_of(magnitude(q) / magnitude(1 m)));
}
rule HeavyLoad strict {
    for v: Rational;
    when load_scalar(v)
        and v >= (44/1);
    then heavy_load();
}

Look at how the two rules divide the work. LoadScalar takes a Quantity fact — a number glued to a unit, such as 5 km — and computes a scalar relation from it in the rule head: magnitude(q) extracts the unit-carrying Magnitude, dividing by magnitude(1 m) forms a dimensionless ratio, and scalar_of turns that ratio into a plain Rational number such as 5000/1. The quantity never meets the threshold directly; it is first melded into load_scalar. HeavyLoad then compares that bare variable against the Rational threshold (44/1). Head computation plus bare-variable comparison: that pair is the meld/scalar chain.

Excerpt 2 — explicit conversion before the same two-step pattern (same file, rules TripLength and LongTrip):

rule TripLength strict {
    for q: Quantity;
    when load_q(q);
    then trip_length(scalar_of(unit_convert(magnitude(q), "m") / magnitude(1 m)));
}
rule LongTrip strict {
    for v: Rational;
    when trip_length(v)
        and v >= (1000/1);
    then long_trip();
}

Look at the head of TripLength: unit_convert(magnitude(q), "m") states the target unit out loud — kilometres become metres here, with no silent coercion. The rest is the same chain: scalar first, threshold second. The only difference from Excerpt 1 is that the conversion step is explicit in the call instead of implied by the divisor.

Excerpt 3 — quantities built from raw numbers (same file, rule ConvOk): with_unit attaches a tag, convert re-expresses the value, and the equality is checked, not assumed.

rule ConvOk strict {
    when convert(with_unit(1, "km"), 1000, 1, "m") == with_unit(1000, "m");
    then conv_ok();
}

Look at the single when line: with_unit builds a quantity from a raw number plus an explicit tag, convert re-expresses it with a stated factor (1000/1) and target tag, and the == checks the result instead of assuming it. 1 km converts to 1000 m only because both sides were constructed with stated units — the rule fires on the equality of two explicit constructions.

Excerpt 4 — custom unit tags resolve locally (from packs/examples/language-demo/boundaries/package.law, declarations plus rule PermitTagged):

unit permit = 1;
derived unit permit_rate = permit / permit;
rule PermitTagged strict {
    when with_unit(5, "permit") == with_unit(5, "permit");
    then permit_tagged();
}

Look at the declarations above the rule: unit permit = 1 coins a local tag, and derived unit permit_rate = permit / permit derives a rate tag from it. The rule then compares two with_unit quantities over the local tag. Units are not limited to the SI registry — a package can declare its own tags for countable non-physical things.

Command and result

law test packs/examples/language-demo/math02

Observed result (engine law 0.1.0) — the header names the pinned world, then 42 passing lines (seven shown, the rest cut for brevity):

law test demo.northbridge.math02: мир demo.northbridge.math02, units.si
  ok   [demo.northbridge.math02] tests/math02.lawtest / scalar of five kilometres in metres
  ok   [demo.northbridge.math02] tests/math02.lawtest / load scalar below the threshold is not derived
  ok   [demo.northbridge.math02] tests/math02.lawtest / kilometres converted to metres
  ok   [demo.northbridge.math02] tests/math02.lawtest / short trip fails the threshold
  ok   [demo.northbridge.math02] tests/math02.lawtest / unit conversion by value
  ok   [demo.northbridge.math02] tests/math02.lawtest / quantity returned into a unit
  ok   [demo.northbridge.math02] tests/math02.lawtest / unit exponent
итого: 42 проверено, 42 прошли, 0 не прошли, 0 не исполнены; код 0

All 42 answers matched their expectations — a passing suite, not a verdict on any truck. The Russian summary reads итого: 42 проверено, 42 прошли, 0 не прошли, 0 не исполнены; код 0 — 42 checked, 42 passed, 0 failed, 0 unexecuted, exit code 0. The header matters too: the world (мир) lists units.si explicitly, and the SI registry resolves only because that dependency is a pinned world member, not merely an import (see Limits). The boundaries package confirms the custom-tag side:

law test packs/examples/language-demo/boundaries

Observed — both tag tests pass inside a 21/21 green suite (итого: 21 проверено, 21 прошли, 0 не прошли, 0 не исполнены; код 0 — 21 checked, 21 passed, 0 failed, 0 unexecuted, exit code 0):

  ok   [demo.northbridge.boundaries] tests/boundaries.lawtest / declared unit tag resolves
  ok   [demo.northbridge.boundaries] tests/boundaries.lawtest / derived tag resolves
итого: 21 проверено, 21 прошли, 0 не прошли, 0 не исполнены; код 0

Both packages also pass the static check (check OK for each package.law), which confirms the sources are well-formed before any test runs:

law engine check packs/examples/language-demo/math02/package.law

Observed: check OK: packs/examples/language-demo/math02/package.law. The source is well-formed; the suite results above are its behavior.

Why this construct

The Quantity keeps number and unit inseparable, so bare numbers never meet thresholds. load_q(5 km) carries its dimension, and nothing compares it until the chain reduces it. The scalar of five kilometres in metres test derives heavy_load() from that fact (5000 ≥ 44).

Conversion states its target instead of guessing it. unit_convert(magnitude(q), "m") names "m" in the call, and convert(with_unit(1, "km"), 1000, 1, "m") names the factor too. The kilometres converted to metres and unit conversion by value tests confirm both with TRUE_ONLY.

The two-rule chain separates computing from judging, so one scalar serves several thresholds. LoadScalar feeds both HeavyLoad (≥ 44) and VeryHeavy (≥ 121): one meld, two verdicts. The five-kilometre test fires HeavyLoad through the shared load_scalar, while scalar capped above by the second threshold leaves very_heavy() NEITHER.

What LoadMax proves (and does not)

LoadMax is a separate clamped derivation: the quantity clamp: max yields scalar 120 test derives load_max(120/1) from load_q(120 kW). It is consumed by no rule, so it proves the clamp runs — not that any verdict reads it.

Custom tags cover non-physical dimensions: the depot counts permits the way metres count length. unit permit = 1 plus with_unit(5, "permit") gives the paperwork its own quantity system, confirmed by the two boundaries tag resolves tests above.

Why not a bare Integer with a comment?

A bare Integer fact plus a comment saying “metres” would pass every suite — and would also let a kilometre figure walk into a metre threshold unconverted. The suite cannot tell the comment is a lie. The Quantity type can, because the conversion step is code, not prose.

The evidence is the 42/42 suite, the 21/21 boundaries suite, and the two check OK runs — each executed above, none asserted in prose. What is not proven is that 44 is the right heaviness bar, or that wire metres are a sane proxy for truck load. The machine proves the declared arithmetic ran; Northbridge’s thresholds are fictional data, not engineering advice.

Changed condition

Feed load_q(5 km): LoadScalar melds it to 5000/1 and HeavyLoad fires — TRUE_ONLY (scalar of five kilometres in metres). Change the single fact to load_q(22 kW) and heavy_load() becomes NEITHER (load scalar below the threshold is not derived).

Note what the suite does not tell you here: no suite test pins load_scalar for a kW reading, so this NEITHER fits two stories — “melded to 22/1, below 44” and “the metre-divisor meld accepted nothing”. A scratch probe outside the suite settles the pair: load_q(22 kW) with the question load_scalar(22/1) returns NEITHER, while load_q(22 m) returns TRUE_ONLY. The second story wins — the silent-meld failure mode documented in Limits — so no threshold comparison ever runs for a kW reading.

The trip pair shows conversion doing the work. load_q(5 km) converts to 5000 m and clears the 1000 bar (kilometres converted to metres, TRUE_ONLY); load_q(0.5 km) converts to 500 m and stays NEITHER (short trip fails the threshold). Without unit_convert, the raw 5 and 0.5 could never meet a metre threshold honestly.

Typical mistake

The mistake is reaching past the 0.2 shelf for a converter from a newer profile — temperature conversion temp_convert (0.7) inside a 0.2 package:

law engine check packs/examples/language-demo/boundaries/evidence/snippets/temp02.law.txt

Observed:

packs/examples/language-demo/boundaries/evidence/snippets/temp02.law.txt:4:10: error LDC-E2403: COMPUTABILITY_NOT_PROVED (LDC-E2403): function "f" не доказана как PURE_DETERMINISTIC: вызов "temp_convert" не имеет доступного effect descriptor (imported/unknown dependency) (§46/§47.5)
packs/examples/language-demo/boundaries/evidence/snippets/temp02.law.txt:4:39: error LDC-E2105: функция "temp_convert" не объявлена (ни в файле, ни в std v1-списке)

The snippet is a four-line probe (function f(x: Rational) -> Rational = temp_convert(x, "absolute", "C", "K");); the engine refuses it twice over — unknown name (LDC-E2105, “not declared”) and unprovable purity (LDC-E2403, “not proved PURE_DETERMINISTIC”). The angle converter fails identically (angle02.law.txt: angle_convert, same two codes).

The fix is to model the quantity with the tools that execute (unit_convert, convert, with_unit), and to treat anything else as a job for nb-17: Numeric families and support boundaries’ profiles, not a silent approximation here. Rule of thumb: if the conversion is not in the 0.2 executable subset, the honest answer is a refusal at check time.

Limits

SI resolution needs explicit world membership. Importing units.si is not enough: it must also be pinned in the test world (the suite header shows it). The package source documents the failure mode — without it, magnitude()/unit_convert() hit UNIT_UNKNOWN and the rules go silently NEITHER. That silence is a recorded open issue of this build, not a verdict on the data.

Computation runs in heads only. magnitude(), scalar_of() and unit_convert() run in rule heads and conditions (the meld pattern); the std catalog marks them not callable from pure functions (function_callable=false, LDC-E2403). Per the package source comment, that is a refusal of this implementation’s purity checker, never a language-wide inability claim.

The boundaries are profile facts. LDC-E2105/LDC-E2403 on temp_convert, angle_convert (0.7), exact_sqrt (0.4), fx_convert and solve_linear describe this implementation (law 0.1.0, semantics law.core/0.2), never the language in general. What refuses here may execute under its own profile in nb-17: Numeric families and support boundaries.

Derived equality is derivation-sensitive. with_unit(5, "permit") == with_unit(5, "permit") holds for identical constructions; equality of computed quantities follows the same derivation rules as bounds (nb-16: Exact computation and proven bounds). This article proves local construction, not a general quantity algebra.

Exercise

Without running the engine, predict, then check with the commands above:

load_q(5 km) versus load_q(22 kW): which truth status does heavy_load() get for each, and which melded scalar feeds the comparison in each case, if any?
load_q(5 km) versus load_q(0.5 km): which clears long_trip(), and which explicit call performs the kilometre-to-metre step?
What does convert(with_unit(1, "km"), 1000, 1, "m") == with_unit(1000, "m") establish, and why must the factor appear in the call?
What do the two boundaries tag resolves tests prove that the SI tests do not?
What does law engine check report for the temp02 snippet, with which two codes — and what must a 0.2 modeller use instead?

Write down each prediction first; run the commands; explain any miss in one sentence. Check your work against the full solution: melded scalars, conversions, tags and refusal codes.

Sources

Source: packs/examples/language-demo/math02/package.law (rules LoadScalar, HeavyLoad, VeryHeavy, TripLength, LongTrip, LoadMax, ConvOk, QBackOk, ExpoOk)
Tests: packs/examples/language-demo/math02/tests/math02.lawtest (42 tests, including the meld/scalar, conversion and clamp cases)
Source: packs/examples/language-demo/boundaries/package.law (unit/derived §49.2: unit permit, permit_rate, rules PermitTagged, RateTagged)
Refusals: packs/examples/language-demo/boundaries/evidence/snippets/temp02.law.txt (temp_convert, 0.7), angle02.law.txt (angle_convert, 0.7)
Suite tour: packs/examples/language-demo/README.md
Prerequisite: nb-01: First permit: facts, a rule and a question, nb-04: The permit fee; next: nb-16: Exact computation and proven bounds

Three levels:

Northbridge use (this article): the depot scale reduces every reading to a scalar in a named unit before any threshold applies — 5 km melds to 5000 and counts as heavy and long, while 22 kW leaves heavy_load() NEITHER with no melded scalar pinned by the suite (see Changed condition) — verified by the 42/42 math02 suite header and the named ok lines above.
Domain template: whenever a regime gates on measured values, keep number and unit glued until the last step; convert with an explicit target and factor; compute the scalar in one rule and judge it in another so several thresholds share one meld; declare local tags for countable non-physical things. Never compare a raw number against a threshold that has a unit.
Confirmed example elsewhere: the boundaries package replays the same with_unit mechanism over locally declared tags (permit, permit_rate) — the 21/21 suite with both tag resolves lines green — proving tag resolution is a property of the construct, not of the SI registry. And the frozen temp02/angle02 refusal slices prove the same boundary from the other side: converters outside the 0.2 subset are refused loudly at check time rather than approximated silently.
Confirmed external formalization (corpus): GloBE Pillar Two thresholds and entity summary (OECD, international) — package oecd.globe_etr, corpus/laws/org/oecd/globe-etr/package.law:45-52: three act thresholds as argument-free functions — the rate is Decimal, the thresholds are Money of the same kind as the compared sums (comparison requires kind agreement) — with the charge aggregate below as sum all amount: Money for ce ..., always collect all, never collect. Evidence: docs/research/constructs/21-expressions-quantities/corpus-forms.en.md §2 (rated exemplary). Limit of verification: presence of the named construct at the cited lines only, confirmed by direct file read; no claim about deployment, runtime behaviour, or legal correctness.

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

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