bend-ml-tensor-array

Search uses release 0.1.19.0 · 321 definitions

Releases (20)

0.1.19.0 indexed
0.1.18.0 unindexed
0.1.17.0 unindexed
0.1.16.0 unindexed
0.1.15.0 unindexed
0.1.14.0 unindexed
0.1.13.0 unindexed
0.1.12.0 unindexed
0.1.11.0 unindexed
0.1.10.0 unindexed
0.1.9.0 unindexed
0.1.8.0 unindexed
0.1.7.0 unindexed
0.1.6.0 unindexed
0.1.5.0 unindexed
0.1.4.0 unindexed
0.1.3.0 unindexed
0.1.2.0 unindexed
0.1.1.0 unindexed
0.1.0.0 unindexed

Definitions (321)

main.bend

def add_row2
def Mat.add_row
type MPair
def mpair_fin
def relu_fin
def Mat.relu
def Mat.relu_bwd
def Mat.sgd
def Mat.add
type MColSum
def colsum_fin
def Mat.col_sums
def Mat.col_sums_acc
type MCE
def ce_fin
def Mat.softmax_ce
type MHits
def hits_fin
def Mat.count_correct
type MRow
def row_fin
def Mat.read_row
def Mat.write_row
def labels_len_isdoes the list of labels have exactly n entries (one per row)?
def ce_checked
def Mat.softmax_ce_checkedlike Mat.softmax_ce, but returns None unless labels has exactly n entries
def hits_checked
def Mat.count_correct_checkedlike Mat.count_correct, but returns None unless labels has exactly n entries
def half.gon / 2 rounded down.
def half
def leb_refla <= a
def add_succ_r1 + (a + b) == a + (1 + b)
def add_zero_ra + 0 == a
def half_go_lehalf.go(n, acc) <= n + acc
def half_lehalf(n) <= n
def add_suba <= r -> r == a + (r - a)
law half_coverLAW (half_cover): the two bands of a node, half(r) rows and r - half(r) rows, add up to exactly r rows: no row is lost and none is counted twice.
type Bands
def Bands.zerosr x c of zeros in 2^d bands (d = 0: a single band, the same as a Mat)
def eq_halfthe row counts of the two bands follow the row count of the node: if rr == r at run time, the same holds for both halves (the bands carry r only in their type)
def eq_rest
def bfill_ldoes a block of n numbers starting at flat index i end before the second band of a node with r rows?
def bfill_r
def fill_nwrites the first n numbers of xs at index i (and nothing past them)
def fill_band
def bfillwrites the first n numbers of xs at flat index i; l and rt say which bands they touch (bfill_l, bfill_r); rr is the row count r at run time.
def bfill_top
def Bands.fill_atwrites the n numbers of xs into b starting at flat index i (row-major, as Mat.fill_at); numbers past r*c are dropped.
type BVB (intact) and y = B · x, typed like Mat.matmul_nt: x is 1 x c, y is 1 x r
type BLthe bands and y as a list in row order (the result of Bands.matvec_l)
def bv_g2
def bv_gthe band's 1 + m rows came out in an Array (one number per row); read them back as a list
def bv_gemmthe rows of one band, one dot product each, with the gemm of Mat.matmul_nt (n = 1), so the results are identical.
def bv_mat
def bv_join
def bmvthe two bands of a node run in parallel, each with its own copy of x (c numbers); xp is a pair of copies of x (a leaf uses one).
def bv_fin
def Bands.matvecy = B · x for B (r x c, one row per output) and x (1 x c); returns B intact and y (1 x r).
def Bands.matvec_lthe same product with x and y as lists (x: c numbers, y: r numbers in row order), without the Mat conversions of Bands.matvec: for callers that already hold the vector as a list
type BRow
def brow_fin
def brow_leaf2n numbers starting at flat index i of one band (a band may have no rows)
def brow_leaf
def brow_l
def brow_r
def browrow i; left says whether i is in the first band of the node (i < half(rr))
def Bands.read_rowrow i (c numbers), for example an embedding lookup
def bl_join
def blist
def Bands.to_listall r*c numbers in row order (in BRow.row)
def bl_len
def succ_outs == a + (1 + b) -> s == 1 + (a + b)
def len_steps == 1 + (p + (1 + l)) -> s == 2 + (p + l)
def zero_outs == n + 0 -> s == n
def app_lenappending adds the lengths
def read_ml_lenthe same count for the list of a whole Mat: to_list2 wraps read_l's answer, and ML.len counts it
law leaf_lena leaf's list: read_l reads mleft + 1 numbers onto acc.
def g_lenwhatever the gemm wrote, reading 1 + p rows back gives 1 + p numbers (G has one constructor, so matching g opens it, and leaf_len counts the list)
law band_lenLAW (band_len): the product of one band with `rows` rows gives exactly `rows` numbers.
def join_lenjoining two halves of h1 and h2 numbers gives h1 + h2 numbers.
def to_list_count_lenMat.to_list_count reads exactly n numbers, and n = 0 reads none.
law to_list_lenLAW (to_list_len): Mat.to_list reads exactly r*c numbers, no more and no fewer.
def ASet.szASet.sz(T, a): the size of a as a plain U32, the second component of the pair Array.size returns
def ASet.Gthe three results the descents build: the swapped pair, the written array, and the read pair
def ASet.NA
def ASet.K
def ASet.FactsASet.Facts: what one pass over the tree a proves, for any n, j, v, z (n need not be a's real size): 1.
def ASet.size_pairArray.size hands back the array it measured, next to ASet.sz(T, a)
def ASet.node_t
def ASet.node_f
def ASet.facts
def ASet.CopyASet.copy(T, a): one pass over a hands back the same array b, its size n as a value, and the facts that tie them to a: b is a, n is ASet.sz(T, b), and Array.size(b) is the pair (b, ASet.sz(T, b))
def ASet.copy_node
def ASet.copy
def ASet.Jthe masked index and the first branch, as Array.swap.at and Array.get.at compute them from a size n
def ASet.Z
def ASet.close_size
def ASet.close_get
def ASet.top_size
def ASet.top_get