law adjoint_seq

bendtorch@1.3.0.0 · LAWS.bend:26

import Base
import bendtorch@1.3.0.0/spec.bend as Spec

26# LAW (adjoint_seq): Seq runs the second layer's backward pass, then the first's. For two linear layers that is
27# W1ᵀ·(W2ᵀ·dy), and it is the adjoint of the composed forward pass W2·(W1·x): the chain rule, for linear maps.
28law adjoint_seq:
29  for +w1: List<&2, List<&2, Nat>>
30  for +w2: List<&2, List<&2, Nat>>
31  for +g: List<&2, Nat>
32  for +v: List<&2, Nat>
33  {Spec.dotn(g, Spec.mv(w2, Spec.mv(w1, v))) == Spec.dotn(Spec.mtv(w1, Spec.mtv(w2, g)), v) : Nat}