Effective Rounding in Tensor Semantics #
This example uses the same shape-indexed tensor operation twice. The FP32 tensor gives the
proof-oriented rounded-real semantics. The ExecFloat.Binary 8 23 tensor executes binary32
arithmetic from
bits. On a finite result, the IEEE bridge and the effective rounding calculation identify the
same canonical mantissa and exponent.
Vector length; four entries is enough to show the pointwise behaviour without a wall of output.
Instances For
The shape shared by every tensor in this example.
Instances For
Executable binary32 tensors used by the example.
Instances For
The constant 2, given by its bit pattern 0x40000000 so no decimal parsing is involved.
Instances For
This addition executes pointwise in the bit-level IEEE32 model.
Instances For
Proof-oriented tensors use the same tensor API with rounded-real FP32 scalars.
Instances For
The rounded-real counterpart of 2. Exactly representable, so rounding is the identity here.
Instances For
A vector of ones in the proof-oriented model.
Instances For
A vector of twos in the proof-oriented model.
Instances For
Their sum, computed by the same addSpec the executable tensors use. The two models share the
tensor
API and differ only in the scalar type, which is what makes the comparison below meaningful.
Instances For
Every proof-oriented tensor entry exposes the effective nearest-even representation.
Every executable tensor entry reaches the same effective representation once finiteness is checked. The finiteness premise is discharged by computation for the concrete $1+2$ example.
Exact subtraction, local spacing, and absorption #
Sterbenz's lemma certifies the concrete binary32 subtraction $2-1$ as exact.
The corresponding executable binary32 operation denotes the exact real subtraction.
The decoded significand at 1.0 has scale 2^-23, its binary32 spacing.
The computed exponent therefore denotes the mathematical ULP at 1.0.
Infinity has no finite dyadic significand or scale.
Adding the smallest positive subnormal does not change executable binary32 1.0.
The executable absorption result transports to the rounded-real binary32 specification.
Named rounding modes and fused enclosures #
The public mode API avoids passing a raw integer-rounding function at each call site.
Instances For
Directed rounding gives a certified lower endpoint, not merely a differently named value.
A concrete fused multiply-add lower endpoint, computed directly from binary32 inputs.
Instances For
The corresponding upper endpoint.
Instances For
The executable directed FMA endpoints enclose the exact single-rounding expression.
Directed binary32 square-root endpoints for the exact input 2.
Instances For
The upper endpoint, rounded away from zero, so the pair brackets the exact sqrt 2.
Instances For
The executable endpoints enclose the exact real value sqrt 2.
Fixed grids, quantization, and double rounding #
A signed affine code set with quarter-unit spacing. The construction is not tied to a tensor layout or storage width; those choices only determine the integer code bounds.
Instances For
Every in-range code is recovered exactly after dequantization and requantization.
When saturation is inactive, nearest-even reconstruction is within half a quantization step.
Four valid codes, represented with the same shape-indexed tensor used by TorchLean models.
Instances For
Pointwise tensor Q/DQ is exact on an in-range code tensor.
Round-to-odd on a sufficiently fine binary grid prevents double rounding on the quarter grid.
IEEE exception status #
The status-bearing API records division by zero separately from invalid operation.
A training-shaped reduction #
A fixed two-term dot-product tree. Its shape records the accumulation order.
Instances For
Every intermediate product and addition in the example remains finite.
The executable dot product decodes to the computed mantissa/exponent representation of its final rounded accumulation. The two leaf multiplications are rounded before this final addition.