* Category type
demonstration category for CoCo 2016
* Problem and Semantics
Our problem is to check ground confluence of many-sorted TRSs.
A many-sorted TRS R is ground confluent if R is confluent on the
set of ground terms. For many-sorted TRSs, we refer e.g. Section 6.5.6 of
the book: Terese, Term Rewriting Systems, Cambridge University Press, 2003.
* Input and Input format
The input of the problem is a many-sorted TRS. To declare many-sorted TRSs,
we add the following changes to the specification of first-order TRSs
(in old TPDB format):
(i) Add sorted function declaration.
Thus, decl is replaced as follows:
...........
decl ::= VAR varlist | RULES listofrules | FUN funlist | id anylist
varlist ::= | id varlist
funlist ::= | fun funlist
fun ::= id : sort
sort ::= id | idlist -> id
idlist ::= id | id , idlist
...........
Furthermore, id should not contain ':'.
* Example
(FUN
b: 0
c: 1
f: 0 -> 0
g: 0 -> 1
h: 1, 1 -> 2
)
(VAR
x
)
(RULES
g(b) -> g(f(f(f(f(b)))))
f(f(x)) -> b
f(b) -> b
g(f(b)) -> c
h(x,g(b)) -> h(c,c)
h(c,x) -> h(c,g(f(f(b))))
)