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

1. (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 is YES.

2. (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 is YES.

Supporting Tools

• renaming tool
• inlining tool for commutation problems

Problem Selection

Problems are selected among those in COPS with the 'commutation' tag.