Term rewriting systems with sort priorities
Zhiqing Shao, Song Guo-xin · International Journal of Computer Mathematics · 1995
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 subterms by assigning a priority to each subterm. We also define a subterm to require attention if it is an instance of the left-hand side of some 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 requires attention and no subterm of a higher (or stronger) priority requires attention. This reduction strategy may transform some nonterminating (unrestricted) reduction sequences into terminating ones. We discuss the semantics of our systems and give an application to the operational semantics of recursive programs