WST'2004 Competitition/Exhibition of termination tools: format of input files

C. Marché and A. Rubio

March 12, 2004

1   Syntax of TRS input files

spec ::= (   decl ) spec | e
decl ::= VAR   idlist | THEORY   listofthdecl | RULES   listofrules
    | STRATEGY   strategydecl | id   anylist
anylist ::= e | id   anylist | string   anylist
    | (   anylist )   anylist | ,   anylist
idlist ::= e | id   idlist
listofthdecl ::= e | (   thdecl   )   listofthdecl
thdecl ::= id   idlist | EQUATIONS   eqlist
eqlist ::= e | equation   eqlist
equation ::= term   ==   term
listofrules ::= e | rule   listofrules
rule ::= term   ->   term | term   ->   term   |   condlist
condlist ::= cond | cond   ,   condlist
cond ::= term   ->   term | term   -><-   term
term ::= id | id   (   ) | id   (   termlist   )
termlist ::= term | term   ,   termlist
strategydecl ::= INNERMOST | CONTEXTSENSITIVE   csstratlist
csstratlist ::= e | ( id   intlist )   csstratlist
intlist ::= e | int   intlist

id are non-empty sequences of characters except space, '(', ')', '"' and ',' ; and excluding special sequences '->', '==', '-><-', '|' and keywords CONTEXTSENSITIVE, EQUATIONS, INNERMOST, RULES, STRATEGY, THEORY and VAR.

string are sequences of any characters between double quotes

int are non-empty sequences of digits

2   Semantical conditions

3   Syntax of SRS input files

spec ::= (   decl ) spec | e
decl ::= RULES   listofrules | STRATEGY   strategydecl | id   anylist
anylist ::= e | id   anylist | string   anylist | (   anylist )   anylist | ,   anylist
listofrules ::= e | rule   ,   listofrules
rule ::= word   ->   word | word   ->
word ::= id | id   word
strategydecl ::= LEFTMOST | RIGHTMOST

id are non-empty sequences of characters except space, '(', ')', '"' and ',' ; and excluding special sequence '->', and keywords LEFTMOST, RIGHTMOST, RULES, and STRATEGY.

string are sequences of any characters between double quotes

This document was translated from LATEX by HEVEA.