Confluence Competition

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

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.