vc2_bit_widths.linexp: A simple Computer Algebra System with affine arithmetic

This module implements a Computer Algebra System (CAS) which is able to perform simple linear algebraic manipulations on linear expressions. In addition, a limited set of non-linear operations (such as truncating division) are supported and modelled using affine arithmetic.

Note

Compared with the mature and powerful sympy CAS, linexp is extremely limited. However, within its restricted domain, linexp is significantly more computationally efficient.

Linear expressions

Linear expressions are defined as being of the form:

\[k_1 v_1 + k_2 v_2 + \cdots + k_j\]

Where \(k_n\) are constants and \(v_n\) are free symbols (i.e. variables). For example, the following represents a linear expression:

\[a + 2b - 3c + 100\]

Where \(a\), \(b\) and \(c\) are the free symbols and 1, 2, -3 and 100 are the relevant constants.

Usage

The expression above may be constructed using this library as follows:

>>> from vc2_bit_widths.linexp import LinExp

>>> # Create expressions containing just the symbols named 'a', 'b' and 'c'.
>>> a = LinExp("a")
>>> b = LinExp("b")
>>> c = LinExp("c")

>>> expr = a + 2*b - 3*c + 100
>>> print(expr)
a + 2*b + -3*c + 100

The LinExp.subs() method may be used to substitute symbols with numbers:

>>> result = expr.subs({"a": 1000, "b": 10000, "c": 100000})
>>> result
LinExp(-278900)

When a LinExp contains just a constant value, the constant may be extracted as a conventional Python number type using constant:

>>> result.is_constant
True
>>> result.constant
-278900

In a similar way, for LinExp instances consisting of a single symbol with weight 1, the symbol name may be extracted like so:

>>> a.is_symbol
True
>>> a.symbol
'a'

>>> # Weighted symbols are considered different
>>> a3 = a * 3
>>> a3.is_symbol
False

Instances of LinExp support all Python operators when the resulting expression would be strictly linear. For example:

>>> expr_times_ten = expr * 10
>>> print(expr_times_ten)
10*a + 20*b + -30*c + 1000

>>> three = (expr * 3) / expr
>>> print(three)
3

>>> # Not allowed since the result would not be linear
>>> expr / a
TypeError: unsupported operand type(s) for /: 'LinExp' and 'LinExp'

Expressions may use Fractions to represent coefficients exactly. Accordingly LinExp implements division using Fraction:

>>> expr_over_three = expr / 3
>>> print(expr_over_three)
(1/3)*a + (2/3)*b + -1*c + 100/3

Internally, linear expressions are represented by a dictionary of the form {symbol: coefficient, ...}. For example:

>>> repr(expr)
"LinExp({'a': 1, 'b': 2, 'c': -3, None: 100})"

Note that the constant term is stored in the special entry None.

The LinExp class provides a number of methods for inspecting the value within an expression. For example, iterating over a LinExp yields the (symbol, coefficient) pairs:

>>> list(expr)
[('a', 1), ('b', 2), ('c', -3), (None, 100)]

Alternatively, just the symbols can be listed:

>>> list(expr.symbols())
['a', 'b', 'c', None]

The coefficients associated with particular symbols can be queried like so:

>>> expr["b"]
2
>>> expr["d"]
0

Affine Arithmetic

Affine arithmetic may be used to bound the effects of non-linear operations such as integer truncation within a linear expression. In affine arithmetic, whenever a non-linear operation is performed, an error term is introduced which represents the range of values the non-linear operation could produce. In this way, the bounds of the effects of the non-linearity may be tracked.

For example, consider the following:

>>> a = LinExp("a")
>>> a_over_2 = a // 2
>>> print(a_over_2)
(1/2)*a + (1/2)*AAError(id=1) + -1/2

Here, the symbol “a” is divded by 2 with truncating integer division. The resulting expression starts with (1/2)*a as usual but is followed by an AAError term and constant representing the rounding error.

In affine arithmetic, AAError symbols represent unknown values in the range \([-1, +1]\). As a result we can see that our expression defines a range \([\frac{a}{2}-1, \frac{a}{2}]\). This range represents the lower- and upper-bounds for the result of the truncating integer division. These bounds may be computed using the affine_lower_bound() and affine_upper_bound() functions respectively:

>>> from vc2_bit_widths.linexp import affine_lower_bound, affine_upper_bound

>>> print(affine_lower_bound(a_over_2))
(1/2)*a + -1
>>> print(affine_upper_bound(a_over_2))
(1/2)*a

Since affine arithmetic AAError symbols are ordinary symbols they will be scaled and manipulated as in ordinary algebra. As such, the affine arithmetic bounds of an expression will remain correct. For example:

>>> expr = ((a // 2) * 2) + 100
>>> print(expr)
a + Error(id=1) + 99
>>> print(affine_lower_bound(expr))
a + 98
>>> print(affine_upper_bound(expr))
a + 100

As well as the inherent limitations of affine arithmetic, :py;class:LinExp is also naive in its implementation leading to additional sources of over-estimates. For example, in the following we might know that ‘a’ is an integer so the expected result should be just ‘a’, but LinExp is unable to use this information:

>>> expr = (a * 2) // 2
>>> print(expr)
a + (1/2)*Error(id=4) + -1/2

As a second example, every truncation produces a new AAError term meaning that sometimes error terms do not cancel when they otherwise could:

>>> # Error terms cancel as expected
>>> print(a_over_2 - a_over_2)
0

>>> # Two different error terms don't cancel as expected
>>> print((a // 2) - (a // 2))
(1/2)*AAError(id=5) + (-1/2)*AAError(id=6)

API

class LinExp(value=0)

classmethod new_affine_error_symbol()

Create a LinExp with a unique AAError symbol.

symbols()

Return an iterator over the symbols in this LinExp where the symbol None represents a constant term.

property is_constant

True iff this LinExp represents only a constant value (including zero) and includes no symbols.

property constant

If is_constant is True, contains the value as a normal numerical Python type. Otherwise raises TypeError on access.

property is_symbol

True iff this LinExp represents only single 1-weighted symbols.

property symbol

Iff this LinExp contains only a single 1-weighted symbol (see is_symbol) returns that symbol. Otherwise raises TypeError on access.

subs(substitutions)

Substitute symbols in this linear expression for new values.

Parameters

substitutions{symbol: number or symbol or LinExp, …}

Substitutions to carry out. Substitutions will be carried out as if performed simultaneously.

Returns

linexpLinExp

A new expression once the substitution has been carried out.

class AAError(id)

An Affine Arithmetic error term. This symbol should be considered to represent an unknown value in the range \([-1, +1]\).

strip_affine_errors(expression)

Return the provided expression with all affine error symbols removed (i.e. set to 0).

affine_lower_bound(expression)

Calculate the lower-bound of an affine arithmetic expression.

affine_upper_bound(expression)

Calculate the upper-bound of an affine arithmetic expression.

affine_error_with_range(lower, upper)

Create an affine arithmetic expression defining the specified range.