* Category type
demonstration category
* Problem and Semantics
Our problem is to check ground confluence of many-sorted term rewriting
systems. A many-sorted term rewriting system R is ground confluent if the
rewrite relation ->R is confluent on the set of ground terms.
For many-sorted term rewriting systems, 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 term rewrite system.
To declare many-sorted term rewrite system, we add the following
changes to the specification of first-order TRS (in old TPDB format):
(i) Add sort to variable declaration.
(ii) Add sorted function declaration.
Thus, decl is replaced as follows:
...........
decl ::= VAR varlist | RULES listofrules | FUN funlist | id anylist
funlist ::= id : sort
varlist ::= id : id
sort ::= id | idlist -> id
idlist ::= id | id , idlist
...........
Furthermore, id should not contain ':'.
* Example
(FUN
plus : Nat, Nat -> Nat
s : Nat -> Nat
0 : Nat
)
(VAR
x : Nat
y : Nat
)
(RULES
plus(0,0) -> 0
plus(s(x),y) -> s(plus(x,y))
plus(x,s(y)) -> s(plus(y,x))
)