law sgd_step_refused

bendtorch-core@0.1.0.0 · src/autograd/sgd_LAWS.bend:195

import Base
import bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend as Backward
import bendtorch-core@0.1.0.0/src/autograd/tensor_backward_LAWS.bend as TensorBackward
import bendtorch-core@0.1.0.0/src/autograd/sgd.bend as Sgd

195# A step with a refused parameter leaves the tape unchanged; with every id
196# accepted, a refused learning rate leaves it unchanged too; otherwise the
197# step updates the parameters in list order.
198law sgd_step_refused:
199  for entries: List<&1, Backward.Entry>
200  for +lr: F32
201  for +params: List<&2, Nat>
202  for +error: Sgd.Error
203  for refused: {Sgd.refusal(TensorBackward.nodes_of(entries), List.length(&2, Backward.Node, TensorBackward.nodes_of(entries)), params) ==
204    Some{error} : Maybe<&2, Sgd.Error>}
205  {Sgd.step(Backward.Tape{entries}, lr, params) == (Backward.Tape{entries}, Fail{error}) :
206    Backward.Tape & Result<&2, &2, Sgd.Error, Unit>}