TorchLean API

Docs HomeGuideExamplesGraphs

NN.Proofs.RuntimeApprox.Graph.LinkAutogradAlgebra

Link Proofs.RuntimeApprox.RevGraph to the executable Proofs.Autograd.Algebra.GraphData #

This is a definitional/structural bridge:

Deduplication note: Proofs.RuntimeApprox.TList is defined as an abbrev for the same heterogeneous context type used by the executable autograd-algebra layer (Proofs.Autograd.Algebra.TList). This means all bridges in this file are genuinely structural/definitional: we do not need to convert between two different context representations.

Note on environments (Δ): Proofs.Autograd.Algebra.GraphData is parameterized by an extra (non-differentiable) environment Δ threaded through evaluation. The runtime-approximation graphs here do not use such an environment, so we instantiate the executable layer at Δ := Unit and pass () during evaluation/backprop.

source
def Proofs.RuntimeApprox.LinkAutogradAlgebra.RevNode.toNodeData {α : Type} {toSpec : α → Spec.SpecScalar} {Γ : List Spec.Shape} {τ : Spec.Shape} (node : RevNode toSpec Γ τ) :
Autograd.Algebra.NodeData α Unit Γ τ

Erase a RuntimeApprox.RevNode into an executable Autograd.Algebra.NodeData.

We take Δ := Unit (no extra environment) and ignore the JVP input, since this bridge is only used for forward evaluation and VJP-based backprop.

Instances For
    source
    def Proofs.RuntimeApprox.LinkAutogradAlgebra.RevGraph.toGraphData {α : Type} {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} (g : RevGraph toSpec Γ ss) :
    Autograd.Algebra.GraphData α Unit Γ ss

    Erase a RuntimeApprox.RevGraph into executable Autograd.Algebra.GraphData (with Δ := Unit).

    This forgets all spec/bound metadata and keeps only the runtime forward and vjp closures.

    Instances For
      source
      theorem Proofs.RuntimeApprox.LinkAutogradAlgebra.RevGraph.evalRuntime_of_toGraphData {α : Type} {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} (g : RevGraph toSpec Γ ss) (xR : TList α Γ) :
      (toGraphData g).eval xR () = g.evalRuntime xR

      Erasing a RevGraph into executable GraphData preserves the runtime forward semantics.

      Informally: if you forget the spec and bound metadata and keep only the runtime closures, you still evaluate to the same runtime context.

      source
      theorem Proofs.RuntimeApprox.LinkAutogradAlgebra.RevGraph.backpropRuntime_of_toGraphData {α : Type} {toSpec : α → Spec.SpecScalar} {Γ : List Spec.Shape} [Add α] {ss : List Spec.Shape} (g : RevGraph toSpec Γ ss) (xR : TList α Γ) (seedR : TList α (Γ ++ ss)) :
      (toGraphData g).backpropCtx xR () seedR = g.backpropRuntime xR seedR

      Erasing a RevGraph into executable GraphData preserves the runtime backward semantics.

      Informally: the executable GraphData.backpropCtx computes the same reverse-mode accumulation as RevGraph.backpropRuntime when given the same runtime input context and seed cotangents.