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 follows the
old TPDB format
where only the
(VAR idlist) and
(RULES listofrules) declarations are used. Rules are
term -> term.
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.
decl part of the
is replaced by
........... decl ::= VAR idlist | RULES listofrules | SIG funlist | id anylist funlist ::= e | fun funlist fun ::= ( id int ) ...........
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 f and constants a and b appearing in the rules.