TRS Format

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.

Basic Format

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, termlist

Here string is any sequence of characters and id is any nonempty sequence of characters not containing

• whitespace
• the characters (   )   "   ,   |   \
• the sequences ->   ==   COMMENT   VAR   RULES

In (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).

Extended Format

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.

Formally, the 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 int is a nonempty sequence of digits.

Examples

1. An example of the basic format is

    (VAR x y)
    (RULES
      +(x,0) -> x
      +(x,s(y)) -> s(+(x,y))
    )
   

2. 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.