Confluence Competition

MSTRS Format

This page explains the format for many-sorted TRSs. Any many-sorted TRS with a unique sort is identified with the TRS in the obvious way.


In the MSTRS format, sorted function symbols and rules are specified. Formally, decl of the grammar of the old TPDB format is replaced as follows:

 decl ::= RULES listofrules | SIG funlist | id anylist
 funlist ::=  | fun funlist
 fun ::= ( id  sort )
 sort ::=  idlist -> id
 idlist ::= e | id idlist


An example of the format is as follows:

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


Here is a converter between the TRS format and the MSTRS format.