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 with the 'trs' tag. Problems that were shown confluent by at least one participating tool in the CoCo 2023 full run are not considered.