TPDB Format

Our choice of input format for Term Rewriting Systems is a very popular one: the TPDB format, which is used since 2003 in the Termination Problem Data Base (TPDB). For more information about the original format you can visit the website of the Termination Problem Data Base. Here is a brief description:

spec          ::= (decl) spec | ε
decl          ::= VAR idlist | FUNCTIONS funclist | 
                  CONSTANTS idlist| RULES listofrules | 
                  TERMS listofterms | COMMENTS listofcoments
idlist        ::= id idlist | ε
funclist      ::= funcdef functlist | ε
funcdef       ::= _id_ | _id | id(int)  
listofrules   ::= rule listofrules | ε
rule          ::= term -> term
term          ::= id | id() | id(termlist) | (term)id(term) |
                  (term)id
termlist      ::= term, termlist | term
listofterms   ::= id = term listofterms | ε
listofcoments ::= string listofcoments | ε

Notes about the grammar:

id are non-empty sequences of characters except space, '(', ')', '"', '=' and ','; and excluding the special sequence '->' and keywords VAR, FUNCTIONS, CONSTANTS, RULES, TERMS and COMMENTS.
string are sequences of any characters between double quotes.
int are non-empty sequences of digits.
A symbol occurring in a RULES section which has not been used before is assumed to denote a function symbol, and must be used afterwards always with the same arity.

This are the changes introduced in the format for use with this tool:

Removed THEORY and STRATEGY sections. There is no need to remove them from the input data, because any unknown section is ignored.
Added FUNCTIONS and CONSTANTS sections. They are optional, and the parser can deduce them from the RULES sections, but has been considered important to include them because can reduce the number of mistakes produced typing the rules.
Added TERMS section. It is used to pass to the tool the terms that have to be use in the execution module.
Added infix and postfix notation for functions, e.g. (op1)+(op2) and (op)++ respectively.