Preferred expressions and other peculiarities

Gappa rewrites expressions by matching them with well-known patterns. The enclosure of an unmatchable expression will necessarily have to be computed through interval arithmetic. As a consequence, to ensure that the expressions will benefit from as much rewriting as possible, special care needs to be taken when expressing the computational errors.

Absolute and relative errors

Let exact be an arithmetic expression and approx an approximation of exact. The approximation usually contains rounding operators while the exact expression does not. The absolute error between these two expressions is their difference: approx - exact.

Writing the errors differently will prevent Gappa from applying theorems on rounding errors: -(x - rnd(x)) may lead to a worse enclosure than rnd(x) - x.

The situation is similar for the relative error. It should be expressed as the quotient between the absolute error and the exact value: (approx - exact) / exact. For enclosures of relative errors, this is the same: approx -/ exact.

Global errors

The approx and exact expressions need to have a similar structure in order for the rewriting rules to kick in. E.g., if exact is a sum of two terms a and b, then approx has to be the sum of two terms c and d such that c and d are approximations of a and b respectively.

Indeed the rewriting rule for the absolute error of the addition is: (a + b) - (c + d) -> (a - c) + (b - d). Similarly, the rewriting rules for the multiplication keep the same ordering of sub-terms. For example, one of the rules is: a * b - c * d -> (a - c) * b + c * (b - d). Therefore, one should try not to mess with the structure of expressions.

If the two sides of an error expression happen to not have a similar structure, then a user rewriting rule has to be added in order to put them in a suitable state. For instance, let us assume we are interested in the absolute error between a and d, but they have dissimilar structures. Yet there are two expressions b and c that are equal and with structures similar to a for b and d for c. Then we just have to add the following hints to help Gappa:

b - c -> 0; # or "b-c in [0,0]" as a hypothesis
a ~ b; # a is an approximation of b
c ~ d; # c is an approximation of d

Discrete values

When an expression is known to take a few separate values that are not equally distributed, a disjunction is the simplest solution but it can be avoided if needed. For instance, if x can only be 0, 2, or 17, one can write:

x = i * (19b-1 * i - 15b-1);
{ @FIX(i, 0) /\ i in [-1,1] -> ... }
$ i in 3; # this dichotomy hint helps Gappa to understand that i is either -1, 0, or 1

Disjunction

When the goal of a formula contains a disjunction, one of the sides of this disjunction has to always hold with respect to the set of hypotheses. This is especially important when performing dichotomies. Even if Gappa is able to prove the formula in each particular branch of a dichotomy, if a different property of the disjunction is used each time, the tool will fail to prove the formula in the general case. Note that, whenever a contradiction is found for a specific set of hypotheses, whichever side of the disjunction holds no longer matter, since Gappa can infer any of them.