Categories – CSR

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

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.

Examples

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.