bendtorch
Search uses release 1.2.0.0 · 966 definitions
Definitions (966)
- law adjointLAW (adjoint): the backward pass of a linear layer, dx = Wᵀ·dy, is the adjoint of its forward pass y = W·x: for any W, dy and x, dy·(W·x) == (Wᵀ·dy)·x.
- law weight_adjointLAW (weight_adjoint): the weight gradient dW = dy ⊗ x is the adjoint in W: dy·(W·x) == <dy ⊗ x, W>.
- law adjoint_seqLAW (adjoint_seq): Seq runs the second layer's backward pass, then the first's.
- law seq_chainLAW (seq_chain): T.Seq's own code, running two linear layers of the exact model one after the other, gives a backward 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 pass returns from the state the forward pass saved.
- law fork_sumLAW (fork_sum): T.Fork's own code, giving one input to two linear layers, gives as input gradient the sum of the two layers' input gradients, and that sum is the adjoint of the pair of outputs: dy1·y1 + dy2·y2 == dx·x.
- law both_sumLAW (both_sum): T.Both's own code, running two linear layers side by side on the two inputs of a pair, gives a backward pass that is the adjoint of its forward pass: dy1·y1 + dy2·y2 == dx1·x1 + dx2·x2.
- law residualLAW (residual): T.Residual's own code (T.ResidualOf: Seq(Fork(Id, f), Add2)), with a linear layer as f, gives a backward pass that is the adjoint of its forward pass: for y = x + W·x and its dx, dy·y == dx·x.
- law causal_keysLAW (causal_keys): T.Attention reads keys only through T.qrow, and the scores it builds for the query at position i come from keys 0..i, one per key: exactly i + 1 of them.
- law causalLAW (causal): in T.Attention, row i of a head's probabilities is a softmax over exactly i + 1 positions.
- law causal_gradLAW (causal_grad): in T.Attention's backward pass, row i of a head's G (the gradient of its scores) is computed over exactly i + 1 positions.
- law attn_par_fwdLAW (attn_par_fwd): T.Attention runs its sequences in a tree of parallel lets (T.fpar: the sequences cut in halves, each half cut again, d levels deep, the leaves' outputs appended).
- law attn_par_bwdLAW (attn_par_bwd): the same for the backward pass: T.bpar's tree gives each sequence's dQ, dK and dV exactly as T.bleaf, one sequence after another.
- law kv_of_groupLAW (kv_of_group): T.kv_of, the function both passes of T.Attention use to pick the key/value head of query head hi, gives j for every head of group j: query heads j·g + 0 ..
- law gqa_headLAW (gqa_head): with g = 1 + i + k query heads per key/value head, query head j·g + i reads key/value head (j·g + i) / g = j, the head of its own group: T.Attention's forward pass picks head hi / g, and its backward pass sums the gradients of heads j·g + 0 ..
- law kv_colsLAW (kv_cols): the attention code takes the columns each query head reads from T.head_cols, in both passes (the head loops pass no head index further, so they cannot compute other columns).
- law bc_symLAW (bc_sym): broadcasting does not depend on the order of the operands: a and b broadcast to o exactly when b and a do, so x + y and y + x (and x * y, y * x) accept the same shapes.
- law sum_numelLAW (sum_numel): summing over axis k partitions the elements: a tensor of shape s has exactly size(k) times as many numbers as its sum over axis k, for every shape and every k (past the last axis the size counts as 1).
- law narrow_restLAW (narrow_rest): narrow (and setting any axis' size) changes only its own axis: with axis d taken out, the shape is what it was.
- law narrow_axisLAW (narrow_axis): narrowing axis d of a tensor that has it gives that axis exactly the length asked for.
- law cat_numelLAW (cat_numel): concatenating along an axis the tensor has adds the counts: a tensor whose axis d is x + y long holds as many numbers as the two with x and y.
- law mat_numelLAW (mat_numel): a Tensor<[r, c]> holds the r·c numbers of a Mat<r, c>, so of_mat and to_mat reuse the array as it is.
- law permute_rankLAW (permute_rank): permuting by p gives as many axes as p has, so a permutation of the axes keeps the rank.
- law block_sumLAW (block_sum): summing a row in blocks gives the row's own sum, bit for bit.
- def dot_vadddot(a + b, v) == dot(a, v) + dot(b, v): induction on the three vectors; at each entry (x + y)·z splits into x·z + y·z (distributivity) and add4 regroups the four terms
- def dot_scaledot(k·r, v) == k · dot(r, v): at each entry (k·x)·z == k·(x·z) (associativity), then k factors out of the sum
- def dot_commdot(a, b) == dot(b, a)
- def disc
- def false_trueFalse == True is impossible: rewriting the goal Empty = disc(False) with it gives disc(True) = Unit
- def len_rcatxs reversed onto acc has the length of both
- def len_drowdrow's row has the current dot, the m after it, and acc: 1 + m + |acc| numbers
- def sub0n - 0 is n
- def cnt_divthe division loop of a softmax counts the 1 + k numbers it divides onto c (pr_of hands the count on as the row's)
- def cnt_psm3the whole softmax over 1 + kk numbers reports 1 + kk, whatever max and exp found (they are matched, not computed)
- def cnt_psm2
- def cnt_pwpw writes xs and counts them from n; the softmax prow3 runs on them reports 1 + (|xs| + n - 1)
- def cnt_drowthe count prow2 hands on for drow's row: 1 + m + |acc|, as len_drow, through cnt_pw
- def cnt_gwgw writes xs and counts them from n: gr3 hands on |xs| + n (as cnt_pw for the forward pass)
- def cnt_gdrowthe count gr2 hands on for drow's row: 1 + m + |acc|, as len_drow, through cnt_gw (cnt_drow's twin)
- def app2a ++ b == a2 ++ b2 from a == a2 and b == b2
- def fmap
- type L1R
- def l1_con
- def l1
- type MAR
- def ma_con
- def map_app
- type GAR
- def ga_con
- def go_app
- type CGR
- def cg_base
- def cg_con
- def cg
- type MR
- def m0cdepth 0: the two leaves' loops, appended
- def m0b
- def m0a
- def m1cdepth 1 + e: each half cut in two and its tree (the closures run main at depth e), then the two maps appended
- def m1b
- def m1a
- def tree
- def par_finthe law: the tree gives what fleaf, the loop over the sequences one after another, gives
- def par_mid
- def b_fmap
- type b_L1R
- def b_l1_con
- def b_l1
- type b_MAR
- def b_ma_con
- def b_map_app
- type b_GAR
- def b_ga_con
- def b_go_app
- type b_CGR
- def b_cg_base
- def b_cg_con
- def b_cg
- type b_MR
- def b_m0cdepth 0: the two leaves' loops, appended
- def b_m0b
- def b_m0a
- def b_m1cdepth 1 + e: each half cut in two and its b_tree (the closures run main at depth e), then the two maps appended
- def b_m1b
- def b_m1a
- def b_tree
- def b_par_finthe law: the b_tree gives what fleaf, the loop over the sequences one after another, gives
- def b_par_mid
- def div_blockone block of 1 + m numbers adds 1 to the quotient (Nat.divmod.go counts down the remainder from m)
- def div_blocksj whole blocks of 1 + s numbers add j to the quotient
- def div_restfewer than 1 + s numbers after the last whole block leave the quotient alone
- def or_comma || b == b || a, and a && b == b && a: every case computes
- def and_comm
- def and_congequal operands give equal conjunctions and disjunctions
- def or_cong
- def bc_dim_symone axis: bc_dim is written as pair(x, y) || pair(y, x), so swapping x and y only swaps the two sides of the ||
- def bc_eq_symaxis by axis: the same on each axis (bc_dim_sym), and by induction on the rest; shapes of different ranks are False either way round
- def bc_rank_symthe ranks: the same two comparisons and the same two equalities, in the other order
- def mul_swaph * (a * r) == a * (h * r): associativity, then commutativity of the first two factors, then associativity back
- def pass_pairone pass over 2k blocks of 2^p cells gives the k blocks of 2^(p+1) cells: the pass adds blocks 2j and 2j+1, the two halves bal puts under one node.
- def cnt22^(p+1) · k cells are 2^p · 2k: (a + a)·k == a·k + a·k == a·(k + k)