Context-Sensitive Category

CoCo 2022 will feature a new competition category on context-sensitive problems.

Format

The input is a context-sensitive rewrite system, specified in the CSTRS format or the CSCTRS format.

The question to be answered is whether the context-sensitive rewrite system is confluent. 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 L X)
   (REPLACEMENT-MAP
     (cons 1)
   )
   (RULES
     incr(nil) -> nil
     incr(cons(X,L)) -> cons(s(X),incr(L))
     adx(nil) -> nil
     adx(cons(X,L)) -> incr(cons(X,adx(L)))
     nats -> adx(zeros)
     zeros -> cons(0,zeros)
     head(cons(X,L)) -> X
     tail(cons(X,L)) -> L
   )
   

   The correct answer is YES.

2. (CONDITIONTYPE ORIENTED)
   (VAR l x y)
   (REPLACEMENT-MAP
     (cons 2) (le 1)
   )
   (RULES
     le(0,s(x)) -> true
     le(x,0) -> false
     le(s(x),s(y)) -> le(x,y)
     min(cons(x,nil)) -> x
     min(cons(x,l)) -> x | le(x,min(l)) == true
     min(cons(x,l)) -> min(l) | le(x,min(l)) == false
     min(cons(x,l)) -> min(l) | min(l) == x
   )
   

   The correct answer is currently unknown.

Problem Selection

Problems are selected among those in COPS with the 'cstrs' or the 'csctrs' tag.