Categories – COM

The COM category deals with commutation problems.

Format

The input is an commutation problem specified in the ARI multiple-TRS format. The question to be answered is whether the two rewrite systems in the problem commute.

Examples

1. ; origin COPS 532 68
   (format TRS :number 2)
   (fun * 2)
   (fun + 2)
   (fun - 1)
   (fun 0 0)
   (fun 1 0)
   (fun b 1)
   (fun w' 1)
   (rule (+ x 0) x)
   (rule (- 0) 0)
   (rule (- (- x)) x)
   (rule (- (+ x y)) (+ (- x) (- y)))
   (rule (+ x (- x)) 0)
   (rule (+ (+ x (- x)) y) y)
   (rule (* x 0) 0)
   (rule (* x 1) x)
   (rule (* x (- y)) (- (* x y)))
   (rule (* (* x (- y)) z) (* (- (* x y)) z))
   (rule (* x (+ y z)) (+ (* x y) (* x z)))
   (rule (* (* x (+ y z)) w) (+ (* (* x y) w) (* (* x z) w)))
   (rule (+ (+ x y) z) (+ x (+ y z)))
   (rule (+ x (+ y z)) (+ (+ x y) z))
   (rule (+ x y) (+ y x))
   (rule (* (* x y) z) (* x (* y z)))
   (rule (* x (* y z)) (* (* x y) z))
   (rule (* x y) (* y x))
   (rule (b (w' x)) (w' (w' (w' (b x)))) :index 2)
   (rule (w' (b x)) (b x) :index 2)
   (rule (b (b x)) (w' (w' (w' (w' x)))) :index 2)
   (rule (w' (w' x)) (w' x) :index 2)
   

   The correct answer is YES.

2. ; origin COPS 82 80
   (format TRS :number 2)
   (fun a 0)
   (fun f 1)
   (fun b 0)
   (fun f' 2)
   (rule (f a) (f (f a)))
   (rule (f x) (f a))
   (rule a (f' a b) :index 2)
   (rule (f' a b) (f' b a) :index 2)
   

   The correct answer is YES.

Problem Selection

Problems are selected from those in the ARI database with the '2trs' tag.