Nodes #
Convenience constructors for algebraic tape nodes/graphs.
Build an SSA/DAG graph from local nodes, then lower it to a runtime tape through
NN.Proofs.Autograd.Runtime.Link.
The nodes here are a unary adapter for any OpSpecCorrect and a binary addition node. Both read
their parents through typed context indices (Idx) and scatter their VJPs into the context with
TensorPack.single.
def
Proofs.Autograd.Algebra.NodeData.add
{α Δ : Type}
[TorchLean.Storage α]
[Zero α]
[Add α]
{Γ : List Spec.Shape}
{s : Spec.Shape}
(a b : Idx Γ s)
:
NodeData α Δ Γ s
Executable binary add node (two parents of the same shape).
Instances For
def
Proofs.Autograd.Algebra.Node.ofOpSpecCorrect
{α Δ : Type}
[TorchLean.Storage α]
[CommSemiring α]
{Γ : List Spec.Shape}
{σ τ : Spec.Shape}
(idx : Idx Γ σ)
(op : OpSpecCorrect α σ τ)
:
Node Δ Γ τ
Build a proof-carrying unary node from an OpSpecCorrect.
Instances For
def
Proofs.Autograd.Algebra.Node.add
{α Δ : Type}
[TorchLean.Storage α]
[CommSemiring α]
{Γ : List Spec.Shape}
{s : Spec.Shape}
(a b : Idx Γ s)
:
Node Δ Γ s
Proof-carrying binary add node (two parents of the same shape).