TERM REWRITING-SYSTEMS WITH SORT PRIORITIES

In this paper we propose a concept of term rewriting system with sort priorities, which is simply a partial order on the sorts. According to the partial order and a set of function symbols specified in a system , for every term we define another partial order on the set of all sub terms by assigning a priority to each subterm. We also define a subter m to require attention if it is an instance of the left-hand side of s ome rewrite rule. The procedural meaning of such a rewriting system is that at some stage a subterm is allowed to be rewritten only if it re quires attention and no subterm of a higher (or stronger) priority req uires attention. This reduction strategy may transform some nontermina ting (unrestricted) reduction sequences into terminating ones. We disc uss the semantics of our systems and give an application to the operat ional semantics of recursive programs.