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, termlistThe restrictions on
stringare the same as in the TRS format. Every
termmust be a well-typed term according the signature declared in
(SIG funlist). Symbols (
id) not declared in
funlistare variables (which can take any sort).
(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)) )
Here is a converter between the TRS and MSTRS formats.