Elementwise eager-engine operations.

This file contains scalar-lifted tensor nodes and their runtime/autograd implementation, including arithmetic, comparisons, activations, and loss-adjacent pointwise operations.

def Runtime.Autograd.Tape.add {α : Type} [Add α] [DecidableEq Spec.Shape] {s : Spec.Shape} (t : Tape α) (aId bId : ℕ) : Result (Tape α × ℕ)

Elementwise addition. PyTorch: torch.add / +.

def Runtime.Autograd.Tape.sub {α : Type} [Sub α] [Zero α] [DecidableEq Spec.Shape] {s : Spec.Shape} (t : Tape α) (aId bId : ℕ) : Result (Tape α × ℕ)

Elementwise subtraction. PyTorch: torch.sub / -.

def Runtime.Autograd.Tape.mul {α : Type} [Mul α] [DecidableEq Spec.Shape] {s : Spec.Shape} (t : Tape α) (aId bId : ℕ) : Result (Tape α × ℕ)

Elementwise multiplication. PyTorch: torch.mul / *.

def Runtime.Autograd.Tape.div {α : Type} [Context α] [DecidableEq Spec.Shape] {s : Spec.Shape} (t : Tape α) (aId bId : ℕ) : Result (Tape α × ℕ)

Elementwise division. PyTorch: torch.div / /. Backward is the ordinary quotient rule, valid for nonzero denominators: ∂(a/b)/∂a = 1/b, ∂(a/b)/∂b = −a/b² (mirrors the CUDA div node; negation reuses subSpec (fill 0) as sub does, so no Neg α is required).

Domain: real calculus does not define the derivative of a/b at b = 0, so this backward is the genuine quotient rule only where b ≠ 0. The carrier's / (and hence divSpec) may totalize or be backend-dependent at b = 0, but no real-valued gradient is implied there.

Requires [Context α] like the sibling abs/sqrt/exp nodes (its divSpec forward rides the carrier's /).

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

Multiply a tensor by a scalar constant. PyTorch: x * c for Python scalar c.

def Runtime.Autograd.Tape.abs {α : Type} [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] [DecidableEq Spec.Shape] {s : Spec.Shape} (t : Tape α) (xId : ℕ) : Result (Tape α × ℕ)

Elementwise absolute value.

Backward uses the sign function (sign_spec) as a subgradient at 0. PyTorch comparison: torch.abs.

def Runtime.Autograd.Tape.sqrt {α : Type} [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] [DecidableEq Spec.Shape] {s : Spec.Shape} (t : Tape α) (xId : ℕ) : Result (Tape α × ℕ)

Elementwise square root.

Backward uses 1 / (2 * sqrt(x)) for x > 0 and 0 otherwise (totalized). PyTorch comparison: torch.sqrt.

def Runtime.Autograd.Tape.clamp {α : Type} [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] [DecidableEq Spec.Shape] {s : Spec.Shape} (t : Tape α) (xId : ℕ) (minVal maxVal : α) : Result (Tape α × ℕ)

Elementwise clamp to [minVal, maxVal].

Backward multiplies by an indicator of the open interval (minVal, maxVal) (zero at boundaries). PyTorch comparison: torch.clamp.

def Runtime.Autograd.Tape.max {α : Type} [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] [DecidableEq Spec.Shape] {s : Spec.Shape} (t : Tape α) (aId bId : ℕ) : Result (Tape α × ℕ)

Elementwise maximum.

Tie-breaking: when a = b, the upstream gradient is split evenly (0.5) between both inputs. PyTorch comparison: torch.maximum.

def Runtime.Autograd.Tape.min {α : Type} [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] [DecidableEq Spec.Shape] {s : Spec.Shape} (t : Tape α) (aId bId : ℕ) : Result (Tape α × ℕ)

Elementwise minimum.

Tie-breaking: when a = b, the upstream gradient is split evenly (0.5) between both inputs. PyTorch comparison: torch.minimum.

def Runtime.Autograd.Tape.relu {α : Type} [Mul α] [Zero α] [Max α] [One α] [LT α] [DecidableRel fun (x1 x2 : α) => x1 > x2] [DecidableEq Spec.Shape] {s : Spec.Shape} (t : Tape α) (xId : ℕ) : Result (Tape α × ℕ)

Elementwise ReLU.

PyTorch comparison: torch.relu(x) / torch.nn.functional.relu(x).