law sgd_update_reaches_target

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

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/sgd.bend as Sgd

95# The update of parameter id reaches exactly the entry with id older entries
96# below it, and keeps every other entry, whatever the list holds.
97law sgd_update_reaches_target:
98  for +lr: F32
99  for newer: List<&1, Backward.Entry>
100  for entry: Backward.Entry
101  for rest: List<&1, Backward.Entry>
102  for +older: Nat
103  for fits: {List.length(&1, Backward.Entry, rest) == older : Nat}
104  {Sgd.descend_at(lr, List.append(&1, Backward.Entry, newer, entry <> rest), 1n+Nat.add(older, List.length(&1, Backward.Entry, newer)),
105      older, Backward.at_head(1n+Nat.add(older, List.length(&1, Backward.Entry, newer)), older)) ==
106    newer_kept(newer, Sgd.placed(rest, Sgd.descend(lr, entry))) : Sgd.Walked()}