The NFP category is concerned with the normal form property (NFP) of first-order rewrite systems.
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. The first line of the output must be
YES, indicating that the input system is NFP,
NO, indicating that the input system is not NFP,
any other answer (e.g.,
MAYBE) indicates that the tool could not determine the status of the input problem.
In the first two cases, the output must be followed by justification that is understandable by a human expert.
(VAR x) (RULES F(x,x) -> A G(x) -> F(x,G(x)) C -> G(C) )The correct answer is
NOand a possible output is
NO The term G(A) and the normal form A are convertible, but G(A) does not rewrite to A.
(RULES a -> b a -> c b -> b c -> c )The correct answer is
YESand a possible output is
YES There are no non-variable normal forms. Since the rules are non-collapsing, NFP holds trivially.