MSTRS Format

The format for many-sorted term rewrite systems is a modification of the TRS format, according to the following grammar:

  trs      ::= (SIG funlist) (RULES rulelist) [(COMMENT string)]
  funlist  ::= fun | fun funlist
  fun      ::= (id sort)
  sort     ::= idlist -> id
  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. Every term must be a well-typed term according the signature declared in (SIG funlist). Symbols (id) not declared in funlist are variables (which can take any sort).

Example

 (SIG 
   (app   List List -> List)
   (cons  Nat List -> List)
   (nil   -> List)
   (s     Nat -> Nat)
   (0     -> Nat)
 )
 (RULES
   app(nil,ys) -> ys
   app(cons(x,xs),ys) -> cons(x,app(xs,ys))
 )

Converter

Here is a converter between the TRS and MSTRS formats.