bendtorch-core

Search uses release 0.1.0.0 · 5,204 definitions

Releases (1)

0.1.0.0 indexed

Definitions (5,204)

src/autograd/sum_to_size.bend

def sum_to_size_dimensions

src/autograd/sum_to_size_fold_LAWS.bend

law sum_to_size_clonesum_to_size through the reduce_to contract, nothing reduced: when the target has the contribution's dimensions, a replayed contribution comes back as its clone.
law sum_to_size_fibersum_to_size through the reduce_to contract, axes reduced: when the dimensions differ and the target broadcasts to exactly the contribution's dimensions, a replayed contribution gives the ReduceToContract of reduce_to_fiber: every target cell holds ReduceLaws.fiber over the contribution's words in index order from +0.0.
def summedWhat sum_to_size gives at target cell index for a contribution whose words, in index order, are `values`, and which has count words.
def ReducedWithWhat the transport form of sum_to_size_replayed asks of P: P holds for the returned contribution, replayed with any history `kept` that keeps every word, next to an output replayed with any history, with the target's dimensions, whose every cell holds `summed`.
law sum_to_size_replayedsum_to_size of a replayed contribution is replayed, in the transport form broadcast_to_replayed uses: when the target broadcasts to exactly the contribution's dimensions and `values` lists the contribution's words, then for every P, if P holds for every result that hands back the contribution with the same words and gives an output with the target's dimensions whose cells hold `summed`, P holds for the result.

src/autograd/sum_to_size_fold_PROOF.bend

def clone_pair_lift
def pair_shift
def clone_liftCloning a replayed tensor gives two replayed tensors: the kept one with the history ops ++ [First] and the copy with ops ++ [Second].
def same_true
def differ_false
def shape_below
def clone_pointA clone half reads the contribution's word: First and Second change no word.
def sum_to_size_clone
def sum_to_size_fiber
def half_keepsA First or Second half of a clone keeps every word.
def words_firstThe First half of a clone lists the same words.
def value_atA list equal to the words of a replayed tensor holds each in-bounds word at its index.
def agree_atTwo histories that list the same words agree at every in-bounds index.
def replayed_clone
def replayed_fiber
def replayed_decided

src/autograd/sum_to_size_LAWS.bend

def Identity
type IdentityModel
law sum_to_size_retains_inputThe contribution owner comes back with the same dimensions and observations.
law sum_to_size_identityA target with the contribution's dimensions always succeeds, and the output has the target's dimensions and the contribution's exact words at every position: -0.0 stays -0.0, as in PyTorch's autograd.
law sum_to_size_reducesA target with other dimensions gives exactly the ordered reduce_to result, so every reduce_to law applies to it.

src/autograd/sum_to_size_PROOF.bend

src/autograd/tensor_backward.bend

type Error
type Node
type SavedThe operand values a product saves at record time.
type Entry
type Tape
type Contribution
type PassWhat one entry's VJP hands back: its saved values and its gradient, unchanged, and the contributions for its operands in operand order.
type Binary
def empty
def at_headWhether the head of a newest-first list of count elements has id `id`.
def entry_listed
def listedThe nodes of a list of entries, newest first, next to the entries.
def prepend
def unsets
def both
def delivered_as
def reducedA contribution for operand target: g reduced to the operand's shape.
def contribution_of
def product_reduced
def added_second
def added_first
def vjp_addd(a+b)/da and d(a+b)/db: g, each reduced to its operand's shape.
def negated_pair
def negated-g, word by word: F32.neg flips the sign bit, as PyTorch's neg does.
def negate
def subtracted_second
def subtracted_first
def vjp_subd(a-b)/da: g; d(a-b)/db: -g, negated before it is reduced, as in PyTorch.
def multiplied_second
def multiplied_first
def vjp_muld(a*b)/da: g * right; d(a*b)/db: g * left, with the operand values saved at record time, each product reduced to its operand's shape.
def expanded
def vjp_sumd(sum a)/da: g broadcast to a's shape, as PyTorch's g.expand(a.shape).
def relabel_decided
def relabeledg with the dimensions of `shape`, which has as many elements: a reshape, which moves no word.
def restoredThe pass with g back in its own shape.
def unsqueezed
def vjp_sum_dimsd(sum of a over some axes)/da: g read with the kept shape, the reduced axes put back as 1 (PyTorch's unsqueeze when keepdim is False), then broadcast to a's shape, as the Sum VJP does.
def multiplied
def left_productg @ right^T for the left operand.
def right_productleft^T @ g for the right operand.
def matmul_fourth
def matmul_third
def matmul_second
def matmul_first
def vjp_matmuld(a@b)/da: g @ b^T; d(a@b)/db: a^T @ g, with the operand values saved at record time.
def nt_leftg @ W for the left operand of x @ W^T: g and W are copied first, so a failure loses neither.
def weight_productg^T @ x, g read in place.
def nt_rightg^T @ x for the right operand.
def nt_fourth
def nt_third
def nt_second
def nt_first
def alone
def nt_alone_second
def nt_alone_first
def vjp_matmul_nt_rightd(x @ W^T)/dW alone, g^T @ x, for a product whose input x takes no gradient: the second contribution of vjp_matmul_nt, computed the same way, without g @ W.
def vjp_matmul_ntd(x @ W^T)/dx: g @ W; d(x @ W^T)/dW: g^T @ x, with the operand values saved at record time.
def relu_passed
def vjp_relud relu(a)/da: the pointwise ReluBackward of the saved input x and g, g's own word where x is above zero or NaN and +0.0 where x is at most zero, reduced to the input's shape.
def mse_second
def mse_first