Formula with physical quantities

Intention

I want to compute the work of a force while keeping the result dimension.

The scenes check 2 N × 3 m = 6 J; converting the result to m is rejected at evaluation.

Correct formFrozen execution sceneBoundary

Incorrect form and why it stays silent

Incorrect form

unit_convert(magnitude(2 N) * magnitude(3 m), "m")

pure function Work(force: Magnitude, distance: Magnitude) -> Magnitude = unit_convert(force * distance, "J");

Dimension and unit are checked at evaluation: the incorrect expression below yields RUNTIME_ERROR. A separate mutation shows an implementation defect: unit_convert inside a pure function is rejected with LDC-E2403, although conversion is defined as deterministic.

Correct form

Arxo Law

language "law.core" version "0.2";
package recipes.l.r12 version "0.1.0";
namespace "urn:recipe:l-calc:12";

unit m dimension Length scale 1 / 1;
unit N dimension Mass * Length / (Time * Time) scale 1 / 1;
unit J dimension Mass * Length * Length / (Time * Time) scale 1 / 1;
pure function Work(force: Magnitude, distance: Magnitude) -> Magnitude = force * distance;
relation measured(x: Magnitude);
rule Example strict { when true; then measured(unit_convert(magnitude(2 N) * magnitude(3 m), "J")); }

Frozen execution scene

Facts and choice	Question	Answer
1. two newtons over three metres	if scalar_of(unit_convert(Work(magnitude(2 N), magnitude(3 m)), "J") / magnitude(1 J)) == 6 / 1 then true else false	true / COMPUTED
2. zero displacement	if scalar_of(unit_convert(Work(magnitude(2 N), magnitude(0 m)), "J") / magnitude(1 J)) == 0 / 1 then true else false	true / COMPUTED
3. energy cannot be converted to length	unit_convert(magnitude(2 N) * magnitude(3 m), "m")	no value / RUNTIME_ERROR

two newtons over three metres

Arxo Law

test "two newtons over three metres" {
    given {
        context {
            legal_time @2026-09-13;
            decision_time @2026-09-13T09:00:00+05:00;
            knowledge_time @2026-09-13T09:00:00+05:00;
            timezone "Asia/Almaty";
        }

    }
    evaluate if scalar_of(unit_convert(Work(magnitude(2 N), magnitude(3 m)), "J") / magnitude(1 J)) == 6 / 1 then true else false;
    expect value == true;
    expect evaluation_status == COMPUTED;

}

zero displacement

Arxo Law

test "zero displacement" {
    given {
        context {
            legal_time @2026-09-13;
            decision_time @2026-09-13T09:00:00+05:00;
            knowledge_time @2026-09-13T09:00:00+05:00;
            timezone "Asia/Almaty";
        }

    }
    evaluate if scalar_of(unit_convert(Work(magnitude(2 N), magnitude(0 m)), "J") / magnitude(1 J)) == 0 / 1 then true else false;
    expect value == true;
    expect evaluation_status == COMPUTED;

}

energy not convertible to length

Arxo Law

test "energy not convertible to length" {
    given {
        context {
            legal_time @2026-09-13;
            decision_time @2026-09-13T09:00:00+05:00;
            knowledge_time @2026-09-13T09:00:00+05:00;
            timezone "Asia/Almaty";
        }

    }
    evaluate unit_convert(magnitude(2 N) * magnitude(3 m), "m");

    expect evaluation_status == RUNTIME_ERROR;
    expect issue(UNIT_DIMENSION_MISMATCH);
}

Counterfactual

Mutation: = force * distance; → = unit_convert(force * distance, "J");; expected LDC-E2403. Additional counterfactuals are shown as separate table rows.

A separate witness checks the absence of the required static rejection for a conversion known to be wrong at compile time. The executable rejection is already pinned by the last scene above; a passing static check does not prove this form correct.

Python

>>> import runpy
>>> checks = runpy.run_path("docs/recipes/l-calc/resources/check.py")
>>> checks["check_static_units"](https://github.com/arxohq/law/blob/master/docs/recipes/l-calc/12)
'ДЕФЕКТ lawc: статически известная ошибка единиц проходит check'

Boundary

The formula is work of a constant force along a displacement. It does not solve arbitrary equations and does not derive the premises of a physical model. For ordinary Quantity the product of two dimensioned quantities is undefined; Magnitude is used instead. A statically known wrong conversion or operation passes the static check but is rejected at evaluation. A unit_convert call inside a pure function is rejected (LDC-E2403); the formula stays pure and conversion is moved into the query.

Pitfall

Energy cannot be converted to length: the dimension check rejects it at evaluation.