* 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})