The format for first-order rewrite systems comes in two versions: a basic version and an extended version. The latter contains an additional signature declaration which is used to define function symbols that do not appear in the rewrite rules.
This format is a simplification of the old TPDB format, according to the following grammar:
trs ::= [(VAR idlist)] (RULES rulelist) [(COMMENT string)] idlist ::= ε | id idlist rulelist ::= ε | rule rulelist rule ::= term -> term term ::= id | id() | id(termlist) termlist ::= term | term, termlistHere
stringis any sequence of characters and
idis any nonempty sequence of characters not containing
(VAR idlist)the variables of the TRS are declared. If this is missing, the TRS is ground. Symbols (
id) appearing in the
(RULES rulelist)declaration that were not declared as variables are function symbols. If they appear multiple times, they must be used with the same number of arguments (arity).
In the extended format, a signature declaration specifying the set of function symbols and their arities is added. In this format, every symbol appearing in the rules must be declared as a function symbol or a variable.
trs declaration in the
basic format is replaced by
trs ::= [(VAR idlist)] (SIG funlist) (RULES rulelist) [(COMMENT string)] funlist ::= ε | fun funlist fun ::= (id int)where
intis a nonempty sequence of digits.
An example of the basic format is
(VAR x y) (RULES +(x,0) -> x +(x,s(y)) -> s(+(x,y)) )
An example of the extended format is
(VAR x y) (SIG (f 2) (a 0) (b 0) (h 1)) (RULES f(x,x) -> x f(a,y) -> f(y,b) )Here the signature of the TRS contains a unary function symbol
h, besides the binary symbol
bappearing in the rules.