Proving Uniqueness of Normal Forms w.r.t Reduction of Term Rewriting Systems

Most of the studies concerning uniqueness of normal forms of rewriting systems address confluence (CR); but other such properties are also known, such as unique normal forms w.r.t. conversion (UNC), etc. Among such properties, we address in this paper unique normal forms w.r.t. reduction (UNR), aiming for automated proof of it for first-order term rewriting systems (TRSs). UNR is less known compared to CR or UNC, but captures a most natural notion of “uniqueness of normal forms” for computational systems. Although CR (UNC) implies UNR, there have been few methods for showing UNR of TRSs not having CR (UNC). Furthermore, UNR is not closed under signature extensions in contrast to CR and UNC, and some subtleties are required to treat UNR. In this paper, we give some transformation methods for proving UNR that can be applied for TRSs without CR/UNC, and report on an implementation and experiments on automated verification of UNR of TRSs.