Broadcasting

Spec-level broadcasting and broadcasted binary maps.

Broadcasting

def Spec.Tensor.broadcastTo {α : Type} [Inhabited α] {s₁ s₂ : Shape} : s₁.CanBroadcastTo s₂ → Tensor α s₁ → Tensor α s₂

Broadcast a tensor along a Shape.CanBroadcastTo proof (spec-level analogue of torch.broadcast_to).

Broadcasted maps

def Spec.Tensor.broadcastLike {α : Type} [Inhabited α] {s : Shape} (_template : Tensor α s) (t : Tensor α Shape.scalar) : Tensor α s

Broadcast a scalar tensor to match a template tensor's shape.

This is the "like" broadcasting form used by specs that want to follow a template shape without spelling out the Shape.CanBroadcastTo evidence.

def Spec.Tensor.mapScalarLeft {α : Type} (f : α → α → α) (x : α) {s : Shape} : Tensor α s → Tensor α s

Helper: map a scalar on the left over any tensor shape.

def Spec.Tensor.mapScalarRight {α : Type} (f : α → α → α) (y : α) {s : Shape} : Tensor α s → Tensor α s

Helper: map a scalar on the right over any tensor shape.

def Spec.Tensor.broadcastMapTo {α : Type} [Inhabited α] (f : α → α → α) {s₁ s₂ t : Shape} (cbx : s₁.CanBroadcastTo t) (cby : s₂.CanBroadcastTo t) : Tensor α s₁ → Tensor α s₂ → Tensor α t

Binary element-wise operation with broadcasting to an explicit target shape.

This is the helper you typically want in spec code:

• pick the output shape t,
• broadcast each operand to t,
• then map2_spec the pointwise operation.

PyTorch analogy: f(x, y) where x and/or y are broadcastable to a common shape. We make the common shape explicit instead of "discovering" it, because at the spec layer we want:

• predictable typing,
• a single source of truth for what the output shape is.