GraphSpec Spatial Primitives

This file extends the sequential GraphSpec core (NN.GraphSpec.Core) with single-input/single-output spatial operations used by convolutional pipelines.

These are not model definitions. They are reusable nodes in the GraphSpec vocabulary:

• Primitive.conv wraps the arbitrary-rank convolution specification and runtime operation;
• Primitive.maxPool wraps arbitrary-rank max pooling;
• Primitive.batchNorm wraps normalization over an arbitrary spatial shape;
• Primitive.flatten is the bridge from image-like tensors to vector classifiers.

The corresponding model examples live under NN.GraphSpec.Models.

Important scope note:

• These primitives all fit the sequential language Chain ps σ τ because they have one input tensor and one output tensor (no merging of paths).
• Residual networks require skip connections ($y+x$), which are multi-input and require sharing. For that, use NN.GraphSpec.DAG, whose DAG primitive constructors reuse these sequential adapters when possible.

Why only these spatial operations?

GraphSpec only exposes an operation once we have both sides of the contract in place:

1. a pure Spec meaning, and
2. an executable TorchLean program meaning.

The general always-available primitives (linear, relu, softmax) live in NN.GraphSpec.Core; this file is the current spatial extension pack. More packs can be added as we decide which runtime/spec operations should become architecture-level GraphSpec nodes.

Parameter convention (sequential GraphSpec)

Each primitive has an explicit type-level parameter-shape list ps : List Shape.

For example, an N-D convolution is parameterized by:

• kernel : Tensor α (outC :: inC :: kernelShape)
• bias : Tensor α [outC]

When you compose graphs with >>>, these parameter-shape lists concatenate, giving a typed interface for model parameters.

References / citations (informal pointers)

• Convolutional networks: LeCun et al. (1998), “Gradient-based learning applied to document recognition”.
• BatchNorm: Ioffe & Szegedy (2015), “Batch Normalization: Accelerating Deep Network Training…”.
• Global average pooling: Lin et al. (2013), “Network In Network”.

def NN.GraphSpec.Primitive.conv {d : ℕ} (inC outC : ℕ) (kernel stride padding spatial : TorchLean.Tensor ℕ [d]) : Primitive [Spec.Shape.ofList (outC :: inC :: kernel.to (List ℕ)), [outC]] (Spec.Shape.ofList (inC :: spatial.to (List ℕ))) (Spec.Shape.ofList (outC :: (Spec.convOutSpatial spatial kernel stride padding).to (List ℕ)))

Arbitrary-rank convolution on a channels-first tensor with no batch axis.

Inputs:

• parameters kernel, bias (in that order),
• input tensor x : (inChannels, spatial...).

Output:

The output has shape (outChannels, convOutSpatial spatial kernel stride padding...).

def NN.GraphSpec.Primitive.maxPool {d : ℕ} (channels : ℕ) (kernel stride padding spatial : TorchLean.Tensor ℕ [d]) {hKernel : ∀ (i : Fin d), kernel.getScalar i ≠ 0} {hStride : ∀ (i : Fin d), stride.getScalar i ≠ 0} : Primitive [] (Spec.Shape.ofList (channels :: spatial.to (List ℕ))) (Spec.Shape.ofList (channels :: (Spec.poolOutSpatialPad spatial kernel stride padding).to (List ℕ)))

Arbitrary-rank max pooling on a channels-first tensor (parameter-free).

Output shapes follow the standard pooling size formulas:

Each spatial axis uses the corresponding kernel, stride, and padding entry.

def NN.GraphSpec.Primitive.flatten (s : Spec.Shape) : Primitive [] s [s.size]

Flatten any tensor to a 1D vector (parameter-free).

Output shape is [Spec.Shape.size s], i.e. a vector whose length is the number of elements of the input shape.

This is a reshape/view operation (no arithmetic), used to connect convolutional features to a vector-valued classifier head.

PyTorch analogy: torch.flatten(x).

def NN.GraphSpec.Primitive.batchNorm (channels : ℕ) (spatial : Spec.Shape) (hWellFormed : (Spec.Shape.dim channels spatial).wellFormed) : Primitive [[channels], [channels]] (Spec.Shape.dim channels spatial) (Spec.Shape.dim channels spatial)

BatchNorm over every axis in spatial, independently for each channel.

Parameters are the affine vectors (gamma, beta). GraphSpec keeps this primitive stateless; running statistics belong to the stateful model layer.

def NN.GraphSpec.Chain.conv {d : ℕ} (inC outC : ℕ) (kernel stride padding spatial : TorchLean.Tensor ℕ [d]) : Chain [Spec.Shape.ofList (outC :: inC :: kernel.to (List ℕ)), [outC]] (Spec.Shape.ofList (inC :: spatial.to (List ℕ))) (Spec.Shape.ofList (outC :: (Spec.convOutSpatial spatial kernel stride padding).to (List ℕ)))

Chain constructor for Primitive.conv.

def NN.GraphSpec.Chain.maxPool {d : ℕ} (channels : ℕ) (kernel stride padding spatial : TorchLean.Tensor ℕ [d]) {hKernel : ∀ (i : Fin d), kernel.getScalar i ≠ 0} {hStride : ∀ (i : Fin d), stride.getScalar i ≠ 0} : Chain [] (Spec.Shape.ofList (channels :: spatial.to (List ℕ))) (Spec.Shape.ofList (channels :: (Spec.poolOutSpatialPad spatial kernel stride padding).to (List ℕ)))

Chain constructor for Primitive.maxPool.

def NN.GraphSpec.Chain.flatten (s : Spec.Shape) : Chain [] s [s.size]

Chain constructor for Primitive.flatten.

def NN.GraphSpec.Chain.batchNorm (channels : ℕ) (spatial : Spec.Shape) (hWellFormed : (Spec.Shape.dim channels spatial).wellFormed) : Chain [[channels], [channels]] (Spec.Shape.dim channels spatial) (Spec.Shape.dim channels spatial)

Chain constructor for Primitive.batchNorm.