Unique Normal Forms for Disjoint Unions of Conditional Term Rewriting Systems

摘要

A previous study showed that every term rewriting system with the unique normalform property can be conservatively extended to a confluent term rewriting system with the same set of normal forms. A simplified construction, which also yields a positive answer to a conjecture of the previous study stating that the normal form property is a modular property of left linear term rewriting systems, is given. The main result of the previous study, the modularity of unique normal forms, can be generalized to semi-equational term rewriting systems; however, for joint and normal conditional term rewriting systems the method fails.