---- coordinate separability ----
An update is separable when each coordinate's results depend only on that
coordinate and on shared values, so different owners can each update the
coordinates they own (optimizer-state partitioning). With q per-coordinate
state words (word j of coordinate i at state index j k + i) and the other
m - q k words shared, an update slot belongs to coordinate i (parameter i,
a state word of coordinate i, mean i) or is shared (a shared state word,
the rate). `dataParallelSlotClass` is succ i for coordinate i and 0 for
shared.
539def dataParallelSlotClass =
540 (lambda unrestricted k : Nat .
541 (lambda unrestricted m : Nat .
542 (lambda unrestricted q : Nat .
543 (lambda unrestricted slot : Nat .
544 (naturalSelect
545 (naturalLess slot k)
546 (succ slot)
547 (naturalSelect
548 (naturalLess slot (naturalAdd k (naturalMultiply q k)))
549 (succ (naturalModuloUnchecked (naturalSaturatingSubtract slot k) k))
550 (naturalSelect
551 (naturalLess slot (naturalAdd k m))
552 0
553 (naturalSelect
554 (naturalLess slot (naturalAdd (naturalMultiply 2 k) m))
555 (succ (naturalSaturatingSubtract slot (naturalAdd k m)))
556 0))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.