Categories – UNC

The UNC category is concerned with the "unique normal forms with respect to conversion" property (UNC) 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 has the property that different normal formals are not convertible.

Examples

1. (format TRS)
   (fun A 0)
   (fun C 0)
   (fun F 2)
   (fun G 1)
   (rule (F x x) A)
   (rule (G x) (F x (G x)))
   (rule C (G C))
   

   The correct answer is YES.

2. (format TRS)
   (fun A 0)
   (fun B 0)
   (fun C 0)
   (fun F 2)
   (fun G 1)
   (rule (F x x) A)
   (rule (F x (G x)) B)
   (rule C (G C))
   

   The correct answer is NO.

Problem Selection

Problems are selected from those in the ARI database that satisfy trs !CR:YES.