Numerical semantics — REAL = ℝ and the Representation Boundary¶

Audience: developer who wants to understand why LoLa's REAL is not a float type, what the numerical assurance chain does, and when a mathematical proof is sufficient vs. when a numerical error bound is needed.\ Language Reference: §13 REAL semantics, §17 Profiles.\ How-to: Configure REAL representation.

The core choice: REAL = ℝ¶

LoLa's REAL and LREAL are mathematical real numbers, not machine floats.

This is not a naming convention or a simplification. It is a deliberate proof-theoretic choice with consequences throughout the compiler:

Z3 reasons in the ℝ sort: exact, without rounding, without NaN or Inf.
Algebraic identities (x/100 * 1000 = 10x) hold without qualification.
An INVARIANT s >= -1.0 is a theorem about ℝ, valid for every s ∈ ℝ.
The proof is independent of which machine type s will eventually be stored in.

The alternative — equating REAL = Float64 at the type level — would mean:

Every proof must reason in IEEE 754 arithmetic: non-associative, with NaN/Inf, with the identity 0.1 + 0.2 ≠ 0.3.
Z3's REAL sort (exact ℝ) cannot be used for REAL variables.
Simple expressions like (a + b) * c and a*c + b*c would require a Gappa proof to be equated.
The invariant s >= -1.0 would be false for any computation that produces -∞ or NaN.

The mathematical semantics is more fundamental and more useful for the verification task. Machine arithmetic is a representation chosen for deployment, not the meaning of the programme.

Three levels that must not be confused¶

Level	What lives here	LoLa tool
A — Mathematical domain (ℝ)	Variables, invariants, contracts	Z3 (REAL sort)
B — Machine arithmetic	Float32, Float64, Fixed-point values	Gappa
C — Physical quantisation	Sensor noise, ADC resolution, timing jitter	Declared assumptions in `.toml`

A Float64 rounding error is ≈ 2×10⁻¹⁶. A typical industrial sensor has ±0.1% error ≈ 10⁻³. An ADC quantisation step is 2⁻¹² ≈ 2.4×10⁻⁴. These are four orders of magnitude apart and come from completely different sources. Mixing them into a single number produces a meaningless bound. The numerical assurance chain keeps them separate and accounts for each contribution explicitly.

The Representation Boundary¶

A Representation Boundary is the explicit point where a mathematical REAL value is assigned a machine type. It requires a proof obligation:

∀ x ∈ [lo, hi] : |repr(x) − x| ≤ ε  ∧  finite(repr(x))

LoLa places Representation Boundaries: - At the output of the block (mathematical result → machine storage) - At inputs (machine sensor value → REAL variable; the gap is declared as a [physical_errors] assumption)

Before the boundary, all algebraic identities of ℝ hold. After it, no simplification is valid without a new Gappa proof.

In the source language, the boundary is declared by profile or project file, not by type annotation: - --profile float64 or [representation] real = "float64" in a project TOML sets Float64 as the representation for all REAL/LREAL variables. - Without a boundary, the compiler verifies the programme mathematically but refuses to emit code — the gap between ℝ and any machine type is unaccounted for.

This fail-closed default prevents silent promotion of mathematical proofs as machine guarantees.

What the numerical assurance chain computes¶

The numerical assurance chain answers: given a declared deployment, how far can the machine implementation deviate from the mathematical specification over time?

The answer is a bound E_N (for N-step trajectories) and E_∞ (steady-state), composed from three separate error sources:

Machine roundoff (ε_m)¶

The per-step error introduced by performing the mathematical computation in Float64 instead of ℝ. Computed (or bounded) by Gappa. For most process-control computations, ε_m ≈ 10⁻¹⁶ — negligible compared to other sources.

Physical input error (ε_p)¶

Declared in [physical_errors] as an engineering assumption. Represents the difference between the value the sensor reports and the true physical quantity. Not a mathematical theorem — a declared specification of the physical world.

Discretisation and jitter (ε_d, ε_j)¶

The error introduced by replacing a continuous ODE with a discrete update rule (Forward Euler, Runge-Kutta, etc.) and by imperfect timing (the actual scan period differs from the nominal). Requires a CONTINUOUS_REFERENCE block declaring the ODE and [sampling.*] fields declaring the deployment parameters.

Trajectory composition¶

Per-step errors compose through the system's Lipschitz constant:

E_N = ε_combined · (L^N − 1) / (L − 1)    [contractive: L < 1]
E_∞ = ε_combined / (1 − L)                 [steady-state bound]

For a contractive system (filter, controller with feedback), E_∞ is finite. For a marginally stable system, the bound grows without limit — a correct warning that the deployment is sensitive to numerical precision.

Provenance: what the bound actually guarantees¶

The E_∞ bound is proved-under-assumptions: it is mathematically derived given the declared assumptions about the deployment. The assumptions are:

[physical_errors] values — sensor specifications, not measured facts
[sampling.*] period and jitter — deployment declarations, not hardware proofs
[sampling.*] input_derivatives] — physical input trajectory assumptions

A bound with proved-under-assumptions provenance is only as strong as the declared assumptions. If the sensor truly has ±1% error but you declared ±0.1%, the bound is wrong. The Engineering Error Report makes this explicit: every declared assumption is listed under "Declared assumptions", and the overall provenance ceiling is the weakest link.

The correct reading of E_∞ = 0.27 is: "If the declared assumptions hold, then with mathematical certainty, |s_machine − s_exact| ≤ 0.27 at all times."

Why Float64 is usually sufficient, but not always¶

Float64 machine epsilon ≈ 2.2×10⁻¹⁶ is typically negligible next to physical sensor errors and discretisation errors. For most process-automation tasks, Float64 roundoff is not the limiting factor in the error budget.

However, Float64 is not sufficient for: - Long accumulation chains (integrators running for millions of cycles) where roundoff accumulates - Cancellation-prone expressions (subtracting two nearly-equal large values) - Algorithms designed for higher precision

The Engineering Error Report makes this visible: if ε_m is the dominant term, the representation needs attention. If ε_j (jitter) dominates, tighter timing hardware or a different control design may be more effective than changing the numeric type.

LREAL vs. REAL¶

Both are mathematical ℝ until a Representation Boundary. At the boundary:

LREAL — minimum representation is Float64. Lowers to f64 (Rust), LREAL (IEC 61131-3 ST).
REAL — minimum representation is Float32 (though Float64 is preferred for 64-bit targets). In the current implementation, both lower to Float64 when --profile float64 is active.

The distinction is a compiler hint about minimum acceptable precision, not a semantic difference. A programme proven over ℝ is equally correct for REAL and LREAL.