DAG Term Combinators #
Reusable typed term constructors whose semantics are stated independently of graph syntax.
def
NN.GraphSpec.DAG.Term.sum
{Γ : List Spec.Shape}
(s : Spec.Shape)
(terms : List (Term Γ s))
:
Term Γ s
Add a list of same-shaped terms, starting from the all-zero tensor.
Instances For
theorem
NN.GraphSpec.DAG.Term.eval_sum
{Γ : List Spec.Shape}
{s : Spec.Shape}
{α : Type}
[TorchLean.Storage α]
[Context α]
(env : TorchLean.TensorPack α Γ)
(terms : List (Term Γ s))
:
eval env (sum s terms) = List.foldl (fun (total : TorchLean.Tensor α s) (term : Term Γ s) => total.addSpec (eval env term))
(TorchLean.Tensor.full s 0) terms
Pure evaluation commutes with Term.sum.