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 x is included in interval I.

ABS(x,I)

The absolute value of expression x is included in interval I.

REL(x,y,I)

The values of expressions x and y satisfy \(x = y \times (1 + \varepsilon)\) with \(\varepsilon\in I\).

LIN(x,y,I)

The values of expressions x and y satisfy \(x = y \times \varepsilon\) with \(\varepsilon\in I\).

FIX(x,k)

The value of expression x is such that \(\exists m \in \mathbb{Z},~x = m \cdot 2^k\).

FLT(x,k)

The value of expression x is such that \(\exists m,e \in \mathbb{Z},~x = m \cdot 2^e \land |m| < 2^k\).

NZR(x)

The value of expression x is not zero.

EQL(x,y)

Expressions x and y have 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 in the hypotheses but only one of them appears on in the goal, 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~

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

bnd_of_rel

BND((b - a) / a)

REL(b, a)

a b

rel_of_nzr_bnd

REL(a, b)

NZR(b), BND((a - b) / b)

a b

add_rr_left

REL(a + b, c + d)

REL(a, c), REL(b, d), LIN(c, c + d)

add_rr_right

REL(a + b, c + d)

REL(a, c), REL(b, d), LIN(d, c + d)

sub_rr_left

REL(a - b, c - d)

REL(a, c), REL(b, d), LIN(c, c - d)

sub_rr_right

REL(a - b, c - d)

REL(a, c), REL(b, d), LIN(d, 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)

a c, b d

inv_r

REL(a / b, a / c)

REL(b, c)

b c

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

bnd_of_bnd_rel_{nop}

BND(b)

REL(b, a), BND(a)

a b, b~

bnd_of_rel_bnd_{nop}

BND(a)

BND(b), REL(b, a)

a b, a~

neg_nzr

NZR(-a)

NZR(a)

mul_nzr

NZR(a * b)

NZR(a), NZR(b)

div_nzr

NZR(a / b)

NZR(a), NZR(b)

div_nzr_rev_l

NZR(a)

NZR(a / b)

USR(a / b)

div_nzr_rev_r

NZR(b)

NZR(a / b)

USR(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)

lin_of_rel

LIN(a, b)

REL(a, b)

lin_of_rel2

LIN(b - a, a)

REL(b, a)

add_flt_lin

FLT(a + b)

FLT(a), FLT(b), LIN(a, b)

add_flt_lin_rev

FLT(a + b)

FLT(a), FLT(b), LIN(b, a)

sub_flt_lin

FLT(a - b)

FLT(a), FLT(b), LIN(a, b)

sub_flt_lin_rev

FLT(a - b)

FLT(a), FLT(b), LIN(b, a)

lin_of_bnd_div

LIN(a, b)

NZR(b), BND(a / b)

bnd_div_of_lin

BND(a / b)

NZR(b), LIN(a, b)

a b

bnd_of_lin

BND(a / b)

LIN(a, b)

a b

add_ll

LIN(a + b, c)

LIN(a, c), LIN(b, c)

sub_ll

LIN(a - b, c)

LIN(a, c), LIN(b, c)

a b

minus_lin

LIN(-a, b)

LIN(a, b)

mul_ll_{nop}{nop}

LIN(a * b, c * d)

LIN(a, c), LIN(b, d)

a c, a d, b c, b d

lin_of_lin_rel_{nop}{nop}

LIN(b - a, c)

LIN(a, c), REL(b, a)

a c

bnd_of_bnd_fix

BND(a)

BND(a), FIX(a)

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

REL(rnd(a), a)

FIX(a)

float

FIX(rnd(a))

fixed, float

FIX(rnd(a))

FIX(a)

fixed, float

FLT(rnd(a))

float

FLT(rnd(a))

FLT(a)

fixed, float

EQL(rnd(a), a)

FIX(a)

fixed

EQL(rnd(a), a)

FIX(a), FLT(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)

lin_rewrite_1

LIN(a, c)

EQL(a, b), LIN(b, c)

lin_rewrite_2

LIN(c, a)

EQL(a, b), LIN(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_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

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_fir

(a * b) / b

a

NZR(b)

div_fil

(a * b) / a

b

NZR(a)

div_xilu

a

(a / b) [*] b

USR(a / b), NZR(b)

div_xiru

b

a [/] (a / b)

USR(a / b), NZR(a)

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_9

a / (a + b)

1 [-] (1 [/] (1 [+] (a / b)))

NZR(b), NZR(a + b)

addf_10

b / (a + b)

1 [-] (1 [/] (1 [+] (b / a)))

NZR(a), NZR(a + b)

addf_11

a / (a - b)

1 [-] (1 [/] (1 [-] (a / b)))

NZR(b), NZR(a - b)

addf_12

b / (a - b)

(1 [/] (1 [-] (b / a))) [-] 1

NZR(a), NZR(a - b)

There are also some rewriting rules dealing with predicates REL and LIN.

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

opp_fibm

LIN(-a, -b)

LIN(a, b)

mul_film

LIN(a * b, a * c)

LIN(b, c)

b c

mul_firm

LIN(a * b, c * b)

LIN(a, c)

a c

mul_fism

LIN(a * b, c * a)

LIN(b, c)

mul_fitm

LIN(a * b, b * c)

LIN(a, c)

div_firq

LIN(a / b, c / b)

LIN(a, c)

a c

val_xabm

LIN(b, c)

LIN((b - a) [+] a, c)

a c, b c

add_mibm

LIN((a + b) - (c + d), e)

LIN((a - c) [+] (b - d), e)

a c, b d

add_film

LIN((a + b) - (a + c), d)

LIN(b - c, d)

b c

add_firm

LIN((a + b) - (c + b), d)

LIN(a - c, d)

a c

sub_mibm

LIN((a - b) - (c - d), e)

LIN((a - c) [-] (b - d), e)

a c, b d

sub_film

LIN((a - b) - (a - c), d)

LIN([-] (b - c), d)

b c

sub_firm

LIN((a - b) - (c - b), d)

LIN(a - c, d)

a c

sub_xalm

LIN(b - c, d)

LIN((b - a) [+] (a - c), d)

a c, b 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