UNR Category
The UNR category is concerned with the "unique normal forms with respect to reduction" property (UNR) of first-order rewrite systems.
Format
The input is a first-order rewrite system without conditions, specified in the basic TRS format or the extended TRS format.
The question to be answered is whether the rewrite system has the property that no term rewrites to different normal forms. The first line of the output must be
-
YES
, indicating that the input system is UNR, -
NO
, indicating that the input system is not UNR, -
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.
Examples
-
(RULES a -> h(f(a),c) a -> f(c) )
The correct answer isNO
and a possible output isNO The term a rewrites to different normal forms f(c) and h(f(f(c)),c).
-
(VAR x) (RULES f(a,a) -> g(f(a,a)) a -> b f(b,x) -> g(f(x,x)) f(x,b) -> g(f(x,x)) )
The correct answer isYES
and a possible output isYES The TRS is left-linear and its critical pairs are development closed, and hence it is confluent and thus also UNR.
Problem Selection
Problems are selected among those in COPS with the 'trs' tag. Problems that were shown confluent by at least one participating tool in the CoCo 2018 full run are not considered.