Confluence Competition

Categories – CSR

The CSR category is concerned with confluence of context-sensitive (conditional) rewrite systems.


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.


  1. (format CSTRS)
    (fun 0 0)
    (fun adx 1)
    (fun cons 2 :replacement-map (1))
    (fun head 1)
    (fun incr 1)
    (fun nats 0)
    (fun nil 0)
    (fun s 1)
    (fun tail 1)
    (fun zeros 0)
    (rule (incr nil) nil)
    (rule (incr (cons X L)) (cons (s X) (incr L)))
    (rule (adx nil) nil)
    (rule (adx (cons X L)) (incr (cons X (adx L))))
    (rule nats (adx zeros))
    (rule zeros (cons 0 zeros))
    (rule (head (cons X L)) X)
    (rule (tail (cons X L)) L)
    The correct answer is YES.
  2. (format CSCTRS oriented)
    (fun 0 0)
    (fun cons 2 :replacement-map (2))
    (fun false 0)
    (fun le 2 :replacement-map (1))
    (fun min 1)
    (fun nil 0)
    (fun s 1)
    (fun true 0)
    (rule (le 0 (s x)) true)
    (rule (le x 0) false)
    (rule (le (s x) (s y)) (le x y))
    (rule (min (cons x nil)) x)
    (rule (min (cons x l)) x (= (le x (min l)) true))
    (rule (min (cons x l)) (min l) (= (le x (min l)) false))
    (rule (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.