bendtorch-core

Search uses release 0.1.0.0 · 5,204 definitions

Releases (1)

0.1.0.0 indexed

Definitions (5,204)

src/autograd/reduce_fiber_proof.bend

def masked_split
def le_step
def lt_of_room
def lt_succ_right
def gt_not_eq
def le_ne_succ
def le_lt_absurd
def lt_self_succ
def axis_zero
def axis_kept
def walk_left_row
def walk_left_belowThe left walk of a position below the output count lies below the left count.
type BoundByBelow a kept row of left stride `left`, every walk of the rows below stays under `left`: the rows are the index rows of an aligned broadcast whose left count is `left` and whose output count is `stride`.
def bound_at
type MaskModeHow the rows below a block decide which positions land on the target: on a reduced row (left stride 0) the rows below land on the target itself; on the kept row's target digit they land on the target's remainder; on any other digit of a kept row nothing lands.
def mode_mask
type OffMode
def off_mask
def shiftedOn a row of stride s, left stride L and right stride R, the positions d * s + q ..
def shifted_off
def blockThe first block of a row, at cursor digit * stride: the rows below at base + right * digit.
def block_off
def next_cursor
def shiftMoving the base moves every offset: base + xs.
def shift_append
def shift_shift
def kept_shift
def masked_base
def visited_base
def RestWalkThe walk below a row, at base 0, visits the masked positions below it.
def rest_at...
def reduced_blocksA reduced row (left stride 0) walks every digit: the blocks digit ..
def kept_afterOn a kept row, the blocks after the target's digit hold no position.
def kept_hit_step
def kept_hitOn a kept row, the blocks from `digit` that cover the target's digit hold exactly the rows below at the target's remainder.
def kept_rowA kept row walks the one digit the target names there.
def RowsWalk
def fiber_cons
def fiber_walkThe fiber-walk lemma: for the index rows of an aligned broadcast and a cell below the left count, the offsets the walk reads, in order, are the masked positions.

src/autograd/reduce_fold.bend

type Cell
def target_offset
def contribution_offset
def source
def lands
def cell

src/autograd/reduce_fold_LAWS.bend

type FiberContractWhat a reduce cell promises, stated only through the result: it gives `expected`, and the returned contribution still holds every word.
law reduce_fold_fiberOrdered-fold family, reduce instance: for a plan whose output has the contribution's shape, every target index and every replayed contribution, the reduce cell gives `ReduceLaws.fiber` over the contribution's words in index order, and returns the contribution with every word kept.
def output_dimensions
def output_point
def input_point
type ReduceToContractWhat reduce_to promises, stated only through the result: it succeeds with the target's dimensions, every in-bounds target cell holds `expected`, and the returned contribution still holds every word.
law reduce_to_fiberreduce_to through the ordered-fold family: when the target broadcasts to exactly the contribution's dimensions, reducing a replayed contribution succeeds with the target's dimensions, every target cell holds `ReduceLaws.fiber` over the contribution's words in index order, the value `reduce_fold_fiber` states for `ReduceFold.cell`, and the returned contribution keeps every word.

src/autograd/reduce_fold_PROOF.bend

src/autograd/reduce_parallel_proof.bend

def numel_pad
def padding_left
def padding_right
def table_walkThe index table of an aligned broadcast is walked as `Fiber.fiber_walk` says.
def plan_walkThe same for the rows of a plan's index map.
def offsets_walkAs in reduce_fold_PROOF.bend: below the output count, the specified offsets are the index walks.
def gatherAdding the words at a list of positions, in order.
def gather_append
def gather_kept
def succ_add
def fiber_maskedThe masked fold of `ReduceLaws.fiber` adds, in order, the words at the masked positions.
def all_belowEvery masked position lies inside the contribution.
def kept_below
def masked_below
def fsum
def fsum_append
def ObsEach word is what A holds at its position.
type ObsStep
def obs_append
type FiberRunA run of `Reduce.fiber`: its total adds the words it saw, in order, and the array comes back unchanged.
def leaf_run
def next_run
def fiber_run
def add_zero
def offset_shiftThe one word that rows of span 1 reach from `base` sits `base` past the one they reach from 0.
def leaf_keptA closure that hands its two arguments back as they are leaves a leaf add as it is.
def span_one
def single_fiberRows of span 1 read one word: the one at `single_offset`.
def fiber_stepOne digit of a row whose rows below take one digit adds the word at its strided offset.
def run_fiberThe strided run of a row whose rows below take one digit is the fiber of that row from the same digit, one more word than the run's fuel.
def strided_fiberThe strided loop of such a row is its fiber.
def SingleOkWhat a fast fiber's flag promises: True only where the rows below the first take one digit each.
def single_ok
def next_sameTwo closures equal on every argument continue a pair alike.
def fast_fiberThe fast fiber returns what the fiber returns.