Commutation Category
CoCo 2019 will feature a new competition category on commutation problems.
Format
Commutation problems are incorporated into COPS as follows:
(PROBLEM COMMUTATION) (COPS number1 number2) (COMMENT string)where
number1
and number2
refer to existing problems in TRS format. To ensure that the union of the
two TRSs is a proper TRS, function symbols in TRS
number2
that appear as variable or as function
symbol with a different arity in TRS number1
are
renamed (by adding a ′). The same holds for variables in TRS
number2
that occur as function symbol in TRS
number1
. The renaming program
is available.
For the competition, the
(COPS number1 number2)
declaration
will be inlined (after renaming), before the problem is passed to
participating tools. The inlining program
is available.
The question to be answered is whether the two TRSs commute:
YES
if they do, NO
if they do not.
Examples

(PROBLEM COMMUTATION) (COPS 532 68) (COMMENT this comment will be removed)
which expands to(PROBLEM COMMUTATION) (COMMENT COPS 532 68) (VAR w x y z) (RULES +(x,0()) > x (0()) > 0() ((x)) > x (+(x,y)) > +((x),(y)) +(x,(x)) > 0() +(+(x,(x)),y) > y *(x,0()) > 0() *(x,1()) > x *(x,(y)) > (*(x,y)) *(*(x,(y)),z) > *((*(x,y)),z) *(x,+(y,z)) > +(*(x,y),*(x,z)) *(*(x,+(y,z)),w) > +(*(*(x,y),w),*(*(x,z),w)) +(+(x,y),z) > +(x,+(y,z)) +(x,+(y,z)) > +(+(x,y),z) +(x,y) > +(y,x) *(*(x,y),z) > *(x,*(y,z)) *(x,*(y,z)) > *(*(x,y),z) *(x,y) > *(y,x) ) (VAR x) (RULES b(w'(x)) > w'(w'(w'(b(x)))) w'(b(x)) > b(x) b(b(x)) > w'(w'(w'(w'(x)))) w'(w'(x)) > w'(x) )
The correct answer isYES
. 
(PROBLEM COMMUTATION) (COPS 82 80) (COMMENT this comment will be removed)
which expands to(PROBLEM COMMUTATION) (COMMENT COPS 82 80) (VAR x) (RULES f(a) > f(f(a)) f(x) > f(a) ) (VAR ) (RULES a > f'(a,b) f'(a,b) > f'(b,a) )
The correct answer isYES
.
Supporting Tools
Problem Selection
Problems are selected among those in COPS with the 'commutation' tag.