Meanings of pointwise operators

Spec.PointwiseOp.meaning gives every operator of Spec.PointwiseOp its meaning at a scalar type with a Context. Negation is the dictionary's negation. The tanh GELU is the dictionary's entry when it has one and Activation.Math.geluSpec otherwise, so every dictionary supports both. FloatLib binary arithmetic has an entry that follows PyTorch's kernel step by step. The exact GELU is x * 0.5 * (1 + erf (x * √½)), PyTorch's order of operations, and needs the dictionary's erf. clamp_min is clampBelow, a comparison and a choice, so every dictionary supports it. The remaining operators are the dictionary's Context.pointwise entries; a dictionary that omits one leaves it unsupported.

References

• PyTorch GELU kernels, aten/src/ATen/native/cpu/Gelu.h: https://github.com/pytorch/pytorch
• Dan Hendrycks and Kevin Gimpel, "Gaussian Error Linear Units (GELUs)", arXiv:1606.08415

def Spec.PointwiseOp.geluErf {α : Type} [Context α] (erf : α → Except String α) (x : α) : Except String α

The exact GELU x * 0.5 * (1 + erf (x * √½)) from an error function, in PyTorch's order.

def Spec.PointwiseOp.clampBelow {α : Type} [Context α] (x bound : α) : α

PyTorch's clamp_min with a scalar bound: bound where x < bound, otherwise x, and the bound where it is a NaN, which bound == bound detects. A NaN x is returned, and the sign of a zero x is kept: eager PyTorch 2.13 returns -0.0 for clamp_min(-0.0, 0) and a NaN for a NaN bound, in binary32, binary64, bfloat16 and binary16 and in both of its loops. Over an ordered field this is max x bound.

def Spec.PointwiseOp.meaning {α : Type} [TorchLean.Storage α] [Context α] (op : PointwiseOp) : Option (PointwiseFn α op.arity)

The meaning of a pointwise operator at a scalar type, or none where the type lacks one.

@[simp]

theorem Spec.PointwiseOp.meaning_neg {α : Type} [TorchLean.Storage α] [Context α] : neg.meaning = some (PointwiseFn.unary fun (x : α) => Except.ok (-x))

Negation is supported by every dictionary.

theorem Spec.PointwiseOp.meaning_gelu_tanh {α : Type} [TorchLean.Storage α] [Context α] (h : Context.pointwise (gelu GeluApproximation.tanh) = none) : (gelu GeluApproximation.tanh).meaning = some (PointwiseFn.unary fun (x : α) => Except.ok (Activation.Math.geluSpec x))

A dictionary without a tanh GELU entry gives it the meaning Activation.Math.geluSpec.