Categories – NFP

The NFP category is concerned with the normal form property (NFP) 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 every term which convertible to a normal form rewrites to that normal form.

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 NO.

2. (format TRS)
   (fun a 0)
   (fun b 0)
   (fun c 0)
   (rule a b)
   (rule a c)
   (rule b b)
   (rule c c)
   

   The correct answer is YES.

Problem Selection

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