Categories – TRS

This is the oldest CoCo category. It is concerned with confluence of first-order rewrite systems.

Format

The input is a first-order rewrite system without conditions, specified in the ARI TRS format. The question to be answered is whether the rewrite system is confluent.

Examples

1. (format TRS)
   (fun a 0)
   (fun b 0)
   (fun f 1)
   (rule (f a) b)
   (rule (f (f x)) a)
   

   The correct answer is NO.

2. (format TRS)
   (fun Ap 2)
   (fun I 0)
   (fun K 0)
   (fun S 0)
   (rule (Ap (Ap (Ap S x) y) z) (Ap (Ap x z) (Ap y z)))
   (rule (Ap (Ap K x) y) x)
   (rule (Ap I x) x)
   

   The correct answer is YES.

Problem Selection

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