Shape-changing eager-engine operations.

This module implements reshape, transpose, broadcast, slice, gather/scatter, and related view-style nodes while preserving the graph metadata needed by autograd.

def Runtime.Autograd.Tape.flatten {α : Type} [Inhabited α] [DecidableEq Spec.Shape] {s : Spec.Shape} (t : Tape α) (xId : ℕ) : Result (Tape α × ℕ)

Flatten a tensor s into a 1D vector of length Shape.size s.

PyTorch comparison: torch.flatten(x) with start_dim=0.

def Runtime.Autograd.Tape.reshape {α : Type} [Inhabited α] [DecidableEq Spec.Shape] {s₁ s₂ : Spec.Shape} (t : Tape α) (xId : ℕ) (h : s₁.size = s₂.size) : Result (Tape α × ℕ)

Reshape a tensor while preserving number of elements.

The proof argument h enforces Shape.size s₁ = Shape.size s₂. PyTorch comparison: x.reshape(new_shape) / x.view(new_shape) (when valid).

def Runtime.Autograd.Tape.transpose2d {α : Type} [DecidableEq Spec.Shape] {m n : ℕ} (t : Tape α) (xId : ℕ) : Result (Tape α × ℕ)

Transpose a 2D matrix. PyTorch: x.t() / x.transpose(0,1).

def Runtime.Autograd.Tape.transpose3dFirstToLast {α : Type} [DecidableEq Spec.Shape] {a b c : ℕ} (t : Tape α) (xId : ℕ) : Result (Tape α × ℕ)

Permute a 3D tensor (a,b,c) → (b,c,a). PyTorch: x.permute(1,2,0).

def Runtime.Autograd.Tape.transpose3dLastToFirst {α : Type} [DecidableEq Spec.Shape] {a b c : ℕ} (t : Tape α) (xId : ℕ) : Result (Tape α × ℕ)

Permute a 3D tensor (a,b,c) → (c,a,b). PyTorch: x.permute(2,0,1).

def Runtime.Autograd.Tape.transpose3dLastTwo {α : Type} [DecidableEq Spec.Shape] {a b c : ℕ} (t : Tape α) (xId : ℕ) : Result (Tape α × ℕ)

Swap the last two axes of a 3D tensor (a,b,c) → (a,c,b). PyTorch: x.transpose(1,2).

def Runtime.Autograd.Tape.swapAdjacentAtDepth {α : Type} [DecidableEq Spec.Shape] {s : Spec.Shape} (t : Tape α) (depth xId : ℕ) : Result (Tape α × ℕ)

Swap adjacent axes at a given depth inside a general Shape.

This is a more general analogue of transpose operations.

def Runtime.Autograd.Tape.broadcastTo {α : Type} [Inhabited α] [Add α] [Zero α] [DecidableEq Spec.Shape] {s₁ s₂ : Spec.Shape} (cb : s₁.CanBroadcastTo s₂) (t : Tape α) (xId : ℕ) : Result (Tape α × ℕ)

Broadcast x : s₁ to s₂ using a proof Shape.CanBroadcastTo s₁ s₂.

PyTorch comparison: implicit broadcasting / x.expand(...).

def Runtime.Autograd.Tape.reduceSum {α : Type} [Add α] [Zero α] [Inhabited α] [DecidableEq Spec.Shape] {s : Spec.Shape} (axis : ℕ) [valid : Spec.Shape.valid_axis_inst axis s] [wf : s.WellFormed] (t : Tape α) (xId : ℕ) : Result (Tape α × ℕ)

Sum-reduce along axis.

PyTorch comparison: torch.sum(x, dim=axis).

def Runtime.Autograd.Tape.reduceMean {α : Type} [Context α] [DecidableEq Spec.Shape] {s : Spec.Shape} (axis : ℕ) [valid : Spec.Shape.valid_axis_inst axis s] [wf : s.WellFormed] (t : Tape α) (xId : ℕ) : Result (Tape α × ℕ)

Mean-reduce along axis.

Backward rule: broadcast the upstream cotangent back to s and divide by the reduced dimension. PyTorch comparison: torch.mean(x, dim=axis).