NF Backward Approximation Backend #
Core approximation lemmas for the rounded NF backend: constants, sparse context writes, and the context-addition bound used when reverse-mode contributions have to be accumulated.
Two context indices pointing at the same position must have the same shape.
An Idx Γ s bundles a position with a proof that Γ holds shape s there, so equal positions
force
equal shapes. This is what makes the disjointness lemmas below usable: a proof that two indices
differ
can be given by comparing positions only, with no shape reasoning.
Cast a tensor across a shape equality induced by equal Idx positions.
Given a : Idx Γ s₁, b : Idx Γ s₂, and h : a.i = b.i, this produces a function
Tensor α s₂ → Tensor α s₁ that casts along the implied equality s₁ = s₂.
Instances For
Approximation is stable under transporting both tensors along the same shape equality.
The all-zero context approximates the all-zero context, at zero error.
This is the base case of every backward-pass bound: gradient accumulation starts from zeros on both the spec and the runtime side, and zero is exactly representable, so nothing is lost yet.
Writing one approximate tensor into an otherwise-zero context keeps the context approximate, with the error recorded at that slot alone.
Two writes at distinct positions do not interfere: each slot carries its own error bound.
Distinctness is essential. If the indices coincided the two contributions would have to be added, and the sum would carry the sum of the errors rather than either one.
Same again for three pairwise-distinct writes, which is what a ternary node's backward pass needs.
Context-wise addition bound (NF runtime vs spec).
This produces an EList of linfNorm bounds for adding two contexts elementwise, and is used when
reverse-mode accumulation must combine contributions from multiple consumers.
Instances For
Soundness of context-wise addition under approxCtx.
If xS ~ xR ± epsx and yS ~ yR ± epsy, then (xS + yS) ~ (xR + yR) with error bounded by
ctxAddBound epsx epsy xR yR.