* Category type demonstration category for CoCo 2016 * Problem and Semantics The problem is to check unique normalization of first-order term rewrite systems. To prevent a proliferation of categories, we propose to consider all the following properties in one category: - UN : from any term we can reach at most one normal form - UNC: any two convertible normal forms are equal - NFP: any term convertible to a normal form reaches that normal form - CR : any two convertible terms are joinable (Recall that CR implies NFP, NFP implies UNC and UNC implies UN. CR is included because we expect that UN tools will be based on confluence tools.) * Input format The input uses TPDB format as in the Cops database, https://www.lri.fr/~marche/tpdb/format.html * Output The first line of the output is one of the following - NO - if the system does not have the UN property - MAYBE - if the answer is unknown - YES - if the system is uniquely normalizing (UN) - YES(UNC) - if the system has the unique normal form property (UNC) - YES(NFP) - if the system has the normal form property (NFP) - YES(CR) - if the system is confluent (CR) The remainder of the output should contain a justification of the answer as text, as usual. * Example (source: http://cops.uibk.ac.at/problems/55.trs) (VAR x y z) (RULES Ap(Ap(Ap(S,x),y),z) -> Ap(Ap(x,z),Ap(y,z)) Ap(Ap(K,x),y) -> x Ap(I,x) -> x Dh(z,z) -> z ) (COMMENT from p.246 of \cite{Klop80})