Unique Normal Forms and Confluence of Rewrite Systems: Persistence

Abstract

Programming language interpreters, proving theorems of the form A = B, abstract data types, and program optimization can all be represented by a finite set of rules called a rewrite system. In this paper, we study two fundamental concepts, uniqueness of normal forms and confluence, for nonlinear systems in the absence of termination. This is a difficult topic with only a few results so far. Through a novel approach, we show that every persistent system has unique normal forms. This result is tight and a substantial generalization of previous work. In the process we derive a necessary and sufficient condition for persistence for the first time and give new classes of persistent systems. We also prove the confluence of the union (function symbols can be shared) of a nonlinear system with a left-linear system under fairly general conditions. Again persistence plays a key role in this proof. We are not aware of any confluence result that allows the same level of function symbol sharing.