Confluence Competition

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 follows the old TPDB format where only the (VAR idlist) and (RULES listofrules) declarations are used. Rules are restricted to term -> term.

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 decl part of the grammar is replaced by

 ...........
 decl ::= VAR idlist | RULES listofrules | SIG funlist | id anylist
 funlist ::= e | fun funlist
 fun ::= ( id  int )
 ...........

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.