Executed Backward Pass on Lowered Graphs #
BackwardDense shows that the executed sweep Tape.backwardDenseAll agrees with the proved sweep
Tape.backwardDenseFrom on every ZeroPreserving tape. This file discharges that hypothesis for
every tape produced by lowerGraphToTape and states the resulting corollaries for the executed
backward pass.
The zero-preservation proof rests on one algebraic fact: a proof-carrying Node satisfies the
adjointness law dot (jvp x dx d) δ = dotList dx (vjp x d δ), and the pairing TensorAlgebra.dot
is nondegenerate over a commutative semiring (eq_full_zero_of_forall_dot_eq_zero). Hence
vjp x d 0 = 0 for every node (node_vjp_full_zero), so a lowered node's backward sends its
zero cotangent to zero contributions of the parents' shapes (lowerGraphToTape_zeroPreserving).
Endpoints:
backwardDenseAll_lowerGraphToTape_eq_backpropAllCtx: the executed sweep on a lowered graph, seeded at any typed output index, returnsbackpropAllCtxof the one-hot seed context.backwardDenseAll_lowerGraphToTape_adjoint_fderiv(and its_atvariant): overℝ, the input block of that result is the adjoint of the Fréchet derivative of the forward map.
As in FDeriv, these are statements about the exact tape model at the given carrier; they say
nothing about Float rounding or the CUDA path.
Nondegeneracy of the algebraic pairing #
The pairing with the all-zero tensor on the left is 0.
The pairing of a stacked tensor is the sum of the pairings of its slices.
A tensor whose pairing with every tensor vanishes is the zero tensor.
dotList with the all-zero context on the left is 0.
A context whose pairing with every context vanishes is the zero context.
A proof-carrying node's VJP sends the zero cotangent to the zero context. This follows from the
adjointness law alone: dotList dx (vjp x d 0) = dot (jvp x dx d) 0 = 0 for every dx.
Shape erasure of the zero context and of single #
Entries of the erased zero context are zero tensors of the recorded shapes.
Every indexed contribution of the zero context is a zero tensor at a valid position.
The shape recorded at position j of an erased context is ss[j].
Erasing single idx v: v at idx, zero tensors of the recorded shapes elsewhere.
Lowered tapes are zero preserving #
The value stored at node j of a lowered tape has the shape recorded at j in Γ ++ ss.
Every tape produced by lowerGraphToTape is ZeroPreserving: leaves have no contributions, and
a lowered node's backward on its zero cotangent runs the stored VJP at zero, which is the zero
context by node_vjp_full_zero, so every emitted contribution is a parent's zero cotangent.
The one-hot seed array is the erased single context #
On a lowered tape, oneHotGrads at a typed index is the erasure of TensorPack.single.
Corollaries for the executed backward pass #
Executed backward pass on a lowered graph = proved backpropagation. Running the trainer's
Tape.backwardDenseAll on the tape produced by lowerGraphToTape, seeded at any typed output
index output with cotangent seed, succeeds and returns the shape erasure of backpropAllCtx
of the one-hot seed context. Unlike backwardDenseFrom_lowerGraphToTape_eq_backpropAllCtx, this
is about the variant that skips unreached nodes; the two agree by lowerGraphToTape_zeroPreserving.
Executed backward pass = adjoint of the Fréchet derivative. Over ℝ, the trainer's
Tape.backwardDenseAll on a lowered graph, seeded at a typed output index, succeeds with the full
backpropagation context, whose input (Γ-prefix) block is the adjoint of the Fréchet derivative
of the graph's forward evaluation applied to the one-hot seed. This composes
backwardDenseAll_lowerGraphToTape_eq_backpropAllCtx with
backwardDenseFrom_lowerGraphToTape_adjoint_fderiv.
Pointwise variant of backwardDenseAll_lowerGraphToTape_adjoint_fderiv.