The Expression System

The idea

A BoundLab abstract value is a sum of typed components. Each component class captures one kind of uncertainty — a concrete offset, a symmetric interval, an affine form over error symbols, a polynomial — and an abstract value is either a single component or an ExprGroup holding one component per class:

\[ x \;=\; \underbrace{c}_{\text{Bias}} \;+\; \underbrace{\pm w}_{\text{Noise}} \;+\; \underbrace{G\,\varepsilon}_{\text{Zono}} \;+\; \cdots \]

Every component class implements the same small set of primitives — one linear workhorse (einsum), the shape operators, same-class addition, and sound concretization (ub/lb) — and everything else (arithmetic operators, matmul, reductions, conversion) is derived from those in the Expr base class. Because all linear structure funnels through einsum, a component only has to know how a linear map acts on its own representation for every derived operation to be sound.

Groups, zeros, intersections

Adding two values of different classes never loses information: the base __add__ simply keeps them side by side in an ExprGroup, merging same-class addends through their own add. Zeros is the empty sum — the identity for addition and the result of splitting off a class that is not present. Intersects conjoins several independent enclosures of the same value, so a pointwise bound may take the best member per element (\(lb = \max_i lb_i\), \(ub = \min_i ub_i\)); the softmax handlers use it to run a symbolic and an interval denominator side by side.

Handlers navigate this structure with classset() (which component classes are present) and split(cls) (peel off the part they know how to transform, pass the rest through).

Error symbols

Uncertainty enters through Error: a named, identity-tracked variable ranging over \([-1, 1]\). Two expressions referencing the same Error stay correlated — x - x concretizes to exactly zero — which is what separates zonotopes and polynomials from plain intervals. Each symbol carries Reasons, a weighted provenance tag (“input”, “relu”, “matmul”) that survives arithmetic, so a final bound’s width can be attributed back to the operations that produced it.

Domains that store coefficients in a flat trailing axis keep a SpanTable mapping each symbol to its slice, canonically ordered by symbol identity. When two values built over different symbol sets meet, the tables are merged and each side’s coefficients are re-laid-out so shared symbols land in the same columns — alignment is the mechanism that makes correlation survive binary operations.

Conversion and concretization

Components convert exactly or not at all: value.to(Zono) succeeds when either class knows the conversion (convert_from / convert_to hooks) and raises otherwise — conversions never approximate. The one deliberately lossy operation is to_intervals(), which collapses a value to its Bias + Noise box hull, dropping all correlations.

Concretization is lb() / ub() (or lbub(), chw() for center/halfwidth): sound elementwise bounds on every concrete tensor the value represents. Every derived quantity — absub(), diagnostics via torch_print() — reduces to these.

The full signatures live in the API reference under boundlab, boundlab.error, and boundlab.utils.