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.toDAGPrimOp_specFwd {α : Type} [TorchLean.Storage α] [Context α] {ps : List Spec.Shape} {σ τ : Spec.Shape} (p : Primitive ps σ τ) (params : TorchLean.TensorPack α ps) (x : TorchLean.Tensor α σ) : (LowerToDAG.Primitive.toDAGPrimOp p).specFwd (params.append (TorchLean.TensorPack.cons x TorchLean.TensorPack.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”.