Theorems of Gappa¶
Predicates¶
Gappa works on sets of facts about real-valued expressions. The following predicates are handled internally:
BND(x,I)- The value of expression
xis included in intervalI. ABS(x,I)- The absolute value of expression
xis included in intervalI. REL(x,y,I)- The values of expressions
xandysatisfy \(x = y \times (1 + \varepsilon)\) with \(\varepsilon\in I\). FIX(x,k)- The value of expression
xis such that \(\exists m \in \mathbb{Z},~x = m \cdot 2^k\). FLT(x,k)- The value of expression
xis such that \(\exists m,e \in \mathbb{Z},~x = m \cdot 2^e \land |m| < 2^k\). NZR(x)- The value of expression
xis not zero. EQL(x,y)- Expressions
xandyhave equal values.
In the definitions above, I denotes an interval whose bounds have
known numerical values, while k is a known integer. In the
description of the theorems, these parameters will usually be ignored.
For instance, BND(x) just means that an enclosure of x is known.
In addition, EQL properties are also used to express rewriting hints
provided by the user.
Theorems¶
There are three categories of theorems in Gappa: theorems about real arithmetic, theorems about rounding operators, and rewriting rules.
In the following, variables a, b, c, and d, represent
arbitrary expressions. Gappa is using backward reasoning, so they are
filled by matching the goal of a theorem against the property Gappa wants
to compute. If some theorem mentions both a and b but only one of
them appears on the right-hand side, then Gappa infers the other one so
that b is an approximate value of a. See Approximated expressions for
more details. There may be additional constraints on the expressions that
require some of them to be syntactically different (denoted a ≠ b),
or to be syntactically constant (denoted a=), or to be syntactically
variable (denoted a~). A constraint written using USR means that
the theorem will be applied only if a matching expression appears in the
input file.
Theorems about real arithmetic¶
| Theorem name | Goal | Hypotheses | Constraints |
|---|---|---|---|
sub_of_eql |
BND(a - b) |
EQL(a, b) |
a ≠ b, (a - b)~ |
eql_of_cst |
EQL(a, b) |
BND(a), BND(b) |
a=, b= |
rel_refl |
REL(a, a) |
||
eql_trans |
EQL(b, c) |
EQL(b, a), EQL(a, c) |
a ≠ c |
eql_trans |
EQL(c, a) |
EQL(c, b), EQL(b, a) |
b ≠ c |
neg |
BND(-a) |
BND(a) |
|
sqrt |
BND(sqrt(a)) |
BND(a) |
|
sub_refl |
BND(a - a) |
||
div_refl |
BND(a / a) |
NZR(a) |
|
square |
BND(a * a) |
ABS(a) |
|
square_rev |
ABS(a) |
BND(a * a) |
USR(a * a) |
neg_a |
ABS(-a) |
ABS(a) |
|
abs_a |
ABS(|a|) |
ABS(a) |
|
add |
BND(a + b) |
BND(a), BND(b) |
|
sub |
BND(a - b) |
BND(a), BND(b) |
a ≠ b |
mul_{nop}{nop} |
BND(a * b) |
BND(a), BND(b) |
|
div_{nop}{np} |
BND(a / b) |
BND(a), BND(b) |
a ≠ b |
add_aa_{nop} |
ABS(a + b) |
ABS(a), ABS(b) |
|
sub_aa_{nop} |
ABS(a - b) |
ABS(a), ABS(b) |
|
mul_aa |
ABS(a * b) |
ABS(a), ABS(b) |
|
div_aa |
ABS(a / b) |
ABS(a), ABS(b) |
|
bnd_of_abs |
BND(a) |
ABS(a) |
a ≠ |?| |
abs_of_bnd_{nop} |
ABS(a) |
BND(a) |
a ≠ |?| |
bnd_of_bnd_abs_{np} |
BND(a) |
BND(a), ABS(a) |
a ≠ |?| |
uabs_of_abs |
BND(|a|) |
ABS(a) |
|
abs_of_uabs |
ABS(a) |
BND(|a|) |
a~, USR(|a|) |
constant{1,2,10} |
BND(a) |
a number |
|
abs_fix |
FIX(|a|) |
FIX(a) |
a~ |
abs_flt |
FLT(|a|) |
FLT(a) |
a~ |
neg_fix |
FIX(-a) |
FIX(a) |
a~ |
neg_flt |
FLT(-a) |
FLT(a) |
a~ |
add_fix |
FIX(a + b) |
FIX(a), FIX(b) |
a~ or b~ |
sub_fix |
FIX(a - b) |
FIX(a), FIX(b) |
a~ or b~ |
sub_flt |
FLT(a - b) |
FLT(a), FLT(b), REL(a,b) |
a~ or b~ |
sub_flt_rev |
FLT(b - a) |
FLT(a), FLT(b), REL(a,b) |
a~ or b~ |
mul_fix |
FIX(a * b) |
FIX(a), FIX(b) |
a~ or b~ |
mul_flt |
FLT(a * b) |
FLT(a), FLT(b) |
a~ or b~ |
fix_of_flt_bnd |
FIX(a) |
FLT(a), ABS(a) |
a~, a ≠ -?, a ≠ |?| |
flt_of_fix_bnd |
FLT(a) |
FIX(a), ABS(a) |
a~, a ≠ -?, a ≠ |?| |
fix_of_singleton_bnd |
FIX(a) |
ABS(a) |
|
flt_of_singleton_bnd |
FLT(a) |
ABS(a) |
|
bnd_of_nzr_rel |
BND((b - a) / a) |
NZR(a), REL(b,a) |
a ≠ b |
rel_of_nzr_bnd |
REL(a, b) |
NZR(b), BND((a - b) / b) |
a ≠ b |
add_rr |
REL(a + b, c + d) |
REL(a, c), REL(b, d), BND(c / (c + d)), NZR(c + d) |
|
sub_rr |
REL(a - b, c - d) |
REL(a, c), REL(b, d), BND(c / (c - d)), NZR(c - d) |
|
mul_rr |
REL(a * b, c * d) |
REL(a, c), REL(b, d) |
a ≠ c, b ≠ d |
div_rr |
REL(a / b, c / d) |
REL(a, c), REL(b, d), NZR(d) |
a ≠ c, b ≠ d |
compose |
REL(b, c) |
REL(b, a), REL(a, c) |
a ≠ c |
compose |
REL(c, a) |
REL(c, b), REL(b, a) |
b ≠ c |
compose_swap |
REL(c * b, d) |
REL(c, d * a'), REL(b, a), NZR(a') |
a = 1 / a' |
error_of_rel_{nop}{nop} |
BND(b - a) |
REL(b, a), BND(a) |
a ≠ b |
nzr_of_abs |
NZR(a) |
ABS(a) |
|
nzr_of_nzr_rel |
NZR(b) |
NZR(a), REL(b, a) |
|
nzr_of_nzr_rel_rev |
NZR(a) |
NZR(b), REL(b, a) |
|
bnd_div_of_rel_bnd_div |
BND((b - a) / c) |
REL(b, a), BND(a / c), NZR(c) |
Theorems about rounding operators¶
The following table describes the kind of theorems that can be applied to rounding operators. These theorems have no specific names, as each rounding operator comes with its dedicated set of theorems. When a specific theorem is not available for a given rounding operator, its effect can usually be obtained through an available one combined with a rewriting rule.
| Goal | Hypothesis | Rounding kind |
|---|---|---|
BND(rnd(a)) |
BND(a) |
fixed, float |
BND(rnd(a)) |
BND(rnd(a)) |
float |
BND(rnd(a) - a) |
fixed | |
BND(rnd(a) - a) |
BND(a) |
fixed (zr, aw), float (zr, aw, up, dn, nu, nd) |
BND(rnd(a) - a) |
ABS(a) |
float (od, ne, nz, na, no) |
BND(rnd(a) - a) |
BND(rnd(a)) |
fixed (zr, aw), float (up, dn, nu, nd) |
BND(rnd(a) - a) |
ABS(rnd(a)) |
float (zr, aw, od, ne, nz, na, no) |
REL(rnd(a), a) |
||
REL(rnd(a), a) |
BND(a) |
|
REL(rnd(a), a) |
ABS(a) |
float |
REL(rnd(a), a) |
BND(rnd(a)) |
|
REL(rnd(a), a) |
ABS(rnd(a)) |
float |
Rewriting rules¶
The following theorems are used to propagate properties about a term to some provably equal term.
| Theorem name | Goal | Hypotheses |
|---|---|---|
bnd_rewrite |
BND(a) |
EQL(a, b), BND(b) |
abs_rewrite |
ABS(a) |
EQL(a, b), ABS(b) |
fix_rewrite |
FIX(a) |
EQL(a, b), FIX(b) |
flt_rewrite |
FLT(a) |
EQL(a, b), FLT(b) |
nzr_rewrite |
NZR(a) |
EQL(a, b), NZR(b) |
rel_rewrite_1 |
REL(a, c) |
EQL(a, b), REL(b, c) |
rel_rewrite_2 |
REL(c, a) |
EQL(a, b), REL(c, b) |
For the sake of readability, the following theorems are not written with
BND predicates but rather with expressions only. When trying to
obtain some enclosure of the target expression (goal), Gappa will first
consider the source one (hypothesis). As a consequence of this layout
and contrarily to previous tables, constraints will also list additional
hypotheses needed to apply the rules. Whenever an operator is put
between square brackets, it means that only theorems that perform basic
interval arithmetic will be able to match it.
| Theorem name | Target | Source | Constraints |
|---|---|---|---|
opp_mibs |
-a - -b |
[-] (a - b) |
a ≠ b |
add_xals |
b + c |
(b - a) [+] (a + c) |
|
add_xars |
c + b |
(c + a) [+] (b - a) |
|
add_mibs |
(a + b) - (c + d) |
(a - c) [+] (b - d) |
a ≠ c, b ≠ d |
add_fils |
(a + b) - (a + c) |
b - c |
b ≠ c |
add_firs |
(a + b) - (c + b) |
a - c |
a ≠ c |
add_filq |
((a + b) - (a + c)) / (a + c) |
(b - c) / (a + c) |
NZR(a + c), b ≠ c |
add_firq |
((a + b) - (c + b)) / (c + b) |
(a - c) / (c + b) |
NZR(c + b), a ≠ c |
add_xilu |
a |
(a + b) [-] b |
USR(a + b) |
add_xiru |
b |
(a + b) [-] a |
USR(a + b) |
sub_xals |
b - c |
(b - a) [+] (a - c) |
a ≠ c, b ≠ c |
sub_xars |
c - b |
(c - a) [-] (b - a) |
b ≠ c |
sub_mibs |
(a - b) - (c - d) |
(a - c) [-] (b - d) |
a ≠ c, b ≠ d |
sub_fils |
(a - b) - (a - c) |
[-] (b - c) |
b ≠ c |
sub_firs |
(a - b) - (c - b) |
a - c |
a ≠ c |
sub_filq |
((a - b) - (a - c)) / (a - c) |
[-] ((b - c) / (a - c)) |
NZR(a - c), b ≠ c |
sub_firq |
((a - b) - (c - b)) / (c - b) |
(a - c) / (c - b) |
NZR(c - b), a ≠ c |
val_xabs |
b |
a [+] (b - a) |
USR(b - a) |
val_xebs |
a |
b [-] (b - a) |
USR(b - a) |
mul_xals |
b * c |
((b - a) [*] c) [+] (a * c) |
|
mul_xars |
c * b |
(c [*] (b - a)) [+] (c * a) |
|
mul_fils |
a * b - a * c |
a [*] (b - c) |
b ≠ c |
mul_firs |
a * b - c * b |
(a - c) [*] b |
a ≠ c |
mul_mars |
a * b - c * d |
(a [*] (b - d)) [+] ((a - c) [*] d) |
a ≠ c, b ≠ d |
mul_mals |
a * b - c * d |
((a - c) [*] b) [+] (c [*] (b - d)) |
a ≠ c, b ≠ d |
mul_mabs |
a * b - c * d |
(a [*] (b - d)) [+] ((a - c) [*] b) [-] ((a - c) [*] (b - d)) |
a ≠ c, b ≠ d |
mul_mibs |
a * b - c * d |
(c [*] (b - d)) [+] ((a - c) [*] d) [+] ((a - c) [*] (b - d)) |
a ≠ c, b ≠ d |
mul_xilu |
a |
(a * b) [/] b |
USR(a * b), NZR(b) |
mul_xiru |
b |
(a * b) [/] a |
USR(a * b), NZR(a) |
div_xals |
b / c |
((b - a) / c) [+] (a / c) |
NZR(c), a ≠ c, b ≠ c |
div_fir |
(a * b) / b |
a |
NZR(b) |
div_fil |
(a * b) / a |
b |
NZR(a) |
div_firs |
a / b - c / b |
(a - c) [/] b |
NZR(b), a ≠ c |
div_xilu |
a |
(a / b) [*] b |
USR(a / b), NZR(b) |
div_xiru |
b |
a [/] (a / b) |
USR(a / b), NZR(a), NZR(b) |
sqrt_mibs |
sqrt(a) - sqrt(b) |
(a - b) [/] (sqrt(a) [+] sqrt(b)) |
BND(a), BND(b), a ≠ b |
sqrt_mibq |
(sqrt(a) - sqrt(b)) / sqrt(b) |
sqrt(1 [+] ((a - b) / b)) [-] 1 |
BND(a), BND(b), a ≠ b |
sqrt_xibu |
a |
sqrt(a) [*] sqrt(a) |
USR(sqrt(a)), BND(a) |
sub_xals |
c - a |
(c - b) [+] (b - a) |
a ≠ c, b ≠ c |
val_xabs |
b |
a [+] (b - a) |
|
val_xebs |
a |
b [-] (b - a) |
|
val_xabq |
b |
a [*] (1 [+] ((b - a) / a)) |
NZR(a) |
val_xebq |
a |
b [/] (1 [+] ((b - a) / a)) |
NZR(a), NZR(b) |
square_sqrt |
sqrt(a) * sqrt(a) |
a |
BND(a) |
addf_1 |
a / (a + b) |
1 [/] (1 [+] (b / a)) |
NZR(a), NZR(a + b) |
addf_2 |
a / (a + b) |
1 [-] (b / (a + b)) |
NZR(a + b) |
addf_3 |
a / (a - b) |
1 [/] (1 [-] (b / a)) |
NZR(a), NZR(a - b), a ≠ b |
addf_4 |
a / (a - b) |
1 [+] (b / (a - b)) |
NZR(a - b), a ≠ b |
addf_5 |
b / (a + b) |
1 [/] ((a / b) [+] 1) |
NZR(b), NZR(a + b), a ≠ b |
addf_6 |
b / (a + b) |
1 [-] (a / (a + b)) |
NZR(a + b), a ≠ b |
addf_7 |
b / (a - b) |
1 [/] ((a / b) [-] 1) |
NZR(b), NZR(a - b), a ≠ b |
addf_8 |
b / (a - b) |
((a / (a - b)) [-] 1) |
NZR(a - b), a ≠ b |
There are also some rewriting rules dealing with REL predicates.
| Theorem name | Target | Source | Constraints |
|---|---|---|---|
opp_fibq |
REL(-a, -b) |
REL(a, b) |
|
mul_filq |
REL(a * b, a * c) |
REL(b, c) |
b ≠ c |
mul_firq |
REL(a * b, c * b) |
REL(a, c) |
a ≠ c |
div_firq |
REL(a / b, c / b) |
REL(a, c) |
a ≠ c |
Finally, there are theorems performing basic congruence.
| Theorem name | Target | Source | Constraints |
|---|---|---|---|
opp_fibe |
EQL(-a, -b) |
EQL(a, b) |
a ≠ b |
add_file |
EQL(a + b, a + c) |
EQL(b, c) |
b ≠ c |
add_fire |
EQL(a + b, c + b) |
EQL(a, c) |
a ≠ c |
sub_file |
EQL(a - b, a - c) |
EQL(b, c) |
b ≠ c |
sub_fire |
EQL(a - b, c - b) |
EQL(a, c) |
a ≠ c |
mul_file |
EQL(a * b, a * c) |
EQL(b, c) |
b ≠ c |
mul_fire |
EQL(a * b, c * b) |
EQL(a, c) |
a ≠ c |
div_file |
EQL(a / b, a / c) |
EQL(b, c) |
b ≠ c |
div_fire |
EQL(a / b, c / b) |
EQL(a, c) |
a ≠ c |