Reductions #
Deployment-aware reduction semantics for ExecFloat.Binary 8 23.
In deployed environments, reductions (sums / dot-products / matmul accumulations) may be evaluated using different valid parenthesizations and, depending on the implementation, different leaf orders. Since floating-point addition is not associative, distinct reduction schedules can produce distinct results.
This module models a reduction as "any result produced by a valid reduction tree over the same leaves" and proves a standard forward-error enclosure that holds uniformly over all such trees.
What this file proves #
Assuming a local rounded-addition model with parameter u, we derive a global enclosure whose
parameters depend only on:
n(the number of leaves), and- $A=\sum_i|\mathtt{leaf}_i|$ (a scale factor).
The bound uses the geometric factor $(1+u)^{n-1}-1$, not the rational $\gamma_k$ bound.
The generic rounding hypothesis quantifies over all real operands. Finiteness of one tree does
not establish it, and binary32 underflow prevents choosing the usual unit roundoff globally over
arbitrary real operands. The _binary32 corollaries instead reuse FloatLib's bounds for the
tree's own representable operands. They admit u = 2⁻²⁴, including subnormal sums, under the
finite-execution hypothesis alone. These are mathematical enclosures, not native-kernel checks.
For ExecFloat.Binary 8 23, we connect the executable add to the real model
Model.roundAt FloatFormat.binary32 (a + b), but only on the finite branch. If Inf/NaN/
overflow is possible, the right semantics is the special-value semantics from FloatLib, so this
file keeps those cases out of scope via FiniteEval*.
Inspiration and related work #
This is a direct formalization of standard numerical-analysis results for parallel sums:
- David Goldberg, “What Every Computer Scientist Should Know About Floating-Point Arithmetic” (1991). DOI: 10.1145/103162.103163
- Nicholas J. Higham, Accuracy and Stability of Numerical Algorithms, 2nd ed., SIAM (2002), especially the summation chapter and the $\gamma_k$-style bounds.
- Sylvie Boldo and Guillaume Melquiond, “Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq” (ARITH 2011). DOI: 10.1109/ARITH.2011.40
Instead of bounding nondeterminism, another design direction is to eliminate it via reproducible accumulators/binned sums. That literature is a complement to this file:
- James Demmel and Hong Diep Nguyen, “Fast Reproducible Floating-Point Summation” (ARITH 2013). DOI: 10.1109/ARITH.2013.9
- Peter Ahrens, James Demmel, and Hong Diep Nguyen, “Algorithms for Efficient Reproducible Floating Point Summation” (ACM TOMS 2020). DOI: 10.1145/3389360
- ReproBLAS (binned reproducible BLAS): https://bebop.cs.berkeley.edu/reproblas/
- ExBLAS (reproducible BLAS kernels): https://github.com/riakymch/exblas
ExecFloat.Binary 8 23: evaluation + nondeterminism (expression tree + permutation) #
Evaluate a reduction tree using the executable ExecFloat.add.
This is the “concrete” semantics: it includes IEEE special values, finite rounding, etc.
Error analysis uses a separate real-valued interpretation (evalRealIEEE).
Instances For
FiniteEvalSumTree t means:
- every leaf is finite, and
- every internal
addevaluates on the finite branch (noInf/NaNresult).
We need this hypothesis when relating the executable semantics to the real model
Model.roundAt FloatFormat.binary32 (toReal a + toReal b): if an add can overflow to Inf or
produce a NaN, the correct semantic layer is FloatLib's special-value semantics, not a small-error
enclosure.
Instances For
If the whole reduction evaluates on the finite branch, then the final result is finite.
Nondeterministic sum result relation.
sumTreeResult xs r means: there exists a reduction tree t whose leaves are a permutation of xs
and such that evaluating t using executable add produces r and stays finite throughout.
Instances For
Real-valued “finite-branch model” of evalIEEE.
Every internal node uses Model.roundAt FloatFormat.binary32 (a+b). This is the usual
round-to-nearest floating-point model when the result stays finite; our bridge lemmas justify
this model under FiniteEvalSumTree.
Instances For
Every internal rounded sum has the canonical effective mantissa/exponent representation.
Exact real sum of the decoded leaves.
Instances For
Leaf scale for sums: Σ |toReal leaf|.
Instances For
Under FiniteEvalSumTree, the decoded executable sum agrees with its real-valued rounding
model.
Enclosure theorem for nondeterministic FP32 sums.
sumTreeResult xs r means: r is the result of adding the elements of xs using executable
ExecFloat.add, but with an evaluation order that is allowed to vary (a reduction tree plus a
permutation of leaves).
The conclusion produces a witness tree t and a bound on how far toReal r can deviate from the
exact real sum of t’s leaves (measured against the leaf scale sumAbsIEEE t).
A finite binary32 sum has the usual unit-roundoff enclosure, including subnormal sums.
FloatLib bounds addition on this tree's own representable operands. Unlike the generic enclosure, this corollary needs no rounding assumption quantified over arbitrary real inputs.
Every finite binary32 sum schedule has the tree-local unit-roundoff enclosure.
Dot-product accumulation (sum of products) #
Leaves are operand pairs, evaluated by executable multiplication; internal nodes use executable addition. The enclosure bounds accumulation error relative to the exact sum of the already-rounded products. Bounding error against the original real dot product additionally needs multiplication error bounds. This schedule does not model fused multiply-add or establish which schedule a native matmul, convolution, or attention kernel uses.
Evaluate a dot-product reduction tree using executable mul at leaves and add at internal nodes.
Instances For
FiniteEvalDot t means:
- each leaf product
mul x yis finite, and - each internal accumulation
addstays finite.
The operand pairs themselves are not separately required to be finite; the predicate concerns their computed products and the accumulation results.
Instances For
If a dot-product reduction stays finite at every step, then the final result is finite.
Nondeterministic dot-product result relation.
dotTreeResult xs r means: there exists a reduction tree over leaf pairs in xs (up to
permutation) whose executable evaluation evalDotIEEE yields r and stays finite throughout.
Instances For
Real-valued finite-branch model of evalDotIEEE.
- Leaves contribute
toReal (mul x y)(the real meaning of the executable product). - Internal nodes add those contributions using
Model.roundAt FloatFormat.binary32 (a+b).
This matches the standard floating-point model for accumulation, under FiniteEvalDot.
Instances For
A finite executable dot-product leaf has the effective rounded-product representation.
Every dot-product accumulation node has the effective rounded-sum representation.
Exact real sum of the rounded leaf products.
This is not the exact real dot product of the original inputs; it is the exact sum of the values
that evalDotIEEE would compute at the leaves (after mul rounding), ignoring only the rounding
introduced by the accumulation adds.
Instances For
Leaf scale for dot-product accumulation: Σ |toReal (mul x y)|.
This is the “A” term that appears in the forward-error bound for reductions.
Instances For
Bridge lemma: on the finite branch, toReal of the executable dot-product reduction agrees with
the real-valued model evalRealDotIEEE.
Enclosure theorem for nondeterministic dot-product accumulation.
dotTreeResult xs r means: the runtime computed r by taking the array of pairs xs, multiplying
each pair, and then summing the products using some reduction tree whose leaves are a permutation
of xs.
The conclusion gives a witness tree t for that schedule and an order-independent enclosure:
the accumulation result is close (in $\mathbb{R}$) to the exact sum of leaf products, with the same
growth factor bound as in the plain-sum case.
Binary32 dot-product accumulation needs only finite products and finite intermediate sums. The reference is the exact sum of the already-rounded products, not the original real dot product.