Formalizing a problem

Sections of a Gappa script

A Gappa script contains three parts. The first one is used to give names to some expressions in order to simplify the writing of the next parts. The second one is the logical formula one wants to prove with the tool. The third one gives some hints to Gappa on how to prove it.

The following script shows these three parts for the example of A simple example to start from: x * (1 - x).

# some notations for making the script readable
@rnd = float<ieee_32, ne>;
x = rnd(xx);
y rnd= x * (1 - x);
z = x * (1 - x);

# the logical formula that Gappa will try (and succeed) to prove
{ x in [0,1] -> y in [0,0.25] /\ y - z in [-3b-27,3b-27] }

# three hints to help Gappa finding the proof
z -> 0.25 - (x - 0.5) * (x - 0.5);
y $ x;
y - z $ x;

Logical formula

This is the fundamental part of the script, it contains the logical formula Gappa is expected to prove. This formula is written between brackets and can contain any implication, disjunction, conjunction, negation of properties of mathematical expressions. These properties can be enclosures, inequalities, relative errors, equalities, and expression precisions. Any identifier without definition is assumed to be universally quantified over the set of real numbers.

Enclosures

Enclosures are either bounded ranges or inequalities. In positive position, ranges can be left unspecified. Gappa will then suggest a range such that the logical formula is verified.

{ x - 2 in [-2,0] /\ (x + 1 in [0,2] -> y in [3,4]) -> not x <= 1 \/ x + y in ? }

Results:
  x + y in [3, 5]

Note that Gappa might be able to prove the formula without even having to fill some unspecified ranges. In that case, Gappa will not display anything about them.

{ x in [1,2] /\ x - 3 >= 0 -> x + 1 in ? }
# notice the contradiction between the hypotheses

Results:
  remaining results are pointless, anything can be proved.

Inequalities that give an upper bound on an absolute value are treated specially. They are assumed to be full enclosures with a lower bound equal to zero. In other words, |x| <= 1 is syntactic sugar for |x| in [0,1].

Gappa does not know much about inequalities, as they never appear as hypotheses of its theorems. They can only be used to refine a previously computed enclosure. For instance, Gappa cannot deduce a contradiction from x * x <= -1 alone. It needs to know either an enclosure of x or a nonnegative enclosure of x * x.

Relative errors

The relative error between an approximate value x and a more precise value y is expressed by (x - y) / y. For instance, when one wants to prove a bound on it, one can write:

{ ... -> |(x - y) / y| <= 0x1p-53 }

However, this bound can only be obtained if y is (proved to be) nonzero. Similarly, if a hypothesis was a bound on a relative error, this hypothesis would be usable by Gappa only if it can prove that its denominator is nonzero.

Gappa provides another way of expressing relative errors which does not depend on the denominator being nonzero. It cannot be used as a subexpression; it can only be used as the left-hand side of an enclosure:

{ ... -> x -/ y in [-0x1p-53,0x1p-53] }

This enclosure on the relative error represents the following proposition: \(\exists \epsilon \in [-2^{-53},2^{-53}],\ x = y \times (1 + \epsilon)\).

As with enclosures, the range can be left unspecified.

{ x -/ x in ? }

Results:
  x -/ x in [0, 0]

When the bounds on a relative error are symmetric, the enclosure can be written as |x -/ y| <= ... instead.

Equalities

While equalities could be encoded with enclosures,

{ ... -> x - y in [0,0] -> ... }

Gappa also understands the following notation:

{ ... -> x = y -> ... }

Note that equalities are implicitly directed from left to right. For instance, when looking for a property on a + x, Gappa will consider a + y (assuming that property x = y holds), but not the other way around. This is similar to the handling of rewriting rules.

Whenever possible, equalities should be expressed as definitions rather than inside the logical formulas, as it offers more opportunities for Gappa to apply its theorems.

Expression precision

In addition to equalities and inequalities, Gappa also supports properties about the precision needed to represent expressions. These are expressed by using the predicates @FIX(x,k) and @FLT(x,k) where x is an expression and k an integer. Both properties state that x can be decomposed as a generic binary floating-point number: \(\exists m,e \in Z,~x = m \cdot 2^e\). For @FIX this decomposition satisfies \(e \ge k\), while for @FLT it satisfies \(|m| < 2^k\). For instance, the following Gappa formula holds:

x = float<ieee_32,ne>(x_);
{ @FIX(x,-149) /\ @FLT(x,24) }

Nonzero expressions

Finally, Gappa has special support for expressions that are not zero (and thus can be properly handled when they appear as denominators).

{ x <> 0 -> x / x in [1,1] }

Definitions

Typing the whole expressions in the logical formula can soon become annoying and error-prone, especially if they contain rounding operators. To ease this work, the user can define in another section beforehand the expressions that will be used more than once. A special syntax also allows to avoid embedding rounding operators everywhere.

First, rounding operators can be given a shorter name by using the @name = definition<parameters> syntax. name can then be used wherever the whole definition would have been used.

Next, common sub-terms of a mathematical expression can be shared by giving them a name with the name = term syntax. This name can then be used in later definitions or in the logical formula or in the hints. The equality itself does not hold any semantic meaning. Gappa will only use the name as a shorter expression when displaying the sub-term, and in the generated proof instead of a randomly generated name.

Finally, when all the arithmetic operations on the right side of a definition are followed by the same rounding operator, this operator can be put once and for all on the left of the equal symbol. For example, with the following script, Gappa will complain that y and z are two different names for the same expression.

@rnd = float<ieee_32, ne>;
y = rnd(x * rnd(1 - x));
z rnd= x * (1 - x);
{ y - z >= 0 }

Hints

Hints for Gappa’s engine can be added in this last section, if the tool is not able to prove the logical formula. These hints are either rewriting rules or bisection directives. Approximate and accurate expressions can also be provided in this section in order to generate implicit rewriting rules.

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.

Providing hints

Rewriting rules

Internally, Gappa tries to compute the range of mathematical terms. For example, if the tool has to bound the product of two factors, it will check if it knows the ranges of both factors. If it does, it will apply the theorem about real multiplication in order to compute the range of the product.

Unfortunately, there may be some expressions that Gappa cannot bound tightly. This usually happens because it has no result on a sub-term or because the expression is badly correlated. In this case, the user can provide an intermediate expression with the following hint.

primary -> secondary;

If Gappa finds a property about the secondary expression, it will use it as if it was about the primary expression. This transformation is valid as long as both expressions are equal. So, when generating a theorem proof, Gappa adds this equality as a hypothesis. It is then up to the user to prove it in order to be able to apply the theorem.

To detect mistyping early, Gappa checks if both expressions can be normalized to the same one according to field rules (and are therefore equal) and warn if they are not. (It will not generate a proof of their equality though.) Note that Gappa does not check if the divisors that appear in the expressions are always nonzero; it just warns about them.

If an equality requires some conditions to be verified, they can be added to the rule:

sqrt(x * x) -> -x { x <= 0 };

Approximated expressions

As mentioned before, Gappa has an internal database of rewriting rules. Some of these rules need to know about accurate and approximate terms. Without this information, they do not match any expression. For example, Gappa will replace the term B by b + -(b - B) only it knows a term b that is an approximation of the term B.

Gappa has two heuristics to detect terms that are approximations of other terms. First, rounded values are approximations of their non-rounded counterparts. Second, any absolute or relative error that appears as a hypothesis of a logical sub-formula will define a pair of accurate and approximate terms.

Since these pairs create lots of already proved rewriting rules, it is helpful for the user to define its own pairs. This can be done with the following syntax.

approximate ~ accurate;

In the following example, the comments show two hints that could be added if they had not already been guessed by Gappa. In particular, the second one enables a rewriting rule that completes the proof.

@floor = int<dn>;
{ x - y in [-0.1,0.1] -> floor(x) - y in ? }
# floor(x) ~ x;
# x ~ y;