law seq_chain

bendtorch@1.3.0.0 · LAWS.bend:35

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

35# LAW (seq_chain): T.Seq's own code, running two linear layers of the exact model one after the other, gives a backward
36# pass that is the adjoint of its forward pass: dy·y == dx·x, for the y the forward pass returns and the dx its backward
37# pass returns from the state the forward pass saved. adjoint_seq says it of the formulas; this says it of the
38# combinator that composes the layers: Seq feeds the second layer's input gradient to the first, the chain rule.
39law seq_chain:
40  for +w1: List<&2, List<&2, Nat>>
41  for +w2: List<&2, List<&2, Nat>>
42  for +x: List<&2, Nat>
43  for +dy: List<&2, Nat>
44  for g1: List<&2, List<&2, Nat>>
45  for g2: List<&2, List<&2, Nat>>
46  {Spec.dotn(dy, Spec.fy(T.Two<List<&2, List<&2, Nat>>, List<&2, List<&2, Nat>>>, List<&2, Nat>, T.Two<List<&2, Nat>, List<&2, Nat>>, T.Layer.fwd(T.Two<List<&2, List<&2, Nat>>, List<&2, List<&2, Nat>>>, List<&2, Nat>, List<&2, Nat>, T.Two<List<&2, Nat>, List<&2, Nat>>, Spec.SeqL(), T.Two{w1, w2}, x))) == Spec.dotn(Spec.bdx(T.Two<List<&2, List<&2, Nat>>, List<&2, List<&2, Nat>>>, List<&2, Nat>, T.Layer.bwd(T.Two<List<&2, List<&2, Nat>>, List<&2, List<&2, Nat>>>, List<&2, Nat>, List<&2, Nat>, T.Two<List<&2, Nat>, List<&2, Nat>>, Spec.SeqL(), T.Two{w1, w2}, Spec.fsv(T.Two<List<&2, List<&2, Nat>>, List<&2, List<&2, Nat>>>, List<&2, Nat>, T.Two<List<&2, Nat>, List<&2, Nat>>, T.Layer.fwd(T.Two<List<&2, List<&2, Nat>>, List<&2, List<&2, Nat>>>, List<&2, Nat>, List<&2, Nat>, T.Two<List<&2, Nat>, List<&2, Nat>>, Spec.SeqL(), T.Two{w1, w2}, x)), dy, T.Two{g1, g2})), x) : Nat}