Gappa language¶
Tokens and operator priority¶
Numbers are either written with a binary representation, or with a
decimal representation. In both representations, the {integer}
parts
are radix-10 natural numbers.
binary {integer}([bBpP][-+]?{integer})?
decimal (({integer}(\.{integer}?)?)|(\.{integer}))([eE][-+]?{integer})?
hexadecimal 0x(({hexa}(\.{hexa}?)?)|(\.{hexa}))([pP][-+]?{integer})?
number -?({binary}|{decimal}|{hexadecimal})
These three expressions represent the same number: 57.5e-1
,
23b-2
, 0x5.Cp0
. They do not have the same semantic for Gappa
though and a different property will be proved in the decimal case.
Indeed, some decimal numbers cannot be expressed as a dyadic number and
Gappa will have to harden the proof and add a layer to take this into
account. In particular, the user should refrain from being inventive
with the constant 1. For example, writing this constant as
00100.000e-2
may prevent some rewriting rules from being applied.
Identifiers (IDENT
) are matched by {alpha}({alpha}|{digit}|_)*
.
Once they have been defined (possibly implicitly), identifiers are
recognized either as variables (VARID
) or rounding operators (FUNID
).
The associativity and precedence of the operators in logical formulas is as follows. It is meant to match the usual conventions.
%right '->'
%left '\/'
%left '/\'
%left 'not'
For mathematical operators, the precedence are as follows.
%left '+' '-' NEG
%left '*' '/'
NEG
denotes the unary minus in front of a numeric literal.
In particular, spacing before a numeric literal is significant.
For example, -1 * x
is parsed as (-1) * x
, while - 1 * x
is parsed as -(1 * x)
.
Other than this special case, space, tabulation, and line-break characters are not significant.
Grammar¶
BLOB: PROG '{' PROP '}' HINTS
PROP: REAL '<=' SNUMBER
| '@FIX' '(' REAL ',' SINTEGER ')'
| '@FLT' '(' REAL ',' INTEGER ')'
| REAL 'in' '[' SNUMBER INTSEP SNUMBER ']'
| REAL 'in' '?'
| REAL '>=' SNUMBER
| REAL '-/' REAL 'in' '[' SNUMBER INTSEP SNUMBER ']'
| '|' REAL '-/' REAL '|' '<=' NUMBER
| REAL '-/' REAL 'in' '?'
| REAL '//' REAL 'in' '[' SNUMBER INTSEP SNUMBER ']'
| '|' REAL '//' REAL '|' '<=' NUMBER
| REAL '//' REAL 'in' '?'
| REAL '=' REAL
| REAL '<>' REAL
| PROP '/\' PROP
| PROP '\/' PROP
| PROP '->' PROP
| 'not' PROP
| '(' PROP ')'
INTSEP: ','
| ';'
MINUS: '-'
| NEG
SNUMBER: NUMBER
| '+' NUMBER
| MINUS NUMBER
INTEGER: NUMBER
SINTEGER: SNUMBER
FUNCTION_PARAM: SINTEGER
| IDENT
FUNCTION_PARAMS_AUX: FUNCTION_PARAM
| FUNCTION_PARAMS_AUX ',' FUNCTION_PARAM
FUNCTION_PARAMS: ε
| '<' FUNCTION_PARAMS_AUX '>'
FUNCTION: FUNID FUNCTION_PARAMS
EQUAL: '='
| FUNCTION '='
PROG: ε
| PROG IDENT EQUAL REAL ';'
| PROG '@' IDENT '=' FUNCTION ';'
REAL: NEG NUMBER
| NUMBER
| VARID
| IDENT
| FUNCTION '(' REALS ')'
| REAL '+' REAL
| REAL MINUS REAL
| REAL '*' REAL
| REAL '/' REAL
| '|' REAL '|'
| 'sqrt' '(' REAL ')'
| 'fma' '(' REAL ',' REAL ',' REAL ')'
| '(' REAL ')'
| '+' REAL
| '-' REAL
REALS: REAL
| REALS ',' REAL
DPOINTS: SNUMBER
| DPOINTS ',' SNUMBER
DVAR: REAL
| REAL 'in' INTEGER
| REAL 'in' '(' DPOINTS ')'
DVARS: DVAR
| DVARS ',' DVAR
PRECOND: REAL '<>' SINTEGER
| REAL '<=' SINTEGER
| REAL '>=' SINTEGER
| REAL '<' SINTEGER
| REAL '>' SINTEGER
PRECONDS_AUX: PRECOND
| PRECONDS_AUX ',' PRECOND
PRECONDS: ε
| '{' PRECONDS_AUX '}'
HINTS: ε
| HINTS REAL '->' REAL PRECONDS ';'
| HINTS REALS '$' DVARS ';'
| HINTS PROP '$' DVARS ';'
| HINTS '$' DVARS ';'
| HINTS REAL '~' REAL ';'
Logical formulas¶
These sections describe some properties of the logical fragment Gappa manipulates. Notice that this fragment is sound, as the generated formal proofs depend on the support libraries, and these libraries are formally proved by relying only on the axioms of basic arithmetic on real numbers.
Undecidability¶
First, notice that the equality of two expressions is equivalent to
checking that their difference is bounded by zero: e - f in
[0,0]
. Second, the property that a real number is a natural number can
be expressed by the equality between its integer part int<dn>(e)
and
its absolute value |e|
.
Thanks to classical logic, a first-order formula can be written in prenex normal form. Moreover, by skolemizing the formula, existential quantifiers can be removed (although Gappa does not allow the user to type arbitrary functional operators in order to prevent mistyping existing operators, the engine can handle them).
As a consequence, a first-order formula with Peano arithmetic (addition, multiplication, and equality, on natural numbers) can be expressed in Gappa’s formalism. It implies that Gappa’s logical fragment is not decidable.
Expressiveness¶
Equality between two expressions can be expressed as a bound on their
difference: e - f in [0,0]
. For inequalities, the difference can be
compared to zero: e - f >= 0
. The negation of the previous
propositions can also be used. Checking the sign of an expression could
also be done with bounds; here are two examples: e - |e| in [0,0]
and e in [0,1] \/
1 / e in [0,1]
. Logical negations of these formulas can be used to
obtain strict inequalities. They can also be defined by discarding only
the zero case: not e in [0,0]
.
Disclaimer: although these properties can be expressed, it does not mean that Gappa is able to handle them efficiently. Yet, if a proposition is proved to be true by Gappa, then it can be considered to be true even if the previous “features” were used in its expression.
Comments and embedded options¶
Comments begin with a sharp sign
#
and go till the end of the line. Comments beginning by#@
are handled as embedded command-line options. All these comments are no different from a space character.