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 :ref:`example-x1mx`. .. code-block:: gappa # some notations for making the script readable @rnd = float; 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. .. code-block:: gappa { 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. .. code-block:: gappa { 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: .. code-block:: gappa { ... -> |(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: .. code-block:: gappa { ... -> x -/ y in [-0x1p-53,0x1p-53] } This enclosure on the relative error represents the following proposition: :math:`\exists \epsilon \in [-2^{-53},2^{-53}],\ x = y \times (1 + \epsilon)`. As with enclosures, the range can be left unspecified. .. code-block:: gappa { 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, .. code-block:: gappa { ... -> x - y in [0,0] -> ... } Gappa also understands the following notation: .. code-block:: gappa { ... -> 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 :ref:`rewriting rules `. Whenever possible, equalities should be expressed as :ref:`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: :math:`\exists m,e \in Z,~x = m \cdot 2^e`. For ``@FIX`` this decomposition satisfies :math:`e \ge k`, while for ``@FLT`` it satisfies :math:`|m| < 2^k`. For instance, the following Gappa formula holds: .. code-block:: gappa x = float(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). .. code-block:: gappa { x <> 0 -> x / x in [1,1] } .. _definitions: 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`` 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. .. code-block:: gappa @rnd = float; 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 :ref:`rewriting rules ` or :ref:`bisection directives `. :ref:`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: .. code-block:: 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: .. code-block:: gappa 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 --------------- .. _hint-rewriting: 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. .. code-block:: gappa 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: .. code-block:: gappa sqrt(x * x) -> -x { x <= 0 }; .. _hint-approx: 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. .. code-block:: gappa @floor = int; { x - y in [-0.1,0.1] -> floor(x) - y in ? } # floor(x) ~ x; # x ~ y; .. _hint-dichotomy: Dichotomy search ~~~~~~~~~~~~~~~~ The last kind of hint can be used when Gappa is unable to prove a formula but would be able to prove it if the hypothesis ranges were not so wide. Such a failure is usually caused by a bad correlation between the sub-terms of the expressions. This can be solved by rewriting the expressions. But the failure can also happen when the proof of the formula is not the same everywhere on the domain, as in the following example. In both cases, the user can ask Gappa to split the ranges into tighter ranges and see if it helps proving the formula. .. code-block:: gappa @rnd = float< ieee_32, ne >; x = rnd(x_); y = x - 1; z = x * (rnd(y) - y); { x in [0,3] -> |z| in ? } With this script, Gappa will answer that :math:`|z| \le 3 \cdot 2^{-24}`. This is not the best answer because Gappa does not notice that ``rnd(y) - y`` is always zero when :math:`\frac{1}{2} \le x \le 3`. The user needs to ask for a bisection with respect to the expression ``rnd(x_)``. There are three types of bisection. The first one splits an interval in as many equally wide sub-intervals as asked by the user. The second one splits an interval along the points provided by the user. .. code-block:: gappa $ x in 6; # split the range of "x" in six sub-intervals $ x in (0.5,1.9999999); # split the range of "x" in three sub-intervals, the middle one being [0.5,~2] $ x; # equivalent to: $ x in 4; The third kind of bisection tries to find by dichotomy the best range split such that a goal of the logical formula holds true. This requires the range of this goal to be specified, and the enclosed expression has to be indicated on the left of the ``$`` symbol. .. code-block:: gappa { x in [0,3] -> |z| <= 1b-26 } |z| $ x; Contrarily to the first two kinds of bisection, this third one keeps the range improvements only if the goal was finally reached. If there was a failure in doing so, all the improvements are discarded. Gappa will display the sub-range on which the goal was not proved. There is a failure when Gappa cannot prove the goal on a range and this range cannot be split into two half ranges, either because its internal precision is not enough anymore or because the maximum depth of dichotomy has been reached. This depth can be set with the :option:`-Edichotomy` option. More than one bisection hint can be used. And hints of the third kind can try to satisfy more than one goal at once. .. code-block:: gappa a, b, c $ u; a, d $ v; These two hints will be used one after the other. In particular, none will be used when Gappa is doing a bisection with the other one. By adding terms on the right of the ``$`` symbol, more complex hints can be built. Beware of combinatorial explosions though. The following hint is an example of a complex bisection: it asks Gappa to find a set of sub-ranges on ``u`` such that the goal on ``b`` is satisfied when the range on ``v`` is split into three sub-intervals. .. code-block:: gappa b $ u, v in 3 Rather than mentioning simple terms on the left-hand side of hints, one can also write a logical formula. As a consequence, Gappa no longer infers the termination condition from the goal but instead performs a bisection until the formula is satisfied. This is especially useful if no enclosures of the terms appear in the goal, or if the termination criteria is not even an expression enclosure. .. code-block:: gappa rnd(a) = a $ u