Confluence Competition

TRS Format

The format for first-order TRSs consists of the basic version and the extended version. The difference of two versions is that the latter contains a signature declaration in addition.

Basic Format

This format follows the old TPDB format, where only VAR and RULES sections concern.

Extended Format

In the extended format, the signature declaration specifying the set of function symbols and their arities is added. In the extended format, all symbols in the rules must be declared as a function symbol or a variable.

Formally, decl of the grammar of the old TPDB format is replaced as follows:

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

Note that we retain (auxiliary) VAR section for backward compatibility. If the function symbols in the signature declaration consist of those appearing in the rules, the input is identified with its basic version.

The motivation for introducing the extended format is that there are cases that the property in concern is not closed under signature extensions. Such properties include NFP and UNR. On the other hand, if the property in concern is closed under signature extensions (e.g. CR and UNC), tools can safely ignore the SIG section.

Example

An example of the basic format is as follow:

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

An example of the extended format is as follows:

(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 h, besides the binary function symbol f and constants a and b appearing in the rules.