Confluence Competition

SRS Category

This category is concerned with confluence of string rewrite systems.

Format

The input is a string rewrite system, specified in the basic TRS format.

The question to be answered is whether the string rewrite system is confluent. The first line of the output must be

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(f(x)) -> g(x)
    )
    
    The correct answer is NO and possible outputs include
    NO
    
    The peak f(g(x)) *<- f(f(f(x))) ->* g(f(x)) is not joinable.
    
    and
    MAYBE
    
  2. (VAR x)
    (RULES
      f(f(x)) -> x
      f(x) -> f(f(x))
    )
    
    The correct answer is YES and a possible output is
    YES
    
    The addition of the redundant rules f(x) -> f(f(f(x))) and f(x) -> x makes
    the critical pairs of the SRS development closed. Hence the SRS is
    confluent.
    

Problem Selection

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