law backward_rejects_unbound_operand

bendtorch-core@0.1.0.0 · src/autograd/backward_LAWS.bend:400

import Base
import bendtorch-core@0.1.0.0/src/autograd/backward.bend as Backward

400# An entry with an operand that is itself, a newer entry or a missing entry
401# makes backward of any output on the tape fail with DanglingOperand.
402law backward_rejects_unbound_operand:
403  for +newer: List<&2, Backward.Entry>
404  for +entry: Backward.Entry
405  for +rest: List<&2, Backward.Entry>
406  for +output: Nat
407  for inside: {Nat.is_lt(output, List.length(&2, Backward.Entry, List.append(&2, Backward.Entry, newer, entry <> rest))) == True{} : Bool}
408  for unbound: {bounded(targets(entry_node(entry)), List.length(&2, Backward.Entry, rest)) == False{} : Bool}
409  {Backward.backward(Backward.Tape{List.append(&2, Backward.Entry, newer, entry <> rest)}, output) == Fail{Backward.DanglingOperand{}} :
410    Result<&2, &2, Backward.Error, Backward.Tape>}