boundlab.diff.expr.DiffExpr3#

final class boundlab.diff.expr.DiffExpr3[source]#

Bases: Expr

A triple (x, y, diff) where diff over-approximates x − y.

x and y bound each network’s activations; diff bounds their difference and is kept correlated with them: linearisation errors that are shared between the branches cancel instead of accumulating.

Linear operators apply to all three components. Sums with plain expressions or pairs land in an ExprGroup (the base Expr.__add__); lift_diff() folds such a group back into a triple, with shared addends — an affine bias, say — cancelling in diff.

Methods

`__init__`
`absub`	Bound on the magnitude: \(\max(\|lb\|, ub) \ge \sup \|x\|\).
`add`	Same-class addition; `__add__` dispatches here when classes match and otherwise groups the addends in an `ExprGroup`.
`broadcast_to`
`chw`	Center/halfwidth form: `c = (ub + lb) / 2`, `w = (ub - lb) / 2`.
`classset`	The set of component classes present in this value.
`convert_from`	Lift any expression into a triple.
`convert_to`	Hook: convert `self` into `expr_type`, or `None` when this class does not know how.
`einsum`	Apply the linear map described by an integer-label einsum.
`from_exprlike`	Lift a tensor/scalar into a broadcast `Bias`; pass `Expr` through.
`lb`	Sound elementwise lower bound on every concrete value represented.
`lbub`	`(lb, ub)` in one call; components override it when computing both at once is cheaper than two passes.
`matmul`
`mean`
`numel`
`reshape`
`rmatmul`
`split`	Split into `(matching, rest)` so that `matching + rest == self`.
`squeeze`
`sum`
`to`	Convert to another component class, exactly.
`to_intervals`	Collapse to the box hull `Bias(c) + Noise(w)`.
`torch_print`	Diagnostics as a `TensorFormat`.
`transpose`
`ub`	Sound elementwise upper bound on every concrete value represented.
`unsqueeze`

x: Expr#

y: Expr#

diff: Expr#

__init__(x, y, diff)[source]#

classmethod convert_from(expr)[source]#

Lift any expression into a triple.

A DiffExpr2 gets diff = x − y; any other expression is treated as shared between the networks, so its diff is exactly zero.

property shape_dtype: ShapeDtype#: Allocation-free (shape, dtype) metadata of the value.

einsum(subscripts, *operands)[source]#

Apply the linear map described by an integer-label einsum.

subscripts holds one label tuple per input followed by the output labels (see boundlab.utils.einsum_parser()). This is the single linear primitive: __mul__, __matmul__, sum and mean all lower to it, so implementing it soundly makes every derived linear operation sound.

reshape(*shape)[source]#

transpose(*perm)[source]#

broadcast_to(*shape)[source]#

add(other)[source]#

Same-class addition; __add__ dispatches here when classes match and otherwise groups the addends in an ExprGroup.

ub()[source]#

Sound elementwise upper bound on every concrete value represented.

lb()[source]#

Sound elementwise lower bound on every concrete value represented.

lbub()[source]#

(lb, ub) in one call; components override it when computing both at once is cheaper than two passes.

torch_print(group='reason')[source]#

Diagnostics as a TensorFormat.

The result is safe to hand to Torch diagnostic output under tracing: only plain arrays cross the callback boundary, never expression metadata (which may hold tracers, e.g. reason weights).

property T: Self#

__add__(other)#

__mul__(other)#

absub()#

Bound on the magnitude: \(\max(|lb|, ub) \ge \sup |x|\).

chw()#

Center/halfwidth form: c = (ub + lb) / 2, w = (ub - lb) / 2.

classset()#

The set of component classes present in this value.

A single component reports {type(self)}, an ExprGroup its member classes, and Zeros the empty set. Handlers use this to decide which part of a value they know how to transform.

convert_to(expr_type)#

Hook: convert self into expr_type, or None when this class does not know how. The other half of to().

property dtype: dtype#

static from_exprlike(expr, shape)#

Lift a tensor/scalar into a broadcast Bias; pass Expr through.

matmul(other)#

mean(axis, keepdims=False)#

property ndim: int#

numel()#

rmatmul(other)#

property shape: Sequence[Any]#

split(ty)#

Split into (matching, rest) so that matching + rest == self.

The main way handlers peel off the component class they transform while passing the remainder through untouched.

squeeze(axes=None)#

sum(axis, keepdims=False)#

to(expr_type)#

Convert to another component class, exactly.

Identity short-circuits; otherwise the target’s convert_from is tried, then this class’s convert_to. Raises TypeError when neither side knows the conversion — conversions never approximate.

to_intervals(name='')#

Collapse to the box hull Bias(c) + Noise(w).

Sound but lossy: every correlation between error symbols is dropped, so downstream cancellation (x - x = 0) no longer happens.

unsqueeze(axes)#