DAG models from sequential GraphSpec chains

This module initializes a chain parameter ABI and packages the structurally lowered term as a single-input DAG model. Zero initialization is total; deterministic initialization reuses each primitive layer conversion and can therefore fail.

def NN.GraphSpec.LowerToDAG.zeroInitParams (ps : List Spec.Shape) : TorchLean.TensorPack Float ps

Initialize a parameter list by filling every tensor with zeros, for proofs and shape-only examples.

Deterministic initialization for chains

Chain.toDAGModelZeroInit is total, but its parameters are all-zero tensors, which is convenient for proofs and shape-only examples but not representative of training setups.

For graphs whose primitives provide Primitive.toLayerM?, we can reuse TorchLean’s deterministic initializers (e.g. Xavier init for linear weights) in a way that matches ToSequential.toSeq:

• we thread an occurrence index i : Nat,
• primitives with countsAsLayer = true increment it,
• and each primitive’s Layer.initState uses seeds derived from i.

We expose this as Chain.toDAGModelDetInit? : Except String (DAG.Model ...): it fails if any primitive lacks a toLayerM? lowering.

def NN.GraphSpec.LowerToDAG.Chain.detInitParamsFrom {ps : List Spec.Shape} {σ τ : Spec.Shape} (g : Chain ps σ τ) (i : ℕ) : Except String (TorchLean.TensorPack Float ps × ℕ)

Compute deterministic initialization tensors for a sequential Chain, threading a “layer occurrence index”.

This matches ToSequential.toSeq’s notion of “occurrence”: only primitives with countsAsLayer = true advance the counter.

def NN.GraphSpec.LowerToDAG.Chain.detInitParams? {ps : List Spec.Shape} {σ τ : Spec.Shape} (g : Chain ps σ τ) : Except String (TorchLean.TensorPack Float ps)

Deterministically initialize all graph parameters, starting the occurrence index at 0.

def NN.GraphSpec.LowerToDAG.Chain.toDAGModelZeroInit {ps : List Spec.Shape} {σ τ : Spec.Shape} (g : Chain ps σ τ) : DAG.Model ps [σ] τ

Lower a sequential Chain to a DAG Model with a simple default init (all zeros).

This is mainly a convenience for GraphSpec example organization; for training-oriented init, see NN.GraphSpec.ToSequential (sequential-model conversion) and/or provide your own initializer.

def NN.GraphSpec.LowerToDAG.Chain.toDAGModelDetInit? {ps : List Spec.Shape} {σ τ : Spec.Shape} (g : Chain ps σ τ) : Except String (DAG.Model ps [σ] τ)

Lower a sequential Chain to a DAG Model, using deterministic initialization.

This is the DAG analogue of ToSequential.toSeq’s initialization semantics: it uses each primitive’s toLayerM? to obtain a TorchLean Layer, then reuses the Layer.initState.

This returns Except String because not every primitive necessarily admits a Layer lowering.