GraphSpec MLP Example

This file contains the smallest GraphSpec architecture example:

Linear(in,hid) → ReLU → Linear(hid,out).

This does not duplicate TorchLean's executable MLP helper. That constructor lives under NN.GraphSpec.Models.TorchLean.Mlp; application code reaches the corresponding public constructor through TorchLean.nn.models. The point here is narrower and proof-oriented:

• show the sequential Graph DSL in its simplest useful form;
• make the parameter ABI visible in the type;
• provide a stable target for GraphSpec equivalence and deterministic-init proofs.

Because this is a pure sequential chain, it is authored with Graph and >>>. The companion mlpDAGModelZeroInit lowers the same chain to the general DAG model representation so DAG-only tooling can consume it.

def NN.GraphSpec.Models.mlp (inDim hidDim outDim : ℕ) : Graph [Spec.Shape.dim hidDim (Spec.Shape.dim inDim Spec.Shape.scalar), Spec.Shape.dim hidDim Spec.Shape.scalar, Spec.Shape.dim outDim (Spec.Shape.dim hidDim Spec.Shape.scalar), Spec.Shape.dim outDim Spec.Shape.scalar] (Spec.Shape.dim inDim Spec.Shape.scalar) (Spec.Shape.dim outDim Spec.Shape.scalar)

2-layer MLP: Linear(in,hid) → ReLU → Linear(hid,out).

Notice how the parameter interface is explicit in the type:

• the first Linear(in,hid) contributes W₁ : Mat hid in and b₁ : Vec hid,
• the second Linear(hid,out) contributes W₂ : Mat out hid and b₂ : Vec out,
• and ReLU contributes no parameters.

So the overall parameter list is exactly: [Mat hid in, Vec hid, Mat out hid, Vec out].

def NN.GraphSpec.Models.mlpDAGModelZeroInit (inDim hidDim outDim : ℕ) : DAG.Model [Spec.Shape.dim hidDim (Spec.Shape.dim inDim Spec.Shape.scalar), Spec.Shape.dim hidDim Spec.Shape.scalar, Spec.Shape.dim outDim (Spec.Shape.dim hidDim Spec.Shape.scalar), Spec.Shape.dim outDim Spec.Shape.scalar] [Spec.Shape.dim inDim Spec.Shape.scalar] (Spec.Shape.dim outDim Spec.Shape.scalar)

The same 2-layer MLP, but exposed as a DAG Model via the structural lowering LowerToDAG.Graph.toDAGModelZeroInit.

This is mainly for GraphSpec example ergonomics: downstream tooling that expects DAG terms can consume this even though it was authored using the sequential >>> syntax.

Initialization: all-zero parameters (see LowerToDAG.Graph.toDAGModelZeroInit).

Example Usage

You can build a simple classifier head by appending a softmax:

def g (inDim hidDim outDim : Nat) :
    Graph
      [ .dim hidDim (.dim inDim .scalar), .dim hidDim .scalar
      , .dim outDim (.dim hidDim .scalar), .dim outDim .scalar ]
      (.dim inDim .scalar) (.dim outDim .scalar) :=
  Models.mlp inDim hidDim outDim >>> Graph.softmax (.dim outDim .scalar)

Then:

• Interp.spec (g …) is a pure function Params → Spec.Tensor → Spec.Tensor;
• Compile.torchProgram (g …) is an executable TorchLean Program with arguments params ++ [input].