Confluence Competition

COM Category

The COM category deals with commutation problems.


Commutation problems are incorporated into COPS as follows:

(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.


    (COPS 532 68)
    (COMMENT this comment will be removed)
    which expands to
    (COMMENT COPS 532 68)
    (VAR w x y z)
        +(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)
        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.
    (COPS 82 80)
    (COMMENT this comment will be removed)
    which expands to
    (COMMENT COPS 82 80)
    (VAR x)
      f(a) -> f(f(a))
      f(x) -> f(a)
    (VAR )
      a -> f'(a,b)
      f'(a,b) -> f'(b,a)
    The correct answer is YES.

Supporting Tools

Problem Selection

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