CSTRS Format

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

  csrs     ::= [(VAR idlist)] (REPLACEMENT-MAP cslist) (RULES rulelist) [(COMMENT string)]
  idlist   ::= ε | id idlist
  rulelist ::= ε | rule rulelist
  rule     ::= 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

 (VAR L X)
 (REPLACEMENT-MAP
   (cons 1)
 )
 (RULES
   incr(nil) -> nil
   incr(cons(X,L)) -> cons(s(X),incr(L))
   adx(nil) -> nil
   adx(cons(X,L)) -> incr(cons(X,adx(L)))
   nats -> adx(zeros)
   zeros -> cons(0,zeros)
   head(cons(X,L)) -> X
   tail(cons(X,L)) -> L
 )