Confluence Competition

UNC Category

The UNC category is concerned with the "unique normal forms with respect to conversion" property (UNC) of first-order rewrite systems

Format

The input is a first-order rewrite system without conditions, specified in the basic TRS format or the extended TRS format (since UNC is preserved under signature extensions, tools are free to ignore the (SIG funlist) declaration).

The question to be answered is whether the rewrite system has the property that distinct normal forms are not convertible. 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(x,x) -> A
      G(x) -> F(x,G(x))
      C -> G(C)
    )
    
    The correct answer is YES and a possible output is
    YES
    
    The result of Stefan Kahrs and Connor Smith (FSCD 2016) stating that
    non-omega-overlapping rewrite systems are UNC applies.
    
  2. (VAR x)
    (RULES
      F(x,x) -> A
      F(x,G(x)) -> B
      C -> G(C)
    )
    
    The correct answer is NO and a possible output is
    NO
    
    The term F(C,C) has different normal forms A and B.
    

Problem Selection

Problems are selected among those in COPS with the 'trs' tag. Problems that were shown confluent by at least one participating tool in the CoCo 2021 full run are not considered.