law parallel_build_balanced

bendtorch-core@0.1.0.0 · src/tensor/parallel_LAWS.bend:14

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/tensor/parallel.bend as Parallel

14# For every split, the parallel build is a balanced tree of its depth.
15law parallel_build_balanced:
16  for ~Q: Data
17  for ~P: Data
18  for ~A: Type
19  for ~B: Type
20  for ~prepare: @+q: Q -> P
21  for ~split: A & B -> (A & B) & (A & B)
22  for ~cell: @+p: P -> @+position: Nat -> (A & B) -> Bool -> F32 & (A & B)
23  for +q: Q
24  for +depth: Nat
25  for +splits: Nat
26  for +count: Nat
27  for +base: Nat
28  for state: (A & B)
29  Model.Balanced(F32, depth, Parallel.build(~Q, ~P, ~A, ~B, ~prepare, ~split, ~cell, q, depth, splits, count, base, state))