TRS Category

This is the oldest CoCo category. It is concerned with confluence of first-order rewrite systems.

Format

The input is a first-order rewrite system without conditions, specified in the basic TRS format.

The question to be answered is whether the rewrite system is confluent on the terms that can be built from the function symbols appearing in (RULES rulelist) and variables. The first line of the output must be

• YES, indicating that the input system is confluent,
• NO, indicating that the input system is non-confluent,
• any other answer (e.g., MAYBE) indicates that the tool could not determine the status of the input problem.

In the first two cases, the output must be followed by justification that is understandable by a human expert.

Examples

1. (VAR x)
   (RULES
     f(a) -> b
     f(f(x)) -> a
   )
   

   The correct answer is NO and possible outputs include

   NO
   
   The peak a *<- f(f(a)) ->* f(b) is not joinable.
   

   and

   MAYBE
   

2. (VAR x y z)
   (RULES
     Ap(Ap(Ap(S,x),y),z) -> Ap(Ap(x,z),Ap(y,z))
     Ap(Ap(K,x),y) -> x
     Ap(I,x) -> x
   )
   

   The correct answer is YES and a possible output is

   YES
   
   The TRS is orthogonal.
   

Problem Selection

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