CSCTRS Format

The format for context-sensitive conditional term rewrite systems is an extension of the CTRS format, according to the following grammar:

  cscrs    ::= (CONDITIONTYPE ctype) [(VAR idlist)] (REPLACEMENT-MAP cslist) (RULES rulelist)
               [(COMMENT string)]
  ctype    ::= SEMI-EQUATIONAL | JOIN | ORIENTED
  idlist   ::= ε | id idlist
  rulelist ::= ε | rule rulelist
  rule     ::= term -> term | term -> term | condlist
  condlist ::= cond | cond, condlist
  cond     ::= term == term
  term     ::= id | id() | id(termlist)
  termlist ::= term | term, termlist

The restrictions on id and string are the same as in the TRS format and cslist specifies the replacement map:

  cslist   ::= fun | fun cslist
  fun      ::= (id intlist)
  intlist  ::= ε | int, intlist

Here int is a nonempty sequence of digits, denoting an argument position. Function symbols declared in cslist must appear as function symbols in (RULES rulelist) and may not appear as variables in (VAR idlist). The intlist declaration is a list of strictly increasing positive integers corresponding to the active (replacing) argument positions of function symbol id. Function symbols may appear only once in (REPLACEMENT-MAP cslist). If a function symbol in (RULES rulelist) is not listed in the (REPLACEMENT-MAP cslist), all its argument positions are considered active.

Example

 (CONDITIONTYPE ORIENTED)
 (VAR l x y)
 (REPLACEMENT-MAP
   (cons 2) (le 1)
 )
 (RULES
   le(0,s(x)) -> true
   le(x,0) -> false
   le(s(x),s(y)) -> le(x,y)
   min(cons(x,nil)) -> x
   min(cons(x,l)) -> x | le(x,min(l)) == true
   min(cons(x,l)) -> min(l) | le(x,min(l)) == false
   min(cons(x,l)) -> min(l) | min(l) == x
)