GraphSpec → TorchLean.NN.Seq (sequential lowering)

This provides a structural lowering from GraphSpec graphs into TorchLean sequential models.

What is this lowering for?

GraphSpec gives us two things already:

• a pure denotational semantics (Interp.spec) for proofs / reference reasoning, and
• a compiler to an executable TorchLean program (Compile.torchProgram) for running/training.

So why do we also lower to TorchLean.NN.Seq?

TorchLean.NN.Seq is a small “training ergonomics” wrapper around a sequence of LayerDefs:

• it packages a parameter shape list (paramShapes) and deterministic parameter initialization,
• it provides a sequential forward program,
• and it plugs easily into existing training-loop code that expects a sequential layer stack.

GraphSpec remains the source of truth for the model structure. Seq is a secondary view for the subset of models that are layer stacks.

Partial compilation: Except String

Important design decision:

• GraphSpec itself is a graph language, not “a training framework”.
• Not every GraphSpec primitive should be forced to be a LayerDef.

So the lowering returns Except String: it succeeds for graphs whose primitives provide Primitive.toLayerDefM?, and fails otherwise.

Deterministic initialization (occurrence index)

We thread a Nat counter to support deterministic, occurrence-indexed initialization. This gives the lowering a stable RNG boundary without making global randomness part of the graph syntax.

For example, the default Primitive.linear uses:

• seedW = 2*i, seedB = 2*i + 1.

See also:

• NN.GraphSpec.Core for the core sequential DSL and its Compile.torchProgram compiler.
• NN.GraphSpec/README.md for the high-level “GraphSpec vs TorchLean” motivation.

Example (informal)

If g : Graph ps σ τ is built from primitives that provide toLayerDefM?, then:

• ToTorchLean.toSeq g : Except String (TorchLean.NN.Seq σ τ) gives a sequential model with deterministic initialization, and
• Compile.torchProgram g : TorchLean.Program α (ps ++ [σ]) τ gives the general executable program view (works even when there is no Seq lowering).

def NN.GraphSpec.ToTorchLean.err {α : Type u_1} (msg : String) : Except String α

Convenience constructor for an error result in the Except String lowering pipeline.

def NN.GraphSpec.ToTorchLean.toSeqAux {ps : List Tensor.Shape} {σ τ : Tensor.Shape} (g : Graph ps σ τ) (i : ℕ) : Except String (Runtime.Autograd.TorchLean.NN.Seq σ τ × ℕ)

Lower a graph to a TorchLean Seq, threading a “layer occurrence index”.

The index is incremented for primitives with countsAsLayer = true.

def NN.GraphSpec.ToTorchLean.toSeq {ps : List Tensor.Shape} {σ τ : Tensor.Shape} (g : Graph ps σ τ) : Except String (Runtime.Autograd.TorchLean.NN.Seq σ τ)

Try to lower a sequential GraphSpec graph into a TorchLean.NN.Seq.

Use this when you specifically want the Seq wrapper for training ergonomics. If all you need is an executable program, prefer Compile.torchProgram: it is the more general path and does not require every primitive to have a LayerDef view.