nb-15 solutions — Quantities and dimensions

← Back to lessonChapter 15 / 25 · Mathematics branch · Worked solution

How to verify

Checkable against law test packs/examples/language-demo/math02 (42 checked, 42 passed), law test packs/examples/language-demo/boundaries (21 checked, 21 passed), law engine check on the math02 package and on the frozen refusal snippets. Identifiers and code as written.

1. load_q(5 km) versus load_q(22 kW) for heavy_load()

Answer: 5 km gives TRUE_ONLY (melded scalar 5000/1); 22 kW gives NEITHER — no scalar is melded at all.

LoadScalar divides each reading’s magnitude by magnitude(1 m) and applies scalar_of: 5 km becomes the Rational 5000/1, which clears the (44/1) bar in HeavyLoad — the rule fires. For 22 kW the suite shows heavy_load() NEITHER but pins no load_scalar value itself; a scratch probe outside the suite settles it — truth(load_scalar(22/1)) given load_q(22 kW) returns NEITHER while load_q(22 m) returns TRUE_ONLY — so the metre-divisor meld accepted nothing (the silent UNIT_UNKNOWN mode from the article’s Limits). No rule derives heavy_load() and the status is NEITHER, not false. The suite’s test names say exactly this: scalar of five kilometres in metres versus load scalar below the threshold is not derived.

2. load_q(5 km) versus load_q(0.5 km) for long_trip()

Answer: 5 km clears it (5000 m ≥ 1000); 0.5 km does not (500 m < 1000). The explicit step is unit_convert(magnitude(q), "m") in TripLength.

The target unit "m" is written in the call — kilometres never meet the metre threshold until converted. 5 km converts to 5000 m (kilometres converted to metres, TRUE_ONLY); 0.5 km converts to 500 m (short trip fails the threshold, NEITHER). The judging rule LongTrip is identical in both cases; only the converted scalar differs.

3. The convert equality and its explicit factor

Answer: it establishes conv_ok() (TRUE_ONLY) — 1 km equals 1000 m — and the factor 1000/1 must appear because the engine performs no silent coercion.

convert(with_unit(1, "km"), 1000, 1, "m") re-expresses the value with a stated numerator and denominator; the equality against with_unit(1000, "m") then checks two explicitly constructed quantities. A bare 1 == 1000 comparison would be meaningless (and dimensionless); the factor in the call is what makes the claim checkable rather than assumed. Suite witness: the unit conversion by value ok line.

4. What the tag resolves tests add

Answer: they prove tag resolution works for locally declared units, not just the SI registry.

declared unit tag resolves (with_unit(5, "permit")) and derived tag resolves (with_unit(2, "permit_rate"), where permit_rate = permit / permit) run over unit permit = 1 declared in the boundaries package itself — no SI import involved. The SI-side tests prove registry conversion; these two prove the construct is general: any package can coin countable tags for non-physical things (permits, rates) and compare them the same way.

5. The temp02 refusal and the 0.2 alternative

Answer: refused with LDC-E2105 (undeclared) plus LDC-E2403 (computability not proved); a 0.2 modeller uses unit_convert, convert, quantity_of and with_unit.

temp_convert belongs to the 0.7 temperature profile, which this implementation (law 0.1.0, law.core/0.2) does not execute — so the checker reports the name unknown and the purity unprovable. angle_convert fails identically. The refusal is a fact about this profile, not about the language: stay inside the executable subset (the ConvOk/QBackOk/ExpoOk rules are the positive pattern) and leave newer-profile converters to nb-17.

How to verify

Terminal

law test packs/examples/language-demo/math02

Expected: мир demo.northbridge.math02, units.si, ok lines for scalar of five kilometres in metres, load scalar below the threshold is not derived, kilometres converted to metres, short trip fails the threshold, unit conversion by value; total 42 проверено, 42 прошли, 0 не прошли.

Terminal

law test packs/examples/language-demo/boundaries

Expected: ok lines declared unit tag resolves and derived tag resolves; total 21 проверено, 21 прошли, 0 не прошли.

Terminal

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

Expected: check OK.

Terminal

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

Expected: LDC-E2105 and LDC-E2403 (likewise for angle02.law.txt with angle_convert).