nb-17 solutions — Numeric families and support boundaries

← Back to lessonChapter 17 / 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) and law engine check over the frozen slices in packs/examples/language-demo/boundaries/evidence/snippets/. Tool law 0.1.0, language 0.2, semantics law.core/0.2, std 0.2.0. Identifiers and code as written.

1. sqrt_self() versus sqrt_x()

Answer: sqrt_self() is TRUE_ONLY; sqrt_x() is NEITHER. The left-hand sides are identical calls; the right-hand sides differ — self versus a foreign derivation.

SqrtSelf compares sqrt_bounds(4, "p8/0.1") with the textually identical call: same derivation, same certificate, so the equality holds and the rule fires. SqrtX compares the same call with bounds_const(2, 1), a hand-written constant with a different derivation: the digits may look right, but the bounds surface compares derivations, not digits, so nothing fires and the status is NEITHER (established neither way), not false. The suite pins both: bounds root is deterministic expects TRUE_ONLY, bounds root: foreign derivation is unequal expects NEITHER.

2. cert_cross(): status and evaluation pair

Answer: truth status NEITHER, evaluation status COMPUTED. Both sides computed successfully; the derivations are unequal.

CertCross compares sin_bounds(0, "p8/0.1") with sin_bounds(0, "p16/0.1"). A different profile name means a different certificate and therefore a different derivation, so the equality does not hold — no rule fires, hence NEITHER. COMPUTED matters: it says the engine really evaluated both certified calls and then compared, as opposed to refusing or missing input. The pair “NEITHER + COMPUTED” is the honest cross-certificate answer: executed, compared, not equal. (The p32-self probe in the article’s Changed condition replays the mirror image step by step and returns TRUE_ONLY, 43 of 43: any profile equals itself.)

3. The two codes over sqrt02.law.txt

Answer: LDC-E2403 first (line 4, column 10), then LDC-E2105 (line 4, column 39). E2403 names the exact-semantics layer, E2105 the implementation-support layer.

E2403 (COMPUTABILITY_NOT_PROVED) says function f is not proved PURE_DETERMINISTIC because the call exact_sqrt has no available effect descriptor — the exact law.core/0.2 semantics cannot vouch for it. E2105 says exact_sqrt is not declared, neither in the file nor in the std v1-list — this build’s support list simply lacks the name. Order in the output is E2403 then E2105 (column 10 before column 39). Neither code touches the language-version layer (the header is plain 0.2, accepted) or claims the name is unusable in the language in general.

4. The code over v04.law.txt

Answer: LDC-E1401 (language version “0.4” unsupported). It claims nothing about the 0.4 language in general.

E1401 fires at the version layer, before any name lookup: tool law 0.1.0 implements no 0.4 semantics. The attached migration report (§266.1) names 0.1 [withdrawn] and 0.2 [supported] with revisions 0.2.1–0.2.4 — it is a statement about what this build reads, not a judgment that 0.4 content is meaningless. A newer tool with a 0.4 implementation would pass this layer; the refusal is build-relative, never language-wide.

5. fx_convert versus DoubleIt-in-condition

Answer: fx02 reports E2403 + E2105 (both layers); query02 reports E2105 alone (support layer only). fx_convert needs a newer std/profile with the name declared and an effect descriptor (support + semantics layers); the query-as-term needs the language to ever admit queries as terms — a language-design change, not a version bump.

fx_convert fails exactly like exact_sqrt: undeclared name (E2105, implementation support) plus no effect descriptor (E2403, exact semantics). Executing it would require a profile whose std v1-list declares it and whose semantics proves it computable — two layers, both outside law 0.1.0 / law.core/0.2. DoubleIt in condition position fails only E2105 (a query declaration is not a term and is not in any callable list), with no E2403 attached: there is no unknown effect to complain about, only a category error (see nb-14). No tool version, language version bump, or std release within this design makes a query declaration a term — that would be a different language rule, so the fix sits outside all five layers as drawn.

How to verify

Terminal

law --version

Expected: law 0.1.0, семантика: law.core/0.2, std для языка 0.2: 0.2.0.

Terminal

law test packs/examples/language-demo/math02

Expected: итого: 42 проверено, 42 прошли, 0 не прошли, 0 не исполнены.

Terminal

law test packs/examples/language-demo/boundaries

Expected: итого: 21 проверено, 21 прошли, 0 не прошли, 0 не исполнены.

Terminal

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

Expected: LDC-E2403 (column 10, exact_sqrt … no effect descriptor) and LDC-E2105 (column 39, exact_sqrt … not declared).

Terminal

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

Expected: the same LDC-E2403 + LDC-E2105 pair for solve_linear.

Terminal

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

Expected: LDC-E1401 (версия языка "0.4" не поддерживается) with the §266.1 migration report.

Terminal

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

Expected: LDC-E2105 alone (функция "DoubleIt" не объявлена), no LDC-E2403.