Primitive Embedding

GraphSpec’s DAG language (NN.GraphSpec.DAG) is the “general graph” IR. To avoid duplicating the operator semantics, unary sequential primitives

p : Primitive ps σ τ

are embedded into DAG primitive ops

LowerToDAG.Primitive.toDAGPrimOp p : DAG.PrimOp (ps ++ [σ]) τ.

This file proves the bookkeeping theorem that keeps the “no duplicated semantics” contract explicit: if you take a sequential primitive, embed it into DAG form, and feed it the obvious argument list params ++ [x], you get exactly the same pure forward computation.

theorem NN.GraphSpec.Primitive.splitAppend_append1 {α : Type} [Context α] {ps : List Shape} {σ : Shape} (params : Runtime.Autograd.Torch.TList α ps) (x : Tensor.Tensor α σ) : Runtime.Autograd.Torch.Proofs.Autograd.Algebra.TList.splitAppend (Runtime.Autograd.Torch.Proofs.Autograd.Algebra.TList.append params (Proofs.Autograd.Algebra.TList.cons x Proofs.Autograd.Algebra.TList.nil)) = (params, Proofs.Autograd.Algebra.TList.cons x Proofs.Autograd.Algebra.TList.nil)

splitAppend undoes append in the one-input case.

This typed-list fact is used internally by LowerToDAG.Primitive.toDAGPrimOp.

theorem NN.GraphSpec.Primitive.toDAGPrimOp_specFwd_eq {α : Type} [Context α] {ps : List Shape} {σ τ : Shape} (p : Primitive ps σ τ) (params : Runtime.Autograd.Torch.TList α ps) (x : Tensor.Tensor α σ) : (LowerToDAG.Primitive.toDAGPrimOp p).specFwd (Runtime.Autograd.Torch.Proofs.Autograd.Algebra.TList.append params (Proofs.Autograd.Algebra.TList.cons x Proofs.Autograd.Algebra.TList.nil)) = p.specFwd params x

Embedding a sequential primitive into DAG form preserves its pure specFwd semantics.

This theorem states that “the DAG primitive is the sequential primitive with its parameters made explicit as ordinary inputs”.