Unique normal form property of compatible term rewriting systems - A new proof of Chew's theorem -

We present a new proof of Chew's theorem, which states that normal forms are unique up to conversion in compatible term rewriting systems. We apply the technique of left-right separated conditional term rewriting systems (LRCTRSs), in which the unique normal form property of a term rewriting system is reduced to the Church-Rosser property of its conditional linearization. In contrast to traditional techniques, such as strong confluence, we introduce a binary relation, called an independence, to prove the Church-Rosser property of the conditional systems. Finally, a suitable independence is constructed for a compatible LRCTRS. 1 Introduction Uniqueness of normal forms up to conversion (or the unique normal form property, UN) is one of the most desirable properties of term rewriting systems (TRSs). This property is necessary to reduce the convertibility of two terms to the coincidence of their normal forms. It is also closely related to consistency of the system [16]. A well-known suffic..